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
|
Axiom magic : False.
(* Submitted by Dachuan Yu (bug #220) *)
Fixpoint T (n : nat) : Type :=
match n with
| O => nat -> Prop
| S n' => T n'
end.
Inductive R : forall n : nat, T n -> nat -> Prop :=
| RO : forall (Psi : T 0) (l : nat), Psi l -> R 0 Psi l
| RS :
forall (n : nat) (Psi : T (S n)) (l : nat), R n Psi l -> R (S n) Psi l.
Definition Psi00 (n : nat) : Prop := False.
Definition Psi0 : T 0 := Psi00.
Lemma Inversion_RO : forall l : nat, R 0 Psi0 l -> Psi00 l.
inversion 1.
Abort.
(* Submitted by Pierre Casteran (bug #540) *)
Set Implicit Arguments.
Unset Strict Implicit.
Parameter rule : Set -> Type.
Inductive extension (I : Set) : Type :=
| NL : extension I
| add_rule : rule I -> extension I -> extension I.
Inductive in_extension (I : Set) (r : rule I) : extension I -> Type :=
| in_first : forall e, in_extension r (add_rule r e)
| in_rest : forall e r', in_extension r e -> in_extension r (add_rule r' e).
Implicit Arguments NL [I].
Inductive super_extension (I : Set) (e : extension I) :
extension I -> Type :=
| super_NL : super_extension e NL
| super_add :
forall r (e' : extension I),
in_extension r e ->
super_extension e e' -> super_extension e (add_rule r e').
Lemma super_def :
forall (I : Set) (e1 e2 : extension I),
super_extension e2 e1 -> forall ru, in_extension ru e1 -> in_extension ru e2.
Proof.
simple induction 1.
inversion 1; auto.
elim magic.
Qed.
(* Example from Norbert Schirmer on Coq-Club, Sep 2000 *)
Set Strict Implicit.
Unset Implicit Arguments.
Definition Q (n m : nat) (prf : n <= m) := True.
Goal forall (n m : nat) (H : S n <= m), Q (S n) m H = True.
intros.
dependent inversion_clear H.
elim magic.
elim magic.
Qed.
(* Submitted by Boris Yakobowski (bug #529) *)
(* Check that Inversion does not fail due to unnormalized evars *)
Set Implicit Arguments.
Unset Strict Implicit.
Require Import Bvector.
Inductive I : nat -> Set :=
| C1 : I 1
| C2 : forall k i : nat, Vector.t (I i) k -> I i.
Inductive SI : forall k : nat, I k -> Vector.t nat k -> nat -> Prop :=
SC2 :
forall (k i vf : nat) (v : Vector.t (I i) k) (xi : Vector.t nat i),
SI (C2 v) xi vf.
Theorem SUnique :
forall (k : nat) (f : I k) (c : Vector.t nat k) v v',
SI f c v -> SI f c v' -> v = v'.
Proof.
induction 1.
intros H; inversion H.
Admitted.
(* Used to failed at some time *)
Set Strict Implicit.
Unset Implicit Arguments.
Parameter bar : forall p q : nat, p = q -> Prop.
Inductive foo : nat -> nat -> Prop :=
C : forall (a b : nat) (Heq : a = b), bar a b Heq -> foo a b.
Lemma depinv : forall a b, foo a b -> True.
intros a b H.
inversion H.
Abort.
(* Check non-regression of bug #1968 *)
Inductive foo2 : option nat -> Prop := Foo : forall t, foo2 (Some t).
Goal forall o, foo2 o -> 0 = 1.
intros.
eapply trans_eq.
inversion H.
(* Check that the part of "injection" that is called by "inversion"
does the same number of intros as the number of equations
introduced, even in presence of dependent equalities that
"injection" renounces to split *)
Fixpoint prodn (n : nat) :=
match n with
| O => unit
| (S m) => prod (prodn m) nat
end.
Inductive U : forall n : nat, prodn n -> bool -> Prop :=
| U_intro : U 0 tt true.
Lemma foo3 : forall n (t : prodn n), U n t true -> False.
Proof.
(* used to fail because dEqThen thought there were 2 new equations but
inject_at_positions actually introduced only one; leading then to
an inconsistent state that disturbed "inversion" *)
intros. inversion H.
Abort.
(* Bug #2314 (simplified): check that errors do not show as anomalies *)
Goal True -> True.
intro.
Fail inversion H using False.
Fail inversion foo using True_ind.
|
