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: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
  19 (*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
  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 Sn_p_n_to_S_npn : ∀n1,n2.(S n1) + n2 = S (n1 + n2).
 114  #n1;
 115  nelim n1;
 116  ##[ ##1: nnormalize; #n2; napply refl_eq
 117  ##| ##2: #n; #H; #n2; nrewrite > (H n2);
 118           ncases n in H:(%) ⊢ %;
 119           ##[ ##1: nnormalize; #H; napply refl_eq
 120           ##| ##2: #n3; nnormalize; #H; napply refl_eq
 121           ##]
 122  ##]
 123 nqed.
 124
 125 nlemma n_p_Sn_to_S_npn : ∀n1,n2.n1 + (S n2) = S (n1 + n2).
 126  #n1;
 127  nelim n1;
 128  ##[ ##1: nnormalize; #n2; napply refl_eq
 129  ##| ##2: #n; #H; #n2;
 130           nrewrite > (Sn_p_n_to_S_npn n (S n2));
 131           nrewrite > (H n2);
 132           napply refl_eq
 133  ##]
 134 nqed.
 135
 136 nlemma Opn_to_n : ∀n.O + n = n.
 137  #n; nnormalize; napply refl_eq.
 138 nqed.
 139
 140 nlemma npO_to_n : ∀n.n + O = n.
 141  #n;
 142  nelim n;
 143  ##[ ##1: nnormalize; napply refl_eq
 144  ##| ##2: #n1; #H;
 145           nrewrite > (Sn_p_n_to_S_npn n1 O);
 146           nrewrite > H;
 147           napply refl_eq
 148  ##]
 149 nqed.
 150
 151 nlemma symmetric_plusnat : symmetricT nat nat plus.
 152  #n1;
 153  nelim n1;
 154  ##[ ##1: #n2; nrewrite > (npO_to_n n2); nnormalize; napply refl_eq
 155  ##| ##2: #n2; #H; #n3;
 156           nrewrite > (Sn_p_n_to_S_npn n2 n3);
 157           nrewrite > (n_p_Sn_to_S_npn n3 n2);
 158           nrewrite > (H n3);
 159           napply refl_eq
 160  ##]
 161 nqed.