]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/ng_assembly2/common/list.ma
arithmetics for λδ
[helm.git] / matita / matita / contribs / ng_assembly2 / common / list.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* ********************************************************************** *)
16 (*                          Progetto FreeScale                            *)
17 (*                                                                        *)
18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
19 (*   Sviluppo: 2008-2010                                                  *)
20 (*                                                                        *)
21 (* ********************************************************************** *)
22
23 include "common/comp.ma".
24 include "common/option.ma".
25 include "common/nat.ma".
26
27 (* *************** *)
28 (* LISTE GENERICHE *)
29 (* *************** *)
30
31 ninductive list (A:Type) : Type ≝
32   nil: list A
33 | cons: A → list A → list A.
34
35 nlet rec append A (l1: list A) l2 on l1 ≝
36  match l1 with
37   [ nil ⇒ l2
38   | (cons hd tl) ⇒ cons A hd (append A tl l2) ].
39
40 notation "hvbox(hd break :: tl)"
41   right associative with precedence 47
42   for @{'cons $hd $tl}.
43
44 notation "[ list0 x sep ; ]"
45   non associative with precedence 90
46   for ${fold right @'nil rec acc @{'cons $x $acc}}.
47
48 notation "hvbox(l1 break @ l2)"
49   right associative with precedence 47
50   for @{'append $l1 $l2 }.
51
52 interpretation "nil" 'nil = (nil ?).
53 interpretation "cons" 'cons hd tl = (cons ? hd tl).
54 interpretation "append" 'append l1 l2 = (append ? l1 l2).
55
56 nlemma list_destruct_1 : ∀T.∀x1,x2:T.∀y1,y2:list T.cons T x1 y1 = cons T x2 y2 → x1 = x2.
57  #T; #x1; #x2; #y1; #y2; #H;
58  nchange with (match cons T x2 y2 with [ nil ⇒ False | cons a _ ⇒ x1 = a ]);
59  nrewrite < H;
60  nnormalize;
61  napply refl_eq.
62 nqed.
63
64 nlemma list_destruct_2 : ∀T.∀x1,x2:T.∀y1,y2:list T.cons T x1 y1 = cons T x2 y2 → y1 = y2.
65  #T; #x1; #x2; #y1; #y2; #H;
66  nchange with (match cons T x2 y2 with [ nil ⇒ False | cons _ b ⇒ y1 = b ]);
67  nrewrite < H;
68  nnormalize;
69  napply refl_eq.
70 nqed.
71
72 nlemma list_destruct_cons_nil : ∀T.∀x:T.∀y:list T.cons T x y = nil T → False.
73  #T; #x; #y; #H;
74  nchange with (match cons T x y with [ nil ⇒ True | cons a b ⇒ False ]);
75  nrewrite > H;
76  nnormalize;
77  napply I.
78 nqed.
79
80 nlemma list_destruct_nil_cons : ∀T.∀x:T.∀y:list T.nil T = cons T x y → False.
81  #T; #x; #y; #H;
82  nchange with (match cons T x y with [ nil ⇒ True | cons a b ⇒ False ]);
83  nrewrite < H;
84  nnormalize;
85  napply I.
86 nqed.
87
88 nlemma append_nil : ∀T:Type.∀l:list T.(l@[]) = l.
89  #T; #l;
90  nelim l;
91  nnormalize;
92  ##[ ##1: napply refl_eq
93  ##| ##2: #x; #y; #H;
94           nrewrite > H;
95           napply refl_eq
96  ##]
97 nqed.
98
99 nlemma associative_list : ∀T.associative (list T) (append T).
100  #T; #x; #y; #z;
101  nelim x;
102  nnormalize;
103  ##[ ##1: napply refl_eq
104  ##| ##2: #a; #b; #H;
105           nrewrite > H;
106           napply refl_eq
107  ##]
108 nqed.
109
110 nlemma cons_append_commute : ∀T:Type.∀l1,l2:list T.∀a:T.a :: (l1 @ l2) = (a :: l1) @ l2.
111  #T; #l1; #l2; #a;
112  nnormalize;
113  napply refl_eq.
114 nqed.
115
116 nlemma append_cons_commute : ∀T:Type.∀a:T.∀l,l1:list T.l @ (a::l1) = (l@[a]) @ l1.
117  #T; #a; #l; #l1;
118  nrewrite > (associative_list T l [a] l1);
119  nnormalize;
120  napply refl_eq.
121 nqed.
122
123 (* listlen *)
124 nlet rec len_list (T:Type) (l:list T) on l ≝
125  match l with [ nil ⇒ O | cons _ t ⇒ S (len_list T t) ].
126
127 (* vuota? *)
128 ndefinition is_empty_list ≝
129 λT:Type.λl:list T.match l with [ nil ⇒ True | cons _ _ ⇒ False ].
130
131 ndefinition isb_empty_list ≝
132 λT:Type.λl:list T.match l with [ nil ⇒ true | cons _ _ ⇒ false ].
133
134 ndefinition isnot_empty_list ≝
135 λT:Type.λl:list T.match l with [ nil ⇒ False | cons _ _ ⇒ True ].
136
137 ndefinition isnotb_empty_list ≝
138 λT:Type.λl:list T.match l with [ nil ⇒ false | cons _ _ ⇒ true ].
139
140 (* reverse *)
141 nlet rec reverse_list (T:Type) (l:list T) on l ≝
142  match l with
143   [ nil ⇒ nil T
144   | cons h t ⇒ (reverse_list T t)@[h]
145   ].
146
147 (* getFirst *)
148 ndefinition get_first_list ≝
149 λT:Type.λl:list T.match l with
150  [ nil ⇒ None ?
151  | cons h _ ⇒ Some ? h ].
152
153 (* getLast *)
154 ndefinition get_last_list ≝
155 λT:Type.λl:list T.match reverse_list T l with
156  [ nil ⇒ None ?
157  | cons h _ ⇒ Some ? h ].
158
159 (* cutFirst *)
160 ndefinition cut_first_list ≝
161 λT:Type.λl:list T.match l with
162  [ nil ⇒ nil T
163  | cons _ t ⇒ t ].
164
165 (* cutLast *)
166 ndefinition cut_last_list ≝
167 λT:Type.λl:list T.match reverse_list T l with
168  [ nil ⇒ nil T
169  | cons _ t ⇒ reverse_list T t ].
170
171 (* apply f *)
172 nlet rec apply_f_list (T1,T2:Type) (l:list T1) (f:T1 → T2) on l ≝
173 match l with
174  [ nil ⇒ nil T2
175  | cons h t ⇒ cons T2 (f h) (apply_f_list T1 T2 t f) ].
176
177 (* fold right *)
178 nlet rec fold_right_list (T1,T2:Type) (f:T1 → T2 → T2) (acc:T2) (l:list T1) on l ≝
179   match l with
180    [ nil ⇒ acc
181    | cons h t ⇒ f h (fold_right_list T1 T2 f acc t)
182    ].
183
184 (* double fold right *)
185 nlemma fold_right_list2_aux1 :
186 ∀T.∀h,t.len_list T [] = len_list T (h::t) → False.
187  #T; #h; #t;
188  nnormalize;
189  #H;
190  ndestruct (*napply (nat_destruct_0_S ? H)*).
191 nqed.
192
193 nlemma fold_right_list2_aux2 :
194 ∀T.∀h,t.len_list T (h::t) = len_list T [] → False.
195  #T; #h; #t;
196  nnormalize;
197  #H;
198  ndestruct (*napply (nat_destruct_S_0 ? H)*).
199 nqed.
200
201 nlemma fold_right_list2_aux3 :
202 ∀T.∀h,h',t,t'.len_list T (h::t) = len_list T (h'::t') → len_list T t = len_list T t'.
203  #T; #h; #h'; #t; #t';
204  nelim t;
205  nelim t';
206  ##[ ##1: nnormalize; #H; napply refl_eq
207  ##| ##2: #a; #l'; #H; #H1;
208           nchange in H1:(%) with ((S O) = (S (S (len_list T l'))));
209           ndestruct (*nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))*)
210  ##| ##3: #a; #l'; #H; #H1;
211           nchange in H1:(%) with ((S (S (len_list T l'))) = (S O));
212           ndestruct (*nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H1))*)
213  ##| ##4: #a; #l; #H; #a1; #l1; #H1; #H2;
214           nchange in H2:(%) with ((S (S (len_list T l1))) = (S (S (len_list T l))));
215           nchange with ((S (len_list T l1)) = (S (len_list T l)));
216           nrewrite > (nat_destruct_S_S … H2);
217           napply refl_eq
218  ##]
219 nqed.
220
221 nlet rec fold_right_list2 (T1,T2:Type) (f:T1 → T1 → T2 → T2) (acc:T2) (l1:list T1) on l1 ≝
222  match l1
223   return λl1.Πl2.len_list T1 l1 = len_list T1 l2 → T2
224  with
225   [ nil ⇒ λl2.match l2 return λl2.len_list T1 [] = len_list T1 l2 → T2 with
226    [ nil ⇒ λp:len_list T1 [] = len_list T1 [].acc
227    | cons h t ⇒ λp:len_list T1 [] = len_list T1 (h::t).
228     False_rect_Type0 ? (fold_right_list2_aux1 T1 h t p)
229    ]
230   | cons h t ⇒ λl2.match l2 return λl2.len_list T1 (h::t) = len_list T1 l2 → T2 with
231    [ nil ⇒ λp:len_list T1 (h::t) = len_list T1 [].
232     False_rect_Type0 ? (fold_right_list2_aux2 T1 h t p)
233    | cons h' t' ⇒ λp:len_list T1 (h::t) = len_list T1 (h'::t').
234     f h h' (fold_right_list2 T1 T2 f acc t t' (fold_right_list2_aux3 T1 h h' t t' p))
235    ]
236   ].
237
238 nlet rec bfold_right_list2 (T1:Type) (f:T1 → T1 → bool) (l1,l2:list T1) on l1 ≝
239  match l1 with
240   [ nil ⇒ match l2 with
241    [ nil ⇒ true | cons h t ⇒ false ]
242   | cons h t ⇒ match l2 with
243    [ nil ⇒ false | cons h' t' ⇒ (f h h') ⊗ (bfold_right_list2 T1 f t t')
244    ]
245   ].
246
247 (* nth elem *)
248 nlet rec nth_list (T:Type) (l:list T) (n:nat) on l ≝
249  match l with
250   [ nil ⇒ None ?
251   | cons h t ⇒ match n with
252    [ O ⇒ Some ? h | S n' ⇒ nth_list T t n' ]
253   ].
254
255 (* abs elem *)
256 ndefinition abs_list_aux1 : ∀T:Type.∀n.((len_list T []) > n) = true → False.
257  #T; nnormalize; #n; #H; ndestruct (*napply (bool_destruct … H)*). nqed.
258
259 ndefinition abs_list_aux2 : ∀T:Type.∀h:T.∀t:list T.∀n.((len_list T (h::t)) > (S n) = true) → ((len_list T t) > n) = true.
260  #T; #h; #t; #n; nnormalize; #H; napply H. nqed.
261
262 nlet rec abs_list (T:Type) (l:list T) on l ≝
263  match l
264   return λl.Πn.(((len_list T l) > n) = true) → T
265  with
266   [ nil ⇒ λn.λp:(((len_list T []) > n) = true).False_rect_Type0 ? (abs_list_aux1 T n p)
267   | cons h t ⇒ λn.
268    match n with
269     [ O ⇒ λp:(((len_list T (h::t)) > O) = true).h
270     | S n' ⇒ λp:(((len_list T (h::t)) > (S n')) = true).
271      abs_list T t n' (abs_list_aux2 T h t n' p)
272     ]
273   ].
274
275 (* esempio: abs_list ? [ 1; 2; 3 ; 4 ] 0 (refl_eq …) = 1. *)
276
277 nlemma symmetric_lenlist : ∀T.∀l1,l2:list T.len_list T l1 = len_list T l2 → len_list T l2 = len_list T l1.
278  #T; #l1;
279  nelim l1;
280  ##[ ##1: #l2; ncases l2; nnormalize;
281           ##[ ##1: #H; napply refl_eq
282           ##| ##2: #h; #t; #H; ndestruct (*nelim (nat_destruct_0_S ? H)*)
283           ##]
284  ##| ##2: #h; #l2; ncases l2; nnormalize;
285           ##[ ##1: #H; #l; #H1; nrewrite < H1; napply refl_eq
286           ##| ##2: #h; #l; #H; #l3; #H1; nrewrite < H1; napply refl_eq
287           ##]
288  ##]
289 nqed.
290
291 nlemma symmetric_foldrightlist2_aux :
292 ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.
293  (∀x,y,z.f x y z = f y x z) →
294  (∀acc:T2.∀l1,l2:list T1.
295   ∀H1:(len_list T1 l1 = len_list T1 l2).
296   ∀H2:(len_list T1 l2 = len_list T1 l1).
297    (fold_right_list2 T1 T2 f acc l1 l2 H1 = fold_right_list2 T1 T2 f acc l2 l1 H2)).
298  #T1; #T2; #f; #H; #acc; #l1;
299  nelim l1;
300  ##[ ##1: #l2; ncases l2;
301           ##[ ##1: nnormalize; #H1; #H2; napply refl_eq
302           ##| ##2: #h; #l; #H1; #H2;
303                    nchange in H1:(%) with (O = (S (len_list ? l)));
304                    ndestruct (*nelim (nat_destruct_0_S ? H1)*)
305           ##]
306  ##| ##2: #h3; #l3; #H1; #l2; ncases l2;
307           ##[ ##1: #H2; #H3; nchange in H2:(%) with ((S (len_list ? l3)) = O);
308                    ndestruct (*nelim (nat_destruct_S_0 ? H1)*)
309           ##| ##2: #h4; #l4; #H2; #H3;
310                    nchange in H2:(%) with ((S (len_list ? l3)) = (S (len_list ? l4)));
311                    nchange in H3:(%) with ((S (len_list ? l4)) = (S (len_list ? l3)));
312                    nchange with ((f h3 h4 (fold_right_list2 T1 T2 f acc l3 l4 (fold_right_list2_aux3 T1 h3 h4 l3 l4 ?))) =
313                                  (f h4 h3 (fold_right_list2 T1 T2 f acc l4 l3 (fold_right_list2_aux3 T1 h4 h3 l4 l3 ?))));
314                    nrewrite < (H1 l4 (fold_right_list2_aux3 T1 h3 h4 l3 l4 H2) (fold_right_list2_aux3 T1 h4 h3 l4 l3 H3));
315                    nrewrite > (H h3 h4 (fold_right_list2 T1 T2 f acc l3 l4 ?));
316                    napply refl_eq
317           ##]
318  ##]
319 nqed.
320
321 nlemma symmetric_foldrightlist2 :
322 ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.
323  (∀x,y,z.f x y z = f y x z) →
324  (∀acc:T2.∀l1,l2:list T1.∀H:len_list T1 l1 = len_list T1 l2.
325    fold_right_list2 T1 T2 f acc l1 l2 H = fold_right_list2 T1 T2 f acc l2 l1 (symmetric_lenlist T1 l1 l2 H)).
326  #T1; #T2; #f; #H; #acc; #l1; #l2; #H1;
327  nrewrite > (symmetric_foldrightlist2_aux T1 T2 f H acc l1 l2 H1 (symmetric_lenlist T1 l1 l2 H1));
328  napply refl_eq.
329 nqed.
330
331 nlemma symmetric_bfoldrightlist2 :
332 ∀T1:Type.∀f:T1 → T1 → bool.
333  (∀x,y.f x y = f y x) →
334  (∀l1,l2:list T1.
335   bfold_right_list2 T1 f l1 l2 = bfold_right_list2 T1 f l2 l1).
336  #T; #f; #H; #l1;
337  nelim l1;
338  ##[ ##1: #l2; ncases l2;
339           ##[ ##1: nnormalize; napply refl_eq
340           ##| ##2: #hh2; #ll2; nnormalize; napply refl_eq
341           ##]
342  ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
343           ##[ ##1: nnormalize; napply refl_eq
344           ##| ##2: #hh2; #ll2; nnormalize;
345                    nrewrite > (H1 ll2);
346                    nrewrite > (H hh1 hh2);
347                    napply refl_eq
348           ##]
349  ##]
350 nqed.
351
352 nlemma bfoldrightlist2_to_eq :
353 ∀T1:Type.∀f:T1 → T1 → bool.
354  (∀x,y.(f x y = true → x = y)) →
355  (∀l1,l2:list T1.
356   (bfold_right_list2 T1 f l1 l2 = true → l1 = l2)).
357  #T; #f; #H; #l1;
358  nelim l1;
359  ##[ ##1: #l2; ncases l2;
360           ##[ ##1: #H1; napply refl_eq
361           ##| ##2: #hh2; #ll2; nnormalize; #H1;
362                    ndestruct (*napply (bool_destruct … H1)*)
363           ##]
364  ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
365           ##[ ##1: nnormalize; #H2;
366                    ndestruct (*napply (bool_destruct … H2)*)
367           ##| ##2: #hh2; #ll2; #H2;
368                    nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_list2 T f ll1 ll2)) = true);
369                    nrewrite > (H hh1 hh2 (andb_true_true_l … H2));
370                    nrewrite > (H1 ll2 (andb_true_true_r … H2));
371                    napply refl_eq
372           ##]
373  ##]
374 nqed.
375
376 nlemma eq_to_bfoldrightlist2 :
377 ∀T1:Type.∀f:T1 → T1 → bool.
378  (∀x,y.(x = y → f x y = true)) →
379  (∀l1,l2:list T1.
380   (l1 = l2 → bfold_right_list2 T1 f l1 l2 = true)).
381  #T; #f; #H; #l1;
382  nelim l1;
383  ##[ ##1: #l2; ncases l2;
384           ##[ ##1: #H1; nnormalize; napply refl_eq
385           ##| ##2: #hh2; #ll2; #H1;
386                    (* !!! ndestruct: assert false *)
387                    nelim (list_destruct_nil_cons ??? H1)
388           ##]
389  ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
390           ##[ ##1: #H2;
391                    (* !!! ndestruct: assert false *)
392                    nelim (list_destruct_cons_nil ??? H2)
393           ##| ##2: #hh2; #ll2; #H2; nnormalize;
394                    nrewrite > (list_destruct_1 … H2);
395                    nrewrite > (H hh2 hh2 (refl_eq …));
396                    nnormalize;
397                    nrewrite > (H1 ll2 (list_destruct_2 … H2));
398                    napply refl_eq
399           ##]
400  ##]
401 nqed.
402
403 nlemma bfoldrightlist2_to_lenlist :
404 ∀T.∀f:T → T → bool.
405  (∀l1,l2:list T.bfold_right_list2 T f l1 l2 = true → len_list T l1 = len_list T l2).
406  #T; #f; #l1;
407  nelim l1;
408  ##[ ##1: #l2; ncases l2;
409           ##[ ##1: nnormalize; #H; napply refl_eq
410           ##| ##2: nnormalize; #hh; #tt; #H;
411                    ndestruct (*napply (bool_destruct … H)*)
412           ##]
413  ##| ##2: #hh; #tt; #H; #l2; ncases l2;
414           ##[ ##1: nnormalize; #H1;
415                    ndestruct (*napply (bool_destruct … H1)*)
416           ##| ##2: #hh1; #tt1; #H1; nnormalize;
417                    nrewrite > (H tt1 ?);
418                    ##[ ##1: napply refl_eq
419                    ##| ##2: nchange in H1:(%) with ((? ⊗ (bfold_right_list2 T f tt tt1)) = true);
420                             napply (andb_true_true_r … H1)
421                    ##]
422           ##]
423  ##]
424 nqed.
425
426 nlemma decidable_list :
427 ∀T.(∀x,y:T.decidable (x = y)) →
428    (∀x,y:list T.decidable (x = y)).
429  #T; #H; #x; nelim x;
430  ##[ ##1: #y; ncases y;
431           ##[ ##1: nnormalize; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
432           ##| ##2: #hh2; #tt2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
433                    nnormalize; #H1;
434                    (* !!! ndestruct: assert false *)
435                    napply (list_destruct_nil_cons T … H1)
436           ##]
437  ##| ##2: #hh1; #tt1; #H1; #y; ncases y;
438           ##[ ##1: nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
439                    nnormalize; #H2;
440                    (* !!! ndestruct: assert false *)
441                    napply (list_destruct_cons_nil T … H2)
442           ##| ##2: #hh2; #tt2; nnormalize; napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H …));
443                    ##[ ##2: #H2; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
444                             nnormalize; #H3; napply (H2 (list_destruct_1 T … H3))
445                    ##| ##1: #H2; napply (or2_elim (tt1 = tt2) (tt1 ≠ tt2) ? (H1 tt2));
446                             ##[ ##2: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
447                                      nnormalize; #H4; napply (H3 (list_destruct_2 T … H4))
448                             ##| ##1: #H3; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
449                                      nrewrite > H2; nrewrite > H3; napply refl_eq
450                             ##]
451                    ##]
452           ##]
453  ##]
454 nqed.
455
456 nlemma nbfoldrightlist2_to_neq :
457 ∀T1:Type.∀f:T1 → T1 → bool.
458  (∀x,y.(f x y = false → x ≠ y)) →
459  (∀l1,l2:list T1.
460   (bfold_right_list2 T1 f l1 l2 = false → l1 ≠ l2)).
461  #T; #f; #H; #l1;
462  nelim l1;
463  ##[ ##1: #l2; ncases l2;
464           ##[ ##1: nnormalize; #H1;
465                    ndestruct (*napply (bool_destruct … H1)*)
466           ##| ##2: #hh2; #ll2; #H1; nnormalize; #H2;
467                    (* !!! ndestruct: assert false *)
468                    napply (list_destruct_nil_cons T … H2)
469           ##]
470  ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
471           ##[ ##1: #H2; nnormalize; #H3;
472                    (* !!! ndestruct: assert false *)
473                    napply (list_destruct_cons_nil T … H3)
474           ##| ##2: #hh2; #ll2; #H2; nnormalize; #H3;
475                    nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_list2 T f ll1 ll2)) = false);
476                    napply (H1 ll2 ? (list_destruct_2 T … H3));
477                    napply (or2_elim ??? (andb_false2 … H2) );
478                    ##[ ##1: #H4; napply (absurd (hh1 = hh2) …);
479                             ##[ ##1: nrewrite > (list_destruct_1 T … H3); napply refl_eq
480                             ##| ##2: napply (H … H4)
481                             ##]
482                    ##| ##2: #H4; napply H4
483                    ##]
484           ##]
485  ##]
486 nqed.
487
488 nlemma list_destruct :
489 ∀T.(∀x,y:T.decidable (x = y)) →
490    (∀h1,h2:T.∀l1,l2:list T.
491     (h1::l1) ≠ (h2::l2) → h1 ≠ h2 ∨ l1 ≠ l2).
492  #T; #H; #h1; #h2; #l1; nelim l1;
493  ##[ ##1: #l2; ncases l2;
494           ##[ ##1: #H1; napply (or2_intro1 (h1 ≠ h2) ([] ≠ []) …);
495                    nnormalize; #H2; nrewrite > H2 in H1:(%);
496                    nnormalize; #H1; napply (H1 (refl_eq …))
497           ##| ##2: #hh2; #ll2; #H1; napply (or2_intro2 (h1 ≠ h2) ([] ≠ (hh2::ll2)) …);
498                    nnormalize; #H2;
499                    (* !!! ndestruct: assert false *)
500                    napply (list_destruct_nil_cons T … H2)
501           ##]
502  ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
503           ##[ ##1: #H2; napply (or2_intro2 (h1 ≠ h2) ((hh1::ll1) ≠ []) …);
504                    nnormalize; #H3;
505                    (* !!! ndestruct: assert false *)
506                    napply (list_destruct_cons_nil T … H3)
507           ##| ##2: #hh2; #ll2; #H2;     
508                    napply (or2_elim (h1 = h2) (h1 ≠ h2) ? (H h1 h2) …);
509                    ##[ ##2: #H3; napply (or2_intro1 (h1 ≠ h2) ((hh1::ll1) ≠ (hh2::ll2)) H3)
510                    ##| ##1: #H3; napply (or2_intro2 (h1 ≠ h2) ((hh1::ll1) ≠ (hh2::ll2) …));
511                             nrewrite > H3 in H2:(%); #H2;
512                             nnormalize; #H4; nrewrite > (list_destruct_1 T … H4) in H2:(%); #H2;
513                             nrewrite > (list_destruct_2 T … H4) in H2:(%); #H2;
514                             napply (H2 (refl_eq …))
515                    ##]
516           ##]
517  ##]
518 nqed.
519
520 nlemma neq_to_nbfoldrightlist2 :
521 ∀T:Type.∀f:T → T → bool.
522  (∀x,y:T.decidable (x = y)) →
523  (∀x,y.(x ≠ y → f x y = false)) →
524  (∀l1,l2:list T.
525   (l1 ≠ l2 → bfold_right_list2 T f l1 l2 = false)).
526  #T; #f; #H; #H1; #l1;
527  nelim l1;
528  ##[ ##1: #l2; ncases l2;
529           ##[ ##1: nnormalize; #H2; nelim (H2 (refl_eq …))
530           ##| ##2: #hh2; #ll2; nnormalize; #H2; napply refl_eq
531           ##]
532  ##| ##2: #hh1; #ll1; #H2; #l2; ncases l2;
533           ##[ ##1: nnormalize; #H3; napply refl_eq
534           ##| ##2: #hh2; #ll2; #H3;
535                    nchange with (((f hh1 hh2)⊗(bfold_right_list2 T f ll1 ll2)) = false);
536                    napply (or2_elim (hh1 ≠ hh2) (ll1 ≠ ll2) ? (list_destruct T H … H3) …);
537                    ##[ ##1: #H4; nrewrite > (H1 hh1 hh2 H4); nnormalize; napply refl_eq
538                    ##| ##2: #H4; nrewrite > (H2 ll2 H4);
539                             nrewrite > (symmetric_andbool (f hh1 hh2) false);
540                             nnormalize; napply refl_eq
541                    ##]
542           ##]
543  ##]
544 nqed.
545
546 nlemma isbemptylist_to_isemptylist : ∀T,l.isb_empty_list T l = true → is_empty_list T l.
547  #T; #l;
548  ncases l;
549  nnormalize;
550  ##[ ##1: #H; napply I
551  ##| ##2: #x; #l; #H; ndestruct (*napply (bool_destruct … H)*)
552  ##]
553 nqed.
554
555 nlemma isnotbemptylist_to_isnotemptylist : ∀T,l.isnotb_empty_list T l = true → isnot_empty_list T l.
556  #T; #l;
557  ncases l;
558  nnormalize;
559  ##[ ##1: #H; ndestruct (*napply (bool_destruct … H)*)
560  ##| ##2: #x; #l; #H; napply I
561  ##]
562 nqed.
563
564 nlemma list_is_comparable : comparable → comparable.
565  #T; napply (mk_comparable (list T));
566  ##[ napply (nil ?)
567  ##| napply (λx.false)
568  ##| napply (bfold_right_list2 T (eqc T))
569  ##| napply (bfoldrightlist2_to_eq … (eqc T));
570      napply (eqc_to_eq T)
571  ##| napply (eq_to_bfoldrightlist2 … (eqc T));
572      napply (eq_to_eqc T)
573  ##| napply (nbfoldrightlist2_to_neq … (eqc T));
574      napply (neqc_to_neq T)
575  ##| napply (neq_to_nbfoldrightlist2 … (eqc T));
576      ##[ napply (decidable_c T)
577      ##| napply (neq_to_neqc T)
578      ##]
579  ##| napply decidable_list;
580      napply (decidable_c T)
581  ##| napply symmetric_bfoldrightlist2;
582      napply (symmetric_eqc T)
583  ##]
584 nqed.
585
586 unification hint 0 ≔ S: comparable;
587          T ≟ (carr S),
588          X ≟ (list_is_comparable S)
589  (*********************************************) ⊢
590          carr X ≡ list T.