]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/arithmetics/nat.ma
Some arithmetics.
[helm.git] / matita / matita / lib / arithmetics / nat.ma
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic        
3     ||A||  Library of Mathematics, developed at the Computer Science     
4     ||T||  Department of the University of Bologna, Italy.                     
5     ||I||                                                                 
6     ||T||  
7     ||A||  This file is distributed under the terms of the 
8     \   /  GNU General Public License Version 2        
9      \ /      
10       V_______________________________________________________________ *)
11
12 include "basics/relations.ma".
13
14 inductive nat : Type[0] ≝
15   | O : nat
16   | S : nat → nat.
17   
18 interpretation "Natural numbers" 'N = nat.
19
20 alias num (instance 0) = "natural number".
21
22 definition pred ≝
23  λn. match n with [ O ⇒ O | S p ⇒ p].
24
25 theorem pred_Sn : ∀n. n = pred (S n).
26 // qed.
27
28 theorem injective_S : injective nat nat S.
29 // qed.
30
31 (*
32 theorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m.
33 //. qed. *)
34
35 theorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m.
36 /2/ qed.
37
38 definition not_zero: nat → Prop ≝
39  λn: nat. match n with [ O ⇒ False | (S p) ⇒ True ].
40
41 theorem not_eq_O_S : ∀n:nat. O ≠ S n.
42 #n @nmk #eqOS (change with (not_zero O)) >eqOS // qed.
43
44 theorem not_eq_n_Sn: ∀n:nat. n ≠ S n.
45 #n (elim n) /2/ qed.
46
47 theorem nat_case:
48  ∀n:nat.∀P:nat → Prop. 
49   (n=O → P O) → (∀m:nat. n= S m → P (S m)) → P n.
50 #n #P (elim n) /2/ qed.
51
52 theorem nat_elim2 :
53  ∀R:nat → nat → Prop.
54   (∀n:nat. R O n) 
55   → (∀n:nat. R (S n) O)
56   → (∀n,m:nat. R n m → R (S n) (S m))
57   → ∀n,m:nat. R n m.
58 #R #ROn #RSO #RSS #n (elim n) // #n0 #Rn0m #m (cases m) /2/ qed.
59
60 theorem decidable_eq_nat : ∀n,m:nat.decidable (n=m).
61 @nat_elim2 #n [ (cases n) /2/ | /3/ | #m #Hind (cases Hind) /3/]
62 qed. 
63
64 (*************************** plus ******************************)
65
66 let rec plus n m ≝ 
67  match n with [ O ⇒ m | S p ⇒ S (plus p m) ].
68
69 interpretation "natural plus" 'plus x y = (plus x y).
70
71 theorem plus_O_n: ∀n:nat. n = O+n.
72 // qed.
73
74 (*
75 theorem plus_Sn_m: ∀n,m:nat. S (n + m) = S n + m.
76 // qed.
77 *)
78
79 theorem plus_n_O: ∀n:nat. n = n+O.
80 #n (elim n) normalize // qed.
81
82 theorem plus_n_Sm : ∀n,m:nat. S (n+m) = n + S m.
83 #n (elim n) normalize // qed.
84
85 (*
86 theorem plus_Sn_m1: ∀n,m:nat. S m + n = n + S m.
87 #n (elim n) normalize // qed.
88 *)
89
90 (* deleterio?
91 theorem plus_n_1 : ∀n:nat. S n = n+1.
92 // qed.
93 *)
94
95 theorem commutative_plus: commutative ? plus.
96 #n (elim n) normalize // qed. 
97
98 theorem associative_plus : associative nat plus.
99 #n (elim n) normalize // qed.
100
101 theorem assoc_plus1: ∀a,b,c. c + (b + a) = b + c + a.
102 // qed. 
103
104 theorem injective_plus_r: ∀n:nat.injective nat nat (λm.n+m).
105 #n (elim n) normalize /3/ qed.
106
107 (* theorem inj_plus_r: \forall p,n,m:nat. p+n = p+m \to n=m
108 \def injective_plus_r. 
109
110 theorem injective_plus_l: ∀m:nat.injective nat nat (λn.n+m).
111 /2/ qed. *)
112
113 (* theorem inj_plus_l: \forall p,n,m:nat. n+p = m+p \to n=m
114 \def injective_plus_l. *)
115
116 (*************************** times *****************************)
117
118 let rec times n m ≝ 
119  match n with [ O ⇒ O | S p ⇒ m+(times p m) ].
120
121 interpretation "natural times" 'times x y = (times x y).
122
123 theorem times_Sn_m: ∀n,m:nat. m+n*m = S n*m.
124 // qed.
125
126 theorem times_O_n: ∀n:nat. O = O*n.
127 // qed.
128
129 theorem times_n_O: ∀n:nat. O = n*O.
130 #n (elim n) // qed.
131
132 theorem times_n_Sm : ∀n,m:nat. n+(n*m) = n*(S m).
133 #n (elim n) normalize // qed.
134
135 theorem commutative_times : commutative nat times. 
136 #n (elim n) normalize // qed. 
137
138 (* variant sym_times : \forall n,m:nat. n*m = m*n \def
139 symmetric_times. *)
140
141 theorem distributive_times_plus : distributive nat times plus.
142 #n (elim n) normalize // qed.
143
144 theorem distributive_times_plus_r :
145   ∀a,b,c:nat. (b+c)*a = b*a + c*a.
146 // qed. 
147
148 theorem associative_times: associative nat times.
149 #n (elim n) normalize // qed.
150
151 lemma times_times: ∀x,y,z. x*(y*z) = y*(x*z).
152 // qed. 
153
154 (* ci servono questi risultati? 
155 theorem times_O_to_O: ∀n,m:nat.n*m=O → n=O ∨ m=O.
156 napply nat_elim2 /2/ 
157 #n #m #H normalize #H1 napply False_ind napply not_eq_O_S
158 // qed.
159   
160 theorem times_n_SO : ∀n:nat. n = n * S O.
161 #n // qed.
162
163 theorem times_SSO_n : ∀n:nat. n + n = (S(S O)) * n.
164 normalize // qed.
165
166 nlemma times_SSO: \forall n.(S(S O))*(S n) = S(S((S(S O))*n)).
167 // qed.
168
169 theorem or_eq_eq_S: \forall n.\exists m. 
170 n = (S(S O))*m \lor n = S ((S(S O))*m).
171 #n (elim n)
172   ##[@ /2/
173   ##|#a #H nelim H #b#ornelim or#aeq
174     ##[@ b @ 2 //
175     ##|@ (S b) @ 1 /2/
176     ##]
177 qed.
178 *)
179
180 (******************** ordering relations ************************)
181
182 inductive le (n:nat) : nat → Prop ≝
183   | le_n : le n n
184   | le_S : ∀ m:nat. le n m → le n (S m).
185
186 interpretation "natural 'less or equal to'" 'leq x y = (le x y).
187
188 interpretation "natural 'neither less nor equal to'" 'nleq x y = (Not (le x y)).
189
190 definition lt: nat → nat → Prop ≝ λn,m. S n ≤ m.
191
192 interpretation "natural 'less than'" 'lt x y = (lt x y).
193 interpretation "natural 'not less than'" 'nless x y = (Not (lt x y)).
194
195 (* lemma eq_lt: ∀n,m. (n < m) = (S n ≤ m).
196 // qed. *)
197
198 definition ge: nat → nat → Prop ≝ λn,m.m ≤ n.
199
200 interpretation "natural 'greater or equal to'" 'geq x y = (ge x y).
201
202 definition gt: nat → nat → Prop ≝ λn,m.m<n.
203
204 interpretation "natural 'greater than'" 'gt x y = (gt x y).
205 interpretation "natural 'not greater than'" 'ngtr x y = (Not (gt x y)).
206
207 theorem transitive_le : transitive nat le.
208 #a #b #c #leab #lebc (elim lebc) /2/
209 qed.
210
211 (*
212 theorem trans_le: \forall n,m,p:nat. n \leq m \to m \leq p \to n \leq p
213 \def transitive_le. *)
214
215 theorem transitive_lt: transitive nat lt.
216 #a #b #c #ltab #ltbc (elim ltbc) /2/qed.
217
218 (*
219 theorem trans_lt: \forall n,m,p:nat. lt n m \to lt m p \to lt n p
220 \def transitive_lt. *)
221
222 theorem le_S_S: ∀n,m:nat. n ≤ m → S n ≤ S m.
223 #n #m #lenm (elim lenm) /2/ qed.
224
225 theorem le_O_n : ∀n:nat. O ≤ n.
226 #n (elim n) /2/ qed.
227
228 theorem le_n_Sn : ∀n:nat. n ≤ S n.
229 /2/ qed.
230
231 theorem le_pred_n : ∀n:nat. pred n ≤ n.
232 #n (elim n) // qed.
233
234 theorem monotonic_pred: monotonic ? le pred.
235 #n #m #lenm (elim lenm) /2/ qed.
236
237 theorem le_S_S_to_le: ∀n,m:nat. S n ≤ S m → n ≤ m.
238 (* demo *)
239 /2/ qed.
240
241 (* this are instances of the le versions 
242 theorem lt_S_S_to_lt: ∀n,m. S n < S m → n < m.
243 /2/ qed. 
244
245 theorem lt_to_lt_S_S: ∀n,m. n < m → S n < S m.
246 /2/ qed. *)
247
248 theorem lt_to_not_zero : ∀n,m:nat. n < m → not_zero m.
249 #n #m #Hlt (elim Hlt) // qed.
250
251 (* lt vs. le *)
252 theorem not_le_Sn_O: ∀ n:nat. S n ≰ O.
253 #n @nmk #Hlen0 @(lt_to_not_zero ?? Hlen0) qed.
254
255 theorem not_le_to_not_le_S_S: ∀ n,m:nat. n ≰ m → S n ≰ S m.
256 /3/ qed.
257
258 theorem not_le_S_S_to_not_le: ∀ n,m:nat. S n ≰ S m → n ≰ m.
259 /3/ qed.
260
261 theorem decidable_le: ∀n,m. decidable (n≤m).
262 @nat_elim2 #n /2/ #m * /3/ qed.
263
264 theorem decidable_lt: ∀n,m. decidable (n < m).
265 #n #m @decidable_le  qed.
266
267 theorem not_le_Sn_n: ∀n:nat. S n ≰ n.
268 #n (elim n) /2/ qed.
269
270 (* this is le_S_S_to_le
271 theorem lt_S_to_le: ∀n,m:nat. n < S m → n ≤ m.
272 /2/ qed.
273 *)
274
275 lemma le_gen: ∀P:nat → Prop.∀n.(∀i. i ≤ n → P i) → P n.
276 /2/ qed.
277
278 theorem not_le_to_lt: ∀n,m. n ≰ m → m < n.
279 @nat_elim2 #n
280  [#abs @False_ind /2/
281  |/2/
282  |#m #Hind #HnotleSS @le_S_S /3/
283  ]
284 qed.
285
286 theorem lt_to_not_le: ∀n,m. n < m → m ≰ n.
287 #n #m #Hltnm (elim Hltnm) /3/ qed.
288
289 theorem not_lt_to_le: ∀n,m:nat. n ≮ m → m ≤ n.
290 /4/ qed.
291
292 theorem le_to_not_lt: ∀n,m:nat. n ≤ m → m ≮ n.
293 #n #m #H @lt_to_not_le /2/ (* /3/ *) qed.
294
295 (* lt and le trans *)
296
297 theorem lt_to_le_to_lt: ∀n,m,p:nat. n < m → m ≤ p → n < p.
298 #n #m #p #H #H1 (elim H1) /2/ qed.
299
300 theorem le_to_lt_to_lt: ∀n,m,p:nat. n ≤ m → m < p → n < p.
301 #n #m #p #H (elim H) /3/ qed.
302
303 theorem lt_S_to_lt: ∀n,m. S n < m → n < m.
304 /2/ qed.
305
306 theorem ltn_to_ltO: ∀n,m:nat. n < m → O < m.
307 /2/ qed.
308
309 (*
310 theorem lt_SO_n_to_lt_O_pred_n: \forall n:nat.
311 (S O) \lt n \to O \lt (pred n).
312 intros.
313 apply (ltn_to_ltO (pred (S O)) (pred n) ?).
314  apply (lt_pred (S O) n)
315  [ apply (lt_O_S O) 
316  | assumption
317  ]
318 qed. *)
319
320 theorem lt_O_n_elim: ∀n:nat. O < n → 
321   ∀P:nat → Prop.(∀m:nat.P (S m)) → P n.
322 #n (elim n) // #abs @False_ind /2/
323 qed.
324
325 (*
326 theorem lt_pred: \forall n,m. 
327   O < n \to n < m \to pred n < pred m. 
328 apply nat_elim2
329   [intros.apply False_ind.apply (not_le_Sn_O ? H)
330   |intros.apply False_ind.apply (not_le_Sn_O ? H1)
331   |intros.simplify.unfold.apply le_S_S_to_le.assumption
332   ]
333 qed.
334
335 theorem S_pred: \forall n:nat.lt O n \to eq nat n (S (pred n)).
336 intro.elim n.apply False_ind.exact (not_le_Sn_O O H).
337 apply eq_f.apply pred_Sn.
338 qed.
339
340 theorem le_pred_to_le:
341  ∀n,m. O < m → pred n ≤ pred m → n ≤ m.
342 intros 2
343 elim n
344 [ apply le_O_n
345 | simplify in H2
346   rewrite > (S_pred m)
347   [ apply le_S_S
348     assumption
349   | assumption
350   ]
351 ].
352 qed.
353
354 *)
355
356 (* le to lt or eq *)
357 theorem le_to_or_lt_eq: ∀n,m:nat. n ≤ m → n < m ∨ n = m.
358 #n #m #lenm (elim lenm) /3/ qed.
359
360 (* not eq *)
361 theorem lt_to_not_eq : ∀n,m:nat. n < m → n ≠ m.
362 #n #m #H @not_to_not /2/ qed.
363
364 (*not lt 
365 theorem eq_to_not_lt: ∀a,b:nat. a = b → a ≮ b.
366 intros.
367 unfold Not.
368 intros.
369 rewrite > H in H1.
370 apply (lt_to_not_eq b b)
371 [ assumption
372 | reflexivity
373 ]
374 qed. 
375
376 theorem lt_n_m_to_not_lt_m_Sn: ∀n,m. n < m → m ≮ S n.
377 intros
378 unfold Not
379 intro
380 unfold lt in H
381 unfold lt in H1
382 generalize in match (le_S_S ? ? H)
383 intro
384 generalize in match (transitive_le ? ? ? H2 H1)
385 intro
386 apply (not_le_Sn_n ? H3).
387 qed. *)
388
389 theorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n<m.
390 #n #m #Hneq #Hle cases (le_to_or_lt_eq ?? Hle) //
391 #Heq /3/ qed.
392 (*
393 nelim (Hneq Heq) qed. *)
394
395 (* le elimination *)
396 theorem le_n_O_to_eq : ∀n:nat. n ≤ O → O=n.
397 #n (cases n) // #a  #abs @False_ind /2/ qed.
398
399 theorem le_n_O_elim: ∀n:nat. n ≤ O → ∀P: nat →Prop. P O → P n.
400 #n (cases n) // #a #abs @False_ind /2/ qed. 
401
402 theorem le_n_Sm_elim : ∀n,m:nat.n ≤ S m → 
403 ∀P:Prop. (S n ≤ S m → P) → (n=S m → P) → P.
404 #n #m #Hle #P (elim Hle) /3/ qed.
405
406 (* le and eq *)
407
408 theorem le_to_le_to_eq: ∀n,m. n ≤ m → m ≤ n → n = m.
409 @nat_elim2 /4/
410 qed. 
411
412 theorem lt_O_S : ∀n:nat. O < S n.
413 /2/ qed.
414
415 (*
416 (* other abstract properties *)
417 theorem antisymmetric_le : antisymmetric nat le.
418 unfold antisymmetric.intros 2.
419 apply (nat_elim2 (\lambda n,m.(n \leq m \to m \leq n \to n=m))).
420 intros.apply le_n_O_to_eq.assumption.
421 intros.apply False_ind.apply (not_le_Sn_O ? H).
422 intros.apply eq_f.apply H.
423 apply le_S_S_to_le.assumption.
424 apply le_S_S_to_le.assumption.
425 qed.
426
427 theorem antisym_le: \forall n,m:nat. n \leq m \to m \leq n \to n=m
428 \def antisymmetric_le.
429
430 theorem le_n_m_to_lt_m_Sn_to_eq_n_m: ∀n,m. n ≤ m → m < S n → n=m.
431 intros
432 unfold lt in H1
433 generalize in match (le_S_S_to_le ? ? H1)
434 intro
435 apply antisym_le
436 assumption.
437 qed.
438 *)
439
440 (* well founded induction principles *)
441
442 theorem nat_elim1 : ∀n:nat.∀P:nat → Prop. 
443 (∀m.(∀p. p < m → P p) → P m) → P n.
444 #n #P #H 
445 cut (∀q:nat. q ≤ n → P q) /2/
446 (elim n) 
447  [#q #HleO (* applica male *) 
448     @(le_n_O_elim ? HleO)
449     @H #p #ltpO @False_ind /2/ (* 3 *)
450  |#p #Hind #q #HleS 
451     @H #a #lta @Hind @le_S_S_to_le /2/
452  ]
453 qed.
454
455 (* some properties of functions *)
456 (*
457 definition increasing \def \lambda f:nat \to nat. 
458 \forall n:nat. f n < f (S n).
459
460 theorem increasing_to_monotonic: \forall f:nat \to nat.
461 increasing f \to monotonic nat lt f.
462 unfold monotonic.unfold lt.unfold increasing.unfold lt.intros.elim H1.apply H.
463 apply (trans_le ? (f n1)).
464 assumption.apply (trans_le ? (S (f n1))).
465 apply le_n_Sn.
466 apply H.
467 qed.
468
469 theorem le_n_fn: \forall f:nat \to nat. (increasing f) 
470 \to \forall n:nat. n \le (f n).
471 intros.elim n.
472 apply le_O_n.
473 apply (trans_le ? (S (f n1))).
474 apply le_S_S.apply H1.
475 simplify in H. unfold increasing in H.unfold lt in H.apply H.
476 qed.
477
478 theorem increasing_to_le: \forall f:nat \to nat. (increasing f) 
479 \to \forall m:nat. \exists i. m \le (f i).
480 intros.elim m.
481 apply (ex_intro ? ? O).apply le_O_n.
482 elim H1.
483 apply (ex_intro ? ? (S a)).
484 apply (trans_le ? (S (f a))).
485 apply le_S_S.assumption.
486 simplify in H.unfold increasing in H.unfold lt in H.
487 apply H.
488 qed.
489
490 theorem increasing_to_le2: \forall f:nat \to nat. (increasing f) 
491 \to \forall m:nat. (f O) \le m \to 
492 \exists i. (f i) \le m \land m <(f (S i)).
493 intros.elim H1.
494 apply (ex_intro ? ? O).
495 split.apply le_n.apply H.
496 elim H3.elim H4.
497 cut ((S n1) < (f (S a)) \lor (S n1) = (f (S a))).
498 elim Hcut.
499 apply (ex_intro ? ? a).
500 split.apply le_S. assumption.assumption.
501 apply (ex_intro ? ? (S a)).
502 split.rewrite < H7.apply le_n.
503 rewrite > H7.
504 apply H.
505 apply le_to_or_lt_eq.apply H6.
506 qed.
507 *)
508
509 (*********************** monotonicity ***************************)
510 theorem monotonic_le_plus_r: 
511 ∀n:nat.monotonic nat le (λm.n + m).
512 #n #a #b (elim n) normalize //
513 #m #H #leab @le_S_S /2/ qed.
514
515 (*
516 theorem le_plus_r: ∀p,n,m:nat. n ≤ m → p + n ≤ p + m
517 ≝ monotonic_le_plus_r. *)
518
519 theorem monotonic_le_plus_l: 
520 ∀m:nat.monotonic nat le (λn.n + m).
521 /2/ qed.
522
523 (*
524 theorem le_plus_l: \forall p,n,m:nat. n \le m \to n + p \le m + p
525 \def monotonic_le_plus_l. *)
526
527 theorem le_plus: ∀n1,n2,m1,m2:nat. n1 ≤ n2  → m1 ≤ m2 
528 → n1 + m1 ≤ n2 + m2.
529 #n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1+m2))
530 /2/ qed.
531
532 theorem le_plus_n :∀n,m:nat. m ≤ n + m.
533 /2/ qed. 
534
535 lemma le_plus_a: ∀a,n,m. n ≤ m → n ≤ a + m.
536 /2/ qed.
537
538 lemma le_plus_b: ∀b,n,m. n + b ≤ m → n ≤ m.
539 /2/ qed.
540
541 theorem le_plus_n_r :∀n,m:nat. m ≤ m + n.
542 /2/ qed.
543
544 theorem eq_plus_to_le: ∀n,m,p:nat.n=m+p → m ≤ n.
545 // qed.
546
547 theorem le_plus_to_le: ∀a,n,m. a + n ≤ a + m → n ≤ m.
548 #a (elim a) normalize /3/ qed. 
549
550 theorem le_plus_to_le_r: ∀a,n,m. n + a ≤ m +a → n ≤ m.
551 /2/ qed. 
552
553 (* plus & lt *)
554
555 theorem monotonic_lt_plus_r: 
556 ∀n:nat.monotonic nat lt (λm.n+m).
557 /2/ qed.
558
559 (*
560 variant lt_plus_r: \forall n,p,q:nat. p < q \to n + p < n + q \def
561 monotonic_lt_plus_r. *)
562
563 theorem monotonic_lt_plus_l: 
564 ∀n:nat.monotonic nat lt (λm.m+n).
565 /2/ qed.
566
567 (*
568 variant lt_plus_l: \forall n,p,q:nat. p < q \to p + n < q + n \def
569 monotonic_lt_plus_l. *)
570
571 theorem lt_plus: ∀n,m,p,q:nat. n < m → p < q → n + p < m + q.
572 #n #m #p #q #ltnm #ltpq
573 @(transitive_lt ? (n+q))/2/ qed.
574
575 theorem lt_plus_to_lt_l :∀n,p,q:nat. p+n < q+n → p<q.
576 /2/ qed.
577
578 theorem lt_plus_to_lt_r :∀n,p,q:nat. n+p < n+q → p<q.
579 /2/ qed.
580
581 (*
582 theorem le_to_lt_to_lt_plus: ∀a,b,c,d:nat.
583 a ≤ c → b < d → a + b < c+d.
584 (* bello /2/ un po' lento *)
585 #a #b #c #d #leac #lebd 
586 normalize napplyS le_plus // qed.
587 *)
588
589 (* times *)
590 theorem monotonic_le_times_r: 
591 ∀n:nat.monotonic nat le (λm. n * m).
592 #n #x #y #lexy (elim n) normalize//(* lento /2/*)
593 #a #lea @le_plus //
594 qed.
595
596 (*
597 theorem le_times_r: \forall p,n,m:nat. n \le m \to p*n \le p*m
598 \def monotonic_le_times_r. *)
599
600 (*
601 theorem monotonic_le_times_l: 
602 ∀m:nat.monotonic nat le (λn.n*m).
603 /2/ qed.
604 *)
605
606 (*
607 theorem le_times_l: \forall p,n,m:nat. n \le m \to n*p \le m*p
608 \def monotonic_le_times_l. *)
609
610 theorem le_times: ∀n1,n2,m1,m2:nat. 
611 n1 ≤ n2  → m1 ≤ m2 → n1*m1 ≤ n2*m2.
612 #n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1*m2)) /2/
613 qed.
614
615 (* interessante *)
616 theorem lt_times_n: ∀n,m:nat. O < n → m ≤ n*m.
617 #n #m #H /2/ qed.
618
619 theorem le_times_to_le: 
620 ∀a,n,m. O < a → a * n ≤ a * m → n ≤ m.
621 #a @nat_elim2 normalize
622   [//
623   |#n #H1 #H2 
624      @(transitive_le ? (a*S n)) /2/
625   |#n #m #H #lta #le
626      @le_S_S @H /2/
627   ]
628 qed.
629
630 (*
631 theorem le_S_times_2: ∀n,m.O < m → n ≤ m → S n ≤ 2*m.
632 #n #m #posm #lenm  (* interessante *)
633 applyS (le_plus n m) // qed. *)
634
635 (* times & lt *)
636 (*
637 theorem lt_O_times_S_S: ∀n,m:nat.O < (S n)*(S m).
638 intros.simplify.unfold lt.apply le_S_S.apply le_O_n.
639 qed. *)
640
641 (*
642 theorem lt_times_eq_O: \forall a,b:nat.
643 O < a → a * b = O → b = O.
644 intros.
645 apply (nat_case1 b)
646 [ intros.
647   reflexivity
648 | intros.
649   rewrite > H2 in H1.
650   rewrite > (S_pred a) in H1
651   [ apply False_ind.
652     apply (eq_to_not_lt O ((S (pred a))*(S m)))
653     [ apply sym_eq.
654       assumption
655     | apply lt_O_times_S_S
656     ]
657   | assumption
658   ]
659 ]
660 qed. 
661
662 theorem O_lt_times_to_O_lt: \forall a,c:nat.
663 O \lt (a * c) \to O \lt a.
664 intros.
665 apply (nat_case1 a)
666 [ intros.
667   rewrite > H1 in H.
668   simplify in H.
669   assumption
670 | intros.
671   apply lt_O_S
672 ]
673 qed.
674
675 lemma lt_times_to_lt_O: \forall i,n,m:nat. i < n*m \to O < m.
676 intros.
677 elim (le_to_or_lt_eq O ? (le_O_n m))
678   [assumption
679   |apply False_ind.
680    rewrite < H1 in H.
681    rewrite < times_n_O in H.
682    apply (not_le_Sn_O ? H)
683   ]
684 qed. *)
685
686 (*
687 theorem monotonic_lt_times_r: 
688 ∀n:nat.monotonic nat lt (λm.(S n)*m).
689 /2/ 
690 simplify.
691 intros.elim n.
692 simplify.rewrite < plus_n_O.rewrite < plus_n_O.assumption.
693 apply lt_plus.assumption.assumption.
694 qed. *)
695
696 theorem monotonic_lt_times_l: 
697   ∀c:nat. O < c → monotonic nat lt (λt.(t*c)).
698 #c #posc #n #m #ltnm
699 (elim ltnm) normalize
700   [/2/ 
701   |#a #_ #lt1 @(transitive_le … lt1) //
702   ]
703 qed.
704
705 theorem monotonic_lt_times_r: 
706   ∀c:nat. O < c → monotonic nat lt (λt.(c*t)).
707 /2/ qed.
708
709 theorem lt_to_le_to_lt_times: 
710 ∀n,m,p,q:nat. n < m → p ≤ q → O < q → n*p < m*q.
711 #n #m #p #q #ltnm #lepq #posq
712 @(le_to_lt_to_lt ? (n*q))
713   [@monotonic_le_times_r //
714   |@monotonic_lt_times_l //
715   ]
716 qed.
717
718 theorem lt_times:∀n,m,p,q:nat. n<m → p<q → n*p < m*q.
719 #n #m #p #q #ltnm #ltpq @lt_to_le_to_lt_times/2/
720 qed.
721
722 theorem lt_times_n_to_lt_l: 
723 ∀n,p,q:nat. p*n < q*n → p < q.
724 #n #p #q #Hlt (elim (decidable_lt p q)) //
725 #nltpq @False_ind @(absurd ? ? (lt_to_not_le ? ? Hlt))
726 applyS monotonic_le_times_r /2/
727 qed.
728
729 theorem lt_times_n_to_lt_r: 
730 ∀n,p,q:nat. n*p < n*q → p < q.
731 /2/ qed.
732
733 (*
734 theorem nat_compare_times_l : \forall n,p,q:nat. 
735 nat_compare p q = nat_compare ((S n) * p) ((S n) * q).
736 intros.apply nat_compare_elim.intro.
737 apply nat_compare_elim.
738 intro.reflexivity.
739 intro.absurd (p=q).
740 apply (inj_times_r n).assumption.
741 apply lt_to_not_eq. assumption.
742 intro.absurd (q<p).
743 apply (lt_times_to_lt_r n).assumption.
744 apply le_to_not_lt.apply lt_to_le.assumption.
745 intro.rewrite < H.rewrite > nat_compare_n_n.reflexivity.
746 intro.apply nat_compare_elim.intro.
747 absurd (p<q).
748 apply (lt_times_to_lt_r n).assumption.
749 apply le_to_not_lt.apply lt_to_le.assumption.
750 intro.absurd (q=p).
751 symmetry.
752 apply (inj_times_r n).assumption.
753 apply lt_to_not_eq.assumption.
754 intro.reflexivity.
755 qed. *)
756
757 (* times and plus 
758 theorem lt_times_plus_times: \forall a,b,n,m:nat. 
759 a < n \to b < m \to a*m + b < n*m.
760 intros 3.
761 apply (nat_case n)
762   [intros.apply False_ind.apply (not_le_Sn_O ? H)
763   |intros.simplify.
764    rewrite < sym_plus.
765    unfold.
766    change with (S b+a*m1 \leq m1+m*m1).
767    apply le_plus
768     [assumption
769     |apply le_times
770       [apply le_S_S_to_le.assumption
771       |apply le_n
772       ]
773     ]
774   ]
775 qed. *)
776
777 (************************** minus ******************************)
778
779 let rec minus n m ≝ 
780  match n with 
781  [ O ⇒ O
782  | S p ⇒ 
783         match m with
784           [ O ⇒ S p
785     | S q ⇒ minus p q ]].
786         
787 interpretation "natural minus" 'minus x y = (minus x y).
788
789 theorem minus_S_S: ∀n,m:nat.S n - S m = n -m.
790 // qed.
791
792 theorem minus_O_n: ∀n:nat.O=O-n.
793 #n (cases n) // qed.
794
795 theorem minus_n_O: ∀n:nat.n=n-O.
796 #n (cases n) // qed.
797
798 theorem minus_n_n: ∀n:nat.O=n-n.
799 #n (elim n) // qed.
800
801 theorem minus_Sn_n: ∀n:nat. S O = (S n)-n.
802 #n (elim n) normalize // qed.
803
804 theorem minus_Sn_m: ∀m,n:nat. m ≤ n → S n -m = S (n-m).
805 (* qualcosa da capire qui 
806 #n #m #lenm nelim lenm napplyS refl_eq. *)
807 @nat_elim2 
808   [//
809   |#n #abs @False_ind /2/ 
810   |#n #m #Hind #c applyS Hind /2/
811   ]
812 qed.
813
814 (*
815 theorem not_eq_to_le_to_le_minus: 
816   ∀n,m.n ≠ m → n ≤ m → n ≤ m - 1.
817 #n * #m (cases m// #m normalize
818 #H #H1 napply le_S_S_to_le
819 napplyS (not_eq_to_le_to_lt n (S m) H H1)
820 qed. *)
821
822 theorem eq_minus_S_pred: ∀n,m. n - (S m) = pred(n -m).
823 @nat_elim2 normalize // qed.
824
825 theorem plus_minus:
826 ∀m,n,p:nat. m ≤ n → (n-m)+p = (n+p)-m.
827 @nat_elim2 
828   [//
829   |#n #p #abs @False_ind /2/
830   |normalize/3/
831   ]
832 qed.
833
834 theorem minus_plus_m_m: ∀n,m:nat.n = (n+m)-m.
835 /2/ qed.
836
837 theorem plus_minus_m_m: ∀n,m:nat.
838   m ≤ n → n = (n-m)+m.
839 #n #m #lemn @sym_eq /2/ qed.
840
841 theorem le_plus_minus_m_m: ∀n,m:nat. n ≤ (n-m)+m.
842 #n (elim n) // #a #Hind #m (cases m) // normalize #n/2/  
843 qed.
844
845 theorem minus_to_plus :∀n,m,p:nat.
846   m ≤ n → n-m = p → n = m+p.
847 #n #m #p #lemn #eqp (applyS plus_minus_m_m) //
848 qed.
849
850 theorem plus_to_minus :∀n,m,p:nat.n = m+p → n-m = p.
851 #n #m #p #eqp @sym_eq (applyS (minus_plus_m_m p m))
852 qed.
853
854 theorem minus_pred_pred : ∀n,m:nat. O < n → O < m → 
855 pred n - pred m = n - m.
856 #n #m #posn #posm @(lt_O_n_elim n posn) @(lt_O_n_elim m posm) //.
857 qed.
858
859 (*
860
861 theorem le_SO_minus: \forall n,m:nat.S n \leq m \to S O \leq m-n.
862 intros.elim H.elim (minus_Sn_n n).apply le_n.
863 rewrite > minus_Sn_m.
864 apply le_S.assumption.
865 apply lt_to_le.assumption.
866 qed.
867
868 theorem minus_le_S_minus_S: \forall n,m:nat. m-n \leq S (m-(S n)).
869 intros.
870 apply (nat_elim2 (\lambda n,m.m-n \leq S (m-(S n)))).
871 intro.elim n1.simplify.apply le_n_Sn.
872 simplify.rewrite < minus_n_O.apply le_n.
873 intros.simplify.apply le_n_Sn.
874 intros.simplify.apply H.
875 qed.
876
877 theorem lt_minus_S_n_to_le_minus_n : \forall n,m,p:nat. m-(S n) < p \to m-n \leq p. 
878 intros 3.intro.
879 (* autobatch *)
880 (* end auto($Revision: 9739 $) proof: TIME=1.33 SIZE=100 DEPTH=100 *)
881 apply (trans_le (m-n) (S (m-(S n))) p).
882 apply minus_le_S_minus_S.
883 assumption.
884 qed.
885
886 theorem le_minus_m: \forall n,m:nat. n-m \leq n.
887 intros.apply (nat_elim2 (\lambda m,n. n-m \leq n)).
888 intros.rewrite < minus_n_O.apply le_n.
889 intros.simplify.apply le_n.
890 intros.simplify.apply le_S.assumption.
891 qed.
892
893 theorem lt_minus_m: \forall n,m:nat. O < n \to O < m \to n-m \lt n.
894 intros.apply (lt_O_n_elim n H).intro.
895 apply (lt_O_n_elim m H1).intro.
896 simplify.unfold lt.apply le_S_S.apply le_minus_m.
897 qed.
898
899 theorem minus_le_O_to_le: \forall n,m:nat. n-m \leq O \to n \leq m.
900 intros 2.
901 apply (nat_elim2 (\lambda n,m:nat.n-m \leq O \to n \leq m)).
902 intros.apply le_O_n.
903 simplify.intros. assumption.
904 simplify.intros.apply le_S_S.apply H.assumption.
905 qed.
906 *)
907
908 (* monotonicity and galois *)
909
910 theorem monotonic_le_minus_l: 
911 ∀p,q,n:nat. q ≤ p → q-n ≤ p-n.
912 @nat_elim2 #p #q
913   [#lePO @(le_n_O_elim ? lePO) //
914   |//
915   |#Hind #n (cases n) // #a #leSS @Hind /2/
916   ]
917 qed.
918
919 theorem le_minus_to_plus: ∀n,m,p. n-m ≤ p → n≤ p+m.
920 #n #m #p #lep @transitive_le
921   [|@le_plus_minus_m_m | @monotonic_le_plus_l // ]
922 qed.
923
924 theorem le_plus_to_minus: ∀n,m,p. n ≤ p+m → n-m ≤ p.
925 #n #m #p #lep /2/ qed.
926
927 theorem monotonic_le_minus_r: 
928 ∀p,q,n:nat. q ≤ p → n-p ≤ n-q.
929 #p #q #n #lepq @le_plus_to_minus
930 @(transitive_le … (le_plus_minus_m_m ? q)) /2/
931 qed.
932
933 theorem eq_minus_O: ∀n,m:nat.
934   n ≤ m → n-m = O.
935 #n #m #lenm @(le_n_O_elim (n-m)) /2/
936 qed.
937
938 theorem distributive_times_minus: distributive ? times minus.
939 #a #b #c
940 (cases (decidable_lt b c)) #Hbc
941  [>(eq_minus_O …) /2/ >(eq_minus_O …) // 
942   @monotonic_le_times_r /2/
943  |@sym_eq (applyS plus_to_minus) <(distributive_times_plus …) 
944  (* STRANO *)
945   @(eq_f …b) (applyS plus_minus_m_m) /2/
946 qed.
947
948 (*********************** boolean arithmetics ********************) 
949 include "basics/bool.ma".
950
951 let rec eqb n m ≝ 
952 match n with 
953   [ O ⇒ match m with [ O ⇒ true | S q ⇒ false] 
954   | S p ⇒ match m with [ O ⇒ false | S q ⇒ eqb p q]
955   ].
956
957 theorem eqb_elim : ∀ n,m:nat.∀ P:bool → Prop.
958 (n=m → (P true)) → (n ≠ m → (P false)) → (P (eqb n m)). 
959 @nat_elim2 
960   [#n (cases n) normalize /3/ 
961   |normalize /3/
962   |normalize /4/ 
963   ] 
964 qed.
965
966 theorem eqb_n_n: ∀n. eqb n n = true.
967 #n (elim n) normalize // qed. 
968
969 theorem eqb_true_to_eq: ∀n,m:nat. eqb n m = true → n = m.
970 #n #m @(eqb_elim n m) // #_ #abs @False_ind /2/ qed.
971
972 theorem eqb_false_to_not_eq: ∀n,m:nat. eqb n m = false → n ≠ m.
973 #n #m @(eqb_elim n m) /2/ qed.
974
975 theorem eq_to_eqb_true: ∀n,m:nat.n = m → eqb n m = true.
976 // qed.
977
978 theorem not_eq_to_eqb_false: ∀n,m:nat.
979   n ≠  m → eqb n m = false.
980 #n #m #noteq @eqb_elim// #Heq @False_ind /2/ qed.
981
982 let rec leb n m ≝ 
983 match n with 
984     [ O ⇒ true
985     | (S p) ⇒
986         match m with 
987         [ O ⇒ false
988               | (S q) ⇒ leb p q]].
989
990 theorem leb_elim: ∀n,m:nat. ∀P:bool → Prop. 
991 (n ≤ m → P true) → (n ≰ m → P false) → P (leb n m).
992 @nat_elim2 normalize
993   [/2/
994   |/3/
995   |#n #m #Hind #P #Pt #Pf @Hind
996     [#lenm @Pt @le_S_S // |#nlenm @Pf /2/ ]
997   ]
998 qed.
999
1000 theorem leb_true_to_le:∀n,m.leb n m = true → n ≤ m.
1001 #n #m @leb_elim // #_ #abs @False_ind /2/ qed.
1002
1003 theorem leb_false_to_not_le:∀n,m.
1004   leb n m = false → n ≰ m.
1005 #n #m @leb_elim // #_ #abs @False_ind /2/ qed.
1006
1007 theorem le_to_leb_true: ∀n,m. n ≤ m → leb n m = true.
1008 #n #m @leb_elim // #H #H1 @False_ind /2/ qed.
1009
1010 theorem not_le_to_leb_false: ∀n,m. n ≰ m → leb n m = false.
1011 #n #m @leb_elim // #H #H1 @False_ind /2/ qed.
1012
1013 theorem lt_to_leb_false: ∀n,m. m < n → leb n m = false.
1014 /3/ qed.
1015
1016 (* serve anche ltb? 
1017 ndefinition ltb ≝λn,m. leb (S n) m.
1018
1019 theorem ltb_elim: ∀n,m:nat. ∀P:bool → Prop. 
1020 (n < m → P true) → (n ≮ m → P false) → P (ltb n m).
1021 #n #m #P #Hlt #Hnlt
1022 napply leb_elim /3/ qed.
1023
1024 theorem ltb_true_to_lt:∀n,m.ltb n m = true → n < m.
1025 #n #m #Hltb napply leb_true_to_le nassumption
1026 qed.
1027
1028 theorem ltb_false_to_not_lt:∀n,m.
1029   ltb n m = false → n ≮ m.
1030 #n #m #Hltb napply leb_false_to_not_le nassumption
1031 qed.
1032
1033 theorem lt_to_ltb_true: ∀n,m. n < m → ltb n m = true.
1034 #n #m #Hltb napply le_to_leb_true nassumption
1035 qed.
1036
1037 theorem le_to_ltb_false: ∀n,m. m \le n → ltb n m = false.
1038 #n #m #Hltb napply lt_to_leb_false /2/
1039 qed. *)
1040
1041 (* min e max *)
1042 definition min: nat →nat →nat ≝
1043 λn.λm. if_then_else ? (leb n m) n m.
1044
1045 definition max: nat →nat →nat ≝
1046 λn.λm. if_then_else ? (leb n m) m n.
1047
1048 lemma commutative_min: commutative ? min.
1049 #n #m normalize @leb_elim 
1050   [@leb_elim normalize /2/
1051   |#notle >(le_to_leb_true …) // @(transitive_le ? (S m)) /2/
1052   ] qed.
1053
1054 lemma le_minr: ∀i,n,m. i ≤ min n m → i ≤ m.
1055 #i #n #m normalize @leb_elim normalize /2/ qed. 
1056
1057 lemma le_minl: ∀i,n,m. i ≤ min n m → i ≤ n.
1058 /2/ qed.
1059
1060 lemma to_min: ∀i,n,m. i ≤ n → i ≤ m → i ≤ min n m.
1061 #i #n #m #lein #leim normalize (cases (leb n m)) 
1062 normalize // qed.
1063
1064 lemma commutative_max: commutative ? max.
1065 #n #m normalize @leb_elim 
1066   [@leb_elim normalize /2/
1067   |#notle >(le_to_leb_true …) // @(transitive_le ? (S m)) /2/
1068   ] qed.
1069
1070 lemma le_maxl: ∀i,n,m. max n m ≤ i → n ≤ i.
1071 #i #n #m normalize @leb_elim normalize /2/ qed. 
1072
1073 lemma le_maxr: ∀i,n,m. max n m ≤ i → m ≤ i.
1074 /2/ qed.
1075
1076 lemma to_max: ∀i,n,m. n ≤ i → m ≤ i → max n m ≤ i.
1077 #i #n #m #leni #lemi normalize (cases (leb n m)) 
1078 normalize // qed.
1079