matita/matita/contribs/ng_assembly2/common/nelist.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/list.ma".
  24
  25 (* ************** *)
  26 (* NON-EMPTY LIST *)
  27 (* ************** *)
  28
  29 (* lista non vuota *)
  30 ninductive ne_list (A:Type) : Type ≝
  31   | ne_nil: A → ne_list A
  32   | ne_cons: A → ne_list A → ne_list A.
  33
  34 (* append *)
  35 nlet rec ne_append (A:Type) (l1,l2:ne_list A) on l1 ≝
  36  match l1 with
  37   [ ne_nil hd ⇒ ne_cons A hd l2
  38   | ne_cons hd tl ⇒ ne_cons A hd (ne_append A tl l2) ].
  39
  40 notation "hvbox(hd break §§ tl)"
  41   right associative with precedence 46
  42   for @{'ne_cons $hd $tl}.
  43
  44 (* \laquo \raquo *)
  45 notation "« list0 x sep ; break £ y break »"
  46   non associative with precedence 90
  47   for ${fold right @{'ne_nil $y } rec acc @{'ne_cons $x $acc}}.
  48
  49 notation "hvbox(l1 break & l2)"
  50   right associative with precedence 47
  51   for @{'ne_append $l1 $l2 }.
  52
  53 interpretation "ne_nil" 'ne_nil hd = (ne_nil ? hd).
  54 interpretation "ne_cons" 'ne_cons hd tl = (ne_cons ? hd tl).
  55 interpretation "ne_append" 'ne_append l1 l2 = (ne_append ? l1 l2).
  56
  57 nlemma nelist_destruct_nil_nil : ∀T.∀x1,x2:T.ne_nil T x1 = ne_nil T x2 → x1 = x2.
  58  #T; #x1; #x2; #H;
  59  nchange with (match ne_nil T x2 with [ ne_cons _ _ ⇒ False | ne_nil a ⇒ x1 = a ]);
  60  nrewrite < H;
  61  nnormalize;
  62  napply refl_eq.
  63 nqed.
  64
  65 nlemma nelist_destruct_cons_cons_1 : ∀T.∀x1,x2:T.∀y1,y2:ne_list T.ne_cons T x1 y1 = ne_cons T x2 y2 → x1 = x2.
  66  #T; #x1; #x2; #y1; #y2; #H;
  67  nchange with (match ne_cons T x2 y2 with [ ne_nil _ ⇒ False | ne_cons a _ ⇒ x1 = a ]);
  68  nrewrite < H;
  69  nnormalize;
  70  napply refl_eq.
  71 nqed.
  72
  73 nlemma nelist_destruct_cons_cons_2 : ∀T.∀x1,x2:T.∀y1,y2:ne_list T.ne_cons T x1 y1 = ne_cons T x2 y2 → y1 = y2.
  74  #T; #x1; #x2; #y1; #y2; #H;
  75  nchange with (match ne_cons T x2 y2 with [ ne_nil _ ⇒ False | ne_cons _ b ⇒ y1 = b ]);
  76  nrewrite < H;
  77  nnormalize;
  78  napply refl_eq.
  79 nqed.
  80
  81 nlemma nelist_destruct_cons_nil : ∀T.∀x1,x2:T.∀y1:ne_list T.ne_cons T x1 y1 = ne_nil T x2 → False.
  82  #T; #x1; #x2; #y1; #H;
  83  nchange with (match ne_cons T x1 y1 with [ ne_nil _ ⇒ True | ne_cons a b ⇒ False ]);
  84  nrewrite > H;
  85  nnormalize;
  86  napply I.
  87 nqed.
  88
  89 nlemma nelist_destruct_nil_cons : ∀T.∀x1,x2:T.∀y2:ne_list T.ne_nil T x1 = ne_cons T x2 y2 → False.
  90  #T; #x1; #x2; #y2; #H;
  91  nchange with (match ne_cons T x2 y2 with [ ne_nil _ ⇒ True | ne_cons a b ⇒ False ]);
  92  nrewrite < H;
  93  nnormalize;
  94  napply I.
  95 nqed.
  96
  97 nlemma associative_nelist : ∀T.associative (ne_list T) (ne_append T).
  98  #T; #x; #y; #z;
  99  nelim x;
 100  nnormalize;
 101  ##[ ##1: #hh; napply refl_eq
 102  ##| ##2: #hh; #tt; #H;
 103           nrewrite > H;
 104           napply refl_eq
 105  ##]
 106 nqed.
 107
 108 nlemma necons_append_commute : ∀T:Type.∀l1,l2:ne_list T.∀a:T.(a §§ (l1 & l2)) = ((a §§ l1) & l2).
 109  #T; #l1; #l2; #a;
 110  nnormalize;
 111  napply refl_eq.
 112 nqed.
 113
 114 nlemma append_necons_commute : ∀T:Type.∀a:T.∀l,l1:ne_list T.(l & (a §§ l1)) = (l & «£a») & l1.
 115  #T; #a; #l; #l1;
 116  nrewrite > (associative_nelist T l «£a» l1);
 117  nnormalize;
 118  napply refl_eq.
 119 nqed.
 120
 121 (* listlen *)
 122 nlet rec len_neList (T:Type) (nl:ne_list T) on nl ≝
 123  match nl with [ ne_nil _ ⇒ (S O) | ne_cons _ t ⇒ S (len_neList T t) ].
 124
 125 (* reverse *)
 126 nlet rec reverse_neList (T:Type) (nl:ne_list T) on nl ≝
 127  match nl with
 128   [ ne_nil h ⇒ ne_nil T h
 129   | ne_cons h t ⇒ (reverse_neList T t)&(ne_nil T h)
 130   ].
 131
 132 (* getFirst *)
 133 ndefinition get_first_neList ≝
 134 λT:Type.λnl:ne_list T.match nl with
 135  [ ne_nil h ⇒ h
 136  | ne_cons h _ ⇒ h ].
 137
 138 (* getLast *)
 139 ndefinition get_last_neList ≝
 140 λT:Type.λnl:ne_list T.match reverse_neList T nl with
 141  [ ne_nil h ⇒ h
 142  | ne_cons h _ ⇒ h ].
 143
 144 (* cutFirst *)
 145 ndefinition cut_first_neList ≝
 146 λT:Type.λnl:ne_list T.match nl with
 147  [ ne_nil h ⇒ ne_nil T h
 148  | ne_cons _ t ⇒ t ].
 149
 150 (* cutLast *)
 151 ndefinition cut_last_neList ≝
 152 λT:Type.λnl:ne_list T.match reverse_neList T nl with
 153  [ ne_nil h ⇒ ne_nil T h
 154  | ne_cons _ t ⇒ reverse_neList T t ].
 155
 156 (* apply f *)
 157 nlet rec apply_f_neList (T1,T2:Type) (nl:ne_list T1) (f:T1 → T2) on nl ≝
 158 match nl with
 159  [ ne_nil h ⇒ ne_nil T2 (f h)
 160  | ne_cons h t ⇒ ne_cons T2 (f h) (apply_f_neList T1 T2 t f) ].
 161
 162 (* fold right *)
 163 nlet rec fold_right_neList (T1,T2:Type) (f:T1 → T2 → T2) (acc:T2) (nl:ne_list T1) on nl ≝
 164   match nl with
 165    [ ne_nil h ⇒ f h acc
 166    | ne_cons h t ⇒ f h (fold_right_neList T1 T2 f acc t)
 167    ].
 168
 169 (* double fold right *)
 170 nlemma fold_right_neList2_aux1 :
 171 ∀T.∀h,h',t'.len_neList T «£h» = len_neList T (h'§§t') → False.
 172  #T; #h; #h'; #t';
 173  nnormalize;
 174  ncases t';
 175  nnormalize;
 176  ##[ ##1: #x; #H; ndestruct (*nelim (nat_destruct_0_S ? (nat_destruct_S_S … H))*)
 177  ##| ##2: #x; #l; #H; ndestruct (*nelim (nat_destruct_0_S ? (nat_destruct_S_S … H))*)
 178  ##]
 179 nqed.
 180
 181 nlemma fold_right_neList2_aux2 :
 182 ∀T.∀h,h',t.len_neList T (h§§t) = len_neList T «£h'» → False.
 183  #T; #h; #h'; #t;
 184  nnormalize;
 185  ncases t;
 186  nnormalize;
 187  ##[ ##1: #x; #H; ndestruct (*nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H))*)
 188  ##| ##2: #x; #l; #H; ndestruct (*nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H))*)
 189  ##]
 190 nqed.
 191
 192 nlemma fold_right_neList2_aux3 :
 193 ∀T.∀h,h',t,t'.len_neList T (h§§t) = len_neList T (h'§§t') → len_neList T t = len_neList T t'.
 194  #T; #h; #h'; #t; #t';
 195  nelim t;
 196  nelim t';
 197  ##[ ##1: nnormalize; #x; #y; #H; napply refl_eq
 198  ##| ##2: #a; #l'; #H; #x; #H1;
 199           nchange in H1:(%) with ((S (len_neList T «£x»)) = (S (len_neList T (a§§l'))));
 200           nrewrite > (nat_destruct_S_S … H1);
 201           napply refl_eq
 202  ##| ##3: #x; #a; #l'; #H; #H1;
 203           nchange in H1:(%) with ((S (len_neList T (a§§l')))= (S (len_neList T «£x»)));
 204           nrewrite > (nat_destruct_S_S … H1);
 205           napply refl_eq
 206  ##| ##4: #a; #l; #H; #a1; #l1; #H1; #H2;
 207           nchange in H2:(%) with ((S (len_neList T (a1§§l1))) = (S (len_neList T (a§§l))));
 208           nrewrite > (nat_destruct_S_S … H2);
 209           napply refl_eq
 210  ##]
 211 nqed.
 212
 213 nlet rec fold_right_neList2 (T1,T2:Type) (f:T1 → T1 → T2 → T2) (acc:T2) (l1:ne_list T1) on l1 ≝
 214  match l1
 215   return λl1.Πl2.len_neList T1 l1 = len_neList T1 l2 → T2
 216  with
 217   [ ne_nil h ⇒ λl2.match l2 return λl2.len_neList T1 «£h» = len_neList T1 l2 → T2 with
 218    [ ne_nil h' ⇒ λp:len_neList T1 «£h» = len_neList T1 «£h'».
 219     f h h' acc
 220    | ne_cons h' t' ⇒ λp:len_neList T1 «£h» = len_neList T1 (h'§§t').
 221     False_rect_Type0 ? (fold_right_neList2_aux1 T1 h h' t' p)
 222    ]
 223   | ne_cons h t ⇒ λl2.match l2 return λl2.len_neList T1 (h§§t) = len_neList T1 l2 → T2 with
 224    [ ne_nil h' ⇒ λp:len_neList T1 (h§§t) = len_neList T1 «£h'».
 225     False_rect_Type0 ? (fold_right_neList2_aux2 T1 h h' t p)
 226    | ne_cons h' t' ⇒ λp:len_neList T1 (h§§t) = len_neList T1 (h'§§t').
 227     f h h' (fold_right_neList2 T1 T2 f acc t t' (fold_right_neList2_aux3 T1 h h' t t' p))
 228    ]
 229   ].
 230
 231 nlet rec bfold_right_neList2 (T1:Type) (f:T1 → T1 → bool) (l1,l2:ne_list T1) on l1 ≝
 232  match l1 with
 233   [ ne_nil h ⇒ match l2 with
 234    [ ne_nil h' ⇒ f h h' | ne_cons h' t' ⇒ false ]
 235   | ne_cons h t ⇒ match l2 with
 236    [ ne_nil h' ⇒ false | ne_cons h' t' ⇒ (f h h') ⊗ (bfold_right_neList2 T1 f t t')
 237    ]
 238   ].
 239
 240 (* nth elem *)
 241 nlet rec nth_neList (T:Type) (nl:ne_list T) (n:nat) on nl ≝
 242  match nl with
 243   [ ne_nil h ⇒ match n with
 244    [ O ⇒ Some ? h | S _ ⇒ None ? ]
 245   | ne_cons h t ⇒ match n with
 246    [ O ⇒ Some ? h | S n' ⇒ nth_neList T t n' ]
 247   ].
 248
 249 (* abs elem *)
 250 ndefinition abs_neList_aux1 : ∀T:Type.∀h:T.∀n.((len_neList T («£h»)) > (S n)) = true → False.
 251  #T; #h; #n; nnormalize; #H; ndestruct (*napply (bool_destruct … H)*). nqed.
 252
 253 ndefinition abs_neList_aux2 : ∀T:Type.∀h:T.∀t:ne_list T.∀n.((len_neList T (h§§t)) > (S n) = true) → ((len_neList T t) > n) = true.
 254  #T; #h; #t; #n; nnormalize; #H; napply H. nqed.
 255
 256 nlet rec abs_neList (T:Type) (l:ne_list T) on l ≝
 257  match l
 258   return λl.Πn.(((len_neList T l) > n) = true) → T
 259  with
 260   [ ne_nil h ⇒ λn.
 261    match n
 262     return λn.(((len_neList T (ne_nil T h)) > n) = true) → T
 263    with
 264     [ O ⇒ λp:(((len_neList T (ne_nil T h)) > O) = true).h
 265     | S n' ⇒ λp:(((len_neList T (ne_nil T h)) > (S n')) = true).
 266      False_rect_Type0 ? (abs_neList_aux1 T h n' p)
 267     ]
 268   | ne_cons h t ⇒ λn.
 269    match n with
 270     [ O ⇒ λp:(((len_neList T (ne_cons T h t)) > O) = true).h
 271     | S n' ⇒ λp:(((len_neList T (ne_cons T h t)) > (S n')) = true).
 272      abs_neList T t n' (abs_neList_aux2 T h t n' p)
 273     ]
 274   ].
 275
 276 (* esempio: abs_neList ? « 1; 2; 3 £ 4 » 0 (refl_eq …) = 1. *)
 277
 278 (* conversione *)
 279 nlet rec neList_to_list (T:Type) (nl:ne_list T) on nl : list T ≝
 280  match nl with [ ne_nil h ⇒ [h] | ne_cons h t ⇒ [h]@(neList_to_list T t) ].
 281
 282 nlemma symmetric_lennelist : ∀T.∀l1,l2:ne_list T.len_neList T l1 = len_neList T l2 → len_neList T l2 = len_neList T l1.
 283  #T; #l1;
 284  nelim l1;
 285  ##[ ##1: #h; #l2; ncases l2; nnormalize;
 286           ##[ ##1: #H; #H1; napply refl_eq
 287           ##| ##2: #h; #t; #H; nrewrite > H; napply refl_eq
 288           ##]
 289  ##| ##2: #h; #l2; ncases l2; nnormalize;
 290           ##[ ##1: #h1; #H; #l; #H1; nrewrite < H1; napply refl_eq
 291           ##| ##2: #h; #l; #H; #l3; #H1; nrewrite < H1; napply refl_eq
 292           ##]
 293  ##]
 294 nqed.
 295
 296 nlemma symmetric_foldrightnelist2_aux :
 297 ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.
 298  (∀x,y,z.f x y z = f y x z) →
 299  (∀acc:T2.∀l1,l2:ne_list T1.
 300   ∀H1:len_neList T1 l1 = len_neList T1 l2.∀H2:len_neList T1 l2 = len_neList T1 l1.
 301    fold_right_neList2 T1 T2 f acc l1 l2 H1 = fold_right_neList2 T1 T2 f acc l2 l1 H2).
 302  #T1; #T2; #f; #H; #acc; #l1;
 303  nelim l1;
 304  ##[ ##1: #h; #l2; ncases l2;
 305           ##[ ##1: #h1; nnormalize; #H1; #H2; nrewrite > (H h h1 acc); napply refl_eq
 306           ##| ##2: #h1; #l; ncases l;
 307                    ##[ ##1: #h3; #H1; #H2;
 308                             nchange in H1:(%) with ((S O) = (S (S O)));
 309                             (* !!! ndestruct: si inceppa su un'ipotesi che non e' H1 *)
 310                             nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))
 311                    ##| ##2: #h3; #l3; #H1; #H2;
 312                             nchange in H1:(%) with ((S O) = (S (S (len_neList ? l3))));
 313                             (* !!! ndestruct: si inceppa su un'ipotesi che non e' H1 *)
 314                             nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))
 315                    ##]
 316           ##]
 317  ##| ##2: #h3; #l3; #H1; #l2; ncases l2;
 318           ##[ ##1: #h4; ncases l3;
 319                    ##[ ##1: #h5; #H2; #H3;
 320                             nchange in H2:(%) with ((S (S O)) = (S O));
 321                             (* !!! ndestruct: si inceppa su un'ipotesi che non e' H1 *)
 322                             nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H2))
 323                    ##| ##2: #h5; #l5; #H2; #H3;
 324                             nchange in H2:(%) with ((S (S (len_neList ? l5))) = (S O));
 325                             (* !!! ndestruct: si inceppa su un'ipotesi che non e' H1 *)
 326                             nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H2))
 327                    ##]
 328           ##| ##2: #h4; #l4; #H2; #H3;
 329                    nchange in H2:(%) with ((S (len_neList ? l3)) = (S (len_neList ? l4)));
 330                    nchange in H3:(%) with ((S (len_neList ? l4)) = (S (len_neList ? l3)));
 331                    nchange with ((f h3 h4 (fold_right_neList2 T1 T2 f acc l3 l4 (fold_right_neList2_aux3 T1 h3 h4 l3 l4 ?))) =
 332                                  (f h4 h3 (fold_right_neList2 T1 T2 f acc l4 l3 (fold_right_neList2_aux3 T1 h4 h3 l4 l3 ?))));
 333                    nrewrite < (H1 l4 (fold_right_neList2_aux3 T1 h3 h4 l3 l4 H2) (fold_right_neList2_aux3 T1 h4 h3 l4 l3 H3));
 334                    nrewrite > (H h3 h4 (fold_right_neList2 T1 T2 f acc l3 l4 ?));
 335                    napply refl_eq
 336           ##]
 337  ##]
 338 nqed.
 339
 340 nlemma symmetric_foldrightnelist2 :
 341 ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.
 342  (∀x,y,z.f x y z = f y x z) →
 343  (∀acc:T2.∀l1,l2:ne_list T1.∀H:len_neList T1 l1 = len_neList T1 l2.
 344   fold_right_neList2 T1 T2 f acc l1 l2 H = fold_right_neList2 T1 T2 f acc l2 l1 (symmetric_lennelist T1 l1 l2 H)).
 345  #T1; #T2; #f; #H; #acc; #l1; #l2; #H1;
 346  nrewrite > (symmetric_foldrightnelist2_aux T1 T2 f H acc l1 l2 H1 (symmetric_lennelist T1 l1 l2 H1));
 347  napply refl_eq.
 348 nqed.
 349
 350 nlemma symmetric_bfoldrightnelist2 :
 351 ∀T1:Type.∀f:T1 → T1 → bool.
 352  (∀x,y.f x y = f y x) →
 353  (∀l1,l2:ne_list T1.
 354   bfold_right_neList2 T1 f l1 l2 = bfold_right_neList2 T1 f l2 l1).
 355  #T; #f; #H; #l1;
 356  nelim l1;
 357  ##[ ##1: #hh1; #l2; ncases l2;
 358           ##[ ##1: #hh2; nnormalize; nrewrite > (H hh1 hh2); napply refl_eq
 359           ##| ##2: #hh2; #ll2; nnormalize; napply refl_eq
 360           ##]
 361  ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
 362           ##[ ##1: #hh2; nnormalize; napply refl_eq
 363           ##| ##2: #hh2; #ll2; nnormalize;
 364                    nrewrite > (H1 ll2);
 365                    nrewrite > (H hh1 hh2);
 366                    napply refl_eq
 367           ##]
 368  ##]
 369 nqed.
 370
 371 nlemma bfoldrightnelist2_to_eq :
 372 ∀T1:Type.∀f:T1 → T1 → bool.
 373  (∀x,y.(f x y = true → x = y)) →
 374  (∀l1,l2:ne_list T1.
 375   (bfold_right_neList2 T1 f l1 l2 = true → l1 = l2)).
 376  #T; #f; #H; #l1;
 377  nelim l1;
 378  ##[ ##1: #hh1; #l2; ncases l2;
 379           ##[ ##1: #hh2; #H1; nnormalize in H1:(%); nrewrite > (H hh1 hh2 H1); napply refl_eq
 380           ##| ##2: #hh2; #ll2; nnormalize; #H1; ndestruct (*napply (bool_destruct … H1)*)
 381           ##]
 382  ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
 383           ##[ ##1: #hh2; nnormalize; #H2; ndestruct (*napply (bool_destruct … H2)*)
 384           ##| ##2: #hh2; #ll2; #H2;
 385                    nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = true);
 386                    nrewrite > (H hh1 hh2 (andb_true_true_l … H2));
 387                    nrewrite > (H1 ll2 (andb_true_true_r … H2));
 388                    napply refl_eq
 389           ##]
 390  ##]
 391 nqed.
 392
 393 nlemma eq_to_bfoldrightnelist2 :
 394 ∀T1:Type.∀f:T1 → T1 → bool.
 395  (∀x,y.(x = y → f x y = true)) →
 396  (∀l1,l2:ne_list T1.
 397   (l1 = l2 → bfold_right_neList2 T1 f l1 l2 = true)).
 398  #T; #f; #H; #l1;
 399  nelim l1;
 400  ##[ ##1: #hh1; #l2; ncases l2;
 401           ##[ ##1: #hh2; #H1; nnormalize;
 402                    nrewrite > (H hh1 hh2 (nelist_destruct_nil_nil … H1));
 403                    napply refl_eq
 404           ##| ##2: #hh2; #ll2; #H1;
 405                    (* !!! ndestruct: assert false *)
 406                    nelim (nelist_destruct_nil_cons ???? H1)
 407           ##]
 408  ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
 409           ##[ ##1: #hh2; #H2;
 410                    (* !!! ndestruct: assert false *)
 411                    nelim (nelist_destruct_cons_nil ???? H2)
 412           ##| ##2: #hh2; #ll2; #H2; nnormalize;
 413                    nrewrite > (nelist_destruct_cons_cons_1 … H2);
 414                    nrewrite > (H hh2 hh2 (refl_eq …));
 415                    nnormalize;
 416                    nrewrite > (H1 ll2 (nelist_destruct_cons_cons_2 … H2));
 417                    napply refl_eq
 418           ##]
 419  ##]
 420 nqed.
 421
 422 nlemma bfoldrightnelist2_to_lennelist :
 423 ∀T.∀f:T → T → bool.
 424  (∀l1,l2:ne_list T.bfold_right_neList2 T f l1 l2 = true → len_neList T l1 = len_neList T l2).
 425  #T; #f; #l1;
 426  nelim l1;
 427  ##[ ##1: #hh1; #l2; ncases l2;
 428           ##[ ##1: nnormalize; #hh2; #H; napply refl_eq
 429           ##| ##2: nnormalize; #hh2; #tt2; #H; ndestruct (*napply (bool_destruct … H)*)
 430           ##]
 431  ##| ##2: #hh1; #tt1; #H; #l2; ncases l2;
 432           ##[ ##1: nnormalize; #hh2; #H1; ndestruct (*napply (bool_destruct … H1)*)
 433           ##| ##2: #hh2; #tt2; #H1; nnormalize;
 434                    nrewrite > (H tt2 ?);
 435                    ##[ ##1: napply refl_eq
 436                    ##| ##2: nchange in H1:(%) with ((? ⊗ (bfold_right_neList2 T f tt1 tt2)) = true);
 437                             napply (andb_true_true_r … H1)
 438                    ##]
 439           ##]
 440  ##]
 441 nqed.
 442
 443 nlemma decidable_nelist :
 444 ∀T.(∀x,y:T.decidable (x = y)) →
 445    (∀x,y:ne_list T.decidable (x = y)).
 446  #T; #H; #x; nelim x;
 447  ##[ ##1: #hh1; #y; ncases y;
 448           ##[ ##1: #hh2; nnormalize; napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H hh1 hh2));
 449                    ##[ ##1: #H1; nrewrite > H1; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
 450                    ##| ##2: #H1; napply (or2_intro2 (? = ?) (? ≠ ?) ?); nnormalize;
 451                             #H2; napply (H1 (nelist_destruct_nil_nil T … H2))
 452                    ##]
 453           ##| ##2: #hh2; #tt2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 454                    nnormalize; #H1;
 455                    (* !!! ndestruct: assert false *)
 456                    napply (nelist_destruct_nil_cons T … H1)
 457           ##]
 458  ##| ##2: #hh1; #tt1; #H1; #y; ncases y;
 459           ##[ ##1: #hh1; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 460                    nnormalize; #H2;
 461                    (* !!! ndestruct: assert false *)
 462                    napply (nelist_destruct_cons_nil T … H2)
 463           ##| ##2: #hh2; #tt2; nnormalize; napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H …));
 464                    ##[ ##2: #H2; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 465                             nnormalize; #H3; napply (H2 (nelist_destruct_cons_cons_1 T … H3))
 466                    ##| ##1: #H2; napply (or2_elim (tt1 = tt2) (tt1 ≠ tt2) ? (H1 tt2));
 467                             ##[ ##2: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 468                                      nnormalize; #H4; napply (H3 (nelist_destruct_cons_cons_2 T … H4))
 469                             ##| ##1: #H3; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
 470                                      nrewrite > H2; nrewrite > H3; napply refl_eq
 471                             ##]
 472                    ##]
 473           ##]
 474  ##]
 475 nqed.
 476
 477 nlemma nbfoldrightnelist2_to_neq :
 478 ∀T1:Type.∀f:T1 → T1 → bool.
 479  (∀x,y.(f x y = false → x ≠ y)) →
 480  (∀l1,l2:ne_list T1.
 481   (bfold_right_neList2 T1 f l1 l2 = false → l1 ≠ l2)).
 482  #T; #f; #H; #l1;
 483  nelim l1;
 484  ##[ ##1: #hh1; #l2; ncases l2;
 485           ##[ ##1: #hh2; nnormalize; #H1; #H2; napply (H hh1 hh2 H1 (nelist_destruct_nil_nil T … H2))
 486           ##| ##2: #hh2; #ll2; #H1; nnormalize; #H2;
 487                    (* !!! ndestruct: assert false *)
 488                    napply (nelist_destruct_nil_cons T … H2)
 489           ##]
 490  ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
 491           ##[ ##1: #hh2; #H2; nnormalize; #H3;
 492                    (* !!! ndestruct: assert false *)
 493                    napply (nelist_destruct_cons_nil T … H3)
 494           ##| ##2: #hh2; #ll2; #H2; nnormalize; #H3;
 495                    nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = false);
 496                    napply (H1 ll2 ? (nelist_destruct_cons_cons_2 T … H3));
 497                    napply (or2_elim ??? (andb_false2 … H2) );
 498                    ##[ ##1: #H4; napply (absurd (hh1 = hh2) …);
 499                             ##[ ##1: nrewrite > (nelist_destruct_cons_cons_1 T … H3); napply refl_eq
 500                             ##| ##2: napply (H … H4)
 501                             ##]
 502                    ##| ##2: #H4; napply H4
 503                    ##]
 504           ##]
 505  ##]
 506 nqed.
 507
 508 nlemma nelist_destruct :
 509 ∀T.(∀x,y:T.decidable (x = y)) →
 510    (∀h1,h2:T.∀l1,l2:ne_list T.
 511     (h1§§l1) ≠ (h2§§l2) → h1 ≠ h2 ∨ l1 ≠ l2).
 512  #T; #H; #h1; #h2; #l1; nelim l1;
 513  ##[ ##1: #hh1; #l2; ncases l2;
 514           ##[ ##1: #hh2; #H1; napply (or2_elim (h1 = h2) (h1 ≠ h2) ? (H …) …);
 515                    ##[ ##2: #H2; napply (or2_intro1 (h1 ≠ h2) («£hh1» ≠ «£hh2») H2)
 516                    ##| ##1: #H2; nrewrite > H2 in H1:(%); #H1;
 517                             napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H …) …);
 518                             ##[ ##2: #H3; napply (or2_intro2 (h2 ≠ h2) («£hh1» ≠ «£hh2») ?);
 519                                      nnormalize; #H4; napply (H3 (nelist_destruct_nil_nil T … H4))
 520                             ##| ##1: #H3; nrewrite > H3 in H1:(%); #H1; nelim (H1 (refl_eq …))
 521                             ##]
 522                    ##]
 523           ##| ##2: #hh2; #ll2; #H1; napply (or2_intro2 (h1 ≠ h2) («£hh1» ≠ (hh2§§ll2)) …);
 524                    nnormalize; #H2;
 525                    (* !!! ndestruct: assert false *)
 526                    napply (nelist_destruct_nil_cons T … H2)
 527           ##]
 528  ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
 529           ##[ ##1: #hh2; #H2; napply (or2_intro2 (h1 ≠ h2) ((hh1§§ll1) ≠ «£hh2») …);
 530                    nnormalize; #H3;
 531                    (* !!! ndestruct: assert false *)
 532                    napply (nelist_destruct_cons_nil T … H3)
 533           ##| ##2: #hh2; #ll2; #H2;
 534                    napply (or2_elim (h1 = h2) (h1 ≠ h2) ? (H h1 h2) …);
 535                    ##[ ##2: #H3; napply (or2_intro1 (h1 ≠ h2) ((hh1§§ll1) ≠ (hh2§§ll2)) H3)
 536                    ##| ##1: #H3; napply (or2_intro2 (h1 ≠ h2) ((hh1§§ll1) ≠ (hh2§§ll2) …));
 537                             nrewrite > H3 in H2:(%); #H2;
 538                             nnormalize; #H4; nrewrite > (nelist_destruct_cons_cons_1 T … H4) in H2:(%); #H2;
 539                             nrewrite > (nelist_destruct_cons_cons_2 T … H4) in H2:(%); #H2;
 540                             napply (H2 (refl_eq …))
 541                    ##]
 542           ##]
 543  ##]
 544 nqed.
 545
 546 nlemma neq_to_nbfoldrightnelist2 :
 547 ∀T:Type.∀f:T → T → bool.
 548  (∀x,y:T.decidable (x = y)) →
 549  (∀x,y.(x ≠ y → f x y = false)) →
 550  (∀l1,l2:ne_list T.
 551   (l1 ≠ l2 → bfold_right_neList2 T f l1 l2 = false)).
 552  #T; #f; #H; #H1; #l1;
 553  nelim l1;
 554  ##[ ##1: #hh1; #l2; ncases l2;
 555           ##[ ##1: #hh2; nnormalize; #H2; napply (H1 hh1 hh2 ?);
 556                    nnormalize; #H3; nrewrite > H3 in H2:(%); #H2; napply (H2 (refl_eq …))
 557           ##| ##2: #hh2; #ll2; nnormalize; #H2; napply refl_eq
 558           ##]
 559  ##| ##2: #hh1; #ll1; #H2; #l2; ncases l2;
 560           ##[ ##1: #hh2; nnormalize; #H3; napply refl_eq
 561           ##| ##2: #hh2; #ll2; #H3;
 562                    nchange with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = false);
 563                    napply (or2_elim (hh1 ≠ hh2) (ll1 ≠ ll2) ? (nelist_destruct T H … H3) …);
 564                    ##[ ##1: #H4; nrewrite > (H1 hh1 hh2 H4); nnormalize; napply refl_eq
 565                    ##| ##2: #H4; nrewrite > (H2 ll2 H4);
 566                             nrewrite > (symmetric_andbool (f hh1 hh2) false);
 567                             nnormalize; napply refl_eq
 568                    ##]
 569           ##]
 570  ##]
 571 nqed.
 572
 573 nlemma nelist_is_comparable : comparable → comparable.
 574  #T; napply (mk_comparable (ne_list T));
 575  ##[ napply (ne_nil ? (zeroc T))
 576  ##| napply (λx.false)
 577  ##| napply (bfold_right_neList2 T (eqc T))
 578  ##| napply (bfoldrightnelist2_to_eq … (eqc T));
 579      napply (eqc_to_eq T)
 580  ##| napply (eq_to_bfoldrightnelist2 … (eqc T));
 581      napply (eq_to_eqc T)
 582  ##| napply (nbfoldrightnelist2_to_neq … (eqc T));
 583      napply (neqc_to_neq T)
 584  ##| napply (neq_to_nbfoldrightnelist2 … (eqc T));
 585      ##[ napply (decidable_c T)
 586      ##| napply (neq_to_neqc T)
 587      ##]
 588  ##| napply decidable_nelist;
 589      napply (decidable_c T)
 590  ##| napply symmetric_bfoldrightnelist2;
 591      napply (symmetric_eqc T)
 592  ##]
 593 nqed.
 594
 595 unification hint 0 ≔ S: comparable;
 596          T ≟ (carr S),
 597          X ≟ (nelist_is_comparable S)
 598  (*********************************************) ⊢
 599          carr X ≡ ne_list T.