1
(* The tactic language *)
3
(* Submitted by Pierre Cr�gut *)
4
(* Checks substitution of x *)
5
Ltac f x := unfold x in |- *; idtac.
7
Lemma lem1 : 0 + 0 = 0.
12
(* Submitted by Pierre Cr�gut *)
13
(* Check syntactic correctness *)
14
Ltac F x := idtac; G x
15
with G y := idtac; F y.
17
(* Check that Match Context keeps a closure *)
18
Ltac U := let a := constr:I in
27
(* Check that Match giving non-tactic arguments are evaluated at Let-time *)
29
Ltac B := let y := (match goal with
34
Lemma lem3 : True -> False -> True -> False.
36
B. (* y is H0 if at let-time, H1 otherwise *)
39
(* Checks the matching order of hypotheses *)
40
Ltac Y := match goal with
41
| x:_,y:_ |- _ => apply x
43
Ltac Z := match goal with
44
| y:_,x:_ |- _ => apply x
47
Lemma lem4 : (True -> False) -> (False -> False) -> False.
54
(* Check backtracking *)
55
Lemma back1 : 0 = 1 -> 0 = 0 -> 1 = 1 -> 0 = 0.
58
| _:(0 = ?X1),_:(1 = 1) |- _ => exact (refl_equal X1)
62
Lemma back2 : 0 = 0 -> 0 = 1 -> 1 = 1 -> 0 = 0.
65
| _:(0 = ?X1),_:(1 = 1) |- _ => exact (refl_equal X1)
69
Lemma back3 : 0 = 0 -> 1 = 1 -> 0 = 1 -> 0 = 0.
72
| _:(0 = ?X1),_:(1 = 1) |- _ => exact (refl_equal X1)
76
(* Check context binding *)
79
| context C[(?X1 = ?X2)] => context C [X1 = X2]
82
Lemma sym : 0 <> 1 -> 1 <> 0.
84
let t := sym type of H in
93
(* Check context binding in match goal *)
94
(* This wasn't working in V8.0pl1, as the list of matched hyps wasn't empty *)
97
| _:True |- context C[(?X1 = ?X2)] =>
98
let t := context C [X2 = X1] in
102
Lemma sym' : True -> 0 <> 1 -> 1 <> 0.
112
(* Check that fails abort the current match context *)
113
Lemma decide : True \/ False.
121
(* Check that "match c with" backtracks on subterms *)
124
(match constr:(1 = 2) with
125
| context [(S ?X1)] => constr:(refl_equal X1:1 = 1)
131
(* Note that backtracking in "match c with" is only on type-checking not on
132
evaluation of tactics. E.g., this does not work
134
Lemma refl : (1)=(1).
136
[[(S ?1)]] -> Apply (refl_equal nat ?1).
141
(* Check the precedences of rel context, ltac context and vars context *)
142
(* (was wrong in V8.0) *)
144
Ltac check_binding y := cut ((fun y => y) = S).
149
(* Check that variables explicitly parsed as ltac variables are not
150
seen as intro pattern or constr (bug #984) *)
152
Ltac afi tac := intros; tac.
156
(* Tactic Notation avec listes *)
158
Tactic Notation "pat" hyp(id) "occs" integer_list(l) := pattern id at l.
160
Goal forall x, x=0 -> x=x.
165
Tactic Notation "revert" ne_hyp_list(l) := generalize l; clear l.
167
Goal forall a b c, a=0 -> b=c+a.
172
(* Used to fail until revision 9280 because of a parasitic App node with
176
match constr:@None with @None => exact I end.
179
(* Check second-order pattern unification *)
183
|- forall x y, @?P x y =>
184
let Q := eval lazy beta in (exists x, forall y, P x y) in
188
Goal forall x y : nat, x = y.
189
to_exist. exact (fun H => H).
192
(* Used to fail in V8.1 *)
194
Tactic Notation "test" constr(t) integer(n) :=
195
set (k := t) in |- * at n.
197
Goal forall x : nat, x = 1 -> x + x + x = 3.
202
(* Utilisation de let rec sans arguments *)
205
let rec i := match goal with |- ?A -> ?B => intro; i | _ => idtac end in
208
Goal True -> True -> True.
213
(* Interf�rence entre espaces des noms *)
216
Ltac Z1 t := set (x:=t).