helm/software/matita/contribs/ng_assembly/common/nat_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/nat.ma".
  24 include "num/bool_lemmas.ma".
  25
  26 (* ******** *)
  27 (* NATURALI *)
  28 (* ******** *)
  29
  30 nlemma nat_destruct_S_S : ∀n1,n2:nat.S n1 = S n2 → n1 = n2.
  31  #n1; #n2; #H;
  32  nchange with (match S n2 with [ O ⇒ False | S a ⇒ n1 = a ]);
  33  nrewrite < H;
  34  nnormalize;
  35  napply refl_eq.
  36 nqed.
  37
  38 nlemma nat_destruct_0_S : ∀n:nat.O = S n → False.
  39  #n; #H;
  40  nchange with (match S n with [ O ⇒ True | S a ⇒ False ]);
  41  nrewrite < H;
  42  nnormalize;
  43  napply I.
  44 nqed.
  45
  46 nlemma nat_destruct_S_0 : ∀n:nat.S n = O → False.
  47  #n; #H;
  48  nchange with (match S n with [ O ⇒ True | S a ⇒ False ]);
  49  nrewrite > H;
  50  nnormalize;
  51  napply I.
  52 nqed.
  53
  54 nlemma symmetric_eqnat : symmetricT nat bool eq_nat.
  55  nnormalize;
  56  #n1;
  57  nelim n1;
  58  ##[ ##1: #n2;
  59           nelim n2;
  60           nnormalize;
  61           ##[ ##1: napply refl_eq
  62           ##| ##2: #n3; #H; napply refl_eq
  63           ##]
  64  ##| ##2: #n2; #H; #n3;
  65           nnormalize;
  66           ncases n3;
  67           nnormalize;
  68           ##[ ##1: napply refl_eq
  69           ##| ##2: #n4; napply (H n4)
  70           ##]
  71  ##]
  72 nqed.
  73
  74 nlemma eq_to_eqnat : ∀n1,n2:nat.n1 = n2 → eq_nat n1 n2 = true.
  75  #n1;
  76  nelim n1;
  77  ##[ ##1: #n2;
  78           nelim n2;
  79           nnormalize;
  80           ##[ ##1: #H; napply refl_eq
  81           ##| ##2: #n3; #H; #H1; nelim (nat_destruct_0_S ? H1)
  82           ##]
  83  ##| ##2: #n2; #H; #n3; #H1;
  84           ncases n3 in H1:(%) ⊢ %;
  85           nnormalize;
  86           ##[ ##1: #H1; nelim (nat_destruct_S_0 ? H1)
  87           ##| ##2: #n4; #H1;
  88                    napply (H n4 (nat_destruct_S_S … H1))
  89           ##]
  90  ##]
  91 nqed.
  92
  93 nlemma eqnat_to_eq : ∀n1,n2:nat.(eq_nat n1 n2 = true → n1 = n2).
  94  #n1;
  95  nelim n1;
  96  ##[ ##1: #n2;
  97           nelim n2;
  98           nnormalize;
  99           ##[ ##1: #H; napply refl_eq
 100           ##| ##2: #n3; #H; #H1; napply (bool_destruct … (O = S n3) H1)
 101           ##]
 102  ##| ##2: #n2; #H; #n3; #H1;
 103           ncases n3 in H1:(%) ⊢ %;
 104           nnormalize;
 105           ##[ ##1: #H1; napply (bool_destruct … (S n2 = O) H1)
 106           ##| ##2: #n4; #H1;
 107                    nrewrite > (H n4 H1);
 108                    napply refl_eq
 109           ##]
 110  ##]
 111 nqed.
 112
 113 nlemma decidable_nat : ∀x,y:nat.decidable (x = y).
 114  #x; nelim x; nnormalize;
 115  ##[ ##1: #y; ncases y;
 116           ##[ ##1: napply (or2_intro1 (O = O) (O ≠ O) (refl_eq …))
 117           ##| ##2: #n2; napply (or2_intro2 (O = (S n2)) (O ≠ (S n2)) ?);
 118                    nnormalize; #H; napply (nat_destruct_0_S n2 H)
 119           ##]
 120  ##| ##2: #n1; #H; #y; ncases y;
 121           ##[ ##1: napply (or2_intro2 ((S n1) = O) ((S n1) ≠ O) ?);
 122                    nnormalize; #H1; napply (nat_destruct_S_0 n1 H1)
 123           ##| ##2: #n2; napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (H n2) …);
 124                    ##[ ##1: #H1; napply (or2_intro1 (? = ?) (? ≠ ?) …);
 125                             nrewrite > H1; napply refl_eq
 126                    ##| ##2: #H1; napply (or2_intro2 (? = ?) (? ≠ ?) …);
 127                             nnormalize; #H2; napply (H1 (nat_destruct_S_S … H2))
 128                    ##]
 129           ##]
 130  ##]
 131 nqed.
 132
 133 nlemma neq_to_neqnat : ∀n1,n2:nat.n1 ≠ n2 → eq_nat n1 n2 = false.
 134  #n1; nelim n1;
 135  ##[ ##1: #n2; ncases n2;
 136           ##[ ##1: nnormalize; #H; nelim (H (refl_eq …))
 137           ##| ##2: #nn2; #H; nnormalize; napply refl_eq
 138           ##]
 139  ##| ##2: #nn1; #H; #n2; ncases n2;
 140           ##[ ##1: #H1; nnormalize; napply refl_eq
 141           ##| ##2: #nn2; nnormalize; #H1;
 142                    napply (H nn2 ?); nnormalize; #H2;
 143                    nrewrite > H2 in H1:(%); #H1;
 144                    napply (H1 (refl_eq …))
 145           ##]
 146  ##]
 147 nqed.
 148
 149 nlemma neqnat_to_neq : ∀n1,n2:nat.(eq_nat n1 n2 = false → n1 ≠ n2).
 150  #n1; nelim n1;
 151  ##[ ##1: #n2; ncases n2;
 152           ##[ ##1: nnormalize; #H; napply (bool_destruct … H)
 153           ##| ##2: #nn2; nnormalize; #H; #H1; nelim (nat_destruct_0_S … H1)
 154           ##]
 155  ##| ##2: #nn1; #H; #n2; ncases n2;
 156           ##[ ##1: nnormalize; #H1; #H2; nelim (nat_destruct_S_0 … H2)
 157           ##| ##2: #nn2; nnormalize; #H1; #H2; napply (H nn2 H1 ?);
 158                    napply (nat_destruct_S_S … H2)
 159           ##]
 160  ##]
 161 nqed.
 162
 163 nlemma Sn_p_n_to_S_npn : ∀n1,n2.(S n1) + n2 = S (n1 + n2).
 164  #n1;
 165  nelim n1;
 166  ##[ ##1: nnormalize; #n2; napply refl_eq
 167  ##| ##2: #n; #H; #n2; nrewrite > (H n2);
 168           ncases n in H:(%) ⊢ %;
 169           ##[ ##1: nnormalize; #H; napply refl_eq
 170           ##| ##2: #n3; nnormalize; #H; napply refl_eq
 171           ##]
 172  ##]
 173 nqed.
 174
 175 nlemma n_p_Sn_to_S_npn : ∀n1,n2.n1 + (S n2) = S (n1 + n2).
 176  #n1;
 177  nelim n1;
 178  ##[ ##1: nnormalize; #n2; napply refl_eq
 179  ##| ##2: #n; #H; #n2;
 180           nrewrite > (Sn_p_n_to_S_npn n (S n2));
 181           nrewrite > (H n2);
 182           napply refl_eq
 183  ##]
 184 nqed.
 185
 186 nlemma Opn_to_n : ∀n.O + n = n.
 187  #n; nnormalize; napply refl_eq.
 188 nqed.
 189
 190 nlemma npO_to_n : ∀n.n + O = n.
 191  #n;
 192  nelim n;
 193  ##[ ##1: nnormalize; napply refl_eq
 194  ##| ##2: #n1; #H;
 195           nrewrite > (Sn_p_n_to_S_npn n1 O);
 196           nrewrite > H;
 197           napply refl_eq
 198  ##]
 199 nqed.
 200
 201 nlemma symmetric_plusnat : symmetricT nat nat plus.
 202  #n1;
 203  nelim n1;
 204  ##[ ##1: #n2; nrewrite > (npO_to_n n2); nnormalize; napply refl_eq
 205  ##| ##2: #n2; #H; #n3;
 206           nrewrite > (Sn_p_n_to_S_npn n2 n3);
 207           nrewrite > (n_p_Sn_to_S_npn n3 n2);
 208           nrewrite > (H n3);
 209           napply refl_eq
 210  ##]
 211 nqed.