matita/matita/lib/arithmetics/nat_commented.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 theorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m.
  17 //. qed.
  18
  19 theorem plus_Sn_m: ∀n,m:nat. S (n + m) = S n + m.
  20 // qed.
  21
  22 theorem plus_Sn_m1: ∀n,m:nat. S m + n = n + S m.
  23 #n (elim n) normalize // qed.
  24
  25
  26 (* deleterio? *)
  27 theorem plus_n_1 : ∀n:nat. S n = n+1.
  28 // qed.
  29
  30 theorem inj_plus_r: \forall p,n,m:nat. p+n = p+m \to n=m
  31 \def injective_plus_r.
  32
  33 theorem injective_plus_l: ∀m:nat.injective nat nat (λn.n+m).
  34 /2/ qed.
  35
  36 theorem inj_plus_l: \forall p,n,m:nat. n+p = m+p \to n=m
  37 \def injective_plus_l.
  38
  39 variant sym_times : \forall n,m:nat. n*m = m*n \def
  40 symmetric_times.
  41
  42 theorem times_O_to_O: ∀n,m:nat.n*m=O → n=O ∨ m=O.
  43 napply nat_elim2 /2/
  44 #n #m #H normalize #H1 napply False_ind napply not_eq_O_S
  45 // qed.
  46
  47 theorem times_n_SO : ∀n:nat. n = n * S O.
  48 #n // qed.
  49
  50 theorem times_SSO_n : ∀n:nat. n + n = (S(S O)) * n.
  51 normalize // qed.
  52
  53 nlemma times_SSO: \forall n.(S(S O))*(S n) = S(S((S(S O))*n)).
  54 // qed.
  55
  56 theorem or_eq_eq_S: \forall n.\exists m.
  57 n = (S(S O))*m \lor n = S ((S(S O))*m).
  58 #n (elim n)
  59   ##[@ /2/
  60   ##|#a #H nelim H #b#ornelim or#aeq
  61     ##[@ b @ 2 //
  62     ##|@ (S b) @ 1 /2/
  63     ##]
  64 qed.
  65
  66 lemma eq_lt: ∀n,m. (n < m) = (S n ≤ m).
  67 // qed.
  68
  69 theorem trans_le: \forall n,m,p:nat. n \leq m \to m \leq p \to n \leq p
  70 \def transitive_le.
  71
  72 theorem trans_lt: \forall n,m,p:nat. lt n m \to lt m p \to lt n p
  73 \def transitive_lt.
  74
  75 (* this are instances of the le versions *)
  76 theorem lt_S_S_to_lt: ∀n,m. S n < S m → n < m.
  77 /2/ qed.
  78
  79 theorem lt_to_lt_S_S: ∀n,m. n < m → S n < S m.
  80 /2/ qed.
  81
  82 (* this is le_S_S_to_le *)
  83 theorem lt_S_to_le: ∀n,m:nat. n < S m → n ≤ m.
  84 /2/ qed.
  85
  86 theorem lt_SO_n_to_lt_O_pred_n: \forall n:nat.
  87 (S O) \lt n \to O \lt (pred n).
  88 intros.
  89 apply (ltn_to_ltO (pred (S O)) (pred n) ?).
  90  apply (lt_pred (S O) n)
  91  [ apply (lt_O_S O)
  92  | assumption
  93  ]
  94 qed.
  95
  96 theorem lt_pred: \forall n,m.
  97   O < n \to n < m \to pred n < pred m.
  98 apply nat_elim2
  99   [intros.apply False_ind.apply (not_le_Sn_O ? H)
 100   |intros.apply False_ind.apply (not_le_Sn_O ? H1)
 101   |intros.simplify.unfold.apply le_S_S_to_le.assumption
 102   ]
 103 qed.
 104
 105 theorem le_pred_to_le:
 106  ∀n,m. O < m → pred n ≤ pred m → n ≤ m.
 107 intros 2
 108 elim n
 109 [ apply le_O_n
 110 | simplify in H2
 111   rewrite > (S_pred m)
 112   [ apply le_S_S
 113     assumption
 114   | assumption
 115   ]
 116 ].
 117 qed.
 118
 119 theorem eq_to_not_lt: ∀a,b:nat. a = b → a ≮ b.
 120 intros.
 121 unfold Not.
 122 intros.
 123 rewrite > H in H1.
 124 apply (lt_to_not_eq b b)
 125 [ assumption
 126 | reflexivity
 127 ]
 128 qed.
 129
 130 theorem lt_n_m_to_not_lt_m_Sn: ∀n,m. n < m → m ≮ S n.
 131 intros
 132 unfold Not
 133 intro
 134 unfold lt in H
 135 unfold lt in H1
 136 generalize in match (le_S_S ? ? H)
 137 intro
 138 generalize in match (transitive_le ? ? ? H2 H1)
 139 intro
 140 apply (not_le_Sn_n ? H3).
 141 qed.
 142
 143 (* other abstract properties *)
 144 theorem antisymmetric_le : antisymmetric nat le.
 145 unfold antisymmetric.intros 2.
 146 apply (nat_elim2 (\lambda n,m.(n \leq m \to m \leq n \to n=m))).
 147 intros.apply le_n_O_to_eq.assumption.
 148 intros.apply False_ind.apply (not_le_Sn_O ? H).
 149 intros.apply eq_f.apply H.
 150 apply le_S_S_to_le.assumption.
 151 apply le_S_S_to_le.assumption.
 152 qed.
 153
 154 theorem antisym_le: \forall n,m:nat. n \leq m \to m \leq n \to n=m
 155 \def antisymmetric_le.
 156
 157 theorem le_n_m_to_lt_m_Sn_to_eq_n_m: ∀n,m. n ≤ m → m < S n → n=m.
 158 intros
 159 unfold lt in H1
 160 generalize in match (le_S_S_to_le ? ? H1)
 161 intro
 162 apply antisym_le
 163 assumption.
 164 qed.
 165
 166 theorem le_plus_r: ∀p,n,m:nat. n ≤ m → p + n ≤ p + m
 167 ≝ monotonic_le_plus_r.
 168
 169 theorem le_plus_l: \forall p,n,m:nat. n \le m \to n + p \le m + p
 170 \def monotonic_le_plus_l.
 171
 172 variant lt_plus_r: \forall n,p,q:nat. p < q \to n + p < n + q \def
 173 monotonic_lt_plus_r.
 174
 175 variant lt_plus_l: \forall n,p,q:nat. p < q \to p + n < q + n \def
 176 monotonic_lt_plus_l.
 177
 178 theorem le_to_lt_to_lt_plus: ∀a,b,c,d:nat.
 179 a ≤ c → b < d → a + b < c+d.
 180 (* bello /2/ un po' lento *)
 181 #a #b #c #d #leac #lebd
 182 normalize napplyS le_plus // qed.
 183
 184 theorem le_times_r: \forall p,n,m:nat. n \le m \to p*n \le p*m
 185 \def monotonic_le_times_r.
 186
 187 theorem monotonic_le_times_l:
 188 ∀m:nat.monotonic nat le (λn.n*m).
 189 /2/ qed.
 190
 191 theorem le_times_l: \forall p,n,m:nat. n \le m \to n*p \le m*p
 192 \def monotonic_le_times_l.
 193
 194 theorem le_S_times_2: ∀n,m.O < m → n ≤ m → S n ≤ 2*m.
 195 #n #m #posm #lenm  (* interessante *)
 196 applyS (le_plus n m) // qed.
 197
 198 theorem lt_O_times_S_S: ∀n,m:nat.O < (S n)*(S m).
 199 intros.simplify.unfold lt.apply le_S_S.apply le_O_n.
 200 qed.
 201
 202 theorem lt_times_eq_O: \forall a,b:nat.
 203 O < a → a * b = O → b = O.
 204 intros.
 205 apply (nat_case1 b)
 206 [ intros.
 207   reflexivity
 208 | intros.
 209   rewrite > H2 in H1.
 210   rewrite > (S_pred a) in H1
 211   [ apply False_ind.
 212     apply (eq_to_not_lt O ((S (pred a))*(S m)))
 213     [ apply sym_eq.
 214       assumption
 215     | apply lt_O_times_S_S
 216     ]
 217   | assumption
 218   ]
 219 ]
 220 qed.
 221
 222 theorem O_lt_times_to_O_lt: \forall a,c:nat.
 223 O \lt (a * c) \to O \lt a.
 224 intros.
 225 apply (nat_case1 a)
 226 [ intros.
 227   rewrite > H1 in H.
 228   simplify in H.
 229   assumption
 230 | intros.
 231   apply lt_O_S
 232 ]
 233 qed.
 234
 235 lemma lt_times_to_lt_O: \forall i,n,m:nat. i < n*m \to O < m.
 236 intros.
 237 elim (le_to_or_lt_eq O ? (le_O_n m))
 238   [assumption
 239   |apply False_ind.
 240    rewrite < H1 in H.
 241    rewrite < times_n_O in H.
 242    apply (not_le_Sn_O ? H)
 243   ]
 244 qed.
 245
 246 theorem monotonic_lt_times_r:
 247 ∀n:nat.monotonic nat lt (λm.(S n)*m).
 248 /2/
 249 simplify.
 250 intros.elim n.
 251 simplify.rewrite < plus_n_O.rewrite < plus_n_O.assumption.
 252 apply lt_plus.assumption.assumption.
 253 qed.
 254
 255 theorem nat_compare_times_l : \forall n,p,q:nat.
 256 nat_compare p q = nat_compare ((S n) * p) ((S n) * q).
 257 intros.apply nat_compare_elim.intro.
 258 apply nat_compare_elim.
 259 intro.reflexivity.
 260 intro.absurd (p=q).
 261 apply (inj_times_r n).assumption.
 262 apply lt_to_not_eq. assumption.
 263 intro.absurd (q<p).
 264 apply (lt_times_to_lt_r n).assumption.
 265 apply le_to_not_lt.apply lt_to_le.assumption.
 266 intro.rewrite < H.rewrite > nat_compare_n_n.reflexivity.
 267 intro.apply nat_compare_elim.intro.
 268 absurd (p<q).
 269 apply (lt_times_to_lt_r n).assumption.
 270 apply le_to_not_lt.apply lt_to_le.assumption.
 271 intro.absurd (q=p).
 272 symmetry.
 273 apply (inj_times_r n).assumption.
 274 apply lt_to_not_eq.assumption.
 275 intro.reflexivity.
 276 qed.
 277
 278 theorem lt_times_plus_times: \forall a,b,n,m:nat.
 279 a < n \to b < m \to a*m + b < n*m.
 280 intros 3.
 281 apply (nat_case n)
 282   [intros.apply False_ind.apply (not_le_Sn_O ? H)
 283   |intros.simplify.
 284    rewrite < sym_plus.
 285    unfold.
 286    change with (S b+a*m1 \leq m1+m*m1).
 287    apply le_plus
 288     [assumption
 289     |apply le_times
 290       [apply le_S_S_to_le.assumption
 291       |apply le_n
 292       ]
 293     ]
 294   ]
 295 qed.
 296
 297 theorem not_eq_to_le_to_le_minus:
 298   ∀n,m.n ≠ m → n ≤ m → n ≤ m - 1.
 299 #n * #m (cases m// #m normalize
 300 #H #H1 napply le_S_S_to_le
 301 napplyS (not_eq_to_le_to_lt n (S m) H H1)
 302 qed.
 303
 304 theorem le_SO_minus: \forall n,m:nat.S n \leq m \to S O \leq m-n.
 305 intros.elim H.elim (minus_Sn_n n).apply le_n.
 306 rewrite > minus_Sn_m.
 307 apply le_S.assumption.
 308 apply lt_to_le.assumption.
 309 qed.
 310
 311 theorem minus_le_S_minus_S: \forall n,m:nat. m-n \leq S (m-(S n)).
 312 intros.
 313 apply (nat_elim2 (\lambda n,m.m-n \leq S (m-(S n)))).
 314 intro.elim n1.simplify.apply le_n_Sn.
 315 simplify.rewrite < minus_n_O.apply le_n.
 316 intros.simplify.apply le_n_Sn.
 317 intros.simplify.apply H.
 318 qed.
 319
 320 theorem lt_minus_S_n_to_le_minus_n : \forall n,m,p:nat. m-(S n) < p \to m-n \leq p.
 321 intros 3.intro.
 322 (* autobatch *)
 323 (* end auto($Revision: 9739 $) proof: TIME=1.33 SIZE=100 DEPTH=100 *)
 324 apply (trans_le (m-n) (S (m-(S n))) p).
 325 apply minus_le_S_minus_S.
 326 assumption.
 327 qed.
 328
 329 theorem le_minus_m: \forall n,m:nat. n-m \leq n.
 330 intros.apply (nat_elim2 (\lambda m,n. n-m \leq n)).
 331 intros.rewrite < minus_n_O.apply le_n.
 332 intros.simplify.apply le_n.
 333 intros.simplify.apply le_S.assumption.
 334 qed.
 335
 336 theorem lt_minus_m: \forall n,m:nat. O < n \to O < m \to n-m \lt n.
 337 intros.apply (lt_O_n_elim n H).intro.
 338 apply (lt_O_n_elim m H1).intro.
 339 simplify.unfold lt.apply le_S_S.apply le_minus_m.
 340 qed.
 341
 342 theorem minus_le_O_to_le: \forall n,m:nat. n-m \leq O \to n \leq m.
 343 intros 2.
 344 apply (nat_elim2 (\lambda n,m:nat.n-m \leq O \to n \leq m)).
 345 intros.apply le_O_n.
 346 simplify.intros. assumption.
 347 simplify.intros.apply le_S_S.apply H.assumption.
 348 qed.
 349
 350 theorem plus_minus: ∀n,m,p. p ≤ m → (n+m)-p = n +(m-p).
 351 #n #m #p #lepm @plus_to_minus >(commutative_plus p)
 352 >associative_plus <plus_minus_m_m //
 353 qed.
 354
 355 (* serve anche ltb? *)
 356 ndefinition ltb ≝λn,m. leb (S n) m.
 357
 358 theorem ltb_elim: ∀n,m:nat. ∀P:bool → Prop.
 359 (n < m → P true) → (n ≮ m → P false) → P (ltb n m).
 360 #n #m #P #Hlt #Hnlt
 361 napply leb_elim /3/ qed.
 362
 363 theorem ltb_true_to_lt:∀n,m.ltb n m = true → n < m.
 364 #n #m #Hltb napply leb_true_to_le nassumption
 365 qed.
 366
 367 theorem ltb_false_to_not_lt:∀n,m.
 368   ltb n m = false → n ≮ m.
 369 #n #m #Hltb napply leb_false_to_not_le nassumption
 370 qed.
 371
 372 theorem lt_to_ltb_true: ∀n,m. n < m → ltb n m = true.
 373 #n #m #Hltb napply le_to_leb_true nassumption
 374 qed.
 375
 376 theorem le_to_ltb_false: ∀n,m. m \le n → ltb n m = false.
 377 #n #m #Hltb napply lt_to_leb_false /2/
 378 qed.
 379
 380 *)