Wrap types (if needed) before comparing or asserting. (impermeable#60)

* Add 'ensure_prop' tactic that converts input constr to be of type Prop.

Tactics like 'Either' used to crash on input of type 'bool' (eg. i == j).
This tactic will make sure that the asserted statement is of type Prop.

* Add ensure_prop to 'Either' tactic.

* Add 'EnsureProp' to 'Case' tactic.

* Make `ensure_prop` more general.

- Renamed `ensure_prop` tactic to `correct_type_for_assert`, as we should also allow assertion of `Set` and `Type`.
- Added paths for afforementioned `Type` and `Set` types to `correct_type_for_assert`.

* Add the correct type for assertion tactic to more wp tactics.

* TypeForAssert: Use `Constr.type` to get the type of the input constr.

* Add correct type for Since tactic

This allows the 'Since' tactic to handle input of the form `i == i`.

* TypeCorrector: Rename the type correction utility function.

* Add Waterproof license header

* TypeCorrector: Update test for type corrector.

The tests have no output in the build process.
Furthermore, the tests also test for leaving terms of type 'Set',
'Type' and 'Prop' unchanged.

* TypeCorrector: Remove debug check from 'SupAndInf.v'

* Update error message in 'TypeCorrector.v'

* Add newline add end of files

* Add tests for tactics modified using TypeCorrector.

* Update tests for ItSuffices

* Update test 11 for ItSuffices

* Add suggested test to ItSuffices.

* Add suggested test to Conclusion

Author: DikieDick

_CoqProject.in

@@ -78,6 +78,7 @@ theories/Util/Hypothesis.v
 theories/Util/Init.v
 theories/Util/Since.v
 theories/Util/MessagesToUser.v
+theories/Util/TypeCorrector.v
 
 theories/Waterproof.v
 theories/Waterprove.v

tests/tactics/Assume.v

@@ -142,3 +142,10 @@ Goal (0 = 0) -> nat -> nat.
   Assume that (0 = 0).
   Fail Assume that nat.
 Abort.
+
+(** * Test 17: should correctly handle boolean goal
+*)
+Goal is_true true -> (0 = 0).
+Proof.
+  Assume that (true).
+Abort.

tests/tactics/BothStatements.v

@@ -105,4 +105,13 @@ Goal forall n : nat, ((n = n) /\ (n + 1 = n + 1)).
 Proof.
     intro n.
     Fail We show both (n + 2 = n + 2) and (n +3 = n + 3).
-Abort.
+Abort.
+
+Goal forall a b : bool, is_true a -> is_true b -> is_true a /\ is_true b.
+    intros a b.
+    intros Ha Hb.
+    We show both statements.
+    - We need to show that (a).
+      exact Ha.
+    - We conclude that (b).
+Qed.

tests/tactics/Claims.v

@@ -40,4 +40,18 @@ Proof.
     intro n.
     We claim that (n = n) (i).
     { reflexivity. }
-Abort.
+Abort.
+
+(** Test 2: This should work with a boolean statement *)
+Goal forall n : nat, exists m : nat, (n = m).
+Proof.
+  intro n.
+  We claim that (true).
+Abort.
+
+(** Test 3: This should work with a boolean statement *)
+Goal forall n : nat, exists m : nat, (n = m).
+Proof.
+  intro n.
+  We claim that (orb false true).
+Abort.

tests/tactics/Conclusion.v

@@ -283,3 +283,21 @@ Proof.
     intro H1.
     We conclude that (& F(k+1) = F(k) = F(0))%nat.
 Qed.
+
+(** * Test 9
+  Test whether the conclude tactic can handle boolean statements 
+*)
+Goal (is_true true).
+Proof.
+  We conclude that (true).
+Qed.
+
+(** * Test 10
+  Test whether the conclude tactic can handle a boolean statement
+  with boolean since-clause.
+*)
+Goal (is_true true).
+Proof.
+  It holds that (true).
+  Since (true) we conclude that (true).
+Qed.

tests/tactics/Either.v

@@ -188,3 +188,16 @@ Fail Either (P) or (~P).
 Abort.
 
 End test_differences_sort_of_goal.
+
+(** Test 13: Check whether we can handle boolean statements *)
+Require Import Coq.Bool.Bool.
+Goal forall b : bool, is_true(eqb b true) \/ is_true(eqb b false) -> True.
+Proof.
+  intro b.
+  Assume that (is_true(eqb b true) \/ is_true(eqb b false)).
+  Either (eqb b true) or (eqb b false).
+  - Case (eqb b true).
+    exact I.
+  - Case (eqb b false).
+    exact I.
+Qed.

tests/tactics/ItHolds.v

@@ -305,3 +305,17 @@ Proof.
   intros Ha Hf.
   By Ha it holds that B.
 Abort.
+
+(* Test 21: we can use "It holds that" using boolean statements *)
+Goal 1 < 2.
+Proof.
+  It holds that (true).
+Abort.
+
+(* Test 22: "Since" works with a boolean statement *)
+Goal 1 < 2.
+Proof.
+  It holds that (orb true false).
+  Since (orb true false) it holds that (1 < 2).
+  assumption.
+Qed.

tests/tactics/ItSuffices.v

@@ -113,3 +113,27 @@ Proof.
   pose g.
   Since (A -> B) it suffices to show that A.
 Abort.
+
+Parameter b : bool.
+(* Test 11: "It suffices" works with a boolean statement *)
+Goal ((is_true b) -> B) -> B.
+Proof.
+  intro H.
+  Since (is_true b -> B) it suffices to show that (b).
+Abort.
+
+(* Test 12: "It suffices" works with a boolean statement *)
+Goal ((is_true b) -> B) -> B.
+Proof.
+  intro H.
+  It suffices to show that (b).
+Abort.
+
+(* Test 13: "It suffices" works with boolean statement and boolean "Since"
+  clause *)
+Goal ((is_true b) -> B) -> B.
+Proof.
+  intro H.
+  It holds that (true).
+  Since (true) it suffices to show that (b).
+Abort.

tests/tactics/ToShow.v

@@ -56,4 +56,19 @@ Lemma two_is_two: 2 = 2.
 Proof.
   Fail We need to show (0 = 2).
   reflexivity.
-Qed.
+Qed.
+
+(** Fourth test: We need to show should handle a boolean statement *)
+Goal forall a b: bool, is_true (orb a b).
+Proof.
+  intros a b.
+  We need to show (orb a b).
+  We need to show (if a then true else b).
+Abort.
+
+(** Fifth test: Test wrong goal with boolean statement *)
+Goal forall a b: bool, is_true (orb a b).
+Proof.
+  intros a b.
+  Fail We need to show that (andb a b).
+Abort.

tests/util/TypeCorrector.v

@@ -0,0 +1,104 @@
+(******************************************************************************)
+(*                  This file is part of Waterproof-lib.                      *)
+(*                                                                            *)
+(*   Waterproof-lib is free software: you can redistribute it and/or modify   *)
+(*    it under the terms of the GNU General Public License as published by    *)
+(*     the Free Software Foundation, either version 3 of the License, or      *)
+(*                    (at your option) any later version.                     *)
+(*                                                                            *)
+(*     Waterproof-lib is distributed in the hope that it will be useful,      *)
+(*      but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*       MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the         *)
+(*               GNU General Public License for more details.                 *)
+(*                                                                            *)
+(*     You should have received a copy of the GNU General Public License      *)
+(*   along with Waterproof-lib. If not, see <https://www.gnu.org/licenses/>.  *)
+(*                                                                            *)
+(******************************************************************************)
+
+From Ltac2 Require Import Ltac2.
+From Waterproof Require Import Waterproof.
+From Waterproof Require Import Util.MessagesToUser.
+From Waterproof Require Import Util.TypeCorrector.
+
+Section assert_tests.
+
+Parameter setS : Set.
+Parameter s : setS.
+
+Parameter typeT : Type.
+Parameter t : typeT.
+
+Lemma test : 0 = 0.
+Proof.
+  (* The statement (0 = 0) has type Prop so nothing should happen and resulting type should be Prop. *)
+  let res := correct_type_by_wrapping constr:(0 = 0) in (
+    match! Constr.type res with 
+    | Prop => ()
+    | _ => throw ( Message.of_string "Expected resulting type to be Prop." )
+    end;
+    let expected_constr := constr:(0 = 0) in
+    if Constr.equal res expected_constr 
+      then () 
+      else throw ( Message.of_string "Expected resulting term to be '0 = 0'." )
+  ).
+
+  (* The statement 'true' has type bool so this should get wrapped in 'is_true (true)' which has type Prop. *)
+  let res := correct_type_by_wrapping constr:(true) in (
+    match! Constr.type res with 
+    | Prop => ()
+    | _ => throw ( Message.of_string "Expected resulting type to be Prop." )
+    end;
+    let expected_constr := constr:(is_true true) in
+    if Constr.equal res expected_constr 
+      then () 
+      else throw ( Message.of_string "Expected resulting term to be 'is_true true'." )
+  ).
+
+  (* The statement 'true = true' has type Prop so nothing should happen and resulting type should be Prop. *)
+  let res := correct_type_by_wrapping constr:(true = true) in (
+    match! Constr.type res with
+    | Prop => ()
+    | _ => throw ( Message.of_string "Expected resulting type to be Prop." )
+    end;
+    let expected_constr := constr:(true = true) in
+    if Constr.equal res expected_constr 
+      then () 
+      else throw ( Message.of_string "Expected resulting term to be 'true = true'." )
+  ).
+
+  (* setS has type Set which should not change *)
+  let res := correct_type_by_wrapping constr:(setS) in (
+    match! Constr.type res with
+    | Set => ()
+    | _ => throw ( Message.of_string "Expected resulting type to be Set." )
+    end;
+    let expected_constr := constr:(setS) in
+    if Constr.equal res expected_constr 
+      then () 
+      else throw ( Message.of_string "Expected resulting term to be 'setS'." )
+  ).
+
+  (* typeT has type Type which should not change *)
+  let res := correct_type_by_wrapping constr:(typeT) in (
+    match! Constr.type res with
+    | Type => ()
+    | _ => throw ( Message.of_string "Expected resulting type to be Type." )
+    end;
+    let expected_constr := constr:(typeT) in
+    if Constr.equal res expected_constr 
+      then () 
+      else throw ( Message.of_string "Expected resulting term to be 'typeT'." )
+  ).
+
+  (* 0 has type nat and this should fail *)
+  Fail Ltac2 Eval correct_type_by_wrapping constr:(0).
+
+  (* s has type setS and this should fail *)
+  Fail Ltac2 Eval correct_type_by_wrapping constr:(s).
+
+  (* t has type typeT and this should fail *)
+  Fail Ltac2 Eval correct_type_by_wrapping constr:(t).
+Abort.
+
+End assert_tests.