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  napply (list_ind ???? 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  napply (list_ind ???? 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_eqlennelist : ∀T.∀l1,l2:ne_list T.len_neList T l1 = len_neList T l2 → len_neList T l2 = len_neList T l1.
 121  #T; #l1;
 122  napply (ne_list_ind ???? l1);
 123  ##[ ##1: #h; #l2; ncases l2; nnormalize;
 124           ##[ ##1: #H; #H1; napply (refl_eq ??)
 125           ##| ##2: #h; #t; #H; nrewrite > H; napply (refl_eq ??)
 126           ##]
 127  ##| ##2: #h; #l2; ncases l2; nnormalize;
 128           ##[ ##1: #h1; #H; #l; #H1; nrewrite < H1; napply (refl_eq ??)
 129           ##| ##2: #h; #l; #H; #l3; #H1; nrewrite < H1; napply (refl_eq ??)
 130           ##]
 131  ##]
 132 nqed.
 133
 134 nlemma symmetric_foldrightnelist2_aux
 135  : ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.∀acc:T2.∀l1,l2:ne_list T1.
 136    ∀H1:len_neList T1 l1 = len_neList T1 l2.∀H2:len_neList T1 l2 = len_neList T1 l1.
 137   (∀x,y,z.f x y z = f y x z) →
 138   fold_right_neList2 T1 T2 f acc l1 l2 H1 = fold_right_neList2 T1 T2 f acc l2 l1 H2.
 139  #T1; #T2; #f; #acc; #l1;
 140  napply (ne_list_ind ???? l1);
 141  ##[ ##1: #h; #l2; ncases l2;
 142           ##[ ##1: #h1; nnormalize; #H1; #H2; #H3; nrewrite > (H3 h h1 acc); napply (refl_eq ??)
 143           ##| ##2: #h1; #l; ncases l;
 144                    ##[ ##1: #h3; #H1; #H2; #H3;
 145                             nchange in H1:(%) with ((S O) = (S (S O)));
 146                             nelim (nat_destruct_0_S ? (nat_destruct_S_S ?? H1))
 147                    ##| ##2: #h3; #l3; #H1; #H2; #H3;
 148                             nchange in H1:(%) with ((S O) = (S (S (len_neList ? l3))));
 149                             nelim (nat_destruct_0_S ? (nat_destruct_S_S ?? H1))
 150                    ##]
 151           ##]
 152  ##| ##2: #h3; #l3; #H; #l2; ncases l2;
 153           ##[ ##1: #h4; ncases l3;
 154                    ##[ ##1: #h5; #H1; #H2; #H3;
 155                             nchange in H1:(%) with ((S (S O)) = (S O));
 156                             nelim (nat_destruct_S_0 ? (nat_destruct_S_S ?? H1))
 157                    ##| ##2: #h5; #l5; #H1; #H2; #H3;
 158                             nchange in H1:(%) with ((S (S (len_neList ? l5))) = (S O));
 159                             nelim (nat_destruct_S_0 ? (nat_destruct_S_S ?? H1))
 160                    ##]
 161           ##| ##2: #h4; #l4; #H1; #H2; #H3;
 162                    nchange in H1:(%) with ((S (len_neList ? l3)) = (S (len_neList ? l4)));
 163                    nchange in H2:(%) with ((S (len_neList ? l4)) = (S (len_neList ? l3)));
 164                    nchange with ((f h3 h4 (fold_right_neList2 T1 T2 f acc l3 l4 (fold_right_neList2_aux3 T1 h3 h4 l3 l4 ?))) =
 165                                  (f h4 h3 (fold_right_neList2 T1 T2 f acc l4 l3 (fold_right_neList2_aux3 T1 h4 h3 l4 l3 ?))));
 166                    nrewrite < (H l4 (fold_right_neList2_aux3 T1 h3 h4 l3 l4 H1) (fold_right_neList2_aux3 T1 h4 h3 l4 l3 H2) H3);
 167                    nrewrite > (H3 h3 h4 (fold_right_neList2 T1 T2 f acc l3 l4 ?));
 168                    napply (refl_eq ??)
 169           ##]
 170  ##]
 171 nqed.
 172
 173 nlemma symmetric_foldrightnelist2
 174  : ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.∀acc:T2.∀l1,l2:ne_list T1.∀H:len_neList T1 l1 = len_neList T1 l2.
 175   (∀x,y,z.f x y z = f y x z) →
 176   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).
 177  #T1; #T2; #f; #acc; #l1; #l2; #H; #H1;
 178  nrewrite > (symmetric_foldrightnelist2_aux T1 T2 f acc l1 l2 H (symmetric_eqlennelist T1 l1 l2 H) H1);
 179  napply (refl_eq ??).
 180 nqed.
 181
 182 nlemma isbemptylist_to_isemptylist : ∀T,l.isb_empty_list T l = true → is_empty_list T l.
 183  #T; #l;
 184  ncases l;
 185  nnormalize;
 186  ##[ ##1: #H; napply I
 187  ##| ##2: #x; #l; #H; napply (bool_destruct ??? H)
 188  ##]
 189 nqed.
 190
 191 nlemma isnotbemptylist_to_isnotemptylist : ∀T,l.isnotb_empty_list T l = true → isnot_empty_list T l.
 192  #T; #l;
 193  ncases l;
 194  nnormalize;
 195  ##[ ##1: #H; napply (bool_destruct ??? H)
 196  ##| ##2: #x; #l; #H; napply I
 197  ##]
 198 nqed.
 199
 200 (* ******** *)
 201 (* naturali *)
 202 (* ******** *)
 203
 204 nlemma iszerob_to_iszero : ∀n.isZerob n = true → isZero n.
 205  #n;
 206  ncases n;
 207  ##[ ##1: nnormalize; #H; napply I
 208  ##| ##2: #n1; nnormalize; #H; napply (bool_destruct ??? H)
 209  ##]
 210 nqed.