Skip to content

Commit a98f2c5

Browse files
thomas-lamiauxthomas-lamiaux
committed
90% sec1
1 parent 6b5dcc1 commit a98f2c5

File tree

1 file changed

+144
-62
lines changed

1 file changed

+144
-62
lines changed

‎src/How_to_Ltac2_contradiction.v

Lines changed: 144 additions & 62 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
(** * How to write a tactic Contracition with Ltac2
1+
(** * How to write a tactic Contradiction with Ltac2
22
33
*** Authors
44
- Thomas Lamiaux
@@ -49,101 +49,184 @@ If [contradiction] takes an argument [t] then, the type of [t] must either be:
4949
*)
5050

5151

52+
(* Let us start by writing a simplified first version without checking if
53+
the types are empty or are singleton types.
54+
This already require matching over goals and quoting. *)
55+
5256
(** ** 1. Step 1:
5357
54-
*** 1.1 A simplified version
58+
*** 1.1 Matching the Goal
5559
56-
Let us start by writing a simplified first version without checking if
57-
the types are empty or are singleton types.
58-
This already require matching over goals and quoting.
60+
To look up for a pair of hypotheses [P] and [~P], we need to match the goal.
61+
There are three commands to match the goal that have different behaviour in
62+
regarding backtracking. The first step is to understand which one we want to use.
5963
64+
- [lazy_match! goal with] that picks a branch, and stick to it.
65+
It will not backtrack to pick another branch if this choice leads to a failure.
66+
For instance, here, it picks the first branch which fails, hence fail.
6067
*)
6168

62-
(* Ltac2 err_contradiction : exn :=
63-
Tactic_failure (Some (fprintf "There are no hypothesis solvable by contradiction")). *)
69+
Goal False.
70+
Fail lazy_match! goal with
71+
| [ |- _ ] => printf "branch 1"; fail
72+
| [ |- _ ] => printf "branch 2"
73+
| [ |- _ ] => printf "branch 3"
74+
end.
75+
Abort.
6476

65-
(** To look up for a pair of hypotheses [P] and [~P], we match the goal using
66-
[lazy_match! goal with].
67-
The patterns are of the form [ [name_hyp1 : type, ..., name_hyp1 : type,] ]
77+
(** - [match! goal with] that picks the first branch that succeeds.
78+
In the example, the first branch fails, it hence backtrack to its choice,
79+
pick the second which this time succeeds
80+
*)
6881

69-
The name of all the variables and meta-variables must start for a small cap.
70-
To match for [P] and [~P], we hence use the pattern [p : ?t, np : ~(?t)].
71-
This provides us the ? of the hypotheses [p : ident] and [q : ident],
72-
and with the type [t : constr].
82+
Goal False.
83+
match! goal with
84+
| [ |- _ ] => printf "branch 1"; fail
85+
| [ |- _ ] => printf "branch 2"
86+
| [ |- _ ] => printf "branch 3"
87+
end.
88+
Abort.
89+
90+
(** - [multi_match! goal with] which is more complex and subtile.
91+
It picks the first branch that makes the whole tactic to succeed,
92+
and not just the [match!] like [match!] does.
93+
In another word, if it choose a branch that succeeds, but this leads to
94+
a subsequent failure when composed with another tactic [; tac],
95+
then it backtracks to pick the next branch that succeeds.
96+
This until either [tac] succeeds, or all the branches have been tried in
97+
which cas it fails.
98+
99+
To understand this better, consider the example below.
100+
[multi_match!] picks the first branch that succeeds, here the second one,
101+
and prints "branch 2".
102+
This choice is combined with [fail] that leads to a failure.
103+
It hence backtrack and picks to the next branch, and prints "branch 3".
104+
This lead again to a failure, and hence backtracks.
105+
There is no branches left, and hence fail.
106+
*)
73107

74-
[[
75-
lazy_match! goal with
76-
| [ p : ?t, q : ~(?t) |- _ ] => ???
77-
| [ |- _ ] => Control.zero (Tactic_failure (Some (fprintf "There are no hypothesis solvable by contradiction")))
78-
end.
79-
]]
108+
Goal False.
109+
Fail multi_match! goal with
110+
| [ |- _ ] => printf "branch 1"; fail
111+
| [ |- _ ] => printf "branch 2"
112+
| [ |- _ ] => printf "branch 3"
113+
end;
114+
fail.
115+
Abort.
116+
117+
(** [lazy_match!] is the easiest command to use and to understand, as there is no
118+
backtracking involved whatsoever. It is sufficient for all applications
119+
where the matching choice is deterministic.
120+
121+
[match!] is useful as soon as matching the syntax is not enough,
122+
and we need additional tests to see if we picked the good branch.
123+
124+
[multi_match!] can be interresting but it can be hard to predict and should
125+
only be used by people that understand what is going on.
126+
We have no use for it here.
127+
*)
80128

81-
To prove the goal, we want to apply [destruct [np p]].
82-
This is not directly possible as [np] and [p] are idents, and not terms.
83-
Consequently, what we want is to apply the term that [np] refers to
84-
the the term that [p] refers to.
85129

86-
To get the term associated to the ident, we first use [Control.hyp : ident -> constr]
87-
to get a Ltac2 ??? out of an ident. We then use [$] to go back to a Rocq term.
88-
This provide us with the script:
89130

90-
[[
91-
let p := Control.hyp p in
92-
let q := Control.hyp q in
93-
exact (False_rect _ ($q $p))
94-
]]
95131

96-
Putting it all together, this give us the following Ltac2 term:
132+
(**
133+
134+
To match the goal, all commands use patterns of form:
135+
136+
[[ [name_hyp1 : type_1, ..., name_hyp1 : type_k] |- to_prove => ... ]]
137+
138+
The name of all the variables and meta-variables must start for a small cap.
139+
140+
To match for [P] and [~P], we hence use the pattern [p : ?t, np : ~(?t)].
141+
This provides us the ? of the hypotheses [p : ident] and [q : ident], and
142+
with the type [t : constr].
97143
*)
98144

99-
Goal forall (P : Prop), P -> ~P -> 0 = 1.
145+
Goal forall P, P -> ~P -> False.
100146
intros.
101147
lazy_match! goal with
102-
| [ p : ?t, np : ~(?t) |- _ ] =>
103-
let p := Control.hyp p in
104-
let np := Control.hyp np in
105-
exact (False_rect _ ($np $p))
106-
| [ |- _ ] => Control.zero (Tactic_failure (Some (fprintf "There are no hypothesis solvable by contradiction")))
148+
| [p : ?t, np : ~(?t) |- _ ] => printf "Matching Worked!";
149+
printf "The names of the hypotheses are %I, %I " p np
150+
| [ |- _ ] => fail
107151
end.
152+
Abort.
108153

109154
(** There are two subtilities to understand here about.
110155
111156
1. Matching is syntactic. This means that [P -> False] will not be matched
112157
by the pattern [~ P], even though [~P] is convertible to [P -> False].
113158
*)
114159

115-
Goal forall (P : Prop), P -> (P -> False) -> 0 = 1.
160+
Goal forall P, P -> (P -> False) -> False.
116161
intros.
117162
Fail lazy_match! goal with
163+
| [p : ?t, np : ~(?t) |- _ ] => printf "Matching Worked!";
164+
printf "The names of the hypotheses are %I, %I " p np
165+
| [ |- _ ] => fail
166+
end.
167+
Abort.
168+
169+
(** 2. However, matching for meta-variables is up to conversion.
170+
This can be seen by adding a trivial expension around [P]:
171+
*)
172+
173+
Goal forall (P : Prop), P -> (~((fun _ => P) 0)) -> 0 = 1.
174+
intros.
175+
lazy_match! goal with
118176
| [ p : ?t, np : ~(?t) |- _ ] =>
119177
let p := Control.hyp p in
120178
let np := Control.hyp np in
121179
exact (False_rect _ ($np $p))
122180
| [ |- _ ] => Control.zero (Tactic_failure (Some (fprintf "There are no hypothesis solvable by contradiction")))
123181
end.
182+
Qed.
124183

125-
(** 2. However, matching for meta-variables is up to conversion.
126-
This can be seen by adding a trivial expension around [P]:
184+
(** *** 1.2 Quoting
185+
186+
To prove the goal, we want to apply [destruct [np p]]. This is not directly
187+
possible as [np] and [p] are idents, they are not terms.
188+
189+
Consequently, what we want is to apply the term that [np] refers to the term
190+
that [p] refers to.
191+
192+
To get the term associated to the ident, we first use [Control.hyp : ident
193+
-> constr] to get a Ltac2 ??? out of an ident. We then use [$] to go back to
194+
a Rocq term. This provide us with the script:
195+
196+
[[
197+
let p := Control.hyp p in let q := Control.hyp q in exact (False_rect _ ($q
198+
$p))
199+
]]
200+
201+
Putting it all together, this give us the following Ltac2 term:
127202
*)
128203

129-
Goal forall (P : Prop), P -> (~((fun _ => P) 0)) -> 0 = 1.
204+
Goal forall (P : Prop), P -> ~P -> 0 = 1.
130205
intros.
131206
lazy_match! goal with
132207
| [ p : ?t, np : ~(?t) |- _ ] =>
133208
let p := Control.hyp p in
134209
let np := Control.hyp np in
135210
exact (False_rect _ ($np $p))
136-
| [ |- _ ] => Control.zero (Tactic_failure (Some (fprintf "There are no hypothesis solvable by contradiction")))
211+
| [ |- _ ] => fail
137212
end.
213+
Abort.
214+
215+
(** 1.3 Error Messages *)
216+
217+
(** 1.4 Putting it all together *)
138218

139219
(** The two other cases proceed similarly. We use:
140220
- [match! goal] to find the hypothesis,
141221
- [Control.hyp] and [$] to use the rocq term associated to the hypotheses.
142222
143-
In the first case, we use [ltac2:(tac)] to build a term using the tactic [constructor].
144-
Note, that here, we really need to use [match] as in the absence of a check to ensure
145-
[t] can be proven by [constructor 1], it may fail.
146-
In which, case we want to backtrack to try the next hypothesis of the form [~t].
223+
The only key difference is that for the last two cases the syntaxtic
224+
match is not enough on its own to select the good hypothesis.
225+
Indeed, there is no reason why matching [~(t)] would imply that [t] is a
226+
singleton type, which can be proven by [constructor 1].
227+
It could very well be a function type, like [~(nat -> False)].
228+
Consequently, we must use [match!] rather than [lazy_match!] as
229+
if the wrong [~t] is picked, we want to backtrack to try the next one.
147230
*)
148231

149232
Goal ~(0 = 0) -> 0 = 1.
@@ -152,26 +235,25 @@ Goal ~(0 = 0) -> 0 = 1.
152235
| [ np : ~(_) |- _] =>
153236
let np := Control.hyp np in
154237
exact (False_rect _ ($np ltac2:(constructor 1)))
155-
| [ |- _ ] => Control.zero (Tactic_failure (Some (fprintf "There are no hypothesis solvable by contradiction")))
238+
| [ |- _ ] => fail
156239
end.
157240
Qed.
158241

159-
(** In the second case, in the absence of a test to check if [t] is an empty type,
160-
[destruct $p] could succeed without solving the goal, for instance for [t := nat].
161-
We hence, link [destruct $p] with [fail] to ensure the goal is solved,
162-
as if they are any remaining goal after [destruct $p], [fail] wil [fail].
163-
*)
164-
165242
Goal False -> 0 = 1.
166243
intros.
167244
match! goal with
168245
| [ p : _ |- _] =>
169246
let p := Control.hyp p in
170247
destruct $p; fail
171-
| [ |- _ ] => Control.zero (Tactic_failure (Some (fprintf "There are no hypothesis solvable by contradiction")))
248+
| [ |- _ ] => fail
172249
end.
250+
Qed.
173251

174-
(** Putting this altogether, this gives us the following tactic *)
252+
(** To put it together, we must pick the match goal that backtracks the more.
253+
As we have used [lazy_match!] and [match!], we must hence pick [match!].
254+
This is gives us the following tactic. Let us not forget the thunk as otherwise
255+
the script would be excuted immediately, which is clearly not what we want.
256+
*)
175257

176258
Ltac2 contradiction_empty_v1_ : unit -> unit :=
177259
fun () =>
@@ -182,17 +264,17 @@ Ltac2 contradiction_empty_v1_ : unit -> unit :=
182264
exact (False_rect _ ($np $p))
183265
| [ np : ~(_) |- _] =>
184266
let np := Control.hyp np in
185-
exact (False_rect _ ($np ltac:(constructor)))
267+
exact (False_rect _ ($np ltac:(constructor 1)))
186268
| [ p : _ |- _ ] =>
187269
let p := Control.hyp p in
188270
destruct $p; fail
189-
| [ |- _] => let err_message := fprintf "No hypothesis is an obvious contradiction" in
190-
Control.zero (Tactic_failure (Some err_message))
271+
| [ |- _] => fail
191272
end.
192273

193-
(** We can now define an abreviation for it and try it out *)
274+
(** Finally, we can define an abreviation for it to try it out *)
194275

195-
Ltac2 Notation contradiction_empty_v1 := intros; contradiction_empty_v1_ ().
276+
Ltac2 Notation contradiction_empty_v1 :=
277+
intros; contradiction_empty_v1_ ().
196278

197279
Goal (1 = 0) -> ~(1 = 0) -> 0 = 1.
198280
contradiction_empty_v1.

0 commit comments

Comments
 (0)