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
|
(* Thinning introduction hypothesis must be done after all introductions *)
(* Submitted by Guillaume Melquiond (BZ#1000) *)
Goal forall A, A -> True.
intros _ _.
Abort.
(* This did not work until March 2013, because of underlying "red" *)
Goal (fun x => True -> True) 0.
intro H.
Abort.
(* This should still work, with "intro" calling "hnf" *)
Goal (fun f => True -> f 0 = f 0) (fun x => x).
intro H.
match goal with [ |- 0 = 0 ] => reflexivity end.
Abort.
(* Somewhat related: This did not work until March 2013 *)
Goal (fun f => f 0 = f 0) (fun x => x).
hnf.
match goal with [ |- 0 = 0 ] => reflexivity end.
Abort.
(* Fixing behavior of "*" and "**" in branches, so that they do not
introduce more than what the branch expects them to introduce at most *)
Goal forall n p, n + p = 0.
intros [|*]; intro p.
Abort.
(* Check non-interference of "_" with name generation *)
Goal True -> True -> True.
intros _ ?.
exact H.
Qed.
(* A short test about introduction pattern pat%c *)
Goal (True -> 0=0) -> True /\ False -> 0=0.
intros H (H1%H,_).
exact H1.
Qed.
(* A test about bugs in 8.5beta2 *)
Goal (True -> 0=0) -> True /\ False -> False -> 0=0.
intros H H0 H1.
destruct H0 as (a%H,_).
(* Check that H0 is removed (was bugged in 8.5beta2) *)
Fail clear H0.
(* Check position of newly created hypotheses when using pat%c (was
left at top in 8.5beta2) *)
match goal with H:_ |- _ => clear H end. (* clear H1:False *)
match goal with H:_ |- _ => exact H end. (* check that next hyp shows 0=0 *)
Qed.
Goal (True -> 0=0) -> True -> 0=0.
intros H H1%H.
exact H1.
Qed.
Goal forall n, n = S n -> 0=0.
intros n H%n_Sn.
destruct H.
Qed.
(* Another check about generated names and cleared hypotheses with
pat%c patterns *)
Goal (True -> 0=0 /\ 1=1) -> True -> 0=0.
intros H (H1,?)%H.
change (1=1) in H0.
exact H1.
Qed.
(* Checking iterated pat%c1...%cn introduction patterns and side conditions *)
Goal forall A B C D:Prop, (A -> B -> C) -> (C -> D) -> B -> A -> D.
intros * H H0 H1.
intros H2%H%H0.
- exact H2.
- exact H1.
Qed.
(* Bug found by Enrico *)
Goal forall x : nat, True.
intros y%(fun x => x).
Abort.
(* Fixing a bug in the order of side conditions of a "->" step *)
Goal (True -> 1=0) -> 1=1.
intros ->.
- reflexivity.
- exact I.
Qed.
Goal forall x, (True -> x=0) -> 0=x.
intros x ->.
- reflexivity.
- exact I.
Qed.
(* Fixing a bug when destructing a type with let-ins in the constructor *)
Inductive I := C : let x:=1 in x=1 -> I.
Goal I -> True.
intros [x H]. (* Was failing in 8.5 *)
Abort.
(* Ensuring that the (pat1,...,patn) intropatterns has the expected size, up
to skipping let-ins *)
Goal I -> 1=1.
intros (H). (* This skips x *)
exact H.
Qed.
Goal I -> 1=1.
Fail intros (x,H,H').
Fail intros [|].
intros (x,H).
exact H.
Qed.
Goal Acc le 0 -> True.
Fail induction 1 as (n,H). (* Induction hypothesis is missing *)
induction 1 as (n,H,IH).
exact Logic.I.
Qed.
(* Make "intro"/"intros" progress on existential variables *)
Module Evar.
Goal exists (A:Prop), A.
eexists.
unshelve (intro x).
- exact nat.
- exact (x=x).
- auto.
Qed.
Goal exists (A:Prop), A.
eexists.
unshelve (intros x).
- exact nat.
- exact (x=x).
- auto.
Qed.
Definition d := ltac:(intro x; exact (x*x)).
Definition d' : nat -> _ := ltac:(intros;exact 0).
End Evar.
|
