helm/software/matita/nlibrary/arithmetics/nat.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* include "higher_order_defs/functions.ma". *)
  16 include "hints_declaration.ma".
  17 include "basics/functions.ma".
  18 include "basics/eq.ma".
  19
  20 ninductive nat : Type[0] ≝
  21   | O : nat
  22   | S : nat → nat.
  23
  24 interpretation "Natural numbers" 'N = nat.
  25
  26 alias num (instance 0) = "nnatural number".
  27
  28 (*
  29 nrecord pos : Type ≝
  30  {n:>nat; is_pos: n ≠ 0}.
  31
  32 ncoercion nat_to_pos: ∀n:nat. n ≠0 →pos ≝ mk_pos on
  33 *)
  34
  35 (* default "natural numbers" cic:/matita/ng/arithmetics/nat/nat.ind.
  36 *)
  37
  38 ndefinition pred ≝
  39  λn. match n with
  40  [ O ⇒  O
  41  | (S p) ⇒ p].
  42
  43 ntheorem pred_Sn : ∀n. n = pred (S n).
  44 //. nqed.
  45
  46 ntheorem injective_S : injective nat nat S.
  47 //; nqed.
  48
  49 (*
  50 ntheorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m.
  51 //. nqed. *)
  52
  53 ntheorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m.
  54 /2/; nqed.
  55
  56 ndefinition not_zero: nat → Prop ≝
  57  λn: nat. match n with
  58   [ O ⇒ False
  59   | (S p) ⇒ True ].
  60
  61 ntheorem not_eq_O_S : ∀n:nat. O ≠ S n.
  62 #n; #eqOS; nchange with (not_zero O); nrewrite > eqOS; //.
  63 nqed.
  64
  65 ntheorem not_eq_n_Sn : ∀n:nat. n ≠ S n.
  66 #n; nelim n; /2/; nqed.
  67
  68 ntheorem nat_case:
  69  ∀n:nat.∀P:nat → Prop.
  70   (n=O → P O) → (∀m:nat. (n=(S m) → P (S m))) → P n.
  71 #n; #P; nelim n; /2/; nqed.
  72
  73 ntheorem nat_elim2 :
  74  ∀R:nat → nat → Prop.
  75   (∀n:nat. R O n)
  76   → (∀n:nat. R (S n) O)
  77   → (∀n,m:nat. R n m → R (S n) (S m))
  78   → ∀n,m:nat. R n m.
  79 #R; #ROn; #RSO; #RSS; #n; nelim n;//;
  80 #n0; #Rn0m; #m; ncases m;/2/; nqed.
  81
  82 ntheorem decidable_eq_nat : \forall n,m:nat.decidable (n=m).
  83 napply nat_elim2;#n;
  84  ##[ ncases n; /2/;
  85  ##| /3/;
  86  ##| #m; #Hind; ncases Hind; /3/; (* ??? /2/;#neqnm; /3/; *)
  87  ##]
  88 nqed.
  89
  90 (*************************** plus ******************************)
  91
  92 nlet rec plus n m ≝
  93  match n with
  94  [ O ⇒ m
  95  | S p ⇒ S (plus p m) ].
  96
  97 interpretation "natural plus" 'plus x y = (plus x y).
  98
  99 ntheorem plus_O_n: ∀n:nat. n = 0+n.
 100 //; nqed.
 101
 102 (*
 103 ntheorem plus_Sn_m: ∀n,m:nat. S (n + m) = S n + m.
 104 //; nqed.
 105 *)
 106
 107 ntheorem plus_n_O: ∀n:nat. n = n+0.
 108 #n; nelim n; nnormalize; //; nqed.
 109
 110 ntheorem plus_n_Sm : ∀n,m:nat. S (n+m) = n + S m.
 111 #n; nelim n; nnormalize; //; nqed.
 112
 113 (*
 114 ntheorem plus_Sn_m1: ∀n,m:nat. S m + n = n + S m.
 115 #n; nelim n; nnormalize; //; nqed.
 116 *)
 117
 118 (*
 119 ntheorem plus_n_SO : ∀n:nat. S n = n+S O.
 120 //; nqed. *)
 121
 122 ntheorem symmetric_plus: symmetric ? plus.
 123 #n; nelim n; nnormalize; //; nqed.
 124
 125 ntheorem associative_plus : associative nat plus.
 126 #n; nelim n; nnormalize; //; nqed.
 127
 128 ntheorem assoc_plus1: ∀a,b,c. b + (a + c) = a + (b + c).
 129 //; nqed.
 130
 131 ntheorem injective_plus_r: ∀n:nat.injective nat nat (λm.n+m).
 132 #n; nelim n; nnormalize; /3/; nqed.
 133
 134 (* ntheorem inj_plus_r: \forall p,n,m:nat. p+n = p+m \to n=m
 135 \def injective_plus_r.
 136
 137 ntheorem injective_plus_l: ∀m:nat.injective nat nat (λn.n+m).
 138 /2/; nqed. *)
 139
 140 (* ntheorem inj_plus_l: \forall p,n,m:nat. n+p = m+p \to n=m
 141 \def injective_plus_l. *)
 142
 143 (*************************** times *****************************)
 144
 145 nlet rec times n m ≝
 146  match n with
 147  [ O ⇒ O
 148  | S p ⇒ m+(times p m) ].
 149
 150 interpretation "natural times" 'times x y = (times x y).
 151
 152 ntheorem times_Sn_m: ∀n,m:nat. m+n*m = S n*m.
 153 //; nqed.
 154
 155 ntheorem times_O_n: ∀n:nat. O = O*n.
 156 //; nqed.
 157
 158 ntheorem times_n_O: ∀n:nat. O = n*O.
 159 #n; nelim n; //; nqed.
 160
 161 ntheorem times_n_Sm : ∀n,m:nat. n+(n*m) = n*(S m).
 162 #n; nelim n; nnormalize; //; nqed.
 163
 164 ntheorem symmetric_times : symmetric nat times.
 165 #n; nelim n; nnormalize; //; nqed.
 166
 167 (* variant sym_times : \forall n,m:nat. n*m = m*n \def
 168 symmetric_times. *)
 169
 170 ntheorem distributive_times_plus : distributive nat times plus.
 171 #n; nelim n; nnormalize; //; nqed.
 172
 173 ntheorem distributive_times_plus_r:
 174 \forall a,b,c:nat. (b+c)*a = b*a + c*a.
 175 //; nqed.
 176
 177 ntheorem associative_times: associative nat times.
 178 #n; nelim n; nnormalize; //; nqed.
 179
 180 nlemma times_times: ∀x,y,z. x*(y*z) = y*(x*z).
 181 //; nqed.
 182
 183 (* ci servono questi risultati?
 184 ntheorem times_O_to_O: ∀n,m:nat.n*m=O → n=O ∨ m=O.
 185 napply nat_elim2; /2/;
 186 #n; #m; #H; nnormalize; #H1; napply False_ind;napply not_eq_O_S;
 187 //; nqed.
 188
 189 ntheorem times_n_SO : ∀n:nat. n = n * S O.
 190 #n; //; nqed.
 191
 192 ntheorem times_SSO_n : ∀n:nat. n + n = (S(S O)) * n.
 193 nnormalize; //; nqed.
 194
 195 nlemma times_SSO: \forall n.(S(S O))*(S n) = S(S((S(S O))*n)).
 196 //; nqed.
 197
 198 ntheorem or_eq_eq_S: \forall n.\exists m.
 199 n = (S(S O))*m \lor n = S ((S(S O))*m).
 200 #n; nelim n;
 201   ##[@; /2/;
 202   ##|#a; #H; nelim H; #b;#or;nelim or;#aeq;
 203     ##[@ b; @ 2; //;
 204     ##|@ (S b); @ 1; /2/;
 205     ##]
 206 nqed.
 207 *)
 208
 209 (************************** compare ****************************)
 210