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 (* ************** *)
 145 (* NON-EMPTY LIST *)
 146 (* ************** *)
 147
 148 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.
 149  #T; #l1;
 150  nelim l1;
 151  ##[ ##1: #h; #l2; ncases l2; nnormalize;
 152           ##[ ##1: #H; #H1; napply refl_eq
 153           ##| ##2: #h; #t; #H; nrewrite > H; napply refl_eq
 154           ##]
 155  ##| ##2: #h; #l2; ncases l2; nnormalize;
 156           ##[ ##1: #h1; #H; #l; #H1; nrewrite < H1; napply refl_eq
 157           ##| ##2: #h; #l; #H; #l3; #H1; nrewrite < H1; napply refl_eq
 158           ##]
 159  ##]
 160 nqed.
 161
 162 nlemma symmetric_foldrightnelist2_aux
 163  : ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.∀acc:T2.∀l1,l2:ne_list T1.
 164    ∀H1:len_neList T1 l1 = len_neList T1 l2.∀H2:len_neList T1 l2 = len_neList T1 l1.
 165   (∀x,y,z.f x y z = f y x z) →
 166   fold_right_neList2 T1 T2 f acc l1 l2 H1 = fold_right_neList2 T1 T2 f acc l2 l1 H2.
 167  #T1; #T2; #f; #acc; #l1;
 168  nelim l1;
 169  ##[ ##1: #h; #l2; ncases l2;
 170           ##[ ##1: #h1; nnormalize; #H1; #H2; #H3; nrewrite > (H3 h h1 acc); napply refl_eq
 171           ##| ##2: #h1; #l; ncases l;
 172                    ##[ ##1: #h3; #H1; #H2; #H3;
 173                             nchange in H1:(%) with ((S O) = (S (S O)));
 174                             nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))
 175                    ##| ##2: #h3; #l3; #H1; #H2; #H3;
 176                             nchange in H1:(%) with ((S O) = (S (S (len_neList ? l3))));
 177                             nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))
 178                    ##]
 179           ##]
 180  ##| ##2: #h3; #l3; #H; #l2; ncases l2;
 181           ##[ ##1: #h4; ncases l3;
 182                    ##[ ##1: #h5; #H1; #H2; #H3;
 183                             nchange in H1:(%) with ((S (S O)) = (S O));
 184                             nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H1))
 185                    ##| ##2: #h5; #l5; #H1; #H2; #H3;
 186                             nchange in H1:(%) with ((S (S (len_neList ? l5))) = (S O));
 187                             nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H1))
 188                    ##]
 189           ##| ##2: #h4; #l4; #H1; #H2; #H3;
 190                    nchange in H1:(%) with ((S (len_neList ? l3)) = (S (len_neList ? l4)));
 191                    nchange in H2:(%) with ((S (len_neList ? l4)) = (S (len_neList ? l3)));
 192                    nchange with ((f h3 h4 (fold_right_neList2 T1 T2 f acc l3 l4 (fold_right_neList2_aux3 T1 h3 h4 l3 l4 ?))) =
 193                                  (f h4 h3 (fold_right_neList2 T1 T2 f acc l4 l3 (fold_right_neList2_aux3 T1 h4 h3 l4 l3 ?))));
 194                    nrewrite < (H l4 (fold_right_neList2_aux3 T1 h3 h4 l3 l4 H1) (fold_right_neList2_aux3 T1 h4 h3 l4 l3 H2) H3);
 195                    nrewrite > (H3 h3 h4 (fold_right_neList2 T1 T2 f acc l3 l4 ?));
 196                    napply refl_eq
 197           ##]
 198  ##]
 199 nqed.
 200
 201 nlemma symmetric_foldrightnelist2
 202  : ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.∀acc:T2.∀l1,l2:ne_list T1.∀H:len_neList T1 l1 = len_neList T1 l2.
 203   (∀x,y,z.f x y z = f y x z) →
 204   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).
 205  #T1; #T2; #f; #acc; #l1; #l2; #H; #H1;
 206  nrewrite > (symmetric_foldrightnelist2_aux T1 T2 f acc l1 l2 H (symmetric_lennelist T1 l1 l2 H) H1);
 207  napply refl_eq.
 208 nqed.
 209
 210 nlemma symmetric_bfoldrightnelist2
 211  : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1.
 212   (∀x,y.f x y = f y x) →
 213   bfold_right_neList2 T1 f l1 l2 = bfold_right_neList2 T1 f l2 l1.
 214  #T; #f; #l1;
 215  nelim l1;
 216  ##[ ##1: #hh1; #l2; ncases l2;
 217           ##[ ##1: #hh2; #H; nnormalize; nrewrite > (H hh1 hh2); napply refl_eq
 218           ##| ##2: #hh2; #ll2; #H; nnormalize; napply refl_eq
 219           ##]
 220  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
 221           ##[ ##1: #hh2; #H1; nnormalize; napply refl_eq
 222           ##| ##2: #hh2; #ll2; #H1; nnormalize;
 223                    nrewrite > (H ll2 H1);
 224                    nrewrite > (H1 hh1 hh2);
 225                    napply refl_eq
 226           ##]
 227  ##]
 228 nqed.
 229
 230 nlemma bfoldrightnelist2_to_eq
 231  : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1.
 232    (∀x,y.(f x y = true → x = y)) →
 233    (bfold_right_neList2 T1 f l1 l2 = true → l1 = l2).
 234  #T; #f; #l1;
 235  nelim l1;
 236  ##[ ##1: #hh1; #l2; ncases l2;
 237           ##[ ##1: #hh2; #H; #H1; nnormalize in H1:(%); nrewrite > (H hh1 hh2 H1); napply refl_eq
 238           ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; napply (bool_destruct … H1)
 239           ##]
 240  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
 241           ##[ ##1: #hh2; #H1; nnormalize; #H2; napply (bool_destruct … H2)
 242           ##| ##2: #hh2; #ll2; #H1; #H2;
 243                    nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = true);
 244                    nrewrite > (H1 hh1 hh2 (andb_true_true_l … H2));
 245                    nrewrite > (H ll2 H1 (andb_true_true_r … H2));
 246                    napply refl_eq
 247           ##]
 248  ##]
 249 nqed.
 250
 251 nlemma eq_to_bfoldrightnelist2
 252  : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1.
 253    (∀x,y.(x = y → f x y = true)) →
 254    (l1 = l2 → bfold_right_neList2 T1 f l1 l2 = true).
 255  #T; #f; #l1;
 256  nelim l1;
 257  ##[ ##1: #hh1; #l2; ncases l2;
 258           ##[ ##1: #hh2; #H; #H1; nnormalize;
 259                    nrewrite > (H hh1 hh2 (nelist_destruct_nil_nil … H1));
 260                    napply refl_eq
 261           ##| ##2: #hh2; #ll2; #H; #H1; nelim (nelist_destruct_nil_cons ???? H1)
 262           ##]
 263  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
 264           ##[ ##1: #hh2; #H1; #H2; nelim (nelist_destruct_cons_nil ???? H2)
 265           ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize;
 266                    nrewrite > (nelist_destruct_cons_cons_1 … H2);
 267                    nrewrite > (H1 hh2 hh2 (refl_eq …));
 268                    nnormalize;
 269                    nrewrite > (H ll2 H1 (nelist_destruct_cons_cons_2 … H2));
 270                    napply refl_eq
 271           ##]
 272  ##]
 273 nqed.
 274
 275 nlemma isbemptylist_to_isemptylist : ∀T,l.isb_empty_list T l = true → is_empty_list T l.
 276  #T; #l;
 277  ncases l;
 278  nnormalize;
 279  ##[ ##1: #H; napply I
 280  ##| ##2: #x; #l; #H; napply (bool_destruct … H)
 281  ##]
 282 nqed.
 283
 284 nlemma isnotbemptylist_to_isnotemptylist : ∀T,l.isnotb_empty_list T l = true → isnot_empty_list T l.
 285  #T; #l;
 286  ncases l;
 287  nnormalize;
 288  ##[ ##1: #H; napply (bool_destruct … H)
 289  ##| ##2: #x; #l; #H; napply I
 290  ##]
 291 nqed.