1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
Require Import Ltac2.Init.
Require Ltac2.Control Ltac2.Int Ltac2.Std.
(** Tacticals *)
Ltac2 orelse t f :=
match Control.case t with
| Err e => f e
| Val ans =>
let ((x, k)) := ans in
Control.plus (fun _ => x) k
end.
Ltac2 ifcatch t s f :=
match Control.case t with
| Err e => f e
| Val ans =>
let ((x, k)) := ans in
Control.plus (fun _ => s x) (fun e => s (k e))
end.
Ltac2 fail0 (_ : unit) := Control.enter (fun _ => Control.zero Tactic_failure).
Ltac2 Notation fail := fail0 ().
Ltac2 try0 t := Control.enter (fun _ => orelse t (fun _ => ())).
Ltac2 Notation try := try0.
Ltac2 rec repeat0 (t : unit -> unit) :=
Control.enter (fun () =>
ifcatch (fun _ => Control.progress t)
(fun _ => Control.check_interrupt (); repeat0 t) (fun _ => ())).
Ltac2 Notation repeat := repeat0.
Ltac2 dispatch0 t ((head, tail)) :=
match tail with
| None => Control.enter (fun _ => t (); Control.dispatch head)
| Some tacs =>
let ((def, rem)) := tacs in
Control.enter (fun _ => t (); Control.extend head def rem)
end.
Ltac2 Notation t(thunk(self)) ">" "[" l(dispatch) "]" : 4 := dispatch0 t l.
Ltac2 do0 n t :=
let rec aux n t := match Int.equal n 0 with
| true => ()
| false => t (); aux (Int.sub n 1) t
end in
aux (n ()) t.
Ltac2 Notation do := do0.
Ltac2 Notation once := Control.once.
Ltac2 progress0 tac := Control.enter (fun _ => Control.progress tac).
Ltac2 Notation progress := progress0.
Ltac2 rec first0 tacs :=
match tacs with
| [] => Control.zero Tactic_failure
| tac :: tacs => Control.enter (fun _ => orelse tac (fun _ => first0 tacs))
end.
Ltac2 Notation "first" "[" tacs(list0(thunk(tactic(6)), "|")) "]" := first0 tacs.
Ltac2 complete tac :=
let ans := tac () in
Control.enter (fun () => Control.zero Tactic_failure);
ans.
Ltac2 rec solve0 tacs :=
match tacs with
| [] => Control.zero Tactic_failure
| tac :: tacs =>
Control.enter (fun _ => orelse (fun _ => complete tac) (fun _ => first0 tacs))
end.
Ltac2 Notation "solve" "[" tacs(list0(thunk(tactic(6)), "|")) "]" := solve0 tacs.
Ltac2 time0 tac := Control.time None tac.
Ltac2 Notation time := time0.
Ltac2 abstract0 tac := Control.abstract None tac.
Ltac2 Notation abstract := abstract0.
(** Base tactics *)
(** Note that we redeclare notations that can be parsed as mere identifiers
as abbreviations, so that it allows to parse them as function arguments
without having to write them within parentheses. *)
(** Enter and check evar resolution *)
Ltac2 enter_h ev f arg :=
match ev with
| true => Control.enter (fun () => f ev (arg ()))
| false =>
Control.enter (fun () =>
Control.with_holes arg (fun x => f ev x))
end.
Ltac2 intros0 ev p :=
Control.enter (fun () => Std.intros false p).
Ltac2 Notation "intros" p(intropatterns) := intros0 false p.
Ltac2 Notation intros := intros.
Ltac2 Notation "eintros" p(intropatterns) := intros0 true p.
Ltac2 Notation eintros := eintros.
Ltac2 split0 ev bnd :=
enter_h ev Std.split bnd.
Ltac2 Notation "split" bnd(thunk(bindings)) := split0 false bnd.
Ltac2 Notation split := split.
Ltac2 Notation "esplit" bnd(thunk(bindings)) := split0 true bnd.
Ltac2 Notation esplit := esplit.
Ltac2 exists0 ev bnds := match bnds with
| [] => split0 ev (fun () => Std.NoBindings)
| _ =>
let rec aux bnds := match bnds with
| [] => ()
| bnd :: bnds => split0 ev bnd; aux bnds
end in
aux bnds
end.
(*
Ltac2 Notation "exists" bnd(list0(thunk(bindings), ",")) := exists0 false bnd.
Ltac2 Notation "eexists" bnd(list0(thunk(bindings), ",")) := exists0 true bnd.
Ltac2 Notation eexists := eexists.
*)
Ltac2 left0 ev bnd := enter_h ev Std.left bnd.
Ltac2 Notation "left" bnd(thunk(bindings)) := left0 false bnd.
Ltac2 Notation left := left.
Ltac2 Notation "eleft" bnd(thunk(bindings)) := left0 true bnd.
Ltac2 Notation eleft := eleft.
Ltac2 right0 ev bnd := enter_h ev Std.right bnd.
Ltac2 Notation "right" bnd(thunk(bindings)) := right0 false bnd.
Ltac2 Notation right := right.
Ltac2 Notation "eright" bnd(thunk(bindings)) := right0 true bnd.
Ltac2 Notation eright := eright.
Ltac2 constructor0 ev n bnd :=
enter_h ev (fun ev bnd => Std.constructor_n ev n bnd) bnd.
Ltac2 Notation "constructor" := Control.enter (fun () => Std.constructor false).
Ltac2 Notation constructor := constructor.
Ltac2 Notation "constructor" n(tactic) bnd(thunk(bindings)) := constructor0 false n bnd.
Ltac2 Notation "econstructor" := Control.enter (fun () => Std.constructor true).
Ltac2 Notation econstructor := econstructor.
Ltac2 Notation "econstructor" n(tactic) bnd(thunk(bindings)) := constructor0 true n bnd.
Ltac2 elim0 ev c bnd use :=
let f ev ((c, bnd, use)) := Std.elim ev (c, bnd) use in
enter_h ev f (fun () => c (), bnd (), use ()).
Ltac2 Notation "elim" c(thunk(constr)) bnd(thunk(bindings))
use(thunk(opt(seq("using", constr, bindings)))) :=
elim0 false c bnd use.
Ltac2 Notation "eelim" c(thunk(constr)) bnd(thunk(bindings))
use(thunk(opt(seq("using", constr, bindings)))) :=
elim0 true c bnd use.
Ltac2 apply0 adv ev cb cl :=
let cl := match cl with
| None => None
| Some p =>
let ((_, id, ipat)) := p in
let p := match ipat with
| None => None
| Some p =>
let ((_, ipat)) := p in
Some ipat
end in
Some (id, p)
end in
Std.apply adv ev cb cl.
Ltac2 Notation "eapply"
cb(list1(thunk(seq(constr, bindings)), ","))
cl(opt(seq(keyword("in"), ident, opt(seq(keyword("as"), intropattern))))) :=
apply0 true true cb cl.
Ltac2 Notation "apply"
cb(list1(thunk(seq(constr, bindings)), ","))
cl(opt(seq(keyword("in"), ident, opt(seq(keyword("as"), intropattern))))) :=
apply0 true false cb cl.
Ltac2 induction0 ev ic use :=
let f ev use := Std.induction ev ic use in
enter_h ev f use.
Ltac2 Notation "induction"
ic(list1(induction_clause, ","))
use(thunk(opt(seq("using", constr, bindings)))) :=
induction0 false ic use.
Ltac2 Notation "einduction"
ic(list1(induction_clause, ","))
use(thunk(opt(seq("using", constr, bindings)))) :=
induction0 true ic use.
Ltac2 destruct0 ev ic use :=
let f ev use := Std.destruct ev ic use in
enter_h ev f use.
Ltac2 Notation "destruct"
ic(list1(induction_clause, ","))
use(thunk(opt(seq("using", constr, bindings)))) :=
destruct0 false ic use.
Ltac2 Notation "edestruct"
ic(list1(induction_clause, ","))
use(thunk(opt(seq("using", constr, bindings)))) :=
destruct0 true ic use.
Ltac2 default_on_concl cl :=
match cl with
| None => { Std.on_hyps := Some []; Std.on_concl := Std.AllOccurrences }
| Some cl => cl
end.
Ltac2 Notation "red" cl(opt(clause)) :=
Std.red (default_on_concl cl).
Ltac2 Notation red := red.
Ltac2 Notation "hnf" cl(opt(clause)) :=
Std.hnf (default_on_concl cl).
Ltac2 Notation hnf := hnf.
Ltac2 Notation "simpl" s(strategy) pl(opt(seq(pattern, occurrences))) cl(opt(clause)) :=
Std.simpl s pl (default_on_concl cl).
Ltac2 Notation simpl := simpl.
Ltac2 Notation "cbv" s(strategy) cl(opt(clause)) :=
Std.cbv s (default_on_concl cl).
Ltac2 Notation cbv := cbv.
Ltac2 Notation "cbn" s(strategy) cl(opt(clause)) :=
Std.cbn s (default_on_concl cl).
Ltac2 Notation cbn := cbn.
Ltac2 Notation "lazy" s(strategy) cl(opt(clause)) :=
Std.lazy s (default_on_concl cl).
Ltac2 Notation lazy := lazy.
Ltac2 Notation "unfold" pl(list1(seq(reference, occurrences), ",")) cl(opt(clause)) :=
Std.unfold pl (default_on_concl cl).
Ltac2 fold0 pl cl :=
let cl := default_on_concl cl in
Control.enter (fun () => Control.with_holes pl (fun pl => Std.fold pl cl)).
Ltac2 Notation "fold" pl(thunk(list1(open_constr))) cl(opt(clause)) :=
fold0 pl cl.
Ltac2 Notation "pattern" pl(list1(seq(constr, occurrences), ",")) cl(opt(clause)) :=
Std.pattern pl (default_on_concl cl).
Ltac2 Notation "vm_compute" pl(opt(seq(pattern, occurrences))) cl(opt(clause)) :=
Std.vm pl (default_on_concl cl).
Ltac2 Notation vm_compute := vm_compute.
Ltac2 Notation "native_compute" pl(opt(seq(pattern, occurrences))) cl(opt(clause)) :=
Std.native pl (default_on_concl cl).
Ltac2 Notation native_compute := native_compute.
Ltac2 rewrite0 ev rw cl tac :=
let cl := default_on_concl cl in
Std.rewrite ev rw cl tac.
Ltac2 Notation "rewrite"
rw(list1(rewriting, ","))
cl(opt(clause))
tac(opt(seq("by", thunk(tactic)))) :=
rewrite0 false rw cl tac.
Ltac2 Notation "erewrite"
rw(list1(rewriting, ","))
cl(opt(clause))
tac(opt(seq("by", thunk(tactic)))) :=
rewrite0 true rw cl tac.
(** coretactics *)
Ltac2 Notation reflexivity := Std.reflexivity ().
Ltac2 Notation assumption := Std.assumption ().
Ltac2 Notation etransitivity := Std.etransitivity ().
Ltac2 Notation admit := Std.admit ().
Ltac2 Notation clear := Std.keep [].
Ltac2 Notation refine := Control.refine.
(** extratactics *)
Ltac2 absurd0 c := Control.enter (fun _ => Std.absurd (c ())).
Ltac2 Notation absurd := absurd0.
Ltac2 subst0 ids := match ids with
| [] => Std.subst_all ()
| _ => Std.subst ids
end.
Ltac2 Notation "subst" ids(list0(ident)) := subst0 ids.
Ltac2 Notation subst := subst.
|
