helm/software/matita/contribs/ng_assembly/common/list_utility_lemmas.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  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_utility.ma".
  24 include "common/list_lemmas.ma".
  25
  26 (* *************** *)
  27 (* LISTE GENERICHE *)
  28 (* *************** *)
  29
  30 nlemma symmetric_lenlist : ∀T.∀l1,l2:list T.len_list T l1 = len_list T l2 → len_list T l2 = len_list T l1.
  31  #T; #l1;
  32  nelim l1;
  33  ##[ ##1: #l2; ncases l2; nnormalize;
  34           ##[ ##1: #H; napply refl_eq
  35           ##| ##2: #h; #t; #H; ndestruct (*nelim (nat_destruct_0_S ? H)*)
  36           ##]
  37  ##| ##2: #h; #l2; ncases l2; nnormalize;
  38           ##[ ##1: #H; #l; #H1; nrewrite < H1; napply refl_eq
  39           ##| ##2: #h; #l; #H; #l3; #H1; nrewrite < H1; napply refl_eq
  40           ##]
  41  ##]
  42 nqed.
  43
  44 nlemma symmetric_foldrightlist2_aux :
  45 ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.
  46  (∀x,y,z.f x y z = f y x z) →
  47  (∀acc:T2.∀l1,l2:list T1.
  48   ∀H1:(len_list T1 l1 = len_list T1 l2).
  49   ∀H2:(len_list T1 l2 = len_list T1 l1).
  50    (fold_right_list2 T1 T2 f acc l1 l2 H1 = fold_right_list2 T1 T2 f acc l2 l1 H2)).
  51  #T1; #T2; #f; #H; #acc; #l1;
  52  nelim l1;
  53  ##[ ##1: #l2; ncases l2;
  54           ##[ ##1: nnormalize; #H1; #H2; napply refl_eq
  55           ##| ##2: #h; #l; #H1; #H2;
  56                    nchange in H1:(%) with (O = (S (len_list ? l)));
  57                    ndestruct (*nelim (nat_destruct_0_S ? H1)*)
  58           ##]
  59  ##| ##2: #h3; #l3; #H1; #l2; ncases l2;
  60           ##[ ##1: #H2; #H3; nchange in H2:(%) with ((S (len_list ? l3)) = O);
  61                    ndestruct (*nelim (nat_destruct_S_0 ? H1)*)
  62           ##| ##2: #h4; #l4; #H2; #H3;
  63                    nchange in H2:(%) with ((S (len_list ? l3)) = (S (len_list ? l4)));
  64                    nchange in H3:(%) with ((S (len_list ? l4)) = (S (len_list ? l3)));
  65                    nchange with ((f h3 h4 (fold_right_list2 T1 T2 f acc l3 l4 (fold_right_list2_aux3 T1 h3 h4 l3 l4 ?))) =
  66                                  (f h4 h3 (fold_right_list2 T1 T2 f acc l4 l3 (fold_right_list2_aux3 T1 h4 h3 l4 l3 ?))));
  67                    nrewrite < (H1 l4 (fold_right_list2_aux3 T1 h3 h4 l3 l4 H2) (fold_right_list2_aux3 T1 h4 h3 l4 l3 H3));
  68                    nrewrite > (H h3 h4 (fold_right_list2 T1 T2 f acc l3 l4 ?));
  69                    napply refl_eq
  70           ##]
  71  ##]
  72 nqed.
  73
  74 nlemma symmetric_foldrightlist2 :
  75 ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.
  76  (∀x,y,z.f x y z = f y x z) →
  77  (∀acc:T2.∀l1,l2:list T1.∀H:len_list T1 l1 = len_list T1 l2.
  78    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)).
  79  #T1; #T2; #f; #H; #acc; #l1; #l2; #H1;
  80  nrewrite > (symmetric_foldrightlist2_aux T1 T2 f H acc l1 l2 H1 (symmetric_lenlist T1 l1 l2 H1));
  81  napply refl_eq.
  82 nqed.
  83
  84 nlemma symmetric_bfoldrightlist2 :
  85 ∀T1:Type.∀f:T1 → T1 → bool.
  86  (∀x,y.f x y = f y x) →
  87  (∀l1,l2:list T1.
  88   bfold_right_list2 T1 f l1 l2 = bfold_right_list2 T1 f l2 l1).
  89  #T; #f; #H; #l1;
  90  nelim l1;
  91  ##[ ##1: #l2; ncases l2;
  92           ##[ ##1: nnormalize; napply refl_eq
  93           ##| ##2: #hh2; #ll2; nnormalize; napply refl_eq
  94           ##]
  95  ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
  96           ##[ ##1: nnormalize; napply refl_eq
  97           ##| ##2: #hh2; #ll2; nnormalize;
  98                    nrewrite > (H1 ll2);
  99                    nrewrite > (H hh1 hh2);
 100                    napply refl_eq
 101           ##]
 102  ##]
 103 nqed.
 104
 105 nlemma bfoldrightlist2_to_eq :
 106 ∀T1:Type.∀f:T1 → T1 → bool.
 107  (∀x,y.(f x y = true → x = y)) →
 108  (∀l1,l2:list T1.
 109   (bfold_right_list2 T1 f l1 l2 = true → l1 = l2)).
 110  #T; #f; #H; #l1;
 111  nelim l1;
 112  ##[ ##1: #l2; ncases l2;
 113           ##[ ##1: #H1; napply refl_eq
 114           ##| ##2: #hh2; #ll2; nnormalize; #H1;
 115                    ndestruct (*napply (bool_destruct … H1)*)
 116           ##]
 117  ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
 118           ##[ ##1: nnormalize; #H2;
 119                    ndestruct (*napply (bool_destruct … H2)*)
 120           ##| ##2: #hh2; #ll2; #H2;
 121                    nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_list2 T f ll1 ll2)) = true);
 122                    nrewrite > (H hh1 hh2 (andb_true_true_l … H2));
 123                    nrewrite > (H1 ll2 (andb_true_true_r … H2));
 124                    napply refl_eq
 125           ##]
 126  ##]
 127 nqed.
 128
 129 nlemma eq_to_bfoldrightlist2 :
 130 ∀T1:Type.∀f:T1 → T1 → bool.
 131  (∀x,y.(x = y → f x y = true)) →
 132  (∀l1,l2:list T1.
 133   (l1 = l2 → bfold_right_list2 T1 f l1 l2 = true)).
 134  #T; #f; #H; #l1;
 135  nelim l1;
 136  ##[ ##1: #l2; ncases l2;
 137           ##[ ##1: #H1; nnormalize; napply refl_eq
 138           ##| ##2: #hh2; #ll2; #H1;
 139                    (* !!! ndestruct: assert false *)
 140                    nelim (list_destruct_nil_cons ??? H1)
 141           ##]
 142  ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
 143           ##[ ##1: #H2;
 144                    (* !!! ndestruct: assert false *)
 145                    nelim (list_destruct_cons_nil ??? H2)
 146           ##| ##2: #hh2; #ll2; #H2; nnormalize;
 147                    nrewrite > (list_destruct_1 … H2);
 148                    nrewrite > (H hh2 hh2 (refl_eq …));
 149                    nnormalize;
 150                    nrewrite > (H1 ll2 (list_destruct_2 … H2));
 151                    napply refl_eq
 152           ##]
 153  ##]
 154 nqed.
 155
 156 nlemma bfoldrightlist2_to_lenlist :
 157 ∀T.∀f:T → T → bool.
 158  (∀l1,l2:list T.bfold_right_list2 T f l1 l2 = true → len_list T l1 = len_list T l2).
 159  #T; #f; #l1;
 160  nelim l1;
 161  ##[ ##1: #l2; ncases l2;
 162           ##[ ##1: nnormalize; #H; napply refl_eq
 163           ##| ##2: nnormalize; #hh; #tt; #H;
 164                    ndestruct (*napply (bool_destruct … H)*)
 165           ##]
 166  ##| ##2: #hh; #tt; #H; #l2; ncases l2;
 167           ##[ ##1: nnormalize; #H1;
 168                    ndestruct (*napply (bool_destruct … H1)*)
 169           ##| ##2: #hh1; #tt1; #H1; nnormalize;
 170                    nrewrite > (H tt1 ?);
 171                    ##[ ##1: napply refl_eq
 172                    ##| ##2: nchange in H1:(%) with ((? ⊗ (bfold_right_list2 T f tt tt1)) = true);
 173                             napply (andb_true_true_r … H1)
 174                    ##]
 175           ##]
 176  ##]
 177 nqed.
 178
 179 nlemma decidable_list :
 180 ∀T.(∀x,y:T.decidable (x = y)) →
 181    (∀x,y:list T.decidable (x = y)).
 182  #T; #H; #x; nelim x;
 183  ##[ ##1: #y; ncases y;
 184           ##[ ##1: nnormalize; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
 185           ##| ##2: #hh2; #tt2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 186                    nnormalize; #H1;
 187                    (* !!! ndestruct: assert false *)
 188                    napply (list_destruct_nil_cons T … H1)
 189           ##]
 190  ##| ##2: #hh1; #tt1; #H1; #y; ncases y;
 191           ##[ ##1: nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 192                    nnormalize; #H2;
 193                    (* !!! ndestruct: assert false *)
 194                    napply (list_destruct_cons_nil T … H2)
 195           ##| ##2: #hh2; #tt2; nnormalize; napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H …));
 196                    ##[ ##2: #H2; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 197                             nnormalize; #H3; napply (H2 (list_destruct_1 T … H3))
 198                    ##| ##1: #H2; napply (or2_elim (tt1 = tt2) (tt1 ≠ tt2) ? (H1 tt2));
 199                             ##[ ##2: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 200                                      nnormalize; #H4; napply (H3 (list_destruct_2 T … H4))
 201                             ##| ##1: #H3; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
 202                                      nrewrite > H2; nrewrite > H3; napply refl_eq
 203                             ##]
 204                    ##]
 205           ##]
 206  ##]
 207 nqed.
 208
 209 nlemma nbfoldrightlist2_to_neq :
 210 ∀T1:Type.∀f:T1 → T1 → bool.
 211  (∀x,y.(f x y = false → x ≠ y)) →
 212  (∀l1,l2:list T1.
 213   (bfold_right_list2 T1 f l1 l2 = false → l1 ≠ l2)).
 214  #T; #f; #H; #l1;
 215  nelim l1;
 216  ##[ ##1: #l2; ncases l2;
 217           ##[ ##1: nnormalize; #H1;
 218                    ndestruct (*napply (bool_destruct … H1)*)
 219           ##| ##2: #hh2; #ll2; #H1; nnormalize; #H2;
 220                    (* !!! ndestruct: assert false *)
 221                    napply (list_destruct_nil_cons T … H2)
 222           ##]
 223  ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
 224           ##[ ##1: #H2; nnormalize; #H3;
 225                    (* !!! ndestruct: assert false *)
 226                    napply (list_destruct_cons_nil T … H3)
 227           ##| ##2: #hh2; #ll2; #H2; nnormalize; #H3;
 228                    nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_list2 T f ll1 ll2)) = false);
 229                    napply (H1 ll2 ? (list_destruct_2 T … H3));
 230                    napply (or2_elim ??? (andb_false2 … H2) );
 231                    ##[ ##1: #H4; napply (absurd (hh1 = hh2) …);
 232                             ##[ ##1: nrewrite > (list_destruct_1 T … H3); napply refl_eq
 233                             ##| ##2: napply (H … H4)
 234                             ##]
 235                    ##| ##2: #H4; napply H4
 236                    ##]
 237           ##]
 238  ##]
 239 nqed.
 240
 241 nlemma list_destruct :
 242 ∀T.(∀x,y:T.decidable (x = y)) →
 243    (∀h1,h2:T.∀l1,l2:list T.
 244     (h1::l1) ≠ (h2::l2) → h1 ≠ h2 ∨ l1 ≠ l2).
 245  #T; #H; #h1; #h2; #l1; nelim l1;
 246  ##[ ##1: #l2; ncases l2;
 247           ##[ ##1: #H1; napply (or2_intro1 (h1 ≠ h2) ([] ≠ []) …);
 248                    nnormalize; #H2; nrewrite > H2 in H1:(%);
 249                    nnormalize; #H1; napply (H1 (refl_eq …))
 250           ##| ##2: #hh2; #ll2; #H1; napply (or2_intro2 (h1 ≠ h2) ([] ≠ (hh2::ll2)) …);
 251                    nnormalize; #H2;
 252                    (* !!! ndestruct: assert false *)
 253                    napply (list_destruct_nil_cons T … H2)
 254           ##]
 255  ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
 256           ##[ ##1: #H2; napply (or2_intro2 (h1 ≠ h2) ((hh1::ll1) ≠ []) …);
 257                    nnormalize; #H3;
 258                    (* !!! ndestruct: assert false *)
 259                    napply (list_destruct_cons_nil T … H3)
 260           ##| ##2: #hh2; #ll2; #H2;
 261                    napply (or2_elim (h1 = h2) (h1 ≠ h2) ? (H h1 h2) …);
 262                    ##[ ##2: #H3; napply (or2_intro1 (h1 ≠ h2) ((hh1::ll1) ≠ (hh2::ll2)) H3)
 263                    ##| ##1: #H3; napply (or2_intro2 (h1 ≠ h2) ((hh1::ll1) ≠ (hh2::ll2) …));
 264                             nrewrite > H3 in H2:(%); #H2;
 265                             nnormalize; #H4; nrewrite > (list_destruct_1 T … H4) in H2:(%); #H2;
 266                             nrewrite > (list_destruct_2 T … H4) in H2:(%); #H2;
 267                             napply (H2 (refl_eq …))
 268                    ##]
 269           ##]
 270  ##]
 271 nqed.
 272
 273 nlemma neq_to_nbfoldrightlist2 :
 274 ∀T:Type.∀f:T → T → bool.
 275  (∀x,y:T.decidable (x = y)) →
 276  (∀x,y.(x ≠ y → f x y = false)) →
 277  (∀l1,l2:list T.
 278   (l1 ≠ l2 → bfold_right_list2 T f l1 l2 = false)).
 279  #T; #f; #H; #H1; #l1;
 280  nelim l1;
 281  ##[ ##1: #l2; ncases l2;
 282           ##[ ##1: nnormalize; #H2; nelim (H2 (refl_eq …))
 283           ##| ##2: #hh2; #ll2; nnormalize; #H2; napply refl_eq
 284           ##]
 285  ##| ##2: #hh1; #ll1; #H2; #l2; ncases l2;
 286           ##[ ##1: nnormalize; #H3; napply refl_eq
 287           ##| ##2: #hh2; #ll2; #H3;
 288                    nchange with (((f hh1 hh2)⊗(bfold_right_list2 T f ll1 ll2)) = false);
 289                    napply (or2_elim (hh1 ≠ hh2) (ll1 ≠ ll2) ? (list_destruct T H … H3) …);
 290                    ##[ ##1: #H4; nrewrite > (H1 hh1 hh2 H4); nnormalize; napply refl_eq
 291                    ##| ##2: #H4; nrewrite > (H2 ll2 H4);
 292                             nrewrite > (symmetric_andbool (f hh1 hh2) false);
 293                             nnormalize; napply refl_eq
 294                    ##]
 295           ##]
 296  ##]
 297 nqed.
 298
 299 nlemma isbemptylist_to_isemptylist : ∀T,l.isb_empty_list T l = true → is_empty_list T l.
 300  #T; #l;
 301  ncases l;
 302  nnormalize;
 303  ##[ ##1: #H; napply I
 304  ##| ##2: #x; #l; #H; ndestruct (*napply (bool_destruct … H)*)
 305  ##]
 306 nqed.
 307
 308 nlemma isnotbemptylist_to_isnotemptylist : ∀T,l.isnotb_empty_list T l = true → isnot_empty_list T l.
 309  #T; #l;
 310  ncases l;
 311  nnormalize;
 312  ##[ ##1: #H; ndestruct (*napply (bool_destruct … H)*)
 313  ##| ##2: #x; #l; #H; napply I
 314  ##]
 315 nqed.
 316
 317 (* ************** *)
 318 (* NON-EMPTY LIST *)
 319 (* ************** *)
 320
 321 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.
 322  #T; #l1;
 323  nelim l1;
 324  ##[ ##1: #h; #l2; ncases l2; nnormalize;
 325           ##[ ##1: #H; #H1; napply refl_eq
 326           ##| ##2: #h; #t; #H; nrewrite > H; napply refl_eq
 327           ##]
 328  ##| ##2: #h; #l2; ncases l2; nnormalize;
 329           ##[ ##1: #h1; #H; #l; #H1; nrewrite < H1; napply refl_eq
 330           ##| ##2: #h; #l; #H; #l3; #H1; nrewrite < H1; napply refl_eq
 331           ##]
 332  ##]
 333 nqed.
 334
 335 nlemma symmetric_foldrightnelist2_aux :
 336 ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.
 337  (∀x,y,z.f x y z = f y x z) →
 338  (∀acc:T2.∀l1,l2:ne_list T1.
 339   ∀H1:len_neList T1 l1 = len_neList T1 l2.∀H2:len_neList T1 l2 = len_neList T1 l1.
 340    fold_right_neList2 T1 T2 f acc l1 l2 H1 = fold_right_neList2 T1 T2 f acc l2 l1 H2).
 341  #T1; #T2; #f; #H; #acc; #l1;
 342  nelim l1;
 343  ##[ ##1: #h; #l2; ncases l2;
 344           ##[ ##1: #h1; nnormalize; #H1; #H2; nrewrite > (H h h1 acc); napply refl_eq
 345           ##| ##2: #h1; #l; ncases l;
 346                    ##[ ##1: #h3; #H1; #H2;
 347                             nchange in H1:(%) with ((S O) = (S (S O)));
 348                             (* !!! ndestruct: si inceppa su un'ipotesi che non e' H1 *)
 349                             nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))
 350                    ##| ##2: #h3; #l3; #H1; #H2;
 351                             nchange in H1:(%) with ((S O) = (S (S (len_neList ? l3))));
 352                             (* !!! ndestruct: si inceppa su un'ipotesi che non e' H1 *)
 353                             nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))
 354                    ##]
 355           ##]
 356  ##| ##2: #h3; #l3; #H1; #l2; ncases l2;
 357           ##[ ##1: #h4; ncases l3;
 358                    ##[ ##1: #h5; #H2; #H3;
 359                             nchange in H2:(%) with ((S (S O)) = (S O));
 360                             (* !!! ndestruct: si inceppa su un'ipotesi che non e' H1 *)
 361                             nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H2))
 362                    ##| ##2: #h5; #l5; #H2; #H3;
 363                             nchange in H2:(%) with ((S (S (len_neList ? l5))) = (S O));
 364                             (* !!! ndestruct: si inceppa su un'ipotesi che non e' H1 *)
 365                             nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H2))
 366                    ##]
 367           ##| ##2: #h4; #l4; #H2; #H3;
 368                    nchange in H2:(%) with ((S (len_neList ? l3)) = (S (len_neList ? l4)));
 369                    nchange in H3:(%) with ((S (len_neList ? l4)) = (S (len_neList ? l3)));
 370                    nchange with ((f h3 h4 (fold_right_neList2 T1 T2 f acc l3 l4 (fold_right_neList2_aux3 T1 h3 h4 l3 l4 ?))) =
 371                                  (f h4 h3 (fold_right_neList2 T1 T2 f acc l4 l3 (fold_right_neList2_aux3 T1 h4 h3 l4 l3 ?))));
 372                    nrewrite < (H1 l4 (fold_right_neList2_aux3 T1 h3 h4 l3 l4 H2) (fold_right_neList2_aux3 T1 h4 h3 l4 l3 H3));
 373                    nrewrite > (H h3 h4 (fold_right_neList2 T1 T2 f acc l3 l4 ?));
 374                    napply refl_eq
 375           ##]
 376  ##]
 377 nqed.
 378
 379 nlemma symmetric_foldrightnelist2 :
 380 ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.
 381  (∀x,y,z.f x y z = f y x z) →
 382  (∀acc:T2.∀l1,l2:ne_list T1.∀H:len_neList T1 l1 = len_neList T1 l2.
 383   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)).
 384  #T1; #T2; #f; #H; #acc; #l1; #l2; #H1;
 385  nrewrite > (symmetric_foldrightnelist2_aux T1 T2 f H acc l1 l2 H1 (symmetric_lennelist T1 l1 l2 H1));
 386  napply refl_eq.
 387 nqed.
 388
 389 nlemma symmetric_bfoldrightnelist2 :
 390 ∀T1:Type.∀f:T1 → T1 → bool.
 391  (∀x,y.f x y = f y x) →
 392  (∀l1,l2:ne_list T1.
 393   bfold_right_neList2 T1 f l1 l2 = bfold_right_neList2 T1 f l2 l1).
 394  #T; #f; #H; #l1;
 395  nelim l1;
 396  ##[ ##1: #hh1; #l2; ncases l2;
 397           ##[ ##1: #hh2; nnormalize; nrewrite > (H hh1 hh2); napply refl_eq
 398           ##| ##2: #hh2; #ll2; nnormalize; napply refl_eq
 399           ##]
 400  ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
 401           ##[ ##1: #hh2; nnormalize; napply refl_eq
 402           ##| ##2: #hh2; #ll2; nnormalize;
 403                    nrewrite > (H1 ll2);
 404                    nrewrite > (H hh1 hh2);
 405                    napply refl_eq
 406           ##]
 407  ##]
 408 nqed.
 409
 410 nlemma bfoldrightnelist2_to_eq :
 411 ∀T1:Type.∀f:T1 → T1 → bool.
 412  (∀x,y.(f x y = true → x = y)) →
 413  (∀l1,l2:ne_list T1.
 414   (bfold_right_neList2 T1 f l1 l2 = true → l1 = l2)).
 415  #T; #f; #H; #l1;
 416  nelim l1;
 417  ##[ ##1: #hh1; #l2; ncases l2;
 418           ##[ ##1: #hh2; #H1; nnormalize in H1:(%); nrewrite > (H hh1 hh2 H1); napply refl_eq
 419           ##| ##2: #hh2; #ll2; nnormalize; #H1; ndestruct (*napply (bool_destruct … H1)*)
 420           ##]
 421  ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
 422           ##[ ##1: #hh2; nnormalize; #H2; ndestruct (*napply (bool_destruct … H2)*)
 423           ##| ##2: #hh2; #ll2; #H2;
 424                    nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = true);
 425                    nrewrite > (H hh1 hh2 (andb_true_true_l … H2));
 426                    nrewrite > (H1 ll2 (andb_true_true_r … H2));
 427                    napply refl_eq
 428           ##]
 429  ##]
 430 nqed.
 431
 432 nlemma eq_to_bfoldrightnelist2 :
 433 ∀T1:Type.∀f:T1 → T1 → bool.
 434  (∀x,y.(x = y → f x y = true)) →
 435  (∀l1,l2:ne_list T1.
 436   (l1 = l2 → bfold_right_neList2 T1 f l1 l2 = true)).
 437  #T; #f; #H; #l1;
 438  nelim l1;
 439  ##[ ##1: #hh1; #l2; ncases l2;
 440           ##[ ##1: #hh2; #H1; nnormalize;
 441                    nrewrite > (H hh1 hh2 (nelist_destruct_nil_nil … H1));
 442                    napply refl_eq
 443           ##| ##2: #hh2; #ll2; #H1;
 444                    (* !!! ndestruct: assert false *)
 445                    nelim (nelist_destruct_nil_cons ???? H1)
 446           ##]
 447  ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
 448           ##[ ##1: #hh2; #H2;
 449                    (* !!! ndestruct: assert false *)
 450                    nelim (nelist_destruct_cons_nil ???? H2)
 451           ##| ##2: #hh2; #ll2; #H2; nnormalize;
 452                    nrewrite > (nelist_destruct_cons_cons_1 … H2);
 453                    nrewrite > (H hh2 hh2 (refl_eq …));
 454                    nnormalize;
 455                    nrewrite > (H1 ll2 (nelist_destruct_cons_cons_2 … H2));
 456                    napply refl_eq
 457           ##]
 458  ##]
 459 nqed.
 460
 461 nlemma bfoldrightnelist2_to_lennelist :
 462 ∀T.∀f:T → T → bool.
 463  (∀l1,l2:ne_list T.bfold_right_neList2 T f l1 l2 = true → len_neList T l1 = len_neList T l2).
 464  #T; #f; #l1;
 465  nelim l1;
 466  ##[ ##1: #hh1; #l2; ncases l2;
 467           ##[ ##1: nnormalize; #hh2; #H; napply refl_eq
 468           ##| ##2: nnormalize; #hh2; #tt2; #H; ndestruct (*napply (bool_destruct … H)*)
 469           ##]
 470  ##| ##2: #hh1; #tt1; #H; #l2; ncases l2;
 471           ##[ ##1: nnormalize; #hh2; #H1; ndestruct (*napply (bool_destruct … H1)*)
 472           ##| ##2: #hh2; #tt2; #H1; nnormalize;
 473                    nrewrite > (H tt2 ?);
 474                    ##[ ##1: napply refl_eq
 475                    ##| ##2: nchange in H1:(%) with ((? ⊗ (bfold_right_neList2 T f tt1 tt2)) = true);
 476                             napply (andb_true_true_r … H1)
 477                    ##]
 478           ##]
 479  ##]
 480 nqed.
 481
 482 nlemma decidable_nelist :
 483 ∀T.(∀x,y:T.decidable (x = y)) →
 484    (∀x,y:ne_list T.decidable (x = y)).
 485  #T; #H; #x; nelim x;
 486  ##[ ##1: #hh1; #y; ncases y;
 487           ##[ ##1: #hh2; nnormalize; napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H hh1 hh2));
 488                    ##[ ##1: #H1; nrewrite > H1; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
 489                    ##| ##2: #H1; napply (or2_intro2 (? = ?) (? ≠ ?) ?); nnormalize;
 490                             #H2; napply (H1 (nelist_destruct_nil_nil T … H2))
 491                    ##]
 492           ##| ##2: #hh2; #tt2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 493                    nnormalize; #H1;
 494                    (* !!! ndestruct: assert false *)
 495                    napply (nelist_destruct_nil_cons T … H1)
 496           ##]
 497  ##| ##2: #hh1; #tt1; #H1; #y; ncases y;
 498           ##[ ##1: #hh1; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 499                    nnormalize; #H2;
 500                    (* !!! ndestruct: assert false *)
 501                    napply (nelist_destruct_cons_nil T … H2)
 502           ##| ##2: #hh2; #tt2; nnormalize; napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H …));
 503                    ##[ ##2: #H2; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 504                             nnormalize; #H3; napply (H2 (nelist_destruct_cons_cons_1 T … H3))
 505                    ##| ##1: #H2; napply (or2_elim (tt1 = tt2) (tt1 ≠ tt2) ? (H1 tt2));
 506                             ##[ ##2: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 507                                      nnormalize; #H4; napply (H3 (nelist_destruct_cons_cons_2 T … H4))
 508                             ##| ##1: #H3; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
 509                                      nrewrite > H2; nrewrite > H3; napply refl_eq
 510                             ##]
 511                    ##]
 512           ##]
 513  ##]
 514 nqed.
 515
 516 nlemma nbfoldrightnelist2_to_neq :
 517 ∀T1:Type.∀f:T1 → T1 → bool.
 518  (∀x,y.(f x y = false → x ≠ y)) →
 519  (∀l1,l2:ne_list T1.
 520   (bfold_right_neList2 T1 f l1 l2 = false → l1 ≠ l2)).
 521  #T; #f; #H; #l1;
 522  nelim l1;
 523  ##[ ##1: #hh1; #l2; ncases l2;
 524           ##[ ##1: #hh2; nnormalize; #H1; #H2; napply (H hh1 hh2 H1 (nelist_destruct_nil_nil T … H2))
 525           ##| ##2: #hh2; #ll2; #H1; nnormalize; #H2;
 526                    (* !!! ndestruct: assert false *)
 527                    napply (nelist_destruct_nil_cons T … H2)
 528           ##]
 529  ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
 530           ##[ ##1: #hh2; #H2; nnormalize; #H3;
 531                    (* !!! ndestruct: assert false *)
 532                    napply (nelist_destruct_cons_nil T … H3)
 533           ##| ##2: #hh2; #ll2; #H2; nnormalize; #H3;
 534                    nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = false);
 535                    napply (H1 ll2 ? (nelist_destruct_cons_cons_2 T … H3));
 536                    napply (or2_elim ??? (andb_false2 … H2) );
 537                    ##[ ##1: #H4; napply (absurd (hh1 = hh2) …);
 538                             ##[ ##1: nrewrite > (nelist_destruct_cons_cons_1 T … H3); napply refl_eq
 539                             ##| ##2: napply (H … H4)
 540                             ##]
 541                    ##| ##2: #H4; napply H4
 542                    ##]
 543           ##]
 544  ##]
 545 nqed.
 546
 547 nlemma nelist_destruct :
 548 ∀T.(∀x,y:T.decidable (x = y)) →
 549    (∀h1,h2:T.∀l1,l2:ne_list T.
 550     (h1§§l1) ≠ (h2§§l2) → h1 ≠ h2 ∨ l1 ≠ l2).
 551  #T; #H; #h1; #h2; #l1; nelim l1;
 552  ##[ ##1: #hh1; #l2; ncases l2;
 553           ##[ ##1: #hh2; #H1; napply (or2_elim (h1 = h2) (h1 ≠ h2) ? (H …) …);
 554                    ##[ ##2: #H2; napply (or2_intro1 (h1 ≠ h2) («£hh1» ≠ «£hh2») H2)
 555                    ##| ##1: #H2; nrewrite > H2 in H1:(%); #H1;
 556                             napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H …) …);
 557                             ##[ ##2: #H3; napply (or2_intro2 (h2 ≠ h2) («£hh1» ≠ «£hh2») ?);
 558                                      nnormalize; #H4; napply (H3 (nelist_destruct_nil_nil T … H4))
 559                             ##| ##1: #H3; nrewrite > H3 in H1:(%); #H1; nelim (H1 (refl_eq …))
 560                             ##]
 561                    ##]
 562           ##| ##2: #hh2; #ll2; #H1; napply (or2_intro2 (h1 ≠ h2) («£hh1» ≠ (hh2§§ll2)) …);
 563                    nnormalize; #H2;
 564                    (* !!! ndestruct: assert false *)
 565                    napply (nelist_destruct_nil_cons T … H2)
 566           ##]
 567  ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
 568           ##[ ##1: #hh2; #H2; napply (or2_intro2 (h1 ≠ h2) ((hh1§§ll1) ≠ «£hh2») …);
 569                    nnormalize; #H3;
 570                    (* !!! ndestruct: assert false *)
 571                    napply (nelist_destruct_cons_nil T … H3)
 572           ##| ##2: #hh2; #ll2; #H2;
 573                    napply (or2_elim (h1 = h2) (h1 ≠ h2) ? (H h1 h2) …);
 574                    ##[ ##2: #H3; napply (or2_intro1 (h1 ≠ h2) ((hh1§§ll1) ≠ (hh2§§ll2)) H3)
 575                    ##| ##1: #H3; napply (or2_intro2 (h1 ≠ h2) ((hh1§§ll1) ≠ (hh2§§ll2) …));
 576                             nrewrite > H3 in H2:(%); #H2;
 577                             nnormalize; #H4; nrewrite > (nelist_destruct_cons_cons_1 T … H4) in H2:(%); #H2;
 578                             nrewrite > (nelist_destruct_cons_cons_2 T … H4) in H2:(%); #H2;
 579                             napply (H2 (refl_eq …))
 580                    ##]
 581           ##]
 582  ##]
 583 nqed.
 584
 585 nlemma neq_to_nbfoldrightnelist2 :
 586 ∀T:Type.∀f:T → T → bool.
 587  (∀x,y:T.decidable (x = y)) →
 588  (∀x,y.(x ≠ y → f x y = false)) →
 589  (∀l1,l2:ne_list T.
 590   (l1 ≠ l2 → bfold_right_neList2 T f l1 l2 = false)).
 591  #T; #f; #H; #H1; #l1;
 592  nelim l1;
 593  ##[ ##1: #hh1; #l2; ncases l2;
 594           ##[ ##1: #hh2; nnormalize; #H2; napply (H1 hh1 hh2 ?);
 595                    nnormalize; #H3; nrewrite > H3 in H2:(%); #H2; napply (H2 (refl_eq …))
 596           ##| ##2: #hh2; #ll2; nnormalize; #H2; napply refl_eq
 597           ##]
 598  ##| ##2: #hh1; #ll1; #H2; #l2; ncases l2;
 599           ##[ ##1: #hh2; nnormalize; #H3; napply refl_eq
 600           ##| ##2: #hh2; #ll2; #H3;
 601                    nchange with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = false);
 602                    napply (or2_elim (hh1 ≠ hh2) (ll1 ≠ ll2) ? (nelist_destruct T H … H3) …);
 603                    ##[ ##1: #H4; nrewrite > (H1 hh1 hh2 H4); nnormalize; napply refl_eq
 604                    ##| ##2: #H4; nrewrite > (H2 ll2 H4);
 605                             nrewrite > (symmetric_andbool (f hh1 hh2) false);
 606                             nnormalize; napply refl_eq
 607                    ##]
 608           ##]
 609  ##]
 610 nqed.