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
|
(************************************************************************)
(* 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.1.2.1 2004/07/16 19:31:28 herbelin Exp $ i*)
(** THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED ***)
Require Le.
Parameter List_Dom:Set.
Definition A := List_Dom.
Inductive list : Set := nil : list | cons : A -> list -> list.
Fixpoint app [l:list] : list -> list
:= [m:list]<list>Cases l of
nil => m
| (cons a l1) => (cons a (app l1 m))
end.
Lemma app_nil_end : (l:list)(l=(app l nil)).
Proof.
Intro l ; Elim l ; Simpl ; Auto.
Induction 1; Auto.
Qed.
Hints Resolve app_nil_end : list v62.
Lemma app_ass : (l,m,n : list)(app (app l m) n)=(app l (app m n)).
Proof.
Intros l m n ; Elim l ; Simpl ; Auto with list.
Induction 1; Auto with list.
Qed.
Hints Resolve app_ass : list v62.
Lemma ass_app : (l,m,n : list)(app l (app m n))=(app (app l m) n).
Proof.
Auto with list.
Qed.
Hints Resolve ass_app : list v62.
Definition tail :=
[l:list] <list>Cases l of (cons _ m) => m | _ => nil end : list->list.
Lemma nil_cons : (a:A)(m:list)~nil=(cons a m).
Intros; Discriminate.
Qed.
(****************************************)
(* Length of lists *)
(****************************************)
Fixpoint length [l:list] : nat
:= <nat>Cases l of (cons _ m) => (S (length m)) | _ => O end.
(******************************)
(* Length order of lists *)
(******************************)
Section length_order.
Definition lel := [l,m:list](le (length l) (length m)).
Hints Unfold lel : list.
Variables a,b:A.
Variables l,m,n:list.
Lemma lel_refl : (lel l l).
Proof.
Unfold lel ; Auto with list.
Qed.
Lemma lel_trans : (lel l m)->(lel m n)->(lel l n).
Proof.
Unfold lel ; 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 ; Simpl ; Auto with list arith.
Qed.
Lemma lel_cons : (lel l m)->(lel l (cons b m)).
Proof.
Unfold lel ; Simpl ; Auto with list arith.
Qed.
Lemma lel_tail : (lel (cons a l) (cons b m)) -> (lel l m).
Proof.
Unfold lel ; Simpl ; Auto with list arith.
Qed.
Lemma lel_nil : (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 (le (S (length y)) O); Auto with list arith.
Qed.
End length_order.
Hints Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons : list v62.
Fixpoint In [a:A;l:list] : Prop :=
Cases l of
nil => False
| (cons b m) => (b=a)\/(In a m)
end.
Lemma in_eq : (a:A)(l:list)(In a (cons a l)).
Proof.
Simpl ; Auto with list.
Qed.
Hints Resolve in_eq : list v62.
Lemma in_cons : (a,b:A)(l:list)(In b l)->(In b (cons a l)).
Proof.
Simpl ; Auto with list.
Qed.
Hints Resolve in_cons : list v62.
Lemma in_app_or : (l,m:list)(a:A)(In a (app l m))->((In a l)\/(In a m)).
Proof.
Intros l m a.
Elim l ; Simpl ; 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.
Hints Immediate in_app_or : list v62.
Lemma in_or_app : (l,m:list)(a:A)((In a l)\/(In a m))->(In a (app l m)).
Proof.
Intros l m a.
Elim l ; Simpl ; 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.
Hints Resolve in_or_app : list v62.
Definition incl := [l,m:list](a:A)(In a l)->(In a m).
Hints Unfold incl : list v62.
Lemma incl_refl : (l:list)(incl l l).
Proof.
Auto with list.
Qed.
Hints Resolve incl_refl : list v62.
Lemma incl_tl : (a:A)(l,m:list)(incl l m)->(incl l (cons a m)).
Proof.
Auto with list.
Qed.
Hints Immediate incl_tl : list v62.
Lemma incl_tran : (l,m,n:list)(incl l m)->(incl m n)->(incl l n).
Proof.
Auto with list.
Qed.
Lemma incl_appl : (l,m,n:list)(incl l n)->(incl l (app n m)).
Proof.
Auto with list.
Qed.
Hints Immediate incl_appl : list v62.
Lemma incl_appr : (l,m,n:list)(incl l n)->(incl l (app m n)).
Proof.
Auto with list.
Qed.
Hints Immediate incl_appr : list v62.
Lemma incl_cons : (a:A)(l,m:list)(In a m)->(incl l m)->(incl (cons a l) m).
Proof.
Unfold incl ; Simpl ; 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.
Hints Resolve incl_cons : list v62.
Lemma incl_app : (l,m,n:list)(incl l n)->(incl m n)->(incl (app l m) n).
Proof.
Unfold incl ; Simpl ; 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.
Hints Resolve incl_app : list v62.
|
