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