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 eq_to_eqnat : ∀n1,n2:nat.n1 = n2 → eq_nat n1 n2 = true.
  55  #n1;
  56  nelim n1;
  57  ##[ ##1: #n2;
  58           nelim n2;
  59           nnormalize;
  60           ##[ ##1: #H; napply refl_eq
  61           ##| ##2: #n3; #H; #H1; nelim (nat_destruct_0_S ? H1)
  62           ##]
  63  ##| ##2: #n2; #H; #n3; #H1;
  64           ncases n3 in H1:(%) ⊢ %;
  65           nnormalize;
  66           ##[ ##1: #H1; nelim (nat_destruct_S_0 ? H1)
  67           ##| ##2: #n4; #H1;
  68                    napply (H n4 (nat_destruct_S_S … H1))
  69           ##]
  70  ##]
  71 nqed.
  72
  73 nlemma neqnat_to_neq : ∀n1,n2:nat.(eq_nat n1 n2 = false → n1 ≠ n2).
  74  #n1; #n2; #H;
  75  napply (not_to_not (n1 = n2) (eq_nat n1 n2 = true) …);
  76  ##[ ##1: napply (eq_to_eqnat n1 n2)
  77  ##| ##2: napply (eqfalse_to_neqtrue … H)
  78  ##]
  79 nqed.
  80
  81 nlemma eqnat_to_eq : ∀n1,n2:nat.(eq_nat n1 n2 = true → n1 = n2).
  82  #n1;
  83  nelim n1;
  84  ##[ ##1: #n2;
  85           nelim n2;
  86           nnormalize;
  87           ##[ ##1: #H; napply refl_eq
  88           ##| ##2: #n3; #H; #H1; napply (bool_destruct … (O = S n3) H1)
  89           ##]
  90  ##| ##2: #n2; #H; #n3; #H1;
  91           ncases n3 in H1:(%) ⊢ %;
  92           nnormalize;
  93           ##[ ##1: #H1; napply (bool_destruct … (S n2 = O) H1)
  94           ##| ##2: #n4; #H1;
  95                    nrewrite > (H n4 H1);
  96                    napply refl_eq
  97           ##]
  98  ##]
  99 nqed.
 100
 101 nlemma neq_to_neqnat : ∀n1,n2:nat.n1 ≠ n2 → eq_nat n1 n2 = false.
 102  #n1; #n2; #H;
 103  napply (neqtrue_to_eqfalse (eq_nat n1 n2));
 104  napply (not_to_not (eq_nat n1 n2 = true) (n1 = n2) ? H);
 105  napply (eqnat_to_eq n1 n2).
 106 nqed.
 107
 108 nlemma decidable_nat : ∀x,y:nat.decidable (x = y).
 109  #x; #y; nnormalize;
 110  napply (or2_elim (eq_nat x y = true) (eq_nat x y = false) ? (decidable_bexpr ?));
 111  ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqnat_to_eq … H))
 112  ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqnat_to_neq … H))
 113  ##]
 114 nqed.
 115
 116 nlemma symmetric_eqnat : symmetricT nat bool eq_nat.
 117  #n1; #n2;
 118  napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_nat n1 n2));
 119  ##[ ##1: #H; nrewrite > H; napply refl_eq
 120  ##| ##2: #H; nrewrite > (neq_to_neqnat n1 n2 H);
 121           napply (symmetric_eq ? (eq_nat n2 n1) false);
 122           napply (neq_to_neqnat n2 n1 (symmetric_neq ? n1 n2 H))
 123  ##]
 124 nqed.
 125
 126 nlemma Sn_p_n_to_S_npn : ∀n1,n2.(S n1) + n2 = S (n1 + n2).
 127  #n1;
 128  nelim n1;
 129  ##[ ##1: nnormalize; #n2; napply refl_eq
 130  ##| ##2: #n; #H; #n2; nrewrite > (H n2);
 131           ncases n in H:(%) ⊢ %;
 132           ##[ ##1: nnormalize; #H; napply refl_eq
 133           ##| ##2: #n3; nnormalize; #H; napply refl_eq
 134           ##]
 135  ##]
 136 nqed.
 137
 138 nlemma n_p_Sn_to_S_npn : ∀n1,n2.n1 + (S n2) = S (n1 + n2).
 139  #n1;
 140  nelim n1;
 141  ##[ ##1: nnormalize; #n2; napply refl_eq
 142  ##| ##2: #n; #H; #n2;
 143           nrewrite > (Sn_p_n_to_S_npn n (S n2));
 144           nrewrite > (H n2);
 145           napply refl_eq
 146  ##]
 147 nqed.
 148
 149 nlemma Opn_to_n : ∀n.O + n = n.
 150  #n; nnormalize; napply refl_eq.
 151 nqed.
 152
 153 nlemma npO_to_n : ∀n.n + O = n.
 154  #n;
 155  nelim n;
 156  ##[ ##1: nnormalize; napply refl_eq
 157  ##| ##2: #n1; #H;
 158           nrewrite > (Sn_p_n_to_S_npn n1 O);
 159           nrewrite > H;
 160           napply refl_eq
 161  ##]
 162 nqed.
 163
 164 nlemma symmetric_plusnat : symmetricT nat nat plus.
 165  #n1;
 166  nelim n1;
 167  ##[ ##1: #n2; nrewrite > (npO_to_n n2); nnormalize; napply refl_eq
 168  ##| ##2: #n2; #H; #n3;
 169           nrewrite > (Sn_p_n_to_S_npn n2 n3);
 170           nrewrite > (n_p_Sn_to_S_npn n3 n2);
 171           nrewrite > (H n3);
 172           napply refl_eq
 173  ##]
 174 nqed.