]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/basics/lists/list.ma
some results on co-composition ...
[helm.git] / matita / matita / lib / basics / lists / list.ma
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic        
3     ||A||  Library of Mathematics, developed at the Computer Science     
4     ||T||  Department of the University of Bologna, Italy.                     
5     ||I||                                                                 
6     ||T||  
7     ||A||  
8     \   /  This file is distributed under the terms of the       
9      \ /   GNU General Public License Version 2   
10       V_______________________________________________________________ *)
11
12 include "basics/types.ma".
13 include "arithmetics/nat.ma".
14
15 inductive list (A:Type[0]) : Type[0] :=
16   | nil: list A
17   | cons: A -> list A -> list A.
18
19 notation "hvbox(hd break :: tl)"
20   right associative with precedence 47
21   for @{'cons $hd $tl}.
22
23 notation "[ list0 term 19 x sep ; ]"
24   non associative with precedence 90
25   for ${fold right @'nil rec acc @{'cons $x $acc}}.
26
27 notation "hvbox(l1 break @ l2)"
28   right associative with precedence 47
29   for @{'append $l1 $l2 }.
30
31 interpretation "nil" 'nil = (nil ?).
32 interpretation "cons" 'cons hd tl = (cons ? hd tl).
33
34 definition is_nil: ∀A:Type[0].list A → Prop ≝
35  λA.λl.match l with [ nil ⇒ True | cons hd tl ⇒ False ].
36
37 theorem nil_cons:
38   ∀A:Type[0].∀l:list A.∀a:A. a::l ≠ [].
39   #A #l #a @nmk #Heq (change with (is_nil ? (a::l))) >Heq //
40 qed.
41
42 (*
43 let rec id_list A (l: list A) on l :=
44   match l with
45   [ nil => []
46   | (cons hd tl) => hd :: id_list A tl ]. *)
47
48 let rec append A (l1: list A) l2 on l1 ≝ 
49   match l1 with
50   [ nil ⇒  l2
51   | cons hd tl ⇒  hd :: append A tl l2 ].
52
53 definition hd ≝ λA.λl: list A.λd:A.
54   match l with [ nil ⇒ d | cons a _ ⇒ a].
55
56 definition tail ≝  λA.λl: list A.
57   match l with [ nil ⇒  [] | cons hd tl ⇒  tl].
58   
59 definition option_hd ≝ 
60   λA.λl:list A. match l with
61   [ nil ⇒ None ?
62   | cons a _ ⇒ Some ? a ].
63
64 interpretation "append" 'append l1 l2 = (append ? l1 l2).
65
66 theorem append_nil: ∀A.∀l:list A.l @ [] = l.
67 #A #l (elim l) normalize // qed.
68
69 theorem associative_append: 
70  ∀A.associative (list A) (append A).
71 #A #l1 #l2 #l3 (elim l1) normalize // qed.
72
73 theorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1.
74 #A #a #l #l1 >associative_append // qed.
75
76 theorem nil_append_elim: ∀A.∀l1,l2: list A.∀P:?→?→Prop. 
77   l1@l2=[] → P (nil A) (nil A) → P l1 l2.
78 #A #l1 #l2 #P (cases l1) normalize //
79 #a #l3 #heq destruct
80 qed.
81
82 theorem nil_to_nil:  ∀A.∀l1,l2:list A.
83   l1@l2 = [] → l1 = [] ∧ l2 = [].
84 #A #l1 #l2 #isnil @(nil_append_elim A l1 l2) /2/
85 qed.
86
87 lemma cons_injective_l : ∀A.∀a1,a2:A.∀l1,l2.a1::l1 = a2::l2 → a1 = a2.
88 #A #a1 #a2 #l1 #l2 #Heq destruct //
89 qed.
90
91 lemma cons_injective_r : ∀A.∀a1,a2:A.∀l1,l2.a1::l1 = a2::l2 → l1 = l2.
92 #A #a1 #a2 #l1 #l2 #Heq destruct //
93 qed.
94
95 (* option cons *)
96
97 definition option_cons ≝ λsig.λc:option sig.λl.
98   match c with [ None ⇒ l | Some c0 ⇒ c0::l ].
99
100 lemma opt_cons_tail_expand : ∀A,l.l = option_cons A (option_hd ? l) (tail ? l). 
101 #A * //
102 qed.
103
104 (* comparing lists *)
105
106 lemma compare_append : ∀A,l1,l2,l3,l4. l1@l2 = l3@l4 → 
107 ∃l:list A.(l1 = l3@l ∧ l4=l@l2) ∨ (l3 = l1@l ∧ l2=l@l4).
108 #A #l1 elim l1
109   [#l2 #l3 #l4 #Heq %{l3} %2 % // @Heq
110   |#a1 #tl1 #Hind #l2 #l3 cases l3
111     [#l4 #Heq %{(a1::tl1)} %1 % // @sym_eq @Heq 
112     |#a3 #tl3 #l4 normalize in ⊢ (%→?); #Heq cases (Hind l2 tl3 l4 ?)
113       [#l * * #Heq1 #Heq2 %{l}
114         [%1 % // >Heq1 >(cons_injective_l ????? Heq) //
115         |%2 % // >Heq1 >(cons_injective_l ????? Heq) //
116         ]
117       |@(cons_injective_r ????? Heq) 
118       ]
119     ]
120   ]
121 qed.
122
123 (**************************** iterators ******************************)
124
125 let rec map (A,B:Type[0]) (f: A → B) (l:list A) on l: list B ≝
126  match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)].
127
128 lemma map_append : ∀A,B,f,l1,l2.
129   (map A B f l1) @ (map A B f l2) = map A B f (l1@l2).
130 #A #B #f #l1 elim l1
131 [ #l2 @refl
132 | #h #t #IH #l2 normalize //
133 ] qed.
134   
135 let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:list A) on l :B ≝  
136  match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
137  
138 definition filter ≝ 
139   λT.λp:T → bool.
140   foldr T (list T) (λx,l0.if p x then x::l0 else l0) (nil T).
141
142 (* compose f [a1;...;an] [b1;...;bm] = 
143   [f a1 b1; ... ;f an b1; ... ;f a1 bm; f an bm] *)
144  
145 definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2.
146     foldr ?? (λi,acc.(map ?? (f i) l2)@acc) [ ] l1.
147
148 lemma filter_true : ∀A,l,a,p. p a = true → 
149   filter A p (a::l) = a :: filter A p l.
150 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
151
152 lemma filter_false : ∀A,l,a,p. p a = false → 
153   filter A p (a::l) = filter A p l.
154 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
155
156 theorem eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
157 #A #B #f #g #l #eqfg (elim l) normalize // qed.
158
159 (**************************** reverse *****************************)
160 let rec rev_append S (l1,l2:list S) on l1 ≝
161   match l1 with 
162   [ nil ⇒ l2
163   | cons a tl ⇒ rev_append S tl (a::l2)
164   ]
165 .
166
167 definition reverse ≝λS.λl.rev_append S l [].
168
169 lemma reverse_single : ∀S,a. reverse S [a] = [a]. 
170 // qed.
171
172 lemma rev_append_def : ∀S,l1,l2. 
173   rev_append S l1 l2 = (reverse S l1) @ l2 .
174 #S #l1 elim l1 normalize // 
175 qed.
176
177 lemma reverse_cons : ∀S,a,l. reverse S (a::l) = (reverse S l)@[a].
178 #S #a #l whd in ⊢ (??%?); // 
179 qed.
180
181 lemma reverse_append: ∀S,l1,l2. 
182   reverse S (l1 @ l2) = (reverse S l2)@(reverse S l1).
183 #S #l1 elim l1 [normalize // | #a #tl #Hind #l2 >reverse_cons
184 >reverse_cons // qed.
185
186 lemma reverse_reverse : ∀S,l. reverse S (reverse S l) = l.
187 #S #l elim l // #a #tl #Hind >reverse_cons >reverse_append 
188 normalize // qed.
189
190 (* an elimination principle for lists working on the tail;
191 useful for strings *)
192 lemma list_elim_left: ∀S.∀P:list S → Prop. P (nil S) →
193 (∀a.∀tl.P tl → P (tl@[a])) → ∀l. P l.
194 #S #P #Pnil #Pstep #l <(reverse_reverse … l) 
195 generalize in match (reverse S l); #l elim l //
196 #a #tl #H >reverse_cons @Pstep //
197 qed.
198
199 (**************************** length ******************************)
200
201 let rec length (A:Type[0]) (l:list A) on l ≝ 
202   match l with 
203     [ nil ⇒ 0
204     | cons a tl ⇒ S (length A tl)].
205
206 interpretation "list length" 'card l = (length ? l).
207
208 lemma length_tail: ∀A,l. length ? (tail A l) = pred (length ? l).
209 #A #l elim l // 
210 qed.
211
212 lemma length_tail1 : ∀A,l.0 < |l| → |tail A l| < |l|.
213 #A * normalize //
214 qed.
215
216 lemma length_append: ∀A.∀l1,l2:list A. 
217   |l1@l2| = |l1|+|l2|.
218 #A #l1 elim l1 // normalize /2/
219 qed.
220
221 lemma length_map: ∀A,B,l.∀f:A→B. length ? (map ?? f l) = length ? l.
222 #A #B #l #f elim l // #a #tl #Hind normalize //
223 qed.
224
225 lemma length_reverse: ∀A.∀l:list A. 
226   |reverse A l| = |l|.
227 #A #l elim l // #a #l0 #IH >reverse_cons >length_append normalize //
228 qed.
229
230 lemma lenght_to_nil: ∀A.∀l:list A.
231   |l| = 0 → l = [ ].
232 #A * // #a #tl normalize #H destruct
233 qed.
234  
235 lemma lists_length_split : 
236  ∀A.∀l1,l2:list A.(∃la,lb.(|la| = |l1| ∧ l2 = la@lb) ∨ (|la| = |l2| ∧ l1 = la@lb)).
237 #A #l1 elim l1
238 [ #l2 %{[ ]} %{l2} % % %
239 | #hd1 #tl1 #IH *
240   [ %{[ ]} %{(hd1::tl1)} %2 % %
241   | #hd2 #tl2 cases (IH tl2) #x * #y *
242     [ * #IH1 #IH2 %{(hd2::x)} %{y} % normalize % //
243     | * #IH1 #IH2 %{(hd1::x)} %{y} %2 normalize % // ]
244   ]
245 ]
246 qed.
247
248 (****************** traversing two lists in parallel *****************)
249 lemma list_ind2 : 
250   ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:list T1 → list T2 → Prop.
251   length ? l1 = length ? l2 →
252   (P [] []) → 
253   (∀tl1,tl2,hd1,hd2. P tl1 tl2 → P (hd1::tl1) (hd2::tl2)) → 
254   P l1 l2.
255 #T1 #T2 #l1 #l2 #P #Hl #Pnil #Pcons
256 generalize in match Hl; generalize in match l2;
257 elim l1
258 [#l2 cases l2 // normalize #t2 #tl2 #H destruct
259 |#t1 #tl1 #IH #l2 cases l2
260    [normalize #H destruct
261    |#t2 #tl2 #H @Pcons @IH normalize in H; destruct // ]
262 ]
263 qed.
264
265 lemma list_cases2 : 
266   ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:Prop.
267   length ? l1 = length ? l2 →
268   (l1 = [] → l2 = [] → P) → 
269   (∀hd1,hd2,tl1,tl2.l1 = hd1::tl1 → l2 = hd2::tl2 → P) → P.
270 #T1 #T2 #l1 #l2 #P #Hl @(list_ind2 … Hl)
271 [ #Pnil #Pcons @Pnil //
272 | #tl1 #tl2 #hd1 #hd2 #IH1 #IH2 #Hp @Hp // ]
273 qed.
274
275 (*********************** properties of append ***********************)
276 lemma append_l1_injective : 
277   ∀A.∀l1,l2,l3,l4:list A. |l1| = |l2| → l1@l3 = l2@l4 → l1 = l2.
278 #a #l1 #l2 #l3 #l4 #Hlen @(list_ind2 … Hlen) //
279 #tl1 #tl2 #hd1 #hd2 #IH normalize #Heq destruct @eq_f /2/
280 qed.
281   
282 lemma append_l2_injective : 
283   ∀A.∀l1,l2,l3,l4:list A. |l1| = |l2| → l1@l3 = l2@l4 → l3 = l4.
284 #a #l1 #l2 #l3 #l4 #Hlen @(list_ind2 … Hlen) normalize //
285 #tl1 #tl2 #hd1 #hd2 #IH normalize #Heq destruct /2/
286 qed.
287
288 lemma append_l1_injective_r :
289   ∀A.∀l1,l2,l3,l4:list A. |l3| = |l4| → l1@l3 = l2@l4 → l1 = l2.
290 #a #l1 #l2 #l3 #l4 #Hlen #Heq lapply (eq_f … (reverse ?) … Heq)
291 >reverse_append >reverse_append #Heq1
292 lapply (append_l2_injective … Heq1) [ // ] #Heq2
293 lapply (eq_f … (reverse ?) … Heq2) //
294 qed.
295   
296 lemma append_l2_injective_r : 
297   ∀A.∀l1,l2,l3,l4:list A. |l3| = |l4| → l1@l3 = l2@l4 → l3 = l4.
298 #a #l1 #l2 #l3 #l4 #Hlen #Heq lapply (eq_f … (reverse ?) … Heq)
299 >reverse_append >reverse_append #Heq1
300 lapply (append_l1_injective … Heq1) [ // ] #Heq2
301 lapply (eq_f … (reverse ?) … Heq2) //
302 qed.
303
304 lemma length_rev_append: ∀A.∀l,acc:list A. 
305   |rev_append ? l acc| = |l|+|acc|.
306 #A #l elim l // #a #tl #Hind normalize 
307 #acc >Hind normalize // 
308 qed.
309
310 (****************************** mem ********************************)
311 let rec mem A (a:A) (l:list A) on l ≝
312   match l with
313   [ nil ⇒ False
314   | cons hd tl ⇒ a=hd ∨ mem A a tl
315   ]. 
316   
317 lemma mem_append: ∀A,a,l1,l2.mem A a (l1@l2) →
318   mem ? a l1 ∨ mem ? a l2.
319 #A #a #l1 elim l1 
320   [#l2 #mema %2 @mema
321   |#b #tl #Hind #l2 * 
322     [#eqab %1 %1 @eqab 
323     |#Hmema cases (Hind ? Hmema) -Hmema #Hmema [%1 %2 //|%2 //]
324     ]
325   ]
326 qed.
327
328 lemma mem_append_l1: ∀A,a,l1,l2.mem A a l1 → mem A a (l1@l2).
329 #A #a #l1 #l2 elim l1
330   [whd in ⊢ (%→?); @False_ind
331   |#b #tl #Hind * [#eqab %1 @eqab |#Hmema %2 @Hind //]
332   ]
333 qed.
334
335 lemma mem_append_l2: ∀A,a,l1,l2.mem A a l2 → mem A a (l1@l2).
336 #A #a #l1 #l2 elim l1 [//|#b #tl #Hind #Hmema %2 @Hind //]
337 qed.
338
339 lemma mem_single: ∀A,a,b. mem A a [b] → a=b.
340 #A #a #b * // @False_ind
341 qed.
342
343 lemma mem_map: ∀A,B.∀f:A→B.∀l,b. 
344   mem ? b (map … f l) → ∃a. mem ? a l ∧ f a = b.
345 #A #B #f #l elim l 
346   [#b normalize @False_ind
347   |#a #tl #Hind #b normalize *
348     [#eqb @(ex_intro … a) /3/
349     |#memb cases (Hind … memb) #a * #mema #eqb
350      @(ex_intro … a) /3/
351     ]
352   ]
353 qed.
354
355 lemma mem_map_forward: ∀A,B.∀f:A→B.∀a,l. 
356   mem A a l → mem B (f a) (map ?? f l).
357  #A #B #f #a #l elim l
358   [normalize @False_ind
359   |#b #tl #Hind * 
360     [#eqab <eqab normalize %1 % |#memtl normalize %2 @Hind @memtl]
361   ]
362 qed.
363
364 (****************************** mem filter ***************************)
365 lemma mem_filter: ∀S,f,a,l. 
366   mem S a (filter S f l) → mem S a l.
367 #S #f #a #l elim l [normalize //]
368 #b #tl #Hind normalize (cases (f b)) normalize
369   [* [#eqab %1 @eqab | #H %2 @Hind @H]
370   |#H %2 @Hind @H]
371 qed.
372
373 lemma mem_filter_true: ∀S,f,a,l. 
374   mem S a (filter S f l)  → f a = true.
375 #S #f #a #l elim l [normalize @False_ind ]
376 #b #tl #Hind cases (true_or_false (f b)) #H
377 normalize >H normalize [2:@Hind]
378 * [#eqab // | @Hind]
379 qed. 
380
381 lemma mem_filter_l: ∀S,f,x,l. (f x = true) → mem S x l →
382 mem S x (filter ? f l).
383 #S #f #x #l #fx elim l [@False_ind]
384 #b #tl #Hind * 
385   [#eqxb <eqxb >(filter_true ???? fx) %1 % 
386   |#Htl cases (true_or_false (f b)) #fb 
387     [>(filter_true ???? fb) %2 @Hind @Htl
388     |>(filter_false ???? fb) @Hind @Htl
389     ]
390   ]
391 qed.
392
393 lemma filter_case: ∀A,p,l,x. mem ? x l → 
394   mem ? x (filter A p l) ∨ mem ? x (filter A (λx.¬ p x) l).
395 #A #p #l elim l 
396   [#x @False_ind 
397   |#a #tl #Hind #x * 
398     [#eqxa >eqxa cases (true_or_false (p a)) #Hcase
399       [%1 >(filter_true A tl a p Hcase) %1 % 
400       |%2 >(filter_true A tl a ??) [%1 % | >Hcase %]
401       ]
402     |#memx cases (Hind … memx) -memx #memx
403       [%1 cases (true_or_false (p a)) #Hpa 
404         [>(filter_true A tl a p Hpa) %2 @memx
405         |>(filter_false A tl a p Hpa) @memx
406         ]
407       |cases (true_or_false (p a)) #Hcase
408         [%2 >(filter_false A tl a) [@memx |>Hcase %]
409         |%2 >(filter_true A tl a) [%2 @memx|>Hcase %]
410         ]
411       ]
412     ]
413   ]
414 qed.
415
416 lemma filter_length2: ∀A,p,l. |filter A p l|+|filter A (λx.¬ p x) l| = |l|.
417 #A #p #l elim l //
418 #a #tl #Hind cases (true_or_false (p a)) #Hcase
419   [>(filter_true A tl a p Hcase) >(filter_false A tl a ??) 
420     [@(eq_f ?? S) @Hind | >Hcase %]
421   |>(filter_false A tl a p Hcase) >(filter_true A tl a ??) 
422     [<plus_n_Sm @(eq_f ?? S) @Hind | >Hcase %]
423   ]
424 qed.
425
426 (***************************** unique *******************************)
427 let rec unique A (l:list A) on l ≝ 
428   match l with 
429   [nil ⇒ True
430   |cons a tl ⇒ ¬ mem A a tl ∧ unique A tl].
431
432 lemma unique_filter : ∀S,l,f.
433  unique S l → unique S (filter S f l).
434 #S #l #f elim l //
435 #a #tl #Hind * 
436 #memba #uniquetl cases (true_or_false … (f a)) #Hfa
437   [>(filter_true ???? Hfa) % 
438     [@(not_to_not … memba) @mem_filter |/2/ ]
439   |>filter_false /2/
440   ]
441 qed.
442
443 lemma filter_eqb : ∀m,l. unique ? l → 
444   (mem ? m l ∧ filter ? (eqb m) l = [m])∨(¬mem ? m l ∧ filter ? (eqb m) l = []).
445 #m #l elim l
446   [#_ %2 % [% @False_ind | //]
447   |#a #tl #Hind * #Hmema #Hunique
448    cases (Hind Hunique)
449     [* #Hmemm #Hind %1 % [%2 //]
450      >filter_false // @not_eq_to_eqb_false % #eqma @(absurd ? Hmemm) //
451     |* #Hmemm #Hind cases (decidable_eq_nat m a) #eqma 
452       [%1 <eqma % [%1 //] >filter_true [2: @eq_to_eqb_true //] >Hind //
453       |%2 % 
454         [@(not_to_not … Hmemm) * // #H @False_ind  @(absurd … H) //
455         |>filter_false // @not_eq_to_eqb_false @eqma
456         ]
457       ]
458     ]
459   ]
460 qed.
461
462 lemma length_filter_eqb: ∀m,l. unique ? l → 
463   |filter ? (eqb m) l| ≤ 1.
464 #m #l #Huni cases (filter_eqb m l Huni) * #_ #H >H // 
465 qed. 
466
467 (***************************** split *******************************)
468 let rec split_rev A (l:list A) acc n on n ≝ 
469   match n with 
470   [O ⇒ 〈acc,l〉
471   |S m ⇒ match l with 
472     [nil ⇒ 〈acc,[]〉
473     |cons a tl ⇒ split_rev A tl (a::acc) m
474     ]
475   ].
476   
477 definition split ≝ λA,l,n.
478   let 〈l1,l2〉 ≝ split_rev A l [] n in 〈reverse ? l1,l2〉.
479
480 lemma split_rev_len: ∀A,n,l,acc. n ≤ |l| →
481   |\fst (split_rev A l acc n)| = n+|acc|.
482 #A #n elim n // #m #Hind *
483   [normalize #acc #Hfalse @False_ind /2/
484   |#a #tl #acc #Hlen normalize >Hind 
485     [normalize // |@le_S_S_to_le //]
486   ]
487 qed.
488
489 lemma split_len: ∀A,n,l. n ≤ |l| →
490   |\fst (split A l n)| = n.
491 #A #n #l #Hlen normalize >(eq_pair_fst_snd ?? (split_rev …))
492 normalize >length_reverse  >(split_rev_len … [ ] Hlen) normalize //
493 qed.
494   
495 lemma split_rev_eq: ∀A,n,l,acc. n ≤ |l| → 
496   reverse ? acc@ l = 
497     reverse ? (\fst (split_rev A l acc n))@(\snd (split_rev A l acc n)).
498  #A #n elim n //
499  #m #Hind * 
500    [#acc whd in ⊢ ((??%)→?); #False_ind /2/ 
501    |#a #tl #acc #Hlen >append_cons <reverse_single <reverse_append 
502     @(Hind tl) @le_S_S_to_le @Hlen
503    ]
504 qed.
505  
506 lemma split_eq: ∀A,n,l. n ≤ |l| → 
507   l = (\fst (split A l n))@(\snd (split A l n)).
508 #A #n #l #Hlen change with ((reverse ? [ ])@l) in ⊢ (??%?);
509 >(split_rev_eq … Hlen) normalize 
510 >(eq_pair_fst_snd ?? (split_rev A l [] n)) %
511 qed.
512
513 lemma split_exists: ∀A,n.∀l:list A. n ≤ |l| → 
514   ∃l1,l2. l = l1@l2 ∧ |l1| = n.
515 #A #n #l #Hlen @(ex_intro … (\fst (split A l n)))
516 @(ex_intro … (\snd (split A l n))) % /2/
517 qed.
518   
519 (****************************** flatten ******************************)
520 definition flatten ≝ λA.foldr (list A) (list A) (append A) [].
521
522 lemma flatten_to_mem: ∀A,n,l,l1,l2.∀a:list A. 0 < n →
523   (∀x. mem ? x l → |x| = n) → |a| = n → flatten ? l = l1@a@l2  →
524     (∃q.|l1| = n*q)  → mem ? a l.
525 #A #n #l elim l
526   [normalize #l1 #l2 #a #posn #Hlen #Ha #Hnil @False_ind
527    cut (|a|=0) [@sym_eq @le_n_O_to_eq 
528    @(transitive_le ? (|nil A|)) // >Hnil >length_append >length_append //] /2/
529   |#hd #tl #Hind #l1 #l2 #a #posn #Hlen #Ha 
530    whd in match (flatten ??); #Hflat * #q cases q
531     [<times_n_O #Hl1 
532      cut (a = hd) [>(lenght_to_nil… Hl1) in Hflat; 
533      whd in ⊢ ((???%)→?); #Hflat @sym_eq @(append_l1_injective … Hflat)
534      >Ha >Hlen // %1 //   
535      ] /2/
536     |#q1 #Hl1 lapply (split_exists … n l1 ?) //
537      * #l11 * #l12 * #Heql1 #Hlenl11 %2
538      @(Hind l12 l2 … posn ? Ha) 
539       [#x #memx @Hlen %2 //
540       |@(append_l2_injective ? hd l11) 
541         [>Hlenl11 @Hlen %1 %
542         |>Hflat >Heql1 >associative_append %
543         ]
544       |@(ex_intro …q1) @(injective_plus_r n) 
545        <Hlenl11 in ⊢ (??%?); <length_append <Heql1 >Hl1 //
546       ]
547     ]
548   ]
549 qed.
550
551 (****************************** nth ********************************)
552 let rec nth n (A:Type[0]) (l:list A) (d:A)  ≝  
553   match n with
554     [O ⇒ hd A l d
555     |S m ⇒ nth m A (tail A l) d].
556
557 lemma nth_nil: ∀A,a,i. nth i A ([]) a = a.
558 #A #a #i elim i normalize //
559 qed.
560
561 (****************************** nth_opt ********************************)
562 let rec nth_opt (A:Type[0]) (n:nat) (l:list A) on l : option A ≝
563 match l with
564 [ nil ⇒ None ?
565 | cons h t ⇒ match n with [ O ⇒ Some ? h | S m ⇒ nth_opt A m t ]
566 ].
567
568 (**************************** All *******************************)
569
570 let rec All (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
571 match l with
572 [ nil ⇒ True
573 | cons h t ⇒ P h ∧ All A P t
574 ].
575
576 lemma All_mp : ∀A,P,Q. (∀a.P a → Q a) → ∀l. All A P l → All A Q l.
577 #A #P #Q #H #l elim l normalize //
578 #h #t #IH * /3/
579 qed.
580
581 lemma All_nth : ∀A,P,n,l.
582   All A P l →
583   ∀a.
584   nth_opt A n l = Some A a →
585   P a.
586 #A #P #n elim n
587 [ * [ #_ #a #E whd in E:(??%?); destruct
588     | #hd #tl * #H #_ #a #E whd in E:(??%?); destruct @H
589     ]
590 | #m #IH *
591   [ #_ #a #E whd in E:(??%?); destruct
592   | #hd #tl * #_ whd in ⊢ (? → ∀_.??%? → ?); @IH
593   ]
594 ] qed.
595
596 lemma All_append: ∀A,P,l1,l2. All A P l1 → All A P l2 → All A P (l1@l2).
597 #A #P #l1 elim l1 -l1 //
598 #a #l1 #IHl1 #l2 * /3 width=1/
599 qed.
600
601 lemma All_inv_append: ∀A,P,l1,l2. All A P (l1@l2) → All A P l1 ∧ All A P l2.
602 #A #P #l1 elim l1 -l1 /2 width=1/
603 #a #l1 #IHl1 #l2 * #Ha #Hl12
604 elim (IHl1 … Hl12) -IHl1 -Hl12 /3 width=1/
605 qed-.
606
607 (**************************** Allr ******************************)
608
609 let rec Allr (A:Type[0]) (R:relation A) (l:list A) on l : Prop ≝
610 match l with
611 [ nil       ⇒ True
612 | cons a1 l ⇒ match l with [ nil ⇒ True | cons a2 _ ⇒ R a1 a2 ∧ Allr A R l ]
613 ].
614
615 lemma Allr_fwd_append_sn: ∀A,R,l1,l2. Allr A R (l1@l2) → Allr A R l1.
616 #A #R #l1 elim l1 -l1 // #a1 * // #a2 #l1 #IHl1 #l2 * /3 width=2/
617 qed-.
618
619 lemma Allr_fwd_cons: ∀A,R,a,l. Allr A R (a::l) → Allr A R l.
620 #A #R #a * // #a0 #l * //
621 qed-.
622
623 lemma Allr_fwd_append_dx: ∀A,R,l1,l2. Allr A R (l1@l2) → Allr A R l2.
624 #A #R #l1 elim l1 -l1 // #a1 #l1 #IHl1 #l2 #H
625 lapply (Allr_fwd_cons … (l1@l2) H) -H /2 width=1/
626 qed-.  
627
628 (**************************** Exists *******************************)
629
630 let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
631 match l with
632 [ nil ⇒ False
633 | cons h t ⇒ (P h) ∨ (Exists A P t)
634 ].
635
636 lemma Exists_append : ∀A,P,l1,l2.
637   Exists A P (l1 @ l2) → Exists A P l1 ∨ Exists A P l2.
638 #A #P #l1 elim l1
639 [ normalize /2/
640 | #h #t #IH #l2 *
641   [ #H /3/
642   | #H cases (IH l2 H) /3/
643   ]
644 ] qed.
645
646 lemma Exists_append_l : ∀A,P,l1,l2.
647   Exists A P l1 → Exists A P (l1@l2).
648 #A #P #l1 #l2 elim l1
649 [ *
650 | #h #t #IH *
651   [ #H %1 @H
652   | #H %2 @IH @H
653   ]
654 ] qed.
655
656 lemma Exists_append_r : ∀A,P,l1,l2.
657   Exists A P l2 → Exists A P (l1@l2).
658 #A #P #l1 #l2 elim l1
659 [ #H @H
660 | #h #t #IH #H %2 @IH @H
661 ] qed.
662
663 lemma Exists_add : ∀A,P,l1,x,l2. Exists A P (l1@l2) → Exists A P (l1@x::l2).
664 #A #P #l1 #x #l2 elim l1
665 [ normalize #H %2 @H
666 | #h #t #IH normalize * [ #H %1 @H | #H %2 @IH @H ]
667 qed.
668
669 lemma Exists_mid : ∀A,P,l1,x,l2. P x → Exists A P (l1@x::l2).
670 #A #P #l1 #x #l2 #H elim l1
671 [ %1 @H
672 | #h #t #IH %2 @IH
673 ] qed.
674
675 lemma Exists_map : ∀A,B,P,Q,f,l.
676 Exists A P l →
677 (∀a.P a → Q (f a)) →
678 Exists B Q (map A B f l).
679 #A #B #P #Q #f #l elim l //
680 #h #t #IH * [ #H #F %1 @F @H | #H #F %2 @IH [ @H | @F ] ] qed.
681
682 lemma Exists_All : ∀A,P,Q,l.
683   Exists A P l →
684   All A Q l →
685   ∃x. P x ∧ Q x.
686 #A #P #Q #l elim l [ * | #hd #tl #IH * [ #H1 * #H2 #_ %{hd} /2/ | #H1 * #_ #H2 @IH // ]
687 qed.
688
689 (**************************** fold *******************************)
690
691 let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→bool) (f:A→B) (l:list A) on l :B ≝  
692  match l with 
693   [ nil ⇒ b 
694   | cons a l ⇒
695      if p a then op (f a) (fold A B op b p f l)
696      else fold A B op b p f l].
697       
698 notation "\fold  [ op , nil ]_{ ident i ∈ l | p} f"
699   with precedence 80
700 for @{'fold $op $nil (λ${ident i}. $p) (λ${ident i}. $f) $l}.
701
702 notation "\fold [ op , nil ]_{ident i ∈ l } f"
703   with precedence 80
704 for @{'fold $op $nil (λ${ident i}.true) (λ${ident i}. $f) $l}.
705
706 interpretation "\fold" 'fold op nil p f l = (fold ? ? op nil p f l).
707
708 theorem fold_true: 
709 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a = true → 
710   \fold[op,nil]_{i ∈ a::l| p i} (f i) = 
711     op (f a) \fold[op,nil]_{i ∈ l| p i} (f i). 
712 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
713
714 theorem fold_false: 
715 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f.
716 p a = false → \fold[op,nil]_{i ∈ a::l| p i} (f i) = 
717   \fold[op,nil]_{i ∈ l| p i} (f i).
718 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
719
720 theorem fold_filter: 
721 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B.
722   \fold[op,nil]_{i ∈ l| p i} (f i) = 
723     \fold[op,nil]_{i ∈ (filter A p l)} (f i).
724 #A #B #a #l #p #op #nil #f elim l //  
725 #a #tl #Hind cases(true_or_false (p a)) #pa 
726   [ >filter_true // > fold_true // >fold_true //
727   | >filter_false // >fold_false // ]
728 qed.
729
730 record Aop (A:Type[0]) (nil:A) : Type[0] ≝
731   {op :2> A → A → A; 
732    nill:∀a. op nil a = a; 
733    nilr:∀a. op a nil = a;
734    assoc: ∀a,b,c.op a (op b c) = op (op a b) c
735   }.
736
737 theorem fold_sum: ∀A,B. ∀I,J:list A.∀nil.∀op:Aop B nil.∀f.
738   op (\fold[op,nil]_{i∈I} (f i)) (\fold[op,nil]_{i∈J} (f i)) =
739     \fold[op,nil]_{i∈(I@J)} (f i).
740 #A #B #I #J #nil #op #f (elim I) normalize 
741   [>nill //|#a #tl #Hind <assoc //]
742 qed.
743
744 (********************** lhd and ltl ******************************)
745
746 let rec lhd (A:Type[0]) (l:list A) n on n ≝ match n with
747    [ O   ⇒ nil …
748    | S n ⇒ match l with [ nil ⇒ nil … | cons a l ⇒ a :: lhd A l n ]
749    ].
750
751 let rec ltl (A:Type[0]) (l:list A) n on n ≝ match n with
752    [ O   ⇒ l
753    | S n ⇒ ltl A (tail … l) n
754    ].
755
756 lemma lhd_nil: ∀A,n. lhd A ([]) n = [].
757 #A #n elim n //
758 qed.
759
760 lemma ltl_nil: ∀A,n. ltl A ([]) n = [].
761 #A #n elim n normalize //
762 qed.
763
764 lemma lhd_cons_ltl: ∀A,n,l. lhd A l n @ ltl A l n = l.
765 #A #n elim n -n //
766 #n #IHn #l elim l normalize //
767 qed.
768
769 lemma length_ltl: ∀A,n,l. |ltl A l n| = |l| - n.
770 #A #n elim n -n // 
771 #n #IHn *; normalize /2/
772 qed.
773
774 (********************** find ******************************)
775 let rec find (A,B:Type[0]) (f:A → option B) (l:list A) on l : option B ≝
776 match l with
777 [ nil ⇒ None B
778 | cons h t ⇒
779     match f h with
780     [ None ⇒ find A B f t
781     | Some b ⇒ Some B b
782     ]
783 ].
784
785 (********************** position_of ******************************)
786 let rec position_of_aux (A:Type[0]) (found: A → bool) (l:list A) (acc:nat) on l : option nat ≝
787 match l with
788 [ nil ⇒ None ?
789 | cons h t ⇒
790    match found h with [true ⇒ Some … acc | false ⇒ position_of_aux … found t (S acc)]].
791
792 definition position_of: ∀A:Type[0]. (A → bool) → list A → option nat ≝
793  λA,found,l. position_of_aux A found l 0.
794
795
796 (********************** make_list ******************************)
797 let rec make_list (A:Type[0]) (a:A) (n:nat) on n : list A ≝
798 match n with
799 [ O ⇒ [ ]
800 | S m ⇒ a::(make_list A a m)
801 ].