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
|
Set Mangle Names.
(* Check that refine policy of redefining previous names make these names private *)
Goal True -> True.
intro.
Fail exact H.
exact _0.
Abort.
Unset Mangle Names.
Goal True -> True.
intro; exact H.
Abort.
Set Mangle Names.
Set Mangle Names Prefix "baz".
Goal True -> True.
intro.
Fail exact H.
Fail exact _0.
exact baz0.
Abort.
Goal True -> True.
intro; assumption.
Abort.
Goal True -> True.
intro x; exact x.
Abort.
Goal forall x y, x+y=0.
intro x.
refine (fun x => _).
Fail Check x0.
Check x.
Abort.
(* Example from Emilio *)
Goal forall b : False, b = b.
intro b.
refine (let b := I in _).
Fail destruct b0.
Abort.
(* Example from Cyprien *)
Goal True -> True.
Proof.
refine (fun _ => _).
Fail exact t.
Abort.
(* Example from Jason *)
Goal False -> False.
intro H.
abstract exact H.
Abort.
(* Variant *)
Goal False -> False.
intro.
Fail abstract exact H.
Abort.
(* Example from Jason *)
Lemma lem1 : False -> False.
intro H.
(* Name H' is from Ltac here, so it preserves the privacy *)
(* But abstract messes everything up *)
let H' := H in abstract exact H'.
Qed.
(* Variant *)
Goal False -> False.
intro.
Fail let H' := H in abstract exact H'.
Abort.
(* Indirectly testing preservation of names by move (derived from Jason) *)
Inductive nat2 := S2 (_ _ : nat2).
Goal forall t : nat2, True.
intro t.
let IHt1 := fresh "IHt1" in
let IHt2 := fresh "IHt2" in
induction t as [? IHt1 ? IHt2].
Fail exact IHt1.
Abort.
(* Example on "pose proof" (from Jason) *)
Goal False -> False.
intro; pose proof I as H0.
Fail exact H.
Abort.
(* Testing the approach for which non alpha-renamed quantified names are user-generated *)
Section foo.
Context (b : True).
Goal forall b : False, b = b.
Fail destruct b0.
Abort.
Lemma lem2 : forall b : False, b = b.
now destruct b.
Qed.
End foo.
(* Test stability of "fix" *)
Lemma a : forall n, n = 0.
Proof.
fix a 1.
Check a.
Fail fix a 1.
Abort.
(* Test stability of "induction" *)
Lemma a : forall n : nat, n = n.
Proof.
intro n; induction n as [ | n IHn ].
- auto.
- Check n.
Check IHn.
Abort.
Inductive I := C : I -> I -> I.
Lemma a : forall n : I, n = n.
Proof.
intro n; induction n as [ n1 IHn1 n2 IHn2 ].
Check n1.
Check n2.
apply f_equal2.
+ apply IHn1.
+ apply IHn2.
Qed.
(* Testing remember *)
Lemma c : 0 = 0.
Proof.
remember 0 as x eqn:Heqx.
Check Heqx.
Abort.
Lemma c : forall Heqx, Heqx -> 0 = 0.
Proof.
intros Heqx X.
remember 0 as x.
Fail Check Heqx0. (* Heqx0 is not canonical *)
Abort.
(* An example by Jason from the discussion for PR #268 *)
Goal nat -> Set -> True.
intros x y.
match goal with
| [ x : _, y : _ |- _ ]
=> let z := fresh "z" in
rename y into z, x into y;
let x' := fresh "x" in
rename z into x'
end.
revert y. (* x has been explicitly moved to y *)
Fail revert x. (* x comes from "fresh" *)
Abort.
Goal nat -> Set -> True.
intros.
match goal with
| [ x : _, y : _ |- _ ]
=> let z := fresh "z" in
rename y into z, x into y;
let x' := fresh "x" in
rename z into x'
end.
Fail revert y. (* generated by intros *)
Fail revert x. (* generated by intros *)
Abort.
|
