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
|
(************************************************************************)
(* 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.Std.
(** 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 "eintros" p(intropatterns) := intros0 true p.
Ltac2 split0 ev bnd :=
enter_h ev Std.split bnd.
Ltac2 Notation "split" bnd(thunk(bindings)) := split0 false bnd.
Ltac2 Notation "esplit" bnd(thunk(bindings)) := split0 true bnd.
Ltac2 left0 ev bnd := enter_h ev Std.left bnd.
Ltac2 Notation "left" bnd(thunk(bindings)) := left0 false bnd.
Ltac2 Notation "eleft" bnd(thunk(bindings)) := left0 true bnd.
Ltac2 right0 ev bnd := enter_h ev Std.right bnd.
Ltac2 Notation "right" bnd(thunk(bindings)) := right0 false bnd.
Ltac2 Notation "eright" bnd(thunk(bindings)) := right0 true bnd.
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" n(tactic) bnd(thunk(bindings)) := constructor0 false n bnd.
Ltac2 Notation "econstructor" := Control.enter (fun () => Std.constructor true).
Ltac2 Notation "econstructor" n(tactic) bnd(thunk(bindings)) := constructor0 true n bnd.
Ltac2 elim0 ev c bnd use :=
let f ev ((c, bnd, use)) :=
let use := match use with
| None => None
| Some u =>
let ((_, c, wth)) := u in Some (c, wth)
end in
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 :=
let use := match use with
| None => None
| Some u =>
let ((_, c, wth)) := u in Some (c, wth)
end in
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 :=
let use := match use with
| None => None
| Some u =>
let ((_, c, wth)) := u in Some (c, wth)
end in
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 "hnf" cl(opt(clause)) :=
Std.hnf (default_on_concl cl).
Ltac2 rewrite0 ev rw cl tac :=
let tac := match tac with
| None => None
| Some p =>
let ((_, tac)) := p in
Some tac
end in
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.
|
