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