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 "basics/functions.ma".
  17 include "basics/eq.ma".
  18
  19 ninductive nat : Type[0] ≝
  20   | O : nat
  21   | S : nat → nat.
  22
  23 interpretation "Natural numbers" 'N = nat.
  24
  25 default "natural numbers" cic:/matita/ng/arithmetics/nat/nat.ind.
  26
  27 alias num (instance 0) = "natural number".
  28
  29 ndefinition pred ≝
  30  λn. match n with
  31  [ O ⇒  O
  32  | (S p) ⇒ p].
  33
  34 ntheorem pred_Sn : ∀n. n = pred (S n).
  35 //. nqed.
  36
  37 ntheorem injective_S : injective nat nat S.
  38 (* nwhd; #a; #b;#H;napplyS pred_Sn. *)
  39 //. nqed.
  40
  41 (*
  42 ntheorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m.
  43 //. nqed. *)
  44
  45 ntheorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m.
  46 /2/; nqed.
  47
  48 ndefinition not_zero: nat → Prop ≝
  49  λn: nat. match n with
  50   [ O ⇒ False
  51   | (S p) ⇒ True ].
  52
  53 ntheorem not_eq_O_S : ∀n:nat. O ≠ S n.
  54 #n; #eqOS; nchange with (not_zero O); nrewrite > eqOS; //.
  55 nqed.
  56
  57 ntheorem not_eq_n_Sn : ∀n:nat. n ≠ S n.
  58 #n; nelim n; /2/; nqed.
  59
  60 ntheorem nat_case:
  61  ∀n:nat.∀P:nat → Prop.
  62   (n=O → P O) → (∀m:nat. (n=(S m) → P (S m))) → P n.
  63 #n; #P; nelim n; /2/; nqed.
  64
  65 ntheorem nat_elim2 :
  66  ∀R:nat → nat → Prop.
  67   (∀n:nat. R O n)
  68   → (∀n:nat. R (S n) O)
  69   → (∀n,m:nat. R n m → R (S n) (S m))
  70   → ∀n,m:nat. R n m.
  71 #R; #ROn; #RSO; #RSS; #n; nelim n;//;
  72 #n0; #Rn0m; #m; ncases m;/2/; nqed.
  73
  74 ntheorem decidable_eq_nat : \forall n,m:nat.decidable (n=m).
  75 napply nat_elim2;#n;
  76  ##[ ncases n; /2/;
  77  ##| /3/;
  78  ##| #m; #Hind; ncases Hind; /3/; (* ??? /2/;#neqnm; /3/; *)
  79  ##]
  80 nqed.
  81
  82 (*************************** plus ******************************)
  83
  84 nlet rec plus n m ≝
  85  match n with
  86  [ O ⇒ m
  87  | S p ⇒ S (plus p m) ].
  88
  89 interpretation "natural plus" 'plus x y = (plus x y).
  90
  91 ntheorem plus_n_O: ∀n:nat. n = n+O.
  92 #n; nelim n; /2/; nqed.
  93
  94 ntheorem plus_n_Sm : ∀n,m:nat. S (n+m) = n+(S m).
  95 #n; nelim n; nnormalize; //; nqed.
  96
  97 ntheorem plus_n_SO : ∀n:nat. S n = n+(S O).
  98 //; nqed.
  99
 100 ntheorem sym_plus: ∀n,m:nat. n+m = m+n.
 101 #n; nelim n; nnormalize; //; nqed.
 102
 103 ntheorem associative_plus : associative nat plus.
 104 #n; nelim n; nnormalize; //; nqed.
 105
 106 (* ntheorem assoc_plus : \forall n,m,p:nat. (n+m)+p = n+(m+p)
 107 \def associative_plus. *)
 108
 109 ntheorem injective_plus_r: ∀n:nat.injective nat nat (λm.n+m).
 110 #n; nelim n; nnormalize; /3/; nqed.
 111
 112 (* ntheorem inj_plus_r: \forall p,n,m:nat. p+n = p+m \to n=m
 113 \def injective_plus_r. *)
 114
 115 ntheorem injective_plus_l: ∀m:nat.injective nat nat (λn.n+m).
 116 /2/; nqed.
 117
 118 (* ntheorem inj_plus_l: \forall p,n,m:nat. n+p = m+p \to n=m
 119 \def injective_plus_l. *)
 120
 121 (*************************** times *****************************)
 122
 123 nlet rec times n m ≝
 124  match n with
 125  [ O ⇒ O
 126  | S p ⇒ m+(times p m) ].
 127
 128 interpretation "natural times" 'times x y = (times x y).
 129
 130 ntheorem times_Sn_m: ∀n,m:nat. m+n*m = S n*m.
 131 //; nqed.
 132
 133 ntheorem times_n_O: ∀n:nat. O = n*O.
 134 #n; nelim n; //; nqed.
 135
 136 ntheorem times_n_Sm : ∀n,m:nat. n+(n*m) = n*(S m).
 137 #n; nelim n; nnormalize; /2/; nqed.
 138
 139 ntheorem times_O_to_O: ∀n,m:nat.n*m=O → n=O ∨ m=O.
 140 napply nat_elim2; (* /2/ slow! *)
 141   ##[#n; #H; @1; //;
 142   ##|#n; #H; @2; //; (* ?? *)
 143   ##|#n; #m; #H; #H1; napply False_ind;napply not_eq_O_S;
 144   (* why two steps? *) /2/;
 145   ##]
 146 nqed.
 147
 148 ntheorem times_n_SO : ∀n:nat. n = n * S O.
 149 //; nqed.
 150
 151 (*
 152
 153 ntheorem times_SSO_n : ∀n:nat. n + n = 2 * n.
 154 intros.
 155 simplify.
 156 rewrite < plus_n_O.
 157 reflexivity.
 158 qed.
 159
 160 alias num (instance 0) = "natural number".
 161 lemma times_SSO: \forall n.2*(S n) = S(S(2*n)).
 162 intro.
 163 simplify.rewrite < plus_n_Sm.reflexivity.
 164 qed.
 165
 166 theorem or_eq_eq_S: \forall n.\exists m.
 167 n = (S(S O))*m \lor n = S ((S(S O))*m).
 168 intro.elim n
 169   [apply (ex_intro ? ? O).
 170    left.reflexivity
 171   |elim H. elim H1
 172     [apply (ex_intro ? ? a).
 173      right.apply eq_f.assumption
 174     |apply (ex_intro ? ? (S a)).
 175      left. rewrite > H2.
 176      apply sym_eq.
 177      apply times_SSO
 178     ]
 179   ]
 180 qed.
 181
 182 theorem symmetric_times : symmetric nat times.
 183 unfold symmetric.
 184 intros.elim x
 185   [simplify.apply times_n_O.
 186   | simplify.rewrite > H.apply times_n_Sm.]
 187 qed.
 188
 189 variant sym_times : \forall n,m:nat. n*m = m*n \def
 190 symmetric_times.
 191
 192 theorem distributive_times_plus : distributive nat times plus.
 193 unfold distributive.
 194 intros.elim x.
 195 simplify.reflexivity.
 196 simplify.
 197 demodulate all.
 198 (*
 199 rewrite > H. rewrite > assoc_plus.rewrite > assoc_plus.
 200 apply eq_f.rewrite < assoc_plus. rewrite < (sym_plus ? z).
 201 rewrite > assoc_plus.reflexivity. *)
 202 qed.
 203
 204 variant distr_times_plus: \forall n,m,p:nat. n*(m+p) = n*m + n*p
 205 \def distributive_times_plus.
 206
 207 theorem associative_times: associative nat times.
 208 unfold associative.
 209 intros.
 210 elim x. simplify.apply refl_eq.
 211 simplify.
 212 demodulate all.
 213 (*
 214 rewrite < sym_times.
 215 >>>>>>> .r9770
 216 rewrite > distr_times_plus.
 217 rewrite < sym_times.
 218 rewrite < (sym_times (times n y) z).
 219 rewrite < H.apply refl_eq.
 220 *)
 221 qed.
 222
 223 variant assoc_times: \forall n,m,p:nat. (n*m)*p = n*(m*p) \def
 224 associative_times.
 225
 226 lemma times_times: ∀x,y,z. x*(y*z) = y*(x*z).
 227 intros.
 228 demodulate. reflexivity.
 229 (* autobatch paramodulation. *)
 230 qed.
 231
 232 *)