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.
7 ||A|| This file is distributed under the terms of the
8 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "basics/relations.ma".
14 inductive nat : Type[0] ≝
18 interpretation "Natural numbers" 'N = nat.
20 alias num (instance 0) = "natural number".
23 λn. match n with [ O ⇒ O | S p ⇒ p].
25 theorem pred_Sn : ∀n. n = pred (S n).
28 theorem injective_S : injective nat nat S.
32 theorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m.
35 theorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m.
38 definition not_zero: nat → Prop ≝
39 λn: nat. match n with [ O ⇒ False | (S p) ⇒ True ].
41 theorem not_eq_O_S : ∀n:nat. O ≠ S n.
42 #n @nmk #eqOS (change with (not_zero O)) >eqOS // qed.
44 theorem not_eq_n_Sn: ∀n:nat. n ≠ S n.
49 (n=O → P O) → (∀m:nat. n= S m → P (S m)) → P n.
50 #n #P (elim n) /2/ qed.
56 → (∀n,m:nat. R n m → R (S n) (S m))
58 #R #ROn #RSO #RSS #n (elim n) // #n0 #Rn0m #m (cases m) /2/ qed.
60 theorem decidable_eq_nat : ∀n,m:nat.decidable (n=m).
61 @nat_elim2 #n [ (cases n) /2/ | /3/ | #m #Hind (cases Hind) /3/]
64 (*************************** plus ******************************)
67 match n with [ O ⇒ m | S p ⇒ S (plus p m) ].
69 interpretation "natural plus" 'plus x y = (plus x y).
71 theorem plus_O_n: ∀n:nat. n = O+n.
75 theorem plus_Sn_m: ∀n,m:nat. S (n + m) = S n + m.
79 theorem plus_n_O: ∀n:nat. n = n+O.
80 #n (elim n) normalize // qed.
82 theorem plus_n_Sm : ∀n,m:nat. S (n+m) = n + S m.
83 #n (elim n) normalize // qed.
86 theorem plus_Sn_m1: ∀n,m:nat. S m + n = n + S m.
87 #n (elim n) normalize // qed.
91 theorem plus_n_1 : ∀n:nat. S n = n+1.
95 theorem commutative_plus: commutative ? plus.
96 #n (elim n) normalize // qed.
98 theorem associative_plus : associative nat plus.
99 #n (elim n) normalize // qed.
101 theorem assoc_plus1: ∀a,b,c. c + (b + a) = b + c + a.
104 theorem injective_plus_r: ∀n:nat.injective nat nat (λm.n+m).
105 #n (elim n) normalize /3/ qed.
107 (* theorem inj_plus_r: \forall p,n,m:nat. p+n = p+m \to n=m
108 \def injective_plus_r.
110 theorem injective_plus_l: ∀m:nat.injective nat nat (λn.n+m).
113 (* theorem inj_plus_l: \forall p,n,m:nat. n+p = m+p \to n=m
114 \def injective_plus_l. *)
116 (*************************** times *****************************)
119 match n with [ O ⇒ O | S p ⇒ m+(times p m) ].
121 interpretation "natural times" 'times x y = (times x y).
123 theorem times_Sn_m: ∀n,m:nat. m+n*m = S n*m.
126 theorem times_O_n: ∀n:nat. O = O*n.
129 theorem times_n_O: ∀n:nat. O = n*O.
132 theorem times_n_Sm : ∀n,m:nat. n+(n*m) = n*(S m).
133 #n (elim n) normalize // qed.
135 theorem commutative_times : commutative nat times.
136 #n (elim n) normalize // qed.
138 (* variant sym_times : \forall n,m:nat. n*m = m*n \def
141 theorem distributive_times_plus : distributive nat times plus.
142 #n (elim n) normalize // qed.
144 theorem distributive_times_plus_r :
145 ∀a,b,c:nat. (b+c)*a = b*a + c*a.
148 theorem associative_times: associative nat times.
149 #n (elim n) normalize // qed.
151 lemma times_times: ∀x,y,z. x*(y*z) = y*(x*z).
154 theorem times_n_1 : ∀n:nat. n = n * 1.
157 (* ci servono questi risultati?
158 theorem times_O_to_O: ∀n,m:nat.n*m=O → n=O ∨ m=O.
160 #n #m #H normalize #H1 napply False_ind napply not_eq_O_S
163 theorem times_n_SO : ∀n:nat. n = n * S O.
166 theorem times_SSO_n : ∀n:nat. n + n = (S(S O)) * n.
169 nlemma times_SSO: \forall n.(S(S O))*(S n) = S(S((S(S O))*n)).
172 theorem or_eq_eq_S: \forall n.\exists m.
173 n = (S(S O))*m \lor n = S ((S(S O))*m).
176 ##|#a #H nelim H #b#ornelim or#aeq
183 (******************** ordering relations ************************)
185 inductive le (n:nat) : nat → Prop ≝
187 | le_S : ∀ m:nat. le n m → le n (S m).
189 interpretation "natural 'less or equal to'" 'leq x y = (le x y).
191 interpretation "natural 'neither less nor equal to'" 'nleq x y = (Not (le x y)).
193 definition lt: nat → nat → Prop ≝ λn,m. S n ≤ m.
195 interpretation "natural 'less than'" 'lt x y = (lt x y).
196 interpretation "natural 'not less than'" 'nless x y = (Not (lt x y)).
198 (* lemma eq_lt: ∀n,m. (n < m) = (S n ≤ m).
201 definition ge: nat → nat → Prop ≝ λn,m.m ≤ n.
203 interpretation "natural 'greater or equal to'" 'geq x y = (ge x y).
205 definition gt: nat → nat → Prop ≝ λn,m.m<n.
207 interpretation "natural 'greater than'" 'gt x y = (gt x y).
208 interpretation "natural 'not greater than'" 'ngtr x y = (Not (gt x y)).
210 theorem transitive_le : transitive nat le.
211 #a #b #c #leab #lebc (elim lebc) /2/
215 theorem trans_le: \forall n,m,p:nat. n \leq m \to m \leq p \to n \leq p
216 \def transitive_le. *)
218 theorem transitive_lt: transitive nat lt.
219 #a #b #c #ltab #ltbc (elim ltbc) /2/qed.
222 theorem trans_lt: \forall n,m,p:nat. lt n m \to lt m p \to lt n p
223 \def transitive_lt. *)
225 theorem le_S_S: ∀n,m:nat. n ≤ m → S n ≤ S m.
226 #n #m #lenm (elim lenm) /2/ qed.
228 theorem le_O_n : ∀n:nat. O ≤ n.
231 theorem le_n_Sn : ∀n:nat. n ≤ S n.
234 theorem le_pred_n : ∀n:nat. pred n ≤ n.
237 theorem monotonic_pred: monotonic ? le pred.
238 #n #m #lenm (elim lenm) /2/ qed.
240 theorem le_S_S_to_le: ∀n,m:nat. S n ≤ S m → n ≤ m.
244 (* this are instances of the le versions
245 theorem lt_S_S_to_lt: ∀n,m. S n < S m → n < m.
248 theorem lt_to_lt_S_S: ∀n,m. n < m → S n < S m.
251 theorem lt_to_not_zero : ∀n,m:nat. n < m → not_zero m.
252 #n #m #Hlt (elim Hlt) // qed.
255 theorem not_le_Sn_O: ∀ n:nat. S n ≰ O.
256 #n @nmk #Hlen0 @(lt_to_not_zero ?? Hlen0) qed.
258 theorem not_le_to_not_le_S_S: ∀ n,m:nat. n ≰ m → S n ≰ S m.
261 theorem not_le_S_S_to_not_le: ∀ n,m:nat. S n ≰ S m → n ≰ m.
264 theorem decidable_le: ∀n,m. decidable (n≤m).
265 @nat_elim2 #n /2/ #m * /3/ qed.
267 theorem decidable_lt: ∀n,m. decidable (n < m).
268 #n #m @decidable_le qed.
270 theorem not_le_Sn_n: ∀n:nat. S n ≰ n.
273 (* this is le_S_S_to_le
274 theorem lt_S_to_le: ∀n,m:nat. n < S m → n ≤ m.
278 lemma le_gen: ∀P:nat → Prop.∀n.(∀i. i ≤ n → P i) → P n.
281 theorem not_le_to_lt: ∀n,m. n ≰ m → m < n.
285 |#m #Hind #HnotleSS @le_S_S /3/
289 theorem lt_to_not_le: ∀n,m. n < m → m ≰ n.
290 #n #m #Hltnm (elim Hltnm) /3/ qed.
292 theorem not_lt_to_le: ∀n,m:nat. n ≮ m → m ≤ n.
295 theorem le_to_not_lt: ∀n,m:nat. n ≤ m → m ≮ n.
296 #n #m #H @lt_to_not_le /2/ (* /3/ *) qed.
298 (* lt and le trans *)
300 theorem lt_to_le_to_lt: ∀n,m,p:nat. n < m → m ≤ p → n < p.
301 #n #m #p #H #H1 (elim H1) /2/ qed.
303 theorem le_to_lt_to_lt: ∀n,m,p:nat. n ≤ m → m < p → n < p.
304 #n #m #p #H (elim H) /3/ qed.
306 theorem lt_S_to_lt: ∀n,m. S n < m → n < m.
309 theorem ltn_to_ltO: ∀n,m:nat. n < m → O < m.
313 theorem lt_SO_n_to_lt_O_pred_n: \forall n:nat.
314 (S O) \lt n \to O \lt (pred n).
316 apply (ltn_to_ltO (pred (S O)) (pred n) ?).
317 apply (lt_pred (S O) n)
323 theorem lt_O_n_elim: ∀n:nat. O < n →
324 ∀P:nat → Prop.(∀m:nat.P (S m)) → P n.
325 #n (elim n) // #abs @False_ind /2/
328 theorem S_pred: ∀n. 0 < n → S(pred n) = n.
329 #n #posn (cases posn) //
333 theorem lt_pred: \forall n,m.
334 O < n \to n < m \to pred n < pred m.
336 [intros.apply False_ind.apply (not_le_Sn_O ? H)
337 |intros.apply False_ind.apply (not_le_Sn_O ? H1)
338 |intros.simplify.unfold.apply le_S_S_to_le.assumption
342 theorem le_pred_to_le:
343 ∀n,m. O < m → pred n ≤ pred m → n ≤ m.
359 theorem le_to_or_lt_eq: ∀n,m:nat. n ≤ m → n < m ∨ n = m.
360 #n #m #lenm (elim lenm) /3/ qed.
363 theorem lt_to_not_eq : ∀n,m:nat. n < m → n ≠ m.
364 #n #m #H @not_to_not /2/ qed.
367 theorem eq_to_not_lt: ∀a,b:nat. a = b → a ≮ b.
372 apply (lt_to_not_eq b b)
378 theorem lt_n_m_to_not_lt_m_Sn: ∀n,m. n < m → m ≮ S n.
384 generalize in match (le_S_S ? ? H)
386 generalize in match (transitive_le ? ? ? H2 H1)
388 apply (not_le_Sn_n ? H3).
391 theorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n<m.
392 #n #m #Hneq #Hle cases (le_to_or_lt_eq ?? Hle) //
395 nelim (Hneq Heq) qed. *)
398 theorem le_n_O_to_eq : ∀n:nat. n ≤ O → O=n.
399 #n (cases n) // #a #abs @False_ind /2/ qed.
401 theorem le_n_O_elim: ∀n:nat. n ≤ O → ∀P: nat →Prop. P O → P n.
402 #n (cases n) // #a #abs @False_ind /2/ qed.
404 theorem le_n_Sm_elim : ∀n,m:nat.n ≤ S m →
405 ∀P:Prop. (S n ≤ S m → P) → (n=S m → P) → P.
406 #n #m #Hle #P (elim Hle) /3/ qed.
410 theorem le_to_le_to_eq: ∀n,m. n ≤ m → m ≤ n → n = m.
414 theorem lt_O_S : ∀n:nat. O < S n.
418 (* other abstract properties *)
419 theorem antisymmetric_le : antisymmetric nat le.
420 unfold antisymmetric.intros 2.
421 apply (nat_elim2 (\lambda n,m.(n \leq m \to m \leq n \to n=m))).
422 intros.apply le_n_O_to_eq.assumption.
423 intros.apply False_ind.apply (not_le_Sn_O ? H).
424 intros.apply eq_f.apply H.
425 apply le_S_S_to_le.assumption.
426 apply le_S_S_to_le.assumption.
429 theorem antisym_le: \forall n,m:nat. n \leq m \to m \leq n \to n=m
430 \def antisymmetric_le.
432 theorem le_n_m_to_lt_m_Sn_to_eq_n_m: ∀n,m. n ≤ m → m < S n → n=m.
435 generalize in match (le_S_S_to_le ? ? H1)
442 (* well founded induction principles *)
444 theorem nat_elim1 : ∀n:nat.∀P:nat → Prop.
445 (∀m.(∀p. p < m → P p) → P m) → P n.
447 cut (∀q:nat. q ≤ n → P q) /2/
449 [#q #HleO (* applica male *)
450 @(le_n_O_elim ? HleO)
451 @H #p #ltpO @False_ind /2/ (* 3 *)
453 @H #a #lta @Hind @le_S_S_to_le /2/
457 (* some properties of functions *)
459 definition increasing ≝ λf:nat → nat. ∀n:nat. f n < f (S n).
461 theorem increasing_to_monotonic: ∀f:nat → nat.
462 increasing f → monotonic nat lt f.
463 #f #incr #n #m #ltnm (elim ltnm) /2/
466 theorem le_n_fn: ∀f:nat → nat.
467 increasing f → ∀n:nat. n ≤ f n.
468 #f #incr #n (elim n) /2/
471 theorem increasing_to_le: ∀f:nat → nat.
472 increasing f → ∀m:nat.∃i.m ≤ f i.
473 #f #incr #m (elim m) /2/#n * #a #lenfa
474 @(ex_intro ?? (S a)) /2/
477 theorem increasing_to_le2: ∀f:nat → nat. increasing f →
478 ∀m:nat. f 0 ≤ m → ∃i. f i ≤ m ∧ m < f (S i).
479 #f #incr #m #lem (elim lem)
480 [@(ex_intro ? ? O) /2/
481 |#n #len * #a * #len #ltnr (cases(le_to_or_lt_eq … ltnr)) #H
482 [@(ex_intro ? ? a) % /2/
483 |@(ex_intro ? ? (S a)) % //
488 theorem increasing_to_injective: ∀f:nat → nat.
489 increasing f → injective nat nat f.
490 #f #incr #n #m cases(decidable_le n m)
491 [#lenm cases(le_to_or_lt_eq … lenm) //
492 #lenm #eqf @False_ind @(absurd … eqf) @lt_to_not_eq
493 @increasing_to_monotonic //
494 |#nlenm #eqf @False_ind @(absurd … eqf) @sym_not_eq
495 @lt_to_not_eq @increasing_to_monotonic /2/
499 (*********************** monotonicity ***************************)
500 theorem monotonic_le_plus_r:
501 ∀n:nat.monotonic nat le (λm.n + m).
502 #n #a #b (elim n) normalize //
503 #m #H #leab @le_S_S /2/ qed.
506 theorem le_plus_r: ∀p,n,m:nat. n ≤ m → p + n ≤ p + m
507 ≝ monotonic_le_plus_r. *)
509 theorem monotonic_le_plus_l:
510 ∀m:nat.monotonic nat le (λn.n + m).
514 theorem le_plus_l: \forall p,n,m:nat. n \le m \to n + p \le m + p
515 \def monotonic_le_plus_l. *)
517 theorem le_plus: ∀n1,n2,m1,m2:nat. n1 ≤ n2 → m1 ≤ m2
519 #n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1+m2))
522 theorem le_plus_n :∀n,m:nat. m ≤ n + m.
525 lemma le_plus_a: ∀a,n,m. n ≤ m → n ≤ a + m.
528 lemma le_plus_b: ∀b,n,m. n + b ≤ m → n ≤ m.
531 theorem le_plus_n_r :∀n,m:nat. m ≤ m + n.
534 theorem eq_plus_to_le: ∀n,m,p:nat.n=m+p → m ≤ n.
537 theorem le_plus_to_le: ∀a,n,m. a + n ≤ a + m → n ≤ m.
538 #a (elim a) normalize /3/ qed.
540 theorem le_plus_to_le_r: ∀a,n,m. n + a ≤ m +a → n ≤ m.
545 theorem monotonic_lt_plus_r:
546 ∀n:nat.monotonic nat lt (λm.n+m).
550 variant lt_plus_r: \forall n,p,q:nat. p < q \to n + p < n + q \def
551 monotonic_lt_plus_r. *)
553 theorem monotonic_lt_plus_l:
554 ∀n:nat.monotonic nat lt (λm.m+n).
558 variant lt_plus_l: \forall n,p,q:nat. p < q \to p + n < q + n \def
559 monotonic_lt_plus_l. *)
561 theorem lt_plus: ∀n,m,p,q:nat. n < m → p < q → n + p < m + q.
562 #n #m #p #q #ltnm #ltpq
563 @(transitive_lt ? (n+q))/2/ qed.
565 theorem lt_plus_to_lt_l :∀n,p,q:nat. p+n < q+n → p<q.
568 theorem lt_plus_to_lt_r :∀n,p,q:nat. n+p < n+q → p<q.
572 theorem le_to_lt_to_lt_plus: ∀a,b,c,d:nat.
573 a ≤ c → b < d → a + b < c+d.
574 (* bello /2/ un po' lento *)
575 #a #b #c #d #leac #lebd
576 normalize napplyS le_plus // qed.
580 theorem monotonic_le_times_r:
581 ∀n:nat.monotonic nat le (λm. n * m).
582 #n #x #y #lexy (elim n) normalize//(* lento /2/*)
587 theorem le_times_r: \forall p,n,m:nat. n \le m \to p*n \le p*m
588 \def monotonic_le_times_r. *)
591 theorem monotonic_le_times_l:
592 ∀m:nat.monotonic nat le (λn.n*m).
597 theorem le_times_l: \forall p,n,m:nat. n \le m \to n*p \le m*p
598 \def monotonic_le_times_l. *)
600 theorem le_times: ∀n1,n2,m1,m2:nat.
601 n1 ≤ n2 → m1 ≤ m2 → n1*m1 ≤ n2*m2.
602 #n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1*m2)) /2/
606 theorem lt_times_n: ∀n,m:nat. O < n → m ≤ n*m.
609 theorem le_times_to_le:
610 ∀a,n,m. O < a → a * n ≤ a * m → n ≤ m.
611 #a @nat_elim2 normalize
614 @(transitive_le ? (a*S n)) /2/
621 theorem le_S_times_2: ∀n,m.O < m → n ≤ m → S n ≤ 2*m.
622 #n #m #posm #lenm (* interessante *)
623 applyS (le_plus n m) // qed. *)
627 theorem lt_O_times_S_S: ∀n,m:nat.O < (S n)*(S m).
628 intros.simplify.unfold lt.apply le_S_S.apply le_O_n.
632 theorem lt_times_eq_O: \forall a,b:nat.
633 O < a → a * b = O → b = O.
640 rewrite > (S_pred a) in H1
642 apply (eq_to_not_lt O ((S (pred a))*(S m)))
645 | apply lt_O_times_S_S
652 theorem O_lt_times_to_O_lt: \forall a,c:nat.
653 O \lt (a * c) \to O \lt a.
665 lemma lt_times_to_lt_O: \forall i,n,m:nat. i < n*m \to O < m.
667 elim (le_to_or_lt_eq O ? (le_O_n m))
671 rewrite < times_n_O in H.
672 apply (not_le_Sn_O ? H)
677 theorem monotonic_lt_times_r:
678 ∀n:nat.monotonic nat lt (λm.(S n)*m).
682 simplify.rewrite < plus_n_O.rewrite < plus_n_O.assumption.
683 apply lt_plus.assumption.assumption.
686 theorem monotonic_lt_times_r:
687 ∀c:nat. O < c → monotonic nat lt (λt.(c*t)).
689 (elim ltnm) normalize
691 |#a #_ #lt1 @(transitive_le … lt1) //
695 theorem monotonic_lt_times_l:
696 ∀c:nat. O < c → monotonic nat lt (λt.(t*c)).
700 theorem lt_to_le_to_lt_times:
701 ∀n,m,p,q:nat. n < m → p ≤ q → O < q → n*p < m*q.
702 #n #m #p #q #ltnm #lepq #posq
703 @(le_to_lt_to_lt ? (n*q))
704 [@monotonic_le_times_r //
705 |@monotonic_lt_times_l //
709 theorem lt_times:∀n,m,p,q:nat. n<m → p<q → n*p < m*q.
710 #n #m #p #q #ltnm #ltpq @lt_to_le_to_lt_times/2/
713 theorem lt_times_n_to_lt_l:
714 ∀n,p,q:nat. p*n < q*n → p < q.
715 #n #p #q #Hlt (elim (decidable_lt p q)) //
716 #nltpq @False_ind @(absurd ? ? (lt_to_not_le ? ? Hlt))
717 applyS monotonic_le_times_r /2/
720 theorem lt_times_n_to_lt_r:
721 ∀n,p,q:nat. n*p < n*q → p < q.
725 theorem nat_compare_times_l : \forall n,p,q:nat.
726 nat_compare p q = nat_compare ((S n) * p) ((S n) * q).
727 intros.apply nat_compare_elim.intro.
728 apply nat_compare_elim.
731 apply (inj_times_r n).assumption.
732 apply lt_to_not_eq. assumption.
734 apply (lt_times_to_lt_r n).assumption.
735 apply le_to_not_lt.apply lt_to_le.assumption.
736 intro.rewrite < H.rewrite > nat_compare_n_n.reflexivity.
737 intro.apply nat_compare_elim.intro.
739 apply (lt_times_to_lt_r n).assumption.
740 apply le_to_not_lt.apply lt_to_le.assumption.
743 apply (inj_times_r n).assumption.
744 apply lt_to_not_eq.assumption.
749 theorem lt_times_plus_times: \forall a,b,n,m:nat.
750 a < n \to b < m \to a*m + b < n*m.
753 [intros.apply False_ind.apply (not_le_Sn_O ? H)
757 change with (S b+a*m1 \leq m1+m*m1).
761 [apply le_S_S_to_le.assumption
768 (************************** minus ******************************)
776 | S q ⇒ minus p q ]].
778 interpretation "natural minus" 'minus x y = (minus x y).
780 theorem minus_S_S: ∀n,m:nat.S n - S m = n -m.
783 theorem minus_O_n: ∀n:nat.O=O-n.
786 theorem minus_n_O: ∀n:nat.n=n-O.
789 theorem minus_n_n: ∀n:nat.O=n-n.
792 theorem minus_Sn_n: ∀n:nat. S O = (S n)-n.
793 #n (elim n) normalize // qed.
795 theorem minus_Sn_m: ∀m,n:nat. m ≤ n → S n -m = S (n-m).
796 (* qualcosa da capire qui
797 #n #m #lenm nelim lenm napplyS refl_eq. *)
800 |#n #abs @False_ind /2/
801 |#n #m #Hind #c applyS Hind /2/
806 theorem not_eq_to_le_to_le_minus:
807 ∀n,m.n ≠ m → n ≤ m → n ≤ m - 1.
808 #n * #m (cases m// #m normalize
809 #H #H1 napply le_S_S_to_le
810 napplyS (not_eq_to_le_to_lt n (S m) H H1)
813 theorem eq_minus_S_pred: ∀n,m. n - (S m) = pred(n -m).
814 @nat_elim2 normalize // qed.
817 ∀m,n,p:nat. m ≤ n → (n-m)+p = (n+p)-m.
820 |#n #p #abs @False_ind /2/
825 theorem minus_plus_m_m: ∀n,m:nat.n = (n+m)-m.
828 theorem plus_minus_m_m: ∀n,m:nat.
830 #n #m #lemn @sym_eq /2/ qed.
832 theorem le_plus_minus_m_m: ∀n,m:nat. n ≤ (n-m)+m.
833 #n (elim n) // #a #Hind #m (cases m) // normalize #n/2/
836 theorem minus_to_plus :∀n,m,p:nat.
837 m ≤ n → n-m = p → n = m+p.
838 #n #m #p #lemn #eqp (applyS plus_minus_m_m) //
841 theorem plus_to_minus :∀n,m,p:nat.n = m+p → n-m = p.
842 #n #m #p #eqp @sym_eq (applyS (minus_plus_m_m p m))
845 theorem minus_pred_pred : ∀n,m:nat. O < n → O < m →
846 pred n - pred m = n - m.
847 #n #m #posn #posm @(lt_O_n_elim n posn) @(lt_O_n_elim m posm) //.
853 theorem le_SO_minus: \forall n,m:nat.S n \leq m \to S O \leq m-n.
854 intros.elim H.elim (minus_Sn_n n).apply le_n.
855 rewrite > minus_Sn_m.
856 apply le_S.assumption.
857 apply lt_to_le.assumption.
860 theorem minus_le_S_minus_S: \forall n,m:nat. m-n \leq S (m-(S n)).
862 apply (nat_elim2 (\lambda n,m.m-n \leq S (m-(S n)))).
863 intro.elim n1.simplify.apply le_n_Sn.
864 simplify.rewrite < minus_n_O.apply le_n.
865 intros.simplify.apply le_n_Sn.
866 intros.simplify.apply H.
869 theorem lt_minus_S_n_to_le_minus_n : \forall n,m,p:nat. m-(S n) < p \to m-n \leq p.
872 (* end auto($Revision: 9739 $) proof: TIME=1.33 SIZE=100 DEPTH=100 *)
873 apply (trans_le (m-n) (S (m-(S n))) p).
874 apply minus_le_S_minus_S.
878 theorem le_minus_m: \forall n,m:nat. n-m \leq n.
879 intros.apply (nat_elim2 (\lambda m,n. n-m \leq n)).
880 intros.rewrite < minus_n_O.apply le_n.
881 intros.simplify.apply le_n.
882 intros.simplify.apply le_S.assumption.
885 theorem lt_minus_m: \forall n,m:nat. O < n \to O < m \to n-m \lt n.
886 intros.apply (lt_O_n_elim n H).intro.
887 apply (lt_O_n_elim m H1).intro.
888 simplify.unfold lt.apply le_S_S.apply le_minus_m.
891 theorem minus_le_O_to_le: \forall n,m:nat. n-m \leq O \to n \leq m.
893 apply (nat_elim2 (\lambda n,m:nat.n-m \leq O \to n \leq m)).
895 simplify.intros. assumption.
896 simplify.intros.apply le_S_S.apply H.assumption.
900 (* monotonicity and galois *)
902 theorem monotonic_le_minus_l:
903 ∀p,q,n:nat. q ≤ p → q-n ≤ p-n.
905 [#lePO @(le_n_O_elim ? lePO) //
907 |#Hind #n (cases n) // #a #leSS @Hind /2/
911 theorem le_minus_to_plus: ∀n,m,p. n-m ≤ p → n≤ p+m.
912 #n #m #p #lep @transitive_le
913 [|@le_plus_minus_m_m | @monotonic_le_plus_l // ]
916 theorem le_minus_to_plus_r: ∀a,b,c. c ≤ b → a ≤ b - c → a + c ≤ b.
917 #a #b #c #Hlecb #H >(plus_minus_m_m … Hlecb) /2/
920 theorem le_plus_to_minus: ∀n,m,p. n ≤ p+m → n-m ≤ p.
921 #n #m #p #lep /2/ qed.
923 theorem le_plus_to_minus_r: ∀a,b,c. a + b ≤ c → a ≤ c -b.
924 #a #b #c #H @(le_plus_to_le_r … b) /2/
927 theorem lt_minus_to_plus: ∀a,b,c. a - b < c → a < c + b.
928 #a #b #c #H @not_le_to_lt
929 @(not_to_not … (lt_to_not_le …H)) /2/
932 theorem lt_minus_to_plus_r: ∀a,b,c. a < b - c → a + c < b.
933 #a #b #c #H @not_le_to_lt @(not_to_not … (le_plus_to_minus …))
937 theorem lt_plus_to_minus: ∀n,m,p. m ≤ n → n < p+m → n-m < p.
938 #n #m #p #lenm #H normalize <minus_Sn_m // @le_plus_to_minus //
941 theorem lt_plus_to_minus_r: ∀a,b,c. a + b < c → a < c - b.
942 #a #b #c #H @le_plus_to_minus_r //
945 theorem monotonic_le_minus_r:
946 ∀p,q,n:nat. q ≤ p → n-p ≤ n-q.
947 #p #q #n #lepq @le_plus_to_minus
948 @(transitive_le … (le_plus_minus_m_m ? q)) /2/
951 theorem eq_minus_O: ∀n,m:nat.
953 #n #m #lenm @(le_n_O_elim (n-m)) /2/
956 theorem distributive_times_minus: distributive ? times minus.
958 (cases (decidable_lt b c)) #Hbc
959 [> eq_minus_O /2/ >eq_minus_O //
960 @monotonic_le_times_r /2/
961 |@sym_eq (applyS plus_to_minus) <distributive_times_plus
962 @eq_f (applyS plus_minus_m_m) /2/
965 theorem minus_plus: ∀n,m,p. n-m-p = n -(m+p).
967 cases (decidable_le (m+p) n) #Hlt
968 [@plus_to_minus @plus_to_minus <associative_plus
970 |cut (n ≤ m+p) [@(transitive_le … (le_n_Sn …)) @not_le_to_lt //]
971 #H >eq_minus_O /2/ >eq_minus_O //
976 theorem plus_minus: ∀n,m,p. p ≤ m → (n+m)-p = n +(m-p).
977 #n #m #p #lepm @plus_to_minus >(commutative_plus p)
978 >associative_plus <plus_minus_m_m //
981 theorem minus_minus: ∀n,m,p:nat. p ≤ m → m ≤ n →
984 @sym_eq @plus_to_minus <associative_plus <plus_minus_m_m //
985 <commutative_plus <plus_minus_m_m //
988 (*********************** boolean arithmetics ********************)
989 include "basics/bool.ma".
993 [ O ⇒ match m with [ O ⇒ true | S q ⇒ false]
994 | S p ⇒ match m with [ O ⇒ false | S q ⇒ eqb p q]
997 theorem eqb_elim : ∀ n,m:nat.∀ P:bool → Prop.
998 (n=m → (P true)) → (n ≠ m → (P false)) → (P (eqb n m)).
1000 [#n (cases n) normalize /3/
1006 theorem eqb_n_n: ∀n. eqb n n = true.
1007 #n (elim n) normalize // qed.
1009 theorem eqb_true_to_eq: ∀n,m:nat. eqb n m = true → n = m.
1010 #n #m @(eqb_elim n m) // #_ #abs @False_ind /2/ qed.
1012 theorem eqb_false_to_not_eq: ∀n,m:nat. eqb n m = false → n ≠ m.
1013 #n #m @(eqb_elim n m) /2/ qed.
1015 theorem eq_to_eqb_true: ∀n,m:nat.n = m → eqb n m = true.
1018 theorem not_eq_to_eqb_false: ∀n,m:nat.
1019 n ≠ m → eqb n m = false.
1020 #n #m #noteq @eqb_elim// #Heq @False_ind /2/ qed.
1028 | (S q) ⇒ leb p q]].
1030 theorem leb_elim: ∀n,m:nat. ∀P:bool → Prop.
1031 (n ≤ m → P true) → (n ≰ m → P false) → P (leb n m).
1032 @nat_elim2 normalize
1035 |#n #m #Hind #P #Pt #Pf @Hind
1036 [#lenm @Pt @le_S_S // |#nlenm @Pf /2/ ]
1040 theorem leb_true_to_le:∀n,m.leb n m = true → n ≤ m.
1041 #n #m @leb_elim // #_ #abs @False_ind /2/ qed.
1043 theorem leb_false_to_not_le:∀n,m.
1044 leb n m = false → n ≰ m.
1045 #n #m @leb_elim // #_ #abs @False_ind /2/ qed.
1047 theorem le_to_leb_true: ∀n,m. n ≤ m → leb n m = true.
1048 #n #m @leb_elim // #H #H1 @False_ind /2/ qed.
1050 theorem not_le_to_leb_false: ∀n,m. n ≰ m → leb n m = false.
1051 #n #m @leb_elim // #H #H1 @False_ind /2/ qed.
1053 theorem lt_to_leb_false: ∀n,m. m < n → leb n m = false.
1057 ndefinition ltb ≝λn,m. leb (S n) m.
1059 theorem ltb_elim: ∀n,m:nat. ∀P:bool → Prop.
1060 (n < m → P true) → (n ≮ m → P false) → P (ltb n m).
1062 napply leb_elim /3/ qed.
1064 theorem ltb_true_to_lt:∀n,m.ltb n m = true → n < m.
1065 #n #m #Hltb napply leb_true_to_le nassumption
1068 theorem ltb_false_to_not_lt:∀n,m.
1069 ltb n m = false → n ≮ m.
1070 #n #m #Hltb napply leb_false_to_not_le nassumption
1073 theorem lt_to_ltb_true: ∀n,m. n < m → ltb n m = true.
1074 #n #m #Hltb napply le_to_leb_true nassumption
1077 theorem le_to_ltb_false: ∀n,m. m \le n → ltb n m = false.
1078 #n #m #Hltb napply lt_to_leb_false /2/
1082 definition min: nat →nat →nat ≝
1083 λn.λm. if_then_else ? (leb n m) n m.
1085 definition max: nat →nat →nat ≝
1086 λn.λm. if_then_else ? (leb n m) m n.
1088 lemma commutative_min: commutative ? min.
1089 #n #m normalize @leb_elim
1090 [@leb_elim normalize /2/
1091 |#notle >(le_to_leb_true …) // @(transitive_le ? (S m)) /2/
1094 lemma le_minr: ∀i,n,m. i ≤ min n m → i ≤ m.
1095 #i #n #m normalize @leb_elim normalize /2/ qed.
1097 lemma le_minl: ∀i,n,m. i ≤ min n m → i ≤ n.
1100 lemma to_min: ∀i,n,m. i ≤ n → i ≤ m → i ≤ min n m.
1101 #i #n #m #lein #leim normalize (cases (leb n m))
1104 lemma commutative_max: commutative ? max.
1105 #n #m normalize @leb_elim
1106 [@leb_elim normalize /2/
1107 |#notle >(le_to_leb_true …) // @(transitive_le ? (S m)) /2/
1110 lemma le_maxl: ∀i,n,m. max n m ≤ i → n ≤ i.
1111 #i #n #m normalize @leb_elim normalize /2/ qed.
1113 lemma le_maxr: ∀i,n,m. max n m ≤ i → m ≤ i.
1116 lemma to_max: ∀i,n,m. n ≤ i → m ≤ i → max n m ≤ i.
1117 #i #n #m #leni #lemi normalize (cases (leb n m))