helm/software/matita/contribs/ng_assembly/utility/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: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
  19 (*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "utility/utility.ma".
  24
  25 (* ************ *)
  26 (* List Utility *)
  27 (* ************ *)
  28
  29 nlemma nelist_destruct_nil_nil : ∀T.∀x1,x2:T.ne_nil T x1 = ne_nil T x2 → x1 = x2.
  30  #T; #x1; #x2; #H;
  31  nchange with (match ne_nil T x2 with [ ne_cons _ _ ⇒ False | ne_nil a ⇒ x1 = a ]);
  32  nrewrite < H;
  33  nnormalize;
  34  napply refl_eq.
  35 nqed.
  36
  37 nlemma nelist_destruct_cons_cons_1 : ∀T.∀x1,x2:T.∀y1,y2:ne_list T.ne_cons T x1 y1 = ne_cons T x2 y2 → x1 = x2.
  38  #T; #x1; #x2; #y1; #y2; #H;
  39  nchange with (match ne_cons T x2 y2 with [ ne_nil _ ⇒ False | ne_cons a _ ⇒ x1 = a ]);
  40  nrewrite < H;
  41  nnormalize;
  42  napply refl_eq.
  43 nqed.
  44
  45 nlemma nelist_destruct_cons_cons_2 : ∀T.∀x1,x2:T.∀y1,y2:ne_list T.ne_cons T x1 y1 = ne_cons T x2 y2 → y1 = y2.
  46  #T; #x1; #x2; #y1; #y2; #H;
  47  nchange with (match ne_cons T x2 y2 with [ ne_nil _ ⇒ False | ne_cons _ b ⇒ y1 = b ]);
  48  nrewrite < H;
  49  nnormalize;
  50  napply refl_eq.
  51 nqed.
  52
  53 nlemma nelist_destruct_cons_nil : ∀T.∀x1,x2:T.∀y1:ne_list T.ne_cons T x1 y1 = ne_nil T x2 → False.
  54  #T; #x1; #x2; #y1; #H;
  55  nchange with (match ne_cons T x1 y1 with [ ne_nil _ ⇒ True | ne_cons a b ⇒ False ]);
  56  nrewrite > H;
  57  nnormalize;
  58  napply I.
  59 nqed.
  60
  61 nlemma nelist_destruct_nil_cons : ∀T.∀x1,x2:T.∀y2:ne_list T.ne_nil T x1 = ne_cons T x2 y2 → False.
  62  #T; #x1; #x2; #y2; #H;
  63  nchange with (match ne_cons T x2 y2 with [ ne_nil _ ⇒ True | ne_cons a b ⇒ False ]);
  64  nrewrite < H;
  65  nnormalize;
  66  napply I.
  67 nqed.
  68
  69 nlemma symmetric_eqlenlist : ∀T.∀l1,l2:list T.len_list T l1 = len_list T l2 → len_list T l2 = len_list T l1.
  70  #T; #l1;
  71  nelim l1;
  72  ##[ ##1: #l2; ncases l2; nnormalize;
  73           ##[ ##1: #H; napply refl_eq
  74           ##| ##2: #h; #t; #H; nelim (nat_destruct_0_S ? H)
  75           ##]
  76  ##| ##2: #h; #l2; ncases l2; nnormalize;
  77           ##[ ##1: #H; #l; #H1; nrewrite < H1; napply refl_eq
  78           ##| ##2: #h; #l; #H; #l3; #H1; nrewrite < H1; napply refl_eq
  79           ##]
  80  ##]
  81 nqed.
  82
  83 nlemma symmetric_foldrightlist2_aux
  84  : ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.∀acc:T2.∀l1,l2:list T1.
  85    ∀H1:len_list T1 l1 = len_list T1 l2.∀H2:len_list T1 l2 = len_list T1 l1.
  86   (∀x,y,z.f x y z = f y x z) →
  87   fold_right_list2 T1 T2 f acc l1 l2 H1 = fold_right_list2 T1 T2 f acc l2 l1 H2.
  88  #T1; #T2; #f; #acc; #l1;
  89  nelim l1;
  90  ##[ ##1: #l2; ncases l2;
  91           ##[ ##1: nnormalize; #H1; #H2; #H3; napply refl_eq
  92           ##| ##2: #h; #l; #H1; #H2; #H3;
  93                    nchange in H1:(%) with (O = (S (len_list ? l)));
  94                    nelim (nat_destruct_0_S ? H1)
  95           ##]
  96  ##| ##2: #h3; #l3; #H; #l2; ncases l2;
  97           ##[ ##1: #H1; #H2; #H3; nchange in H1:(%) with ((S (len_list ? l3)) = O);
  98                    nelim (nat_destruct_S_0 ? H1)
  99           ##| ##2: #h4; #l4; #H1; #H2; #H3;
 100                    nchange in H1:(%) with ((S (len_list ? l3)) = (S (len_list ? l4)));
 101                    nchange in H2:(%) with ((S (len_list ? l4)) = (S (len_list ? l3)));
 102                    nchange with ((f h3 h4 (fold_right_list2 T1 T2 f acc l3 l4 (fold_right_list2_aux3 T1 h3 h4 l3 l4 ?))) =
 103                                  (f h4 h3 (fold_right_list2 T1 T2 f acc l4 l3 (fold_right_list2_aux3 T1 h4 h3 l4 l3 ?))));
 104                    nrewrite < (H l4 (fold_right_list2_aux3 T1 h3 h4 l3 l4 H1) (fold_right_list2_aux3 T1 h4 h3 l4 l3 H2) H3);
 105                    nrewrite > (H3 h3 h4 (fold_right_list2 T1 T2 f acc l3 l4 ?));
 106                    napply refl_eq
 107           ##]
 108  ##]
 109 nqed.
 110
 111 nlemma symmetric_foldrightlist2
 112  : ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.∀acc:T2.∀l1,l2:list T1.∀H:len_list T1 l1 = len_list T1 l2.
 113   (∀x,y,z.f x y z = f y x z) →
 114   fold_right_list2 T1 T2 f acc l1 l2 H = fold_right_list2 T1 T2 f acc l2 l1 (symmetric_eqlenlist T1 l1 l2 H).
 115  #T1; #T2; #f; #acc; #l1; #l2; #H; #H1;
 116  nrewrite > (symmetric_foldrightlist2_aux T1 T2 f acc l1 l2 H (symmetric_eqlenlist T1 l1 l2 H) H1);
 117  napply refl_eq.
 118 nqed.
 119
 120 nlemma symmetric_bfoldrightlist2
 121  : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:list T1.
 122   (∀x,y.f x y = f y x) →
 123   bfold_right_list2 T1 f l1 l2 = bfold_right_list2 T1 f l2 l1.
 124  #T; #f; #l1;
 125  nelim l1;
 126  ##[ ##1: #l2; ncases l2;
 127           ##[ ##1: #H; nnormalize; napply refl_eq
 128           ##| ##2: #hh2; #ll2; #H; nnormalize; napply refl_eq
 129           ##]
 130  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
 131           ##[ ##1: #H1; nnormalize; napply refl_eq
 132           ##| ##2: #hh2; #ll2; #H1; nnormalize;
 133                    nrewrite > (H ll2 H1);
 134                    nrewrite > (H1 hh1 hh2);
 135                    napply refl_eq
 136           ##]
 137  ##]
 138 nqed.
 139
 140 nlemma bfoldrightlist2_to_eq
 141  : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:list T1.
 142    (∀x,y.(f x y = true → x = y)) →
 143    (bfold_right_list2 T1 f l1 l2 = true → l1 = l2).
 144  #T; #f; #l1;
 145  nelim l1;
 146  ##[ ##1: #l2; ncases l2;
 147           ##[ ##1: #H; #H1; napply refl_eq
 148           ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; napply (bool_destruct … H1)
 149           ##]
 150  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
 151           ##[ ##1: #H1; nnormalize; #H2; napply (bool_destruct … H2)
 152           ##| ##2: #hh2; #ll2; #H1; #H2;
 153                    nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_list2 T f ll1 ll2)) = true);
 154                    nrewrite > (H1 hh1 hh2 (andb_true_true_l … H2));
 155                    nrewrite > (H ll2 H1 (andb_true_true_r … H2));
 156                    napply refl_eq
 157           ##]
 158  ##]
 159 nqed.
 160
 161 nlemma eq_to_bfoldrightlist2
 162  : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:list T1.
 163    (∀x,y.(x = y → f x y = true)) →
 164    (l1 = l2 → bfold_right_list2 T1 f l1 l2 = true).
 165  #T; #f; #l1;
 166  nelim l1;
 167  ##[ ##1: #l2; ncases l2;
 168           ##[ ##1: #H; #H1; nnormalize; napply refl_eq
 169           ##| ##2: #hh2; #ll2; #H; #H1; nelim (list_destruct_nil_cons ??? H1)
 170           ##]
 171  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
 172           ##[ ##1: #H1; #H2; nelim (list_destruct_cons_nil ??? H2)
 173           ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize;
 174                    nrewrite > (list_destruct_1 … H2);
 175                    nrewrite > (H1 hh2 hh2 (refl_eq …));
 176                    nnormalize;
 177                    nrewrite > (H ll2 H1 (list_destruct_2 … H2));
 178                    napply refl_eq
 179           ##]
 180  ##]
 181 nqed.
 182
 183 nlemma symmetric_eqlennelist : ∀T.∀l1,l2:ne_list T.len_neList T l1 = len_neList T l2 → len_neList T l2 = len_neList T l1.
 184  #T; #l1;
 185  nelim l1;
 186  ##[ ##1: #h; #l2; ncases l2; nnormalize;
 187           ##[ ##1: #H; #H1; napply refl_eq
 188           ##| ##2: #h; #t; #H; nrewrite > H; napply refl_eq
 189           ##]
 190  ##| ##2: #h; #l2; ncases l2; nnormalize;
 191           ##[ ##1: #h1; #H; #l; #H1; nrewrite < H1; napply refl_eq
 192           ##| ##2: #h; #l; #H; #l3; #H1; nrewrite < H1; napply refl_eq
 193           ##]
 194  ##]
 195 nqed.
 196
 197 nlemma symmetric_foldrightnelist2_aux
 198  : ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.∀acc:T2.∀l1,l2:ne_list T1.
 199    ∀H1:len_neList T1 l1 = len_neList T1 l2.∀H2:len_neList T1 l2 = len_neList T1 l1.
 200   (∀x,y,z.f x y z = f y x z) →
 201   fold_right_neList2 T1 T2 f acc l1 l2 H1 = fold_right_neList2 T1 T2 f acc l2 l1 H2.
 202  #T1; #T2; #f; #acc; #l1;
 203  nelim l1;
 204  ##[ ##1: #h; #l2; ncases l2;
 205           ##[ ##1: #h1; nnormalize; #H1; #H2; #H3; nrewrite > (H3 h h1 acc); napply refl_eq
 206           ##| ##2: #h1; #l; ncases l;
 207                    ##[ ##1: #h3; #H1; #H2; #H3;
 208                             nchange in H1:(%) with ((S O) = (S (S O)));
 209                             nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))
 210                    ##| ##2: #h3; #l3; #H1; #H2; #H3;
 211                             nchange in H1:(%) with ((S O) = (S (S (len_neList ? l3))));
 212                             nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))
 213                    ##]
 214           ##]
 215  ##| ##2: #h3; #l3; #H; #l2; ncases l2;
 216           ##[ ##1: #h4; ncases l3;
 217                    ##[ ##1: #h5; #H1; #H2; #H3;
 218                             nchange in H1:(%) with ((S (S O)) = (S O));
 219                             nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H1))
 220                    ##| ##2: #h5; #l5; #H1; #H2; #H3;
 221                             nchange in H1:(%) with ((S (S (len_neList ? l5))) = (S O));
 222                             nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H1))
 223                    ##]
 224           ##| ##2: #h4; #l4; #H1; #H2; #H3;
 225                    nchange in H1:(%) with ((S (len_neList ? l3)) = (S (len_neList ? l4)));
 226                    nchange in H2:(%) with ((S (len_neList ? l4)) = (S (len_neList ? l3)));
 227                    nchange with ((f h3 h4 (fold_right_neList2 T1 T2 f acc l3 l4 (fold_right_neList2_aux3 T1 h3 h4 l3 l4 ?))) =
 228                                  (f h4 h3 (fold_right_neList2 T1 T2 f acc l4 l3 (fold_right_neList2_aux3 T1 h4 h3 l4 l3 ?))));
 229                    nrewrite < (H l4 (fold_right_neList2_aux3 T1 h3 h4 l3 l4 H1) (fold_right_neList2_aux3 T1 h4 h3 l4 l3 H2) H3);
 230                    nrewrite > (H3 h3 h4 (fold_right_neList2 T1 T2 f acc l3 l4 ?));
 231                    napply refl_eq
 232           ##]
 233  ##]
 234 nqed.
 235
 236 nlemma symmetric_foldrightnelist2
 237  : ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.∀acc:T2.∀l1,l2:ne_list T1.∀H:len_neList T1 l1 = len_neList T1 l2.
 238   (∀x,y,z.f x y z = f y x z) →
 239   fold_right_neList2 T1 T2 f acc l1 l2 H = fold_right_neList2 T1 T2 f acc l2 l1 (symmetric_eqlennelist T1 l1 l2 H).
 240  #T1; #T2; #f; #acc; #l1; #l2; #H; #H1;
 241  nrewrite > (symmetric_foldrightnelist2_aux T1 T2 f acc l1 l2 H (symmetric_eqlennelist T1 l1 l2 H) H1);
 242  napply refl_eq.
 243 nqed.
 244
 245 nlemma symmetric_bfoldrightnelist2
 246  : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1.
 247   (∀x,y.f x y = f y x) →
 248   bfold_right_neList2 T1 f l1 l2 = bfold_right_neList2 T1 f l2 l1.
 249  #T; #f; #l1;
 250  nelim l1;
 251  ##[ ##1: #hh1; #l2; ncases l2;
 252           ##[ ##1: #hh2; #H; nnormalize; nrewrite > (H hh1 hh2); napply refl_eq
 253           ##| ##2: #hh2; #ll2; #H; nnormalize; napply refl_eq
 254           ##]
 255  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
 256           ##[ ##1: #hh2; #H1; nnormalize; napply refl_eq
 257           ##| ##2: #hh2; #ll2; #H1; nnormalize;
 258                    nrewrite > (H ll2 H1);
 259                    nrewrite > (H1 hh1 hh2);
 260                    napply refl_eq
 261           ##]
 262  ##]
 263 nqed.
 264
 265 nlemma bfoldrightnelist2_to_eq
 266  : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1.
 267    (∀x,y.(f x y = true → x = y)) →
 268    (bfold_right_neList2 T1 f l1 l2 = true → l1 = l2).
 269  #T; #f; #l1;
 270  nelim l1;
 271  ##[ ##1: #hh1; #l2; ncases l2;
 272           ##[ ##1: #hh2; #H; #H1; nnormalize in H1:(%); nrewrite > (H hh1 hh2 H1); napply refl_eq
 273           ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; napply (bool_destruct … H1)
 274           ##]
 275  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
 276           ##[ ##1: #hh2; #H1; nnormalize; #H2; napply (bool_destruct … H2)
 277           ##| ##2: #hh2; #ll2; #H1; #H2;
 278                    nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = true);
 279                    nrewrite > (H1 hh1 hh2 (andb_true_true_l … H2));
 280                    nrewrite > (H ll2 H1 (andb_true_true_r … H2));
 281                    napply refl_eq
 282           ##]
 283  ##]
 284 nqed.
 285
 286 nlemma eq_to_bfoldrightnelist2
 287  : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1.
 288    (∀x,y.(x = y → f x y = true)) →
 289    (l1 = l2 → bfold_right_neList2 T1 f l1 l2 = true).
 290  #T; #f; #l1;
 291  nelim l1;
 292  ##[ ##1: #hh1; #l2; ncases l2;
 293           ##[ ##1: #hh2; #H; #H1; nnormalize;
 294                    nrewrite > (H hh1 hh2 (nelist_destruct_nil_nil … H1));
 295                    napply refl_eq
 296           ##| ##2: #hh2; #ll2; #H; #H1; nelim (nelist_destruct_nil_cons ???? H1)
 297           ##]
 298  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
 299           ##[ ##1: #hh2; #H1; #H2; nelim (nelist_destruct_cons_nil ???? H2)
 300           ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize;
 301                    nrewrite > (nelist_destruct_cons_cons_1 … H2);
 302                    nrewrite > (H1 hh2 hh2 (refl_eq …));
 303                    nnormalize;
 304                    nrewrite > (H ll2 H1 (nelist_destruct_cons_cons_2 … H2));
 305                    napply refl_eq
 306           ##]
 307  ##]
 308 nqed.
 309
 310 nlemma isbemptylist_to_isemptylist : ∀T,l.isb_empty_list T l = true → is_empty_list T l.
 311  #T; #l;
 312  ncases l;
 313  nnormalize;
 314  ##[ ##1: #H; napply I
 315  ##| ##2: #x; #l; #H; napply (bool_destruct … H)
 316  ##]
 317 nqed.
 318
 319 nlemma isnotbemptylist_to_isnotemptylist : ∀T,l.isnotb_empty_list T l = true → isnot_empty_list T l.
 320  #T; #l;
 321  ncases l;
 322  nnormalize;
 323  ##[ ##1: #H; napply (bool_destruct … H)
 324  ##| ##2: #x; #l; #H; napply I
 325  ##]
 326 nqed.
 327
 328 (* ******** *)
 329 (* naturali *)
 330 (* ******** *)
 331
 332 nlemma iszerob_to_iszero : ∀n.isZerob n = true → isZero n.
 333  #n;
 334  ncases n;
 335  ##[ ##1: nnormalize; #H; napply I
 336  ##| ##2: #n1; nnormalize; #H; napply (bool_destruct … H)
 337  ##]
 338 nqed.