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
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id: MonoList.v,v 1.2.2.1 2004/07/16 19:31:05 herbelin Exp $ i*)
(** THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED ***)
Require Import Le.
Parameter List_Dom : Set.
Definition A := List_Dom.
Inductive list : Set :=
| nil : list
| cons : A -> list -> list.
Fixpoint app (l m:list) {struct l} : list :=
match l return list with
| nil => m
| cons a l1 => cons a (app l1 m)
end.
Lemma app_nil_end : forall l:list, l = app l nil.
Proof.
intro l; elim l; simpl in |- *; auto.
simple induction 1; auto.
Qed.
Hint Resolve app_nil_end: list v62.
Lemma app_ass : forall l m n:list, app (app l m) n = app l (app m n).
Proof.
intros l m n; elim l; simpl in |- *; auto with list.
simple induction 1; auto with list.
Qed.
Hint Resolve app_ass: list v62.
Lemma ass_app : forall l m n:list, app l (app m n) = app (app l m) n.
Proof.
auto with list.
Qed.
Hint Resolve ass_app: list v62.
Definition tail (l:list) : list :=
match l return list with
| cons _ m => m
| _ => nil
end.
Lemma nil_cons : forall (a:A) (m:list), nil <> cons a m.
intros; discriminate.
Qed.
(****************************************)
(* Length of lists *)
(****************************************)
Fixpoint length (l:list) : nat :=
match l return nat with
| cons _ m => S (length m)
| _ => 0
end.
(******************************)
(* Length order of lists *)
(******************************)
Section length_order.
Definition lel (l m:list) := length l <= length m.
Hint Unfold lel: list.
Variables a b : A.
Variables l m n : list.
Lemma lel_refl : lel l l.
Proof.
unfold lel in |- *; auto with list.
Qed.
Lemma lel_trans : lel l m -> lel m n -> lel l n.
Proof.
unfold lel in |- *; intros.
apply le_trans with (length m); auto with list.
Qed.
Lemma lel_cons_cons : lel l m -> lel (cons a l) (cons b m).
Proof.
unfold lel in |- *; simpl in |- *; auto with list arith.
Qed.
Lemma lel_cons : lel l m -> lel l (cons b m).
Proof.
unfold lel in |- *; simpl in |- *; auto with list arith.
Qed.
Lemma lel_tail : lel (cons a l) (cons b m) -> lel l m.
Proof.
unfold lel in |- *; simpl in |- *; auto with list arith.
Qed.
Lemma lel_nil : forall l':list, lel l' nil -> nil = l'.
Proof.
intro l'; elim l'; auto with list arith.
intros a' y H H0.
(* <list>nil=(cons a' y)
============================
H0 : (lel (cons a' y) nil)
H : (lel y nil)->(<list>nil=y)
y : list
a' : A
l' : list *)
absurd (S (length y) <= 0); auto with list arith.
Qed.
End length_order.
Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons: list
v62.
Fixpoint In (a:A) (l:list) {struct l} : Prop :=
match l with
| nil => False
| cons b m => b = a \/ In a m
end.
Lemma in_eq : forall (a:A) (l:list), In a (cons a l).
Proof.
simpl in |- *; auto with list.
Qed.
Hint Resolve in_eq: list v62.
Lemma in_cons : forall (a b:A) (l:list), In b l -> In b (cons a l).
Proof.
simpl in |- *; auto with list.
Qed.
Hint Resolve in_cons: list v62.
Lemma in_app_or : forall (l m:list) (a:A), In a (app l m) -> In a l \/ In a m.
Proof.
intros l m a.
elim l; simpl in |- *; auto with list.
intros a0 y H H0.
(* ((<A>a0=a)\/(In a y))\/(In a m)
============================
H0 : (<A>a0=a)\/(In a (app y m))
H : (In a (app y m))->((In a y)\/(In a m))
y : list
a0 : A
a : A
m : list
l : list *)
elim H0; auto with list.
intro H1.
(* ((<A>a0=a)\/(In a y))\/(In a m)
============================
H1 : (In a (app y m)) *)
elim (H H1); auto with list.
Qed.
Hint Immediate in_app_or: list v62.
Lemma in_or_app : forall (l m:list) (a:A), In a l \/ In a m -> In a (app l m).
Proof.
intros l m a.
elim l; simpl in |- *; intro H.
(* 1 (In a m)
============================
H : False\/(In a m)
a : A
m : list
l : list *)
elim H; auto with list; intro H0.
(* (In a m)
============================
H0 : False *)
elim H0. (* subProof completed *)
intros y H0 H1.
(* 2 (<A>H=a)\/(In a (app y m))
============================
H1 : ((<A>H=a)\/(In a y))\/(In a m)
H0 : ((In a y)\/(In a m))->(In a (app y m))
y : list *)
elim H1; auto 4 with list.
intro H2.
(* (<A>H=a)\/(In a (app y m))
============================
H2 : (<A>H=a)\/(In a y) *)
elim H2; auto with list.
Qed.
Hint Resolve in_or_app: list v62.
Definition incl (l m:list) := forall a:A, In a l -> In a m.
Hint Unfold incl: list v62.
Lemma incl_refl : forall l:list, incl l l.
Proof.
auto with list.
Qed.
Hint Resolve incl_refl: list v62.
Lemma incl_tl : forall (a:A) (l m:list), incl l m -> incl l (cons a m).
Proof.
auto with list.
Qed.
Hint Immediate incl_tl: list v62.
Lemma incl_tran : forall l m n:list, incl l m -> incl m n -> incl l n.
Proof.
auto with list.
Qed.
Lemma incl_appl : forall l m n:list, incl l n -> incl l (app n m).
Proof.
auto with list.
Qed.
Hint Immediate incl_appl: list v62.
Lemma incl_appr : forall l m n:list, incl l n -> incl l (app m n).
Proof.
auto with list.
Qed.
Hint Immediate incl_appr: list v62.
Lemma incl_cons :
forall (a:A) (l m:list), In a m -> incl l m -> incl (cons a l) m.
Proof.
unfold incl in |- *; simpl in |- *; intros a l m H H0 a0 H1.
(* (In a0 m)
============================
H1 : (<A>a=a0)\/(In a0 l)
a0 : A
H0 : (a:A)(In a l)->(In a m)
H : (In a m)
m : list
l : list
a : A *)
elim H1.
(* 1 (<A>a=a0)->(In a0 m) *)
elim H1; auto with list; intro H2.
(* (<A>a=a0)->(In a0 m)
============================
H2 : <A>a=a0 *)
elim H2; auto with list. (* solves subgoal *)
(* 2 (In a0 l)->(In a0 m) *)
auto with list.
Qed.
Hint Resolve incl_cons: list v62.
Lemma incl_app : forall l m n:list, incl l n -> incl m n -> incl (app l m) n.
Proof.
unfold incl in |- *; simpl in |- *; intros l m n H H0 a H1.
(* (In a n)
============================
H1 : (In a (app l m))
a : A
H0 : (a:A)(In a m)->(In a n)
H : (a:A)(In a l)->(In a n)
n : list
m : list
l : list *)
elim (in_app_or l m a); auto with list.
Qed.
Hint Resolve incl_app: list v62.
|
