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
|
(* Submitted by Robert Schneck *)
Parameters A B C D : Prop.
Axiom X : A -> B -> C /\ D.
Lemma foo : A -> B -> C.
Proof.
intros.
destruct X. (* Should find axiom X and should handle arguments of X *)
assumption.
assumption.
assumption.
Qed.
(* Simplification of bug 711 *)
Parameter f : true = false.
Goal let p := f in True.
intro p.
set (b := true) in *.
(* Check that it doesn't fail with an anomaly *)
(* Ultimately, adapt destruct to make it succeeding *)
try destruct b.
Abort.
(* Used to fail with error "n is used in conclusion" before revision 9447 *)
Goal forall n, n = S n.
induction S.
Abort.
(* Check that elimination with remaining evars do not raise an bad
error message *)
Theorem Refl : forall P, P <-> P. tauto. Qed.
Goal True.
case Refl || ecase Refl.
Abort.
(* Submitted by B. Baydemir (bug #1882) *)
Require Import List.
Definition alist R := list (nat * R)%type.
Section Properties.
Variable A : Type.
Variable a : A.
Variable E : alist A.
Lemma silly : E = E.
Proof.
clear. induction E. (* this fails. *)
Abort.
End Properties.
(* This used not to work before revision 11944 *)
Goal forall P:(forall n, 0=n -> Prop), forall H: 0=0, P 0 H.
destruct H.
Abort.
(* The calls to "destruct" below did not work before revision 12356 *)
Variable A0:Type.
Variable P:A0->Type.
Require Import JMeq.
Goal forall a b (p:P a) (q:P b),
forall H:a = b, eq_rect a P p b H = q -> JMeq (existT _ a p) (existT _ b q).
intros.
destruct H.
destruct H0.
reflexivity.
Qed.
(* These did not work before 8.4 *)
Goal (exists x, x=0) -> True.
destruct 1 as (_,_); exact I.
Abort.
Goal (exists x, x=0 /\ True) -> True.
destruct 1 as (_,(_,H)); exact H.
Abort.
Goal (exists x, x=0 /\ True) -> True.
destruct 1 as (_,(_,x)); exact x.
Abort.
Goal let T:=nat in forall (x:nat) (g:T -> nat), g x = 0.
intros.
destruct (g _). (* This was failing in at least r14571 *)
Abort.
(* Check that subterm selection does not solve existing evars *)
Goal exists x, S x = S 0.
eexists.
Fail destruct (S _). (* Incompatible occurrences *)
Abort.
Goal exists x, S 0 = S x.
eexists.
Fail destruct (S _). (* Incompatible occurrences *)
Abort.
Goal exists n p:nat, (S n,S n) = (S p,S p) /\ p = n.
do 2 eexists.
Fail destruct (_, S _). (* Was succeeding at some time in trunk *)
Show Proof.
(* Avoid unnatural selection of a subterm larger than expected *)
Goal let g := fun x:nat => x in g (S 0) = 0.
intro.
destruct S.
(* Check that it is not the larger subterm "f (S 0)" which is
selected, as it was the case in 8.4 *)
unfold g at 1.
Abort.
|
