helm/software/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.