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 (*   Ultima modifica: 05/08/2009                                          *)
  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; 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                    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                    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; napply (bool_destruct … H1)
 110           ##]
 111  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
 112           ##[ ##1: #H1; nnormalize; #H2; napply (bool_destruct … H2)
 113           ##| ##2: #hh2; #ll2; #H1; #H2;
 114                    nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_list2 T f ll1 ll2)) = true);
 115                    nrewrite > (H1 hh1 hh2 (andb_true_true_l … H2));
 116                    nrewrite > (H ll2 H1 (andb_true_true_r … H2));
 117                    napply refl_eq
 118           ##]
 119  ##]
 120 nqed.
 121
 122 nlemma eq_to_bfoldrightlist2
 123  : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:list T1.
 124    (∀x,y.(x = y → f x y = true)) →
 125    (l1 = l2 → bfold_right_list2 T1 f l1 l2 = true).
 126  #T; #f; #l1;
 127  nelim l1;
 128  ##[ ##1: #l2; ncases l2;
 129           ##[ ##1: #H; #H1; nnormalize; napply refl_eq
 130           ##| ##2: #hh2; #ll2; #H; #H1; nelim (list_destruct_nil_cons ??? H1)
 131           ##]
 132  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
 133           ##[ ##1: #H1; #H2; nelim (list_destruct_cons_nil ??? H2)
 134           ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize;
 135                    nrewrite > (list_destruct_1 … H2);
 136                    nrewrite > (H1 hh2 hh2 (refl_eq …));
 137                    nnormalize;
 138                    nrewrite > (H ll2 H1 (list_destruct_2 … H2));
 139                    napply refl_eq
 140           ##]
 141  ##]
 142 nqed.
 143
 144 nlemma bfoldrightlist2_to_lenlist
 145  : ∀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.
 146  #T; #f; #l1;
 147  nelim l1;
 148  ##[ ##1: #l2; ncases l2;
 149           ##[ ##1: nnormalize; #H; napply refl_eq
 150           ##| ##2: nnormalize; #hh; #tt; #H; napply (bool_destruct … H)
 151           ##]
 152  ##| ##2: #hh; #tt; #H; #l2; ncases l2;
 153           ##[ ##1: nnormalize; #H1; napply (bool_destruct … H1)
 154           ##| ##2: #hh1; #tt1; #H1; nnormalize;
 155                    nrewrite > (H tt1 ?);
 156                    ##[ ##1: napply refl_eq
 157                    ##| ##2: nchange in H1:(%) with ((? ⊗ (bfold_right_list2 T f tt tt1)) = true);
 158                             napply (andb_true_true_r … H1)
 159                    ##]
 160           ##]
 161  ##]
 162 nqed.
 163
 164 nlemma decidable_list : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀x,y:list T.decidable (x = y).
 165  #T; #H; #x; nelim x;
 166  ##[ ##1: #y; ncases y;
 167           ##[ ##1: nnormalize; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
 168           ##| ##2: #hh2; #tt2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 169                    nnormalize; #H1; napply (list_destruct_nil_cons T … H1)
 170           ##]
 171  ##| ##2: #hh1; #tt1; #H1; #y; ncases y;
 172           ##[ ##1: nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 173                    nnormalize; #H2; napply (list_destruct_cons_nil T … H2)
 174           ##| ##2: #hh2; #tt2; nnormalize; napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H …));
 175                    ##[ ##2: #H2; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 176                             nnormalize; #H3; napply (H2 (list_destruct_1 T … H3))
 177                    ##| ##1: #H2; napply (or2_elim (tt1 = tt2) (tt1 ≠ tt2) ? (H1 tt2));
 178                             ##[ ##2: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 179                                      nnormalize; #H4; napply (H3 (list_destruct_2 T … H4))
 180                             ##| ##1: #H3; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
 181                                      nrewrite > H2; nrewrite > H3; napply refl_eq
 182                             ##]
 183                    ##]
 184           ##]
 185  ##]
 186 nqed.
 187
 188 nlemma nbfoldrightlist2_to_neq
 189  : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:list T1.
 190    (∀x,y.(f x y = false → x ≠ y)) →
 191    (bfold_right_list2 T1 f l1 l2 = false → l1 ≠ l2).
 192  #T; #f; #l1;
 193  nelim l1;
 194  ##[ ##1: #l2; ncases l2;
 195           ##[ ##1: #H; nnormalize; #H1; napply (bool_destruct … H1)
 196           ##| ##2: #hh2; #ll2; #H; #H1; nnormalize; #H2; napply (list_destruct_nil_cons T … H2)
 197           ##]
 198  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
 199           ##[ ##1: #H1; #H2; nnormalize; #H3; napply (list_destruct_cons_nil T … H3)
 200           ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize; #H3;
 201                    nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_list2 T f ll1 ll2)) = false);
 202                    napply (H ll2 H1 ? (list_destruct_2 T … H3));
 203                    napply (or2_elim ??? (andb_false2 … H2) );
 204                    ##[ ##1: #H4; napply (absurd (hh1 = hh2) …);
 205                             ##[ ##1: nrewrite > (list_destruct_1 T … H3); napply refl_eq
 206                             ##| ##2: napply (H1 … H4)
 207                             ##]
 208                    ##| ##2: #H4; napply H4
 209                    ##]
 210           ##]
 211  ##]
 212 nqed.
 213
 214 nlemma list_destruct
 215  : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀h1,h2:T.∀l1,l2:list T.(h1::l1) ≠ (h2::l2) → h1 ≠ h2 ∨ l1 ≠ l2.
 216  #T; #H; #h1; #h2; #l1; nelim l1;
 217  ##[ ##1: #l2; ncases l2;
 218           ##[ ##1: #H1; napply (or2_intro1 (h1 ≠ h2) ([] ≠ []) …);
 219                    nnormalize; #H2; nrewrite > H2 in H1:(%);
 220                    nnormalize; #H1; napply (H1 (refl_eq …))
 221           ##| ##2: #hh2; #ll2; #H1; napply (or2_intro2 (h1 ≠ h2) ([] ≠ (hh2::ll2)) …);
 222                    nnormalize; #H2; napply (list_destruct_nil_cons T … H2)
 223           ##]
 224  ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
 225           ##[ ##1: #H2; napply (or2_intro2 (h1 ≠ h2) ((hh1::ll1) ≠ []) …);
 226                    nnormalize; #H3; napply (list_destruct_cons_nil T … H3)
 227           ##| ##2: #hh2; #ll2; #H2;
 228                    napply (or2_elim (h1 = h2) (h1 ≠ h2) ? (H h1 h2) …);
 229                    ##[ ##2: #H3; napply (or2_intro1 (h1 ≠ h2) ((hh1::ll1) ≠ (hh2::ll2)) H3)
 230                    ##| ##1: #H3; napply (or2_intro2 (h1 ≠ h2) ((hh1::ll1) ≠ (hh2::ll2) …));
 231                             nrewrite > H3 in H2:(%); #H2;
 232                             nnormalize; #H4; nrewrite > (list_destruct_1 T … H4) in H2:(%); #H2;
 233                             nrewrite > (list_destruct_2 T … H4) in H2:(%); #H2;
 234                             napply (H2 (refl_eq …))
 235                    ##]
 236           ##]
 237  ##]
 238 nqed.
 239
 240 nlemma neq_to_nbfoldrightlist2
 241  : ∀T:Type.∀f:T → T → bool.∀l1,l2:list T.
 242    (∀x,y:T.decidable (x = y)) →
 243    (∀x,y.(x ≠ y → f x y = false)) →
 244    (l1 ≠ l2 → bfold_right_list2 T f l1 l2 = false).
 245  #T; #f; #l1;
 246  nelim l1;
 247  ##[ ##1: #l2; ncases l2;
 248           ##[ ##1: #H; #H1; nnormalize; #H2; nelim (H2 (refl_eq …))
 249           ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; #H2; napply refl_eq
 250           ##]
 251  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
 252           ##[ ##1: #H1; #H2; nnormalize; #H3; napply refl_eq
 253           ##| ##2: #hh2; #ll2; #H1; #H2; #H3;
 254                    nchange with (((f hh1 hh2)⊗(bfold_right_list2 T f ll1 ll2)) = false);
 255                    napply (or2_elim (hh1 ≠ hh2) (ll1 ≠ ll2) ? (list_destruct T H1 … H3) …);
 256                    ##[ ##1: #H4; nrewrite > (H2 hh1 hh2 H4); nnormalize; napply refl_eq
 257                    ##| ##2: #H4; nrewrite > (H ll2 H1 H2 H4);
 258                             nrewrite > (symmetric_andbool (f hh1 hh2) false);
 259                             nnormalize; napply refl_eq
 260                    ##]
 261           ##]
 262  ##]
 263 nqed.
 264
 265 nlemma isbemptylist_to_isemptylist : ∀T,l.isb_empty_list T l = true → is_empty_list T l.
 266  #T; #l;
 267  ncases l;
 268  nnormalize;
 269  ##[ ##1: #H; napply I
 270  ##| ##2: #x; #l; #H; napply (bool_destruct … H)
 271  ##]
 272 nqed.
 273
 274 nlemma isnotbemptylist_to_isnotemptylist : ∀T,l.isnotb_empty_list T l = true → isnot_empty_list T l.
 275  #T; #l;
 276  ncases l;
 277  nnormalize;
 278  ##[ ##1: #H; napply (bool_destruct … H)
 279  ##| ##2: #x; #l; #H; napply I
 280  ##]
 281 nqed.
 282
 283 (* ************** *)
 284 (* NON-EMPTY LIST *)
 285 (* ************** *)
 286
 287 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.
 288  #T; #l1;
 289  nelim l1;
 290  ##[ ##1: #h; #l2; ncases l2; nnormalize;
 291           ##[ ##1: #H; #H1; napply refl_eq
 292           ##| ##2: #h; #t; #H; nrewrite > H; napply refl_eq
 293           ##]
 294  ##| ##2: #h; #l2; ncases l2; nnormalize;
 295           ##[ ##1: #h1; #H; #l; #H1; nrewrite < H1; napply refl_eq
 296           ##| ##2: #h; #l; #H; #l3; #H1; nrewrite < H1; napply refl_eq
 297           ##]
 298  ##]
 299 nqed.
 300
 301 nlemma symmetric_foldrightnelist2_aux
 302  : ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.∀acc:T2.∀l1,l2:ne_list T1.
 303    ∀H1:len_neList T1 l1 = len_neList T1 l2.∀H2:len_neList T1 l2 = len_neList T1 l1.
 304   (∀x,y,z.f x y z = f y x z) →
 305   fold_right_neList2 T1 T2 f acc l1 l2 H1 = fold_right_neList2 T1 T2 f acc l2 l1 H2.
 306  #T1; #T2; #f; #acc; #l1;
 307  nelim l1;
 308  ##[ ##1: #h; #l2; ncases l2;
 309           ##[ ##1: #h1; nnormalize; #H1; #H2; #H3; nrewrite > (H3 h h1 acc); napply refl_eq
 310           ##| ##2: #h1; #l; ncases l;
 311                    ##[ ##1: #h3; #H1; #H2; #H3;
 312                             nchange in H1:(%) with ((S O) = (S (S O)));
 313                             nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))
 314                    ##| ##2: #h3; #l3; #H1; #H2; #H3;
 315                             nchange in H1:(%) with ((S O) = (S (S (len_neList ? l3))));
 316                             nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))
 317                    ##]
 318           ##]
 319  ##| ##2: #h3; #l3; #H; #l2; ncases l2;
 320           ##[ ##1: #h4; ncases l3;
 321                    ##[ ##1: #h5; #H1; #H2; #H3;
 322                             nchange in H1:(%) with ((S (S O)) = (S O));
 323                             nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H1))
 324                    ##| ##2: #h5; #l5; #H1; #H2; #H3;
 325                             nchange in H1:(%) with ((S (S (len_neList ? l5))) = (S O));
 326                             nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H1))
 327                    ##]
 328           ##| ##2: #h4; #l4; #H1; #H2; #H3;
 329                    nchange in H1:(%) with ((S (len_neList ? l3)) = (S (len_neList ? l4)));
 330                    nchange in H2:(%) 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 < (H l4 (fold_right_neList2_aux3 T1 h3 h4 l3 l4 H1) (fold_right_neList2_aux3 T1 h4 h3 l4 l3 H2) H3);
 334                    nrewrite > (H3 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.∀acc:T2.∀l1,l2:ne_list T1.∀H:len_neList T1 l1 = len_neList T1 l2.
 342   (∀x,y,z.f x y z = f y x z) →
 343   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).
 344  #T1; #T2; #f; #acc; #l1; #l2; #H; #H1;
 345  nrewrite > (symmetric_foldrightnelist2_aux T1 T2 f acc l1 l2 H (symmetric_lennelist T1 l1 l2 H) H1);
 346  napply refl_eq.
 347 nqed.
 348
 349 nlemma symmetric_bfoldrightnelist2
 350  : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1.
 351   (∀x,y.f x y = f y x) →
 352   bfold_right_neList2 T1 f l1 l2 = bfold_right_neList2 T1 f l2 l1.
 353  #T; #f; #l1;
 354  nelim l1;
 355  ##[ ##1: #hh1; #l2; ncases l2;
 356           ##[ ##1: #hh2; #H; nnormalize; nrewrite > (H hh1 hh2); napply refl_eq
 357           ##| ##2: #hh2; #ll2; #H; nnormalize; napply refl_eq
 358           ##]
 359  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
 360           ##[ ##1: #hh2; #H1; nnormalize; napply refl_eq
 361           ##| ##2: #hh2; #ll2; #H1; nnormalize;
 362                    nrewrite > (H ll2 H1);
 363                    nrewrite > (H1 hh1 hh2);
 364                    napply refl_eq
 365           ##]
 366  ##]
 367 nqed.
 368
 369 nlemma bfoldrightnelist2_to_eq
 370  : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1.
 371    (∀x,y.(f x y = true → x = y)) →
 372    (bfold_right_neList2 T1 f l1 l2 = true → l1 = l2).
 373  #T; #f; #l1;
 374  nelim l1;
 375  ##[ ##1: #hh1; #l2; ncases l2;
 376           ##[ ##1: #hh2; #H; #H1; nnormalize in H1:(%); nrewrite > (H hh1 hh2 H1); napply refl_eq
 377           ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; napply (bool_destruct … H1)
 378           ##]
 379  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
 380           ##[ ##1: #hh2; #H1; nnormalize; #H2; napply (bool_destruct … H2)
 381           ##| ##2: #hh2; #ll2; #H1; #H2;
 382                    nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = true);
 383                    nrewrite > (H1 hh1 hh2 (andb_true_true_l … H2));
 384                    nrewrite > (H ll2 H1 (andb_true_true_r … H2));
 385                    napply refl_eq
 386           ##]
 387  ##]
 388 nqed.
 389
 390 nlemma eq_to_bfoldrightnelist2
 391  : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1.
 392    (∀x,y.(x = y → f x y = true)) →
 393    (l1 = l2 → bfold_right_neList2 T1 f l1 l2 = true).
 394  #T; #f; #l1;
 395  nelim l1;
 396  ##[ ##1: #hh1; #l2; ncases l2;
 397           ##[ ##1: #hh2; #H; #H1; nnormalize;
 398                    nrewrite > (H hh1 hh2 (nelist_destruct_nil_nil … H1));
 399                    napply refl_eq
 400           ##| ##2: #hh2; #ll2; #H; #H1; nelim (nelist_destruct_nil_cons ???? H1)
 401           ##]
 402  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
 403           ##[ ##1: #hh2; #H1; #H2; nelim (nelist_destruct_cons_nil ???? H2)
 404           ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize;
 405                    nrewrite > (nelist_destruct_cons_cons_1 … H2);
 406                    nrewrite > (H1 hh2 hh2 (refl_eq …));
 407                    nnormalize;
 408                    nrewrite > (H ll2 H1 (nelist_destruct_cons_cons_2 … H2));
 409                    napply refl_eq
 410           ##]
 411  ##]
 412 nqed.
 413
 414 nlemma bfoldrightnelist2_to_lennelist
 415  : ∀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.
 416  #T; #f; #l1;
 417  nelim l1;
 418  ##[ ##1: #hh1; #l2; ncases l2;
 419           ##[ ##1: nnormalize; #hh2; #H; napply refl_eq
 420           ##| ##2: nnormalize; #hh2; #tt2; #H; napply (bool_destruct … H)
 421           ##]
 422  ##| ##2: #hh1; #tt1; #H; #l2; ncases l2;
 423           ##[ ##1: nnormalize; #hh2; #H1; napply (bool_destruct … H1)
 424           ##| ##2: #hh2; #tt2; #H1; nnormalize;
 425                    nrewrite > (H tt2 ?);
 426                    ##[ ##1: napply refl_eq
 427                    ##| ##2: nchange in H1:(%) with ((? ⊗ (bfold_right_neList2 T f tt1 tt2)) = true);
 428                             napply (andb_true_true_r … H1)
 429                    ##]
 430           ##]
 431  ##]
 432 nqed.
 433
 434 nlemma decidable_nelist : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀x,y:ne_list T.decidable (x = y).
 435  #T; #H; #x; nelim x;
 436  ##[ ##1: #hh1; #y; ncases y;
 437           ##[ ##1: #hh2; nnormalize; napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H hh1 hh2));
 438                    ##[ ##1: #H1; nrewrite > H1; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
 439                    ##| ##2: #H1; napply (or2_intro2 (? = ?) (? ≠ ?) ?); nnormalize;
 440                             #H2; napply (H1 (nelist_destruct_nil_nil T … H2))
 441                    ##]
 442           ##| ##2: #hh2; #tt2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 443                    nnormalize; #H1; napply (nelist_destruct_nil_cons T … H1)
 444           ##]
 445  ##| ##2: #hh1; #tt1; #H1; #y; ncases y;
 446           ##[ ##1: #hh1; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 447                    nnormalize; #H2; napply (nelist_destruct_cons_nil T … H2)
 448           ##| ##2: #hh2; #tt2; nnormalize; napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H …));
 449                    ##[ ##2: #H2; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 450                             nnormalize; #H3; napply (H2 (nelist_destruct_cons_cons_1 T … H3))
 451                    ##| ##1: #H2; napply (or2_elim (tt1 = tt2) (tt1 ≠ tt2) ? (H1 tt2));
 452                             ##[ ##2: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 453                                      nnormalize; #H4; napply (H3 (nelist_destruct_cons_cons_2 T … H4))
 454                             ##| ##1: #H3; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
 455                                      nrewrite > H2; nrewrite > H3; napply refl_eq
 456                             ##]
 457                    ##]
 458           ##]
 459  ##]
 460 nqed.
 461
 462 nlemma nbfoldrightnelist2_to_neq
 463  : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1.
 464    (∀x,y.(f x y = false → x ≠ y)) →
 465    (bfold_right_neList2 T1 f l1 l2 = false → l1 ≠ l2).
 466  #T; #f; #l1;
 467  nelim l1;
 468  ##[ ##1: #hh1; #l2; ncases l2;
 469           ##[ ##1: #hh2; #H; nnormalize; #H1; #H2; napply (H hh1 hh2 H1 (nelist_destruct_nil_nil T … H2))
 470           ##| ##2: #hh2; #ll2; #H; #H1; nnormalize; #H2; napply (nelist_destruct_nil_cons T … H2)
 471           ##]
 472  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
 473           ##[ ##1: #hh2; #H1; #H2; nnormalize; #H3; napply (nelist_destruct_cons_nil T … H3)
 474           ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize; #H3;
 475                    nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = false);
 476                    napply (H ll2 H1 ? (nelist_destruct_cons_cons_2 T … H3));
 477                    napply (or2_elim ??? (andb_false2 … H2) );
 478                    ##[ ##1: #H4; napply (absurd (hh1 = hh2) …);
 479                             ##[ ##1: nrewrite > (nelist_destruct_cons_cons_1 T … H3); napply refl_eq
 480                             ##| ##2: napply (H1 … H4)
 481                             ##]
 482                    ##| ##2: #H4; napply H4
 483                    ##]
 484           ##]
 485  ##]
 486 nqed.
 487
 488 nlemma nelist_destruct
 489  : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀h1,h2:T.∀l1,l2:ne_list T.(h1§§l1) ≠ (h2§§l2) → h1 ≠ h2 ∨ l1 ≠ l2.
 490  #T; #H; #h1; #h2; #l1; nelim l1;
 491  ##[ ##1: #hh1; #l2; ncases l2;
 492           ##[ ##1: #hh2; #H1; napply (or2_elim (h1 = h2) (h1 ≠ h2) ? (H …) …);
 493                    ##[ ##2: #H2; napply (or2_intro1 (h1 ≠ h2) («£hh1» ≠ «£hh2») H2)
 494                    ##| ##1: #H2; nrewrite > H2 in H1:(%); #H1;
 495                             napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H …) …);
 496                             ##[ ##2: #H3; napply (or2_intro2 (h2 ≠ h2) («£hh1» ≠ «£hh2») ?);
 497                                      nnormalize; #H4; napply (H3 (nelist_destruct_nil_nil T … H4))
 498                             ##| ##1: #H3; nrewrite > H3 in H1:(%); #H1; nelim (H1 (refl_eq …))
 499                             ##]
 500                    ##]
 501           ##| ##2: #hh2; #ll2; #H1; napply (or2_intro2 (h1 ≠ h2) («£hh1» ≠ (hh2§§ll2)) …);
 502                    nnormalize; #H2; napply (nelist_destruct_nil_cons T … H2)
 503           ##]
 504  ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
 505           ##[ ##1: #hh2; #H2; napply (or2_intro2 (h1 ≠ h2) ((hh1§§ll1) ≠ «£hh2») …);
 506                    nnormalize; #H3; napply (nelist_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 > (nelist_destruct_cons_cons_1 T … H4) in H2:(%); #H2;
 513                             nrewrite > (nelist_destruct_cons_cons_2 T … H4) in H2:(%); #H2;
 514                             napply (H2 (refl_eq …))
 515                    ##]
 516           ##]
 517  ##]
 518 nqed.
 519
 520 nlemma neq_to_nbfoldrightnelist2
 521  : ∀T:Type.∀f:T → T → bool.∀l1,l2:ne_list T.
 522    (∀x,y:T.decidable (x = y)) →
 523    (∀x,y.(x ≠ y → f x y = false)) →
 524    (l1 ≠ l2 → bfold_right_neList2 T f l1 l2 = false).
 525  #T; #f; #l1;
 526  nelim l1;
 527  ##[ ##1: #hh1; #l2; ncases l2;
 528           ##[ ##1: #hh2; #H; #H1; nnormalize; #H2; napply (H1 hh1 hh2 ?);
 529                    nnormalize; #H3; nrewrite > H3 in H2:(%); #H2; napply (H2 (refl_eq …))
 530           ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; #H2; napply refl_eq
 531           ##]
 532  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
 533           ##[ ##1: #hh2; #H1; #H2; nnormalize; #H3; napply refl_eq
 534           ##| ##2: #hh2; #ll2; #H1; #H2; #H3;
 535                    nchange with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = false);
 536                    napply (or2_elim (hh1 ≠ hh2) (ll1 ≠ ll2) ? (nelist_destruct T H1 … H3) …);
 537                    ##[ ##1: #H4; nrewrite > (H2 hh1 hh2 H4); nnormalize; napply refl_eq
 538                    ##| ##2: #H4; nrewrite > (H ll2 H1 H2 H4);
 539                             nrewrite > (symmetric_andbool (f hh1 hh2) false);
 540                             nnormalize; napply refl_eq
 541                    ##]
 542           ##]
 543  ##]
 544 nqed.