Skip to content

Commit fb0bd1d

Browse files
jim-portegiesjim-portegies
authored
Merge feature from main: allow for boolean statements in tactics, such as the Assume tactic (impermeable#62)
Original PR is impermeable#60
1 parent 463871a commit fb0bd1d

22 files changed

Lines changed: 287 additions & 4 deletions

‎_CoqProject.in‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -78,6 +78,7 @@ theories/Util/Hypothesis.v
7878
theories/Util/Init.v
7979
theories/Util/Since.v
8080
theories/Util/MessagesToUser.v
81+
theories/Util/TypeCorrector.v
8182

8283
theories/Waterproof.v
8384
theories/Waterprove.v

‎tests/tactics/Assume.v‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -142,3 +142,10 @@ Goal (0 = 0) -> nat -> nat.
142142
Assume that (0 = 0).
143143
Fail Assume that nat.
144144
Abort.
145+
146+
(** * Test 17: should correctly handle boolean goal
147+
*)
148+
Goal is_true true -> (0 = 0).
149+
Proof.
150+
Assume that (true).
151+
Abort.

‎tests/tactics/BothStatements.v‎

Lines changed: 10 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -105,4 +105,13 @@ Goal forall n : nat, ((n = n) /\ (n + 1 = n + 1)).
105105
Proof.
106106
intro n.
107107
Fail We show both (n + 2 = n + 2) and (n +3 = n + 3).
108-
Abort.
108+
Abort.
109+
110+
Goal forall a b : bool, is_true a -> is_true b -> is_true a /\ is_true b.
111+
intros a b.
112+
intros Ha Hb.
113+
We show both statements.
114+
- We need to show that (a).
115+
exact Ha.
116+
- We conclude that (b).
117+
Qed.

‎tests/tactics/Claims.v‎

Lines changed: 15 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -40,4 +40,18 @@ Proof.
4040
intro n.
4141
We claim that (n = n) (i).
4242
{ reflexivity. }
43-
Abort.
43+
Abort.
44+
45+
(** Test 2: This should work with a boolean statement *)
46+
Goal forall n : nat, exists m : nat, (n = m).
47+
Proof.
48+
intro n.
49+
We claim that (true).
50+
Abort.
51+
52+
(** Test 3: This should work with a boolean statement *)
53+
Goal forall n : nat, exists m : nat, (n = m).
54+
Proof.
55+
intro n.
56+
We claim that (orb false true).
57+
Abort.

‎tests/tactics/Conclusion.v‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -283,3 +283,21 @@ Proof.
283283
intro H1.
284284
We conclude that (& F(k+1) = F(k) = F(0))%nat.
285285
Qed.
286+
287+
(** * Test 9
288+
Test whether the conclude tactic can handle boolean statements
289+
*)
290+
Goal (is_true true).
291+
Proof.
292+
We conclude that (true).
293+
Qed.
294+
295+
(** * Test 10
296+
Test whether the conclude tactic can handle a boolean statement
297+
with boolean since-clause.
298+
*)
299+
Goal (is_true true).
300+
Proof.
301+
It holds that (true).
302+
Since (true) we conclude that (true).
303+
Qed.

‎tests/tactics/Either.v‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -188,3 +188,16 @@ Fail Either (P) or (~P).
188188
Abort.
189189

190190
End test_differences_sort_of_goal.
191+
192+
(** Test 13: Check whether we can handle boolean statements *)
193+
Require Import Coq.Bool.Bool.
194+
Goal forall b : bool, is_true(eqb b true) \/ is_true(eqb b false) -> True.
195+
Proof.
196+
intro b.
197+
Assume that (is_true(eqb b true) \/ is_true(eqb b false)).
198+
Either (eqb b true) or (eqb b false).
199+
- Case (eqb b true).
200+
exact I.
201+
- Case (eqb b false).
202+
exact I.
203+
Qed.

‎tests/tactics/ItHolds.v‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -305,3 +305,17 @@ Proof.
305305
intros Ha Hf.
306306
By Ha it holds that B.
307307
Abort.
308+
309+
(* Test 21: we can use "It holds that" using boolean statements *)
310+
Goal 1 < 2.
311+
Proof.
312+
It holds that (true).
313+
Abort.
314+
315+
(* Test 22: "Since" works with a boolean statement *)
316+
Goal 1 < 2.
317+
Proof.
318+
It holds that (orb true false).
319+
Since (orb true false) it holds that (1 < 2).
320+
assumption.
321+
Qed.

‎tests/tactics/ItSuffices.v‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -113,3 +113,27 @@ Proof.
113113
pose g.
114114
Since (A -> B) it suffices to show that A.
115115
Abort.
116+
117+
Parameter b : bool.
118+
(* Test 11: "It suffices" works with a boolean statement *)
119+
Goal ((is_true b) -> B) -> B.
120+
Proof.
121+
intro H.
122+
Since (is_true b -> B) it suffices to show that (b).
123+
Abort.
124+
125+
(* Test 12: "It suffices" works with a boolean statement *)
126+
Goal ((is_true b) -> B) -> B.
127+
Proof.
128+
intro H.
129+
It suffices to show that (b).
130+
Abort.
131+
132+
(* Test 13: "It suffices" works with boolean statement and boolean "Since"
133+
clause *)
134+
Goal ((is_true b) -> B) -> B.
135+
Proof.
136+
intro H.
137+
It holds that (true).
138+
Since (true) it suffices to show that (b).
139+
Abort.

‎tests/tactics/ToShow.v‎

Lines changed: 16 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -56,4 +56,19 @@ Lemma two_is_two: 2 = 2.
5656
Proof.
5757
Fail We need to show (0 = 2).
5858
reflexivity.
59-
Qed.
59+
Qed.
60+
61+
(** Fourth test: We need to show should handle a boolean statement *)
62+
Goal forall a b: bool, is_true (orb a b).
63+
Proof.
64+
intros a b.
65+
We need to show (orb a b).
66+
We need to show (if a then true else b).
67+
Abort.
68+
69+
(** Fifth test: Test wrong goal with boolean statement *)
70+
Goal forall a b: bool, is_true (orb a b).
71+
Proof.
72+
intros a b.
73+
Fail We need to show that (andb a b).
74+
Abort.

‎tests/util/TypeCorrector.v‎

Lines changed: 104 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,104 @@
1+
(******************************************************************************)
2+
(* This file is part of Waterproof-lib. *)
3+
(* *)
4+
(* Waterproof-lib is free software: you can redistribute it and/or modify *)
5+
(* it under the terms of the GNU General Public License as published by *)
6+
(* the Free Software Foundation, either version 3 of the License, or *)
7+
(* (at your option) any later version. *)
8+
(* *)
9+
(* Waterproof-lib is distributed in the hope that it will be useful, *)
10+
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
11+
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
12+
(* GNU General Public License for more details. *)
13+
(* *)
14+
(* You should have received a copy of the GNU General Public License *)
15+
(* along with Waterproof-lib. If not, see <https://www.gnu.org/licenses/>. *)
16+
(* *)
17+
(******************************************************************************)
18+
19+
From Ltac2 Require Import Ltac2.
20+
From Waterproof Require Import Waterproof.
21+
From Waterproof Require Import Util.MessagesToUser.
22+
From Waterproof Require Import Util.TypeCorrector.
23+
24+
Section assert_tests.
25+
26+
Parameter setS : Set.
27+
Parameter s : setS.
28+
29+
Parameter typeT : Type.
30+
Parameter t : typeT.
31+
32+
Lemma test : 0 = 0.
33+
Proof.
34+
(* The statement (0 = 0) has type Prop so nothing should happen and resulting type should be Prop. *)
35+
let res := correct_type_by_wrapping constr:(0 = 0) in (
36+
match! Constr.type res with
37+
| Prop => ()
38+
| _ => throw ( Message.of_string "Expected resulting type to be Prop." )
39+
end;
40+
let expected_constr := constr:(0 = 0) in
41+
if Constr.equal res expected_constr
42+
then ()
43+
else throw ( Message.of_string "Expected resulting term to be '0 = 0'." )
44+
).
45+
46+
(* The statement 'true' has type bool so this should get wrapped in 'is_true (true)' which has type Prop. *)
47+
let res := correct_type_by_wrapping constr:(true) in (
48+
match! Constr.type res with
49+
| Prop => ()
50+
| _ => throw ( Message.of_string "Expected resulting type to be Prop." )
51+
end;
52+
let expected_constr := constr:(is_true true) in
53+
if Constr.equal res expected_constr
54+
then ()
55+
else throw ( Message.of_string "Expected resulting term to be 'is_true true'." )
56+
).
57+
58+
(* The statement 'true = true' has type Prop so nothing should happen and resulting type should be Prop. *)
59+
let res := correct_type_by_wrapping constr:(true = true) in (
60+
match! Constr.type res with
61+
| Prop => ()
62+
| _ => throw ( Message.of_string "Expected resulting type to be Prop." )
63+
end;
64+
let expected_constr := constr:(true = true) in
65+
if Constr.equal res expected_constr
66+
then ()
67+
else throw ( Message.of_string "Expected resulting term to be 'true = true'." )
68+
).
69+
70+
(* setS has type Set which should not change *)
71+
let res := correct_type_by_wrapping constr:(setS) in (
72+
match! Constr.type res with
73+
| Set => ()
74+
| _ => throw ( Message.of_string "Expected resulting type to be Set." )
75+
end;
76+
let expected_constr := constr:(setS) in
77+
if Constr.equal res expected_constr
78+
then ()
79+
else throw ( Message.of_string "Expected resulting term to be 'setS'." )
80+
).
81+
82+
(* typeT has type Type which should not change *)
83+
let res := correct_type_by_wrapping constr:(typeT) in (
84+
match! Constr.type res with
85+
| Type => ()
86+
| _ => throw ( Message.of_string "Expected resulting type to be Type." )
87+
end;
88+
let expected_constr := constr:(typeT) in
89+
if Constr.equal res expected_constr
90+
then ()
91+
else throw ( Message.of_string "Expected resulting term to be 'typeT'." )
92+
).
93+
94+
(* 0 has type nat and this should fail *)
95+
Fail Ltac2 Eval correct_type_by_wrapping constr:(0).
96+
97+
(* s has type setS and this should fail *)
98+
Fail Ltac2 Eval correct_type_by_wrapping constr:(s).
99+
100+
(* t has type typeT and this should fail *)
101+
Fail Ltac2 Eval correct_type_by_wrapping constr:(t).
102+
Abort.
103+
104+
End assert_tests.

0 commit comments

Comments
 (0)