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
190
191
192
193
194
195
196
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* Test des definitions inductives imbriquees *)
Require Import List.
Inductive X : Set :=
cons1 : list X -> X.
Inductive Y : Set :=
cons2 : list (Y * Y) -> Y.
(* Test inductive types with local definitions *)
Inductive eq1 : forall A:Type, let B:=A in A -> Prop :=
refl1 : eq1 True I.
Check
fun (P : forall A : Type, let B := A in A -> Type) (f : P True I) (A : Type) =>
let B := A in
fun (a : A) (e : eq1 A a) =>
match e in (eq1 A0 a0) return (P A0 a0) with
| refl1 => f
end.
Inductive eq2 (A:Type) (a:A)
: forall B C:Type, let D:=(A*B*C)%type in D -> Prop :=
refl2 : eq2 A a unit bool (a,tt,true).
(* Check that induction variables are cleared even with in clause *)
Lemma foo : forall n m : nat, n + m = n + m.
Proof.
intros; induction m as [|m] in n |- *.
auto.
auto.
Qed.
(* Check selection of occurrences by pattern *)
Goal forall x, S x = S (S x).
intros.
induction (S _) in |- * at -2.
now_show (0=1).
Undo 2.
induction (S _) in |- * at 1 3.
now_show (0=1).
Undo 2.
induction (S _) in |- * at 1.
now_show (0=S (S x)).
Undo 2.
induction (S _) in |- * at 2.
now_show (S x=0).
Undo 2.
induction (S _) in |- * at 3.
now_show (S x=1).
Undo 2.
Fail induction (S _) in |- * at 4.
Abort.
(* Check use of "as" clause *)
Inductive I := C : forall x, x<0 -> I -> I.
Goal forall x:I, x=x.
intros.
induction x as [y * IHx].
change (x = x) in IHx. (* We should have IHx:x=x *)
Abort.
(* This was not working in 8.4 *)
Goal forall h:nat->nat, h 0 = h 1 -> h 1 = h 2 -> h 0 = h 2.
intros.
induction h.
2:change (n = h 1 -> n = h 2) in IHn.
Abort.
(* This was not working in 8.4 *)
Goal forall h:nat->nat, h 0 = h 1 -> h 1 = h 2 -> h 0 = h 2.
intros h H H0.
induction h in H |- *.
Abort.
(* "at" was not granted in 8.4 in the next two examples *)
Goal forall h:nat->nat, h 0 = h 1 -> h 1 = h 2 -> h 0 = h 2.
intros h H H0.
induction h in H at 2, H0 at 1.
change (h 0 = 0) in H.
Abort.
Goal forall h:nat->nat, h 0 = h 1 -> h 1 = h 2 -> h 0 = h 2.
intros h H H0.
Fail induction h in H at 2 |- *. (* Incompatible occurrences *)
Abort.
(* Check generalization with dependencies in section variables *)
Section S3.
Variables x : nat.
Definition cond := x = x.
Goal cond -> x = 0.
intros H.
induction x as [|n IHn].
2:change (n = 0) in IHn. (* We don't want a generalization over cond *)
Abort.
End S3.
(* These examples show somehow arbitrary choices of generalization wrt
to indices, when those indices are not linear. We check here 8.4
compatibility: when an index is a subterm of a parameter of the
inductive type, it is not generalized. *)
Inductive repr (x:nat) : nat -> Prop := reprc z : repr x z -> repr x z.
Goal forall x, 0 = x -> repr x x -> True.
intros x H1 H.
induction H.
change True in IHrepr.
Abort.
Goal forall x, 0 = S x -> repr (S x) (S x) -> True.
intros x H1 H.
induction H.
change True in IHrepr.
Abort.
Inductive repr' (x:nat) : nat -> Prop := reprc' z : repr' x (S z) -> repr' x z.
Goal forall x, 0 = x -> repr' x x -> True.
intros x H1 H.
induction H.
change True in IHrepr'.
Abort.
(* In this case, generalization was done in 8.4 and we preserve it; this
is arbitrary choice *)
Inductive repr'' : nat -> nat -> Prop := reprc'' x z : repr'' x z -> repr'' x z.
Goal forall x, 0 = x -> repr'' x x -> True.
intros x H1 H.
induction H.
change (0 = z -> True) in IHrepr''.
Abort.
(* Test double induction *)
(* This was failing in 8.5 and before because of a bug in the order of
hypotheses *)
Inductive I2 : Type :=
C2 : forall x:nat, x=x -> I2.
Goal forall a b:I2, a = b.
double induction a b.
Abort.
(* This was leaving useless hypotheses in 8.5 and before because of
the same bug. This is a change of compatibility. *)
Inductive I3 : Prop :=
C3 : forall x:nat, x=x -> I3.
Goal forall a b:I3, a = b.
double induction a b.
Fail clear H. (* H should have been erased *)
Abort.
(* This one had quantification in reverse order in 8.5 and before *)
(* This is a change of compatibility. *)
Goal forall m n, le m n -> le n m -> n=m.
intros m n. double induction 1 2.
3:destruct 1. (* Should be "S m0 <= m0" *)
Abort.
(* Idem *)
Goal forall m n p q, le m n -> le p q -> n+p=m+q.
intros *. double induction 1 2.
3:clear H2. (* H2 should have been erased *)
Abort.
(* This is unchanged *)
Goal forall m n:nat, n=m.
double induction m n.
Abort.
|
