matita/matita/re_complete/basics/nat.ma

   1 include "basics/relations.ma".
   2 include "basics/bool.ma".
   3
   4 (* natural numbers *)
   5
   6 inductive nat : Type[0] ≝
   7   | O : nat
   8   | S : nat → nat.
   9
  10 interpretation "Natural numbers" 'N = nat.
  11
  12 alias num (instance 0) = "natural number".
  13
  14 definition pred ≝
  15  λn. match n with [ O ⇒ O | S p ⇒ p].
  16
  17 definition not_zero: nat → Prop ≝
  18  λn: nat. match n with [ O ⇒ False | (S p) ⇒ True ].
  19
  20 (* order relations *)
  21
  22 inductive le (n:nat) : nat → Prop ≝
  23   | le_n : le n n
  24   | le_S : ∀ m:nat. le n m → le n (S m).
  25
  26 interpretation "natural 'less or equal to'" 'leq x y = (le x y).
  27
  28 interpretation "natural 'neither less nor equal to'" 'nleq x y = (Not (le x y)).
  29
  30 definition lt: nat → nat → Prop ≝ λn,m. S n ≤ m.
  31
  32 interpretation "natural 'less than'" 'lt x y = (lt x y).
  33
  34 interpretation "natural 'not less than'" 'nless x y = (Not (lt x y)).
  35
  36 (* abstract properties *)
  37
  38 definition increasing ≝ λf:nat → nat. ∀n:nat. f n < f (S n).
  39
  40 (* arithmetic operations *)
  41
  42 let rec plus n m ≝
  43  match n with [ O ⇒ m | S p ⇒ S (plus p m) ].
  44
  45 interpretation "natural plus" 'plus x y = (plus x y).
  46
  47 (* Generic conclusion ******************************************************)
  48
  49 theorem nat_case:
  50  ∀n:nat.∀P:nat → Prop.
  51   (n=O → P O) → (∀m:nat. n= S m → P (S m)) → P n.
  52 #n #P (elim n) /2/ qed.
  53
  54 theorem nat_elim2 :
  55  ∀R:nat → nat → Prop.
  56   (∀n:nat. R O n)
  57   → (∀n:nat. R (S n) O)
  58   → (∀n,m:nat. R n m → R (S n) (S m))
  59   → ∀n,m:nat. R n m.
  60 #R #ROn #RSO #RSS #n (elim n) // #n0 #Rn0m #m (cases m) /2/ qed.
  61
  62 lemma le_gen: ∀P:nat → Prop.∀n.(∀i. i ≤ n → P i) → P n.
  63 /2/ qed.
  64
  65 (* Equalities ***************************************************************)
  66
  67 theorem pred_Sn : ∀n. n = pred (S n).
  68 // qed.
  69
  70 theorem injective_S : injective nat nat S.
  71 #a #b #H >(pred_Sn a) >(pred_Sn b) @eq_f // qed.
  72
  73 theorem S_pred: ∀n. O < n → S(pred n) = n.
  74 #n #posn (cases posn) //
  75 qed.
  76
  77 theorem plus_O_n: ∀n:nat. n = O + n.
  78 // qed.
  79
  80 theorem plus_n_O: ∀n:nat. n = n + O.
  81 #n (elim n) normalize // qed.
  82
  83 theorem plus_n_Sm : ∀n,m:nat. S (n+m) = n + S m.
  84 #n (elim n) normalize // qed.
  85
  86 theorem commutative_plus: commutative ? plus.
  87 #n (elim n) normalize // qed.
  88
  89 theorem associative_plus : associative nat plus.
  90 #n (elim n) normalize // qed.
  91
  92 theorem assoc_plus1: ∀a,b,c. c + (b + a) = b + c + a.
  93 // qed.
  94
  95 theorem injective_plus_r: ∀n:nat.injective nat nat (λm.n+m).
  96 #n (elim n) normalize /3/ qed.
  97
  98 theorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m.
  99 /2/ qed.
 100
 101 (* not_zero *)
 102
 103 theorem lt_to_not_zero : ∀n,m:nat. n < m → not_zero m.
 104 #n #m #Hlt (elim Hlt) // qed.
 105
 106 (* le *)
 107
 108 theorem le_S_S: ∀n,m:nat. n ≤ m → S n ≤ S m.
 109 #n #m #lenm (elim lenm) /2/ qed.
 110
 111 theorem le_O_n : ∀n:nat. O ≤ n.
 112 #n (elim n) /2/ qed.
 113
 114 theorem le_n_Sn : ∀n:nat. n ≤ S n.
 115 /2/ qed.
 116
 117 theorem transitive_le : transitive nat le.
 118 #a #b #c #leab #lebc (elim lebc) /2/
 119 qed.
 120
 121 theorem le_pred_n : ∀n:nat. pred n ≤ n.
 122 #n (elim n) // qed.
 123
 124 theorem monotonic_pred: monotonic ? le pred.
 125 #n #m #lenm (elim lenm) /2/ qed.
 126
 127 theorem le_S_S_to_le: ∀n,m:nat. S n ≤ S m → n ≤ m.
 128 (* demo *)
 129 /2/ qed-.
 130
 131 theorem monotonic_le_plus_r:
 132 ∀n:nat.monotonic nat le (λm.n + m).
 133 #n #a #b (elim n) normalize //
 134 #m #H #leab @le_S_S /2/ qed.
 135
 136 theorem monotonic_le_plus_l:
 137 ∀m:nat.monotonic nat le (λn.n + m).
 138 /2/ qed.
 139
 140 theorem le_plus: ∀n1,n2,m1,m2:nat. n1 ≤ n2  → m1 ≤ m2
 141 → n1 + m1 ≤ n2 + m2.
 142 #n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1+m2))
 143 /2/ qed-.
 144
 145 theorem le_plus_n :∀n,m:nat. m ≤ n + m.
 146 /2/ qed.
 147
 148 lemma le_plus_a: ∀a,n,m. n ≤ m → n ≤ a + m.
 149 /2/ qed.
 150
 151 lemma le_plus_b: ∀b,n,m. n + b ≤ m → n ≤ m.
 152 /2/ qed.
 153
 154 theorem le_plus_n_r :∀n,m:nat. m ≤ m + n.
 155 /2/ qed.
 156
 157 theorem eq_plus_to_le: ∀n,m,p:nat.n=m+p → m ≤ n.
 158 // qed-.
 159
 160 theorem le_plus_to_le: ∀a,n,m. a + n ≤ a + m → n ≤ m.
 161 #a (elim a) normalize /3/ qed.
 162
 163 theorem le_plus_to_le_r: ∀a,n,m. n + a ≤ m +a → n ≤ m.
 164 /2/ qed-.
 165
 166 (* lt *)
 167
 168 theorem transitive_lt: transitive nat lt.
 169 #a #b #c #ltab #ltbc (elim ltbc) /2/
 170 qed.
 171
 172 theorem lt_to_le_to_lt: ∀n,m,p:nat. n < m → m ≤ p → n < p.
 173 #n #m #p #H #H1 (elim H1) /2/ qed.
 174
 175 theorem le_to_lt_to_lt: ∀n,m,p:nat. n ≤ m → m < p → n < p.
 176 #n #m #p #H (elim H) /3/ qed.
 177
 178 theorem lt_S_to_lt: ∀n,m. S n < m → n < m.
 179 /2/ qed.
 180
 181 theorem ltn_to_ltO: ∀n,m:nat. n < m → O < m.
 182 /2/ qed.
 183
 184 theorem lt_O_S : ∀n:nat. O < S n.
 185 /2/ qed.
 186
 187 theorem monotonic_lt_plus_r:
 188 ∀n:nat.monotonic nat lt (λm.n+m).
 189 /2/ qed.
 190
 191 theorem monotonic_lt_plus_l:
 192 ∀n:nat.monotonic nat lt (λm.m+n).
 193 /2/ qed.
 194
 195 theorem lt_plus: ∀n,m,p,q:nat. n < m → p < q → n + p < m + q.
 196 #n #m #p #q #ltnm #ltpq
 197 @(transitive_lt ? (n+q))/2/ qed.
 198
 199 theorem lt_plus_to_lt_l :∀n,p,q:nat. p+n < q+n → p<q.
 200 /2/ qed.
 201
 202 theorem lt_plus_to_lt_r :∀n,p,q:nat. n+p < n+q → p<q.
 203 /2/ qed-.
 204
 205 theorem increasing_to_monotonic: ∀f:nat → nat.
 206   increasing f → monotonic nat lt f.
 207 #f #incr #n #m #ltnm (elim ltnm) /2/
 208 qed.
 209
 210 (* not le, lt *)
 211
 212 theorem not_le_Sn_O: ∀ n:nat. S n ≰ O.
 213 #n @nmk #Hlen0 @(lt_to_not_zero ?? Hlen0) qed.
 214
 215 theorem not_le_to_not_le_S_S: ∀ n,m:nat. n ≰ m → S n ≰ S m.
 216 /3/ qed.
 217
 218 theorem not_le_S_S_to_not_le: ∀ n,m:nat. S n ≰ S m → n ≰ m.
 219 /3/ qed.
 220
 221 theorem not_le_Sn_n: ∀n:nat. S n ≰ n.
 222 #n (elim n) /2/ qed.
 223
 224 theorem lt_to_not_le: ∀n,m. n < m → m ≰ n.
 225 #n #m #Hltnm (elim Hltnm) /3/ qed.
 226
 227 theorem not_le_to_lt: ∀n,m. n ≰ m → m < n.
 228 @nat_elim2 #n
 229  [#abs @False_ind /2/
 230  |/2/
 231  |#m #Hind #HnotleSS @le_S_S /3/
 232  ]
 233 qed.
 234
 235 (* not lt, le *)
 236
 237 theorem not_lt_to_le: ∀n,m:nat. n ≮ m → m ≤ n.
 238 /4/ qed.
 239
 240 theorem le_to_not_lt: ∀n,m:nat. n ≤ m → m ≮ n.
 241 #n #m #H @lt_to_not_le /2/ (* /3/ *) qed.
 242
 243 (*********************** boolean arithmetics ********************)
 244
 245
 246 let rec eqbnat n m ≝
 247 match n with
 248   [ O ⇒ match m with [ O ⇒ true | S q ⇒ false]
 249   | S p ⇒ match m with [ O ⇒ false | S q ⇒ eqbnat p q]
 250   ].
 251
 252 theorem eqbnat_elim : ∀ n,m:nat.∀ P:bool → Prop.
 253 (n=m → (P true)) → (n ≠ m → (P false)) → (P (eqbnat n m)).
 254 @nat_elim2
 255   [#n (cases n) normalize /3/
 256   |normalize /3/
 257   |normalize /4/
 258   ]
 259 qed.
 260
 261 theorem eqbnat_n_n: ∀n. eqbnat n n = true.
 262 #n (elim n) normalize // qed.
 263
 264 theorem eqbnat_true_to_eq: ∀n,m:nat. eqbnat n m = true → n = m.
 265 #n #m @(eqbnat_elim n m) // #_ #abs @False_ind /2/ qed.
 266
 267 (* theorem eqb_false_to_not_eq: ∀n,m:nat. eqbnat n m = false → n ≠ m.
 268 #n #m @(eqbnat_elim n m) /2/ qed. *)
 269
 270 theorem eq_to_eqbnat_true: ∀n,m:nat.n = m → eqbnat n m = true.
 271 // qed.