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 (* Definitions **************************************************************)
18 inductive nat : Type[0] ≝
22 interpretation "Natural numbers" 'N = nat.
24 alias num (instance 0) = "natural number".
27 λn. match n with [ O ⇒ O | S p ⇒ p].
29 definition not_zero: nat → Prop ≝
30 λn: nat. match n with [ O ⇒ False | (S p) ⇒ True ].
34 inductive le (n:nat) : nat → Prop ≝
36 | le_S : ∀ m:nat. le n m → le n (S m).
38 interpretation "natural 'less or equal to'" 'leq x y = (le x y).
40 interpretation "natural 'neither less nor equal to'" 'nleq x y = (Not (le x y)).
42 definition lt: nat → nat → Prop ≝ λn,m. S n ≤ m.
44 interpretation "natural 'less than'" 'lt x y = (lt x y).
46 interpretation "natural 'not less than'" 'nless x y = (Not (lt x y)).
48 definition ge: nat → nat → Prop ≝ λn,m.m ≤ n.
50 interpretation "natural 'greater or equal to'" 'geq x y = (ge x y).
52 definition gt: nat → nat → Prop ≝ λn,m.m<n.
54 interpretation "natural 'greater than'" 'gt x y = (gt x y).
56 interpretation "natural 'not greater than'" 'ngtr x y = (Not (gt x y)).
58 (* abstract properties *)
60 definition increasing ≝ λf:nat → nat. ∀n:nat. f n < f (S n).
62 (* arithmetic operations *)
65 match n with [ O ⇒ m | S p ⇒ S (plus p m) ].
67 interpretation "natural plus" 'plus x y = (plus x y).
70 match n with [ O ⇒ 0 | S p ⇒ m + (times p m) ].
72 interpretation "natural times" 'times x y = (times x y).
82 interpretation "natural minus" 'minus x y = (minus x y).
84 (* Generic conclusion ******************************************************)
88 (n=O → P O) → (∀m:nat. n= S m → P (S m)) → P n.
95 → (∀n,m:nat. R n m → R (S n) (S m))
97 #R #ROn #RSO #RSS #n elim n // #n0 #Rn0m #m cases m /2/ qed.
99 lemma le_gen: ∀P:nat → Prop.∀n.(∀i. i ≤ n → P i) → P n.
102 (* Equalities ***************************************************************)
104 theorem pred_Sn : ∀n. n = pred (S n).
107 theorem injective_S : injective nat nat S.
110 theorem S_pred: ∀n. 0 < n → S(pred n) = n.
111 #n #posn (cases posn) //
114 theorem plus_O_n: ∀n:nat. n = 0 + n.
117 theorem plus_n_O: ∀n:nat. n = n + 0.
118 #n elim n normalize // qed.
120 theorem plus_n_Sm : ∀n,m:nat. S (n+m) = n + S m.
121 #n elim n normalize // qed.
123 theorem commutative_plus: commutative ? plus.
124 #n elim n normalize // qed.
126 theorem associative_plus : associative nat plus.
127 #n elim n normalize // qed.
129 theorem assoc_plus1: ∀a,b,c. c + (b + a) = b + c + a.
132 theorem injective_plus_r: ∀n:nat.injective nat nat (λm.n+m).
133 #n elim n normalize /3 width=1 by injective_S/ qed.
135 theorem injective_plus_l: ∀n:nat.injective nat nat (λm.m+n).
136 /2 width=2 by injective_plus_r/ qed.
138 theorem times_Sn_m: ∀n,m:nat. m+n*m = S n*m.
141 theorem times_O_n: ∀n:nat. 0 = 0 * n.
144 theorem times_n_O: ∀n:nat. 0 = n * 0.
147 theorem times_n_Sm : ∀n,m:nat. n+(n*m) = n*(S m).
148 #n elim n normalize // qed.
150 theorem commutative_times : commutative nat times.
151 #n elim n normalize // qed.
153 theorem distributive_times_plus : distributive nat times plus.
154 #n elim n normalize // qed.
156 theorem distributive_times_plus_r :
157 ∀a,b,c:nat. (b+c)*a = b*a + c*a.
160 theorem associative_times: associative nat times.
161 #n elim n normalize // qed.
163 lemma times_times: ∀x,y,z. x*(y*z) = y*(x*z).
166 theorem times_n_1 : ∀n:nat. n = n * 1.
169 theorem minus_S_S: ∀n,m:nat.S n - S m = n -m.
172 theorem minus_O_n: ∀n:nat.0=0-n.
175 theorem minus_n_O: ∀n:nat.n=n-0.
178 theorem minus_n_n: ∀n:nat.0=n-n.
181 theorem minus_Sn_n: ∀n:nat. S 0 = (S n)-n.
182 #n elim n normalize // qed.
184 theorem eq_minus_S_pred: ∀n,m. n - (S m) = pred(n -m).
185 @nat_elim2 normalize // qed.
187 lemma plus_plus_comm_23: ∀x,y,z. x + y + z = x + z + y.
190 lemma discr_plus_xy_minus_xz: ∀x,z,y. x + y = x - z → y = 0.
191 #x elim x -x // #x #IHx * normalize
192 [ #y #H @(IHx 0) <minus_n_O /2 width=1 by injective_S/
193 | #z #y >plus_n_Sm #H lapply (IHx … H) -x -z #H destruct
197 (* Negated equalities *******************************************************)
199 theorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m.
200 /2 width=3 by not_to_not/ qed.
202 theorem not_eq_O_S : ∀n:nat. 0 ≠ S n.
203 #n @nmk #eqOS change with (not_zero 0) >eqOS // qed.
205 theorem not_eq_n_Sn: ∀n:nat. n ≠ S n.
206 #n elim n /2 width=1 by not_eq_S/ qed.
208 (* Atomic conclusion *******************************************************)
212 theorem lt_to_not_zero : ∀n,m:nat. n < m → not_zero m.
213 #n #m #Hlt elim Hlt // qed.
217 theorem le_S_S: ∀n,m:nat. n ≤ m → S n ≤ S m.
218 #n #m #lenm elim lenm /2 width=1 by le_S/ qed.
220 theorem le_O_n : ∀n:nat. 0 ≤ n.
221 #n elim n /2 width=1 by le_S/ qed.
223 theorem le_n_Sn : ∀n:nat. n ≤ S n.
224 /2 width=1 by le_S/ qed.
226 theorem transitive_le : transitive nat le.
227 #a #b #c #leab #lebc elim lebc /2 width=1 by le_S/
230 theorem le_pred_n : ∀n:nat. pred n ≤ n.
233 theorem monotonic_pred: monotonic ? le pred.
234 #n #m #lenm elim lenm /2 width=3 by transitive_le/ qed.
236 theorem le_S_S_to_le: ∀n,m:nat. S n ≤ S m → n ≤ m.
238 /2 width=1 by monotonic_pred/ qed-.
240 theorem monotonic_le_plus_r:
241 ∀n:nat.monotonic nat le (λm.n + m).
242 #n #a #b elim n normalize //
243 #m #H #leab /3 width=1 by le_S_S/
246 theorem monotonic_le_plus_l:
247 ∀m:nat.monotonic nat le (λn.n + m).
248 /2 width=1 by monotonic_le_plus_r/ qed.
250 theorem le_plus: ∀n1,n2,m1,m2:nat. n1 ≤ n2 → m1 ≤ m2
252 #n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1+m2))
253 /2 width=1 by monotonic_le_plus_l, monotonic_le_plus_r/ qed.
255 theorem le_plus_n :∀n,m:nat. m ≤ n + m.
256 /2 width=1 by monotonic_le_plus_l/ qed.
258 lemma le_plus_a: ∀a,n,m. n ≤ m → n ≤ a + m.
259 /2 width=1 by le_plus/ qed.
261 lemma le_plus_b: ∀b,n,m. n + b ≤ m → n ≤ m.
262 /2 width=3 by transitive_le/ qed.
264 theorem le_plus_n_r :∀n,m:nat. m ≤ m + n.
267 theorem eq_plus_to_le: ∀n,m,p:nat.n=m+p → m ≤ n.
270 theorem le_plus_to_le: ∀a,n,m. a + n ≤ a + m → n ≤ m.
271 #a elim a normalize /3 width=1 by monotonic_pred/ qed.
273 theorem le_plus_to_le_r: ∀a,n,m. n + a ≤ m +a → n ≤ m.
274 /2 width=2 by le_plus_to_le/ qed-.
276 theorem monotonic_le_times_r:
277 ∀n:nat.monotonic nat le (λm. n * m).
278 #n #x #y #lexy elim n normalize /2 width=1 by le_plus/
281 theorem le_times: ∀n1,n2,m1,m2:nat.
282 n1 ≤ n2 → m1 ≤ m2 → n1*m1 ≤ n2*m2.
283 #n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1*m2))
284 /2 width=1 by monotonic_le_times_r/
288 theorem lt_times_n: ∀n,m:nat. O < n → m ≤ n*m.
289 /2 width=1 by monotonic_le_times_r/ qed.
291 theorem le_times_to_le:
292 ∀a,n,m. O < a → a * n ≤ a * m → n ≤ m.
293 #a @nat_elim2 normalize
296 @(transitive_le ? (a*S n)) /2 width=1 by monotonic_le_times_r/
297 |#n #m #H #lta #le /4 width=2 by le_plus_to_le, le_S_S/
301 theorem le_plus_minus_m_m: ∀n,m:nat. n ≤ (n-m)+m.
302 #n elim n // #a #Hind #m cases m // normalize #n /2 width=1 by le_S_S/
305 theorem le_plus_to_minus_r: ∀a,b,c. a + b ≤ c → a ≤ c -b.
306 #a #b #c #H @(le_plus_to_le_r … b) /2 width=3 by transitive_le/
309 lemma lt_to_le: ∀x,y. x < y → x ≤ y.
310 /2 width=2 by le_plus_b/ qed.
312 lemma inv_eq_minus_O: ∀x,y. x - y = 0 → x ≤ y.
315 lemma le_x_times_x: ∀x. x ≤ x * x.
321 theorem transitive_lt: transitive nat lt.
322 #a #b #c #ltab #ltbc elim ltbc /2 width=1 by le_S/
325 theorem lt_to_le_to_lt: ∀n,m,p:nat. n < m → m ≤ p → n < p.
326 #n #m #p #H #H1 elim H1 /2 width=3 by transitive_lt/ qed.
328 theorem le_to_lt_to_lt: ∀n,m,p:nat. n ≤ m → m < p → n < p.
329 #n #m #p #H elim H /3 width=3 by transitive_lt/ qed.
331 theorem lt_S_to_lt: ∀n,m. S n < m → n < m.
332 /2 width=3 by transitive_lt/ qed.
334 theorem ltn_to_ltO: ∀n,m:nat. n < m → 0 < m.
335 /2 width=3 by lt_to_le_to_lt/ qed.
337 theorem lt_O_S : ∀n:nat. O < S n.
338 /2 width=1 by ltn_to_ltO/ qed.
340 theorem monotonic_lt_plus_r:
341 ∀n:nat.monotonic nat lt (λm.n+m).
342 /2 width=1 by monotonic_le_plus_r/ qed.
344 theorem monotonic_lt_plus_l:
345 ∀n:nat.monotonic nat lt (λm.m+n).
346 /2 width=1 by monotonic_le_plus_r/ qed.
348 theorem lt_plus: ∀n,m,p,q:nat. n < m → p < q → n + p < m + q.
349 #n #m #p #q #ltnm #ltpq
350 @(transitive_lt ? (n+q)) /2 width=1 by monotonic_lt_plus_l, monotonic_le_plus_r/ qed.
352 theorem lt_plus_to_lt_l :∀n,p,q:nat. p+n < q+n → p<q.
353 /2 width=2 by le_plus_to_le/ qed.
355 theorem lt_plus_to_lt_r :∀n,p,q:nat. n+p < n+q → p<q.
356 /2 width=2 by lt_plus_to_lt_l/ qed-.
358 theorem increasing_to_monotonic: ∀f:nat → nat.
359 increasing f → monotonic nat lt f.
360 #f #incr #n #m #ltnm elim ltnm /2 width=3 by transitive_lt/
363 theorem monotonic_lt_times_r:
364 ∀c:nat. O < c → monotonic nat lt (λt.(c*t)).
367 [/2 width=1 by monotonic_lt_plus_l/
368 |#a #_ #lt1 /2 width=3 by transitive_le/
372 theorem monotonic_lt_times_l:
373 ∀c:nat. 0 < c → monotonic nat lt (λt.(t*c)).
374 /2 width=1 by monotonic_lt_times_r/
377 theorem lt_to_le_to_lt_times:
378 ∀n,m,p,q:nat. n < m → p ≤ q → O < q → n*p < m*q.
379 #n #m #p #q #ltnm #lepq #posq
380 @(le_to_lt_to_lt ? (n*q))
381 [/2 width=1 by monotonic_le_times_r/
382 |/2 width=1 by monotonic_lt_times_l/
386 theorem lt_times:∀n,m,p,q:nat. n<m → p<q → n*p < m*q.
387 /3 width=2 by lt_to_le_to_lt_times, ltn_to_ltO, lt_to_le/
390 theorem lt_plus_to_minus_r: ∀a,b,c. a + b < c → a < c - b.
391 /2 width=1 by le_plus_to_minus_r/
394 lemma lt_plus_Sn_r: ∀a,x,n. a < a + x + (S n).
395 /2 width=1 by le_S_S/ qed.
397 theorem lt_S_S_to_lt: ∀n,m:nat. S n < S m → n < m.
399 /2 width=2 by lt_plus_to_lt_l/ qed-.
403 theorem not_le_Sn_O: ∀ n:nat. S n ≰ 0.
404 #n @nmk #Hlen0 @(lt_to_not_zero ?? Hlen0) qed.
406 theorem not_le_to_not_le_S_S: ∀ n,m:nat. n ≰ m → S n ≰ S m.
407 /3 width=3 by monotonic_pred, not_to_not/ qed.
409 theorem not_le_S_S_to_not_le: ∀ n,m:nat. S n ≰ S m → n ≰ m.
410 /3 width=3 by le_S_S, not_to_not/ qed.
412 theorem not_le_Sn_n: ∀n:nat. S n ≰ n.
413 #n elim n /2 width=1 by not_le_to_not_le_S_S/ qed.
415 theorem lt_to_not_le: ∀n,m. n < m → m ≰ n.
416 #n #m #Hltnm elim Hltnm /3 width=3 by lt_to_le, not_to_not/ qed.
418 theorem not_le_to_lt: ∀n,m. n ≰ m → m < n.
420 [#abs @False_ind /2 width=3 by absurd/
422 |/4 width=1 by le_S_S, not_le_S_S_to_not_le/
428 theorem not_lt_to_le: ∀n,m:nat. n ≮ m → m ≤ n.
429 /4 width=3 by le_S_S_to_le, not_le_to_lt, not_to_not/
432 theorem le_to_not_lt: ∀n,m:nat. n ≤ m → m ≮ n.
433 /3 width=3 by lt_to_not_le, le_to_lt_to_lt/
436 (* Compound conclusion ******************************************************)
438 theorem decidable_eq_nat : ∀n,m:nat.decidable (n=m).
439 @nat_elim2 #n [ cases n || #m #Hind cases Hind ]
440 /3 width=1 by or_introl, or_intror, sym_not_eq, not_eq_S/
443 theorem decidable_le: ∀n,m. decidable (n≤m).
444 @nat_elim2 #n /2 width=1 by or_introl, or_intror/
445 #m * /3 width=1 by not_le_to_not_le_S_S, le_S_S, or_introl, or_intror/
448 theorem decidable_lt: ∀n,m. decidable (n < m).
449 #n #m @decidable_le qed.
451 theorem le_to_or_lt_eq: ∀n,m:nat. n ≤ m → n < m ∨ n = m.
452 #n #m #lenm elim lenm /3 width=3 by le_to_lt_to_lt, or_introl/ qed.
454 theorem eq_or_gt: ∀n. 0 = n ∨ 0 < n.
455 #n elim (le_to_or_lt_eq 0 n ?) /2 width=1 by or_introl, or_intror/
458 theorem increasing_to_le2: ∀f:nat → nat. increasing f →
459 ∀m:nat. f 0 ≤ m → ∃i. f i ≤ m ∧ m < f (S i).
460 #f #incr #m #lem elim lem
461 [@(ex_intro ? ? O) % //
462 |#n #len * #a * #len #ltnr cases (le_to_or_lt_eq … ltnr) #H
463 [@(ex_intro ? ? a) % /2 width=1 by le_S/
464 |@(ex_intro ? ? (S a)) % //
469 lemma le_inv_plus_l: ∀x,y,z. x + y ≤ z → x ≤ z - y ∧ y ≤ z.
470 /3 width=2 by le_plus_to_minus_r, le_plus_b, conj/ qed-.
472 lemma lt_inv_plus_l: ∀x,y,z. x + y < z → x < z ∧ y < z - x.
473 /3 width=3 by lt_plus_to_minus_r, lt_to_le_to_lt, conj/ qed-.
475 lemma lt_or_ge: ∀m,n. m < n ∨ n ≤ m.
476 #m #n elim (decidable_lt m n)
477 /3 width=1 by not_lt_to_le, or_introl, or_intror/
480 lemma le_or_ge: ∀m,n. m ≤ n ∨ n ≤ m.
481 #m #n elim (decidable_le m n)
482 /4 width=1 by not_le_to_lt, lt_to_le, or_intror, or_introl/
485 lemma le_inv_S1: ∀x,y. S x ≤ y → ∃∃z. x ≤ z & y = S z.
486 #x #y #H elim H -y /2 width=3 by ex2_intro/
487 #y #_ * #n #Hxn #H destruct /3 width=3 by le_S, ex2_intro/
490 (* More general conclusion **************************************************)
492 theorem nat_ind_plus: ∀R:predicate nat.
493 R 0 → (∀n. R n → R (n + 1)) → ∀n. R n.
494 /3 width=1 by nat_ind/ qed-.
496 theorem lt_O_n_elim: ∀n:nat. 0 < n →
497 ∀P:nat → Prop.(∀m:nat.P (S m)) → P n.
498 #n elim n // #abs @False_ind /2 width=3 by absurd/
501 theorem le_n_O_elim: ∀n:nat. n ≤ O → ∀P: nat →Prop. P O → P n.
502 #n cases n // #a #abs @False_ind /2 width=3 by absurd/ qed.
504 theorem le_n_Sm_elim : ∀n,m:nat.n ≤ S m →
505 ∀P:Prop. (S n ≤ S m → P) → (n=S m → P) → P.
506 #n #m #Hle #P elim Hle /3 width=1 by le_S_S/ qed.
508 theorem nat_elim1 : ∀n:nat.∀P:nat → Prop.
509 (∀m.(∀p. p < m → P p) → P m) → P n.
511 cut (∀q:nat. q ≤ n → P q) /2/
513 [#q #HleO (* applica male *)
514 @(le_n_O_elim ? HleO)
515 @H #p #ltpO /3 width=3 by False_ind, absurd/
517 @H #a #lta @Hind @le_S_S_to_le /2 width=3 by transitive_le/
521 fact f_ind_aux: ∀A. ∀f:A→ℕ. ∀P:predicate A.
522 (∀n. (∀a. f a < n → P a) → ∀a. f a = n → P a) →
524 #A #f #P #H #n @(nat_elim1 … n) -n #n /3 width=3/ (**) (* auto slow (34s) without #n *)
527 lemma f_ind: ∀A. ∀f:A→ℕ. ∀P:predicate A.
528 (∀n. (∀a. f a < n → P a) → ∀a. f a = n → P a) → ∀a. P a.
530 @(f_ind_aux … H) -H [2: // | skip ]
533 fact f2_ind_aux: ∀A1,A2. ∀f:A1→A2→ℕ. ∀P:relation2 A1 A2.
534 (∀n. (∀a1,a2. f a1 a2 < n → P a1 a2) → ∀a1,a2. f a1 a2 = n → P a1 a2) →
535 ∀n,a1,a2. f a1 a2 = n → P a1 a2.
536 #A1 #A2 #f #P #H #n @(nat_elim1 … n) -n #n /3 width=3/ (**) (* auto slow (34s) without #n *)
539 lemma f2_ind: ∀A1,A2. ∀f:A1→A2→ℕ. ∀P:relation2 A1 A2.
540 (∀n. (∀a1,a2. f a1 a2 < n → P a1 a2) → ∀a1,a2. f a1 a2 = n → P a1 a2) →
542 #A1 #A2 #f #P #H #a1 #a2
543 @(f2_ind_aux … H) -H [2: // | skip ]
546 fact f3_ind_aux: ∀A1,A2,A3. ∀f:A1→A2→A3→ℕ. ∀P:relation3 A1 A2 A3.
547 (∀n. (∀a1,a2,a3. f a1 a2 a3 < n → P a1 a2 a3) → ∀a1,a2,a3. f a1 a2 a3 = n → P a1 a2 a3) →
548 ∀n,a1,a2,a3. f a1 a2 a3 = n → P a1 a2 a3.
549 #A1 #A2 #A3 #f #P #H #n @(nat_elim1 … n) -n #n /3 width=3/ (**) (* auto slow (34s) without #n *)
552 lemma f3_ind: ∀A1,A2,A3. ∀f:A1→A2→A3→ℕ. ∀P:relation3 A1 A2 A3.
553 (∀n. (∀a1,a2,a3. f a1 a2 a3 < n → P a1 a2 a3) → ∀a1,a2,a3. f a1 a2 a3 = n → P a1 a2 a3) →
554 ∀a1,a2,a3. P a1 a2 a3.
555 #A1 #A2 #A3 #f #P #H #a1 #a2 #a3
556 @(f3_ind_aux … H) -H [2: // | skip ]
559 (* More negated equalities **************************************************)
561 theorem lt_to_not_eq : ∀n,m:nat. n < m → n ≠ m.
562 /2 width=3 by not_to_not, absurd, nmk/ qed.
564 (* More equalities **********************************************************)
566 theorem le_n_O_to_eq : ∀n:nat. n ≤ 0 → 0=n.
567 #n cases n // #a #abs @False_ind /2 width=3 by absurd/ qed.
569 theorem le_to_le_to_eq: ∀n,m. n ≤ m → m ≤ n → n = m.
570 @nat_elim2 /4 width=1 by le_n_O_to_eq, monotonic_pred, eq_f, sym_eq/
573 theorem increasing_to_injective: ∀f:nat → nat.
574 increasing f → injective nat nat f.
575 #f #incr #n #m cases (decidable_le n m)
576 [#lenm cases (le_to_or_lt_eq … lenm) //
577 #lenm #eqf @False_ind @(absurd … eqf) @lt_to_not_eq
578 @increasing_to_monotonic //
579 |#nlenm #eqf @False_ind @(absurd … eqf) @sym_not_eq
580 @lt_to_not_eq @increasing_to_monotonic /2 width=1 by not_le_to_lt/
584 theorem minus_Sn_m: ∀m,n:nat. m ≤ n → S n -m = S (n-m).
585 (* qualcosa da capire qui
586 #n #m #lenm elim lenm applyS refl *)
589 |#n #abs @False_ind /2 width=3 by absurd/
590 |#n #m #Hind #c applyS Hind /2 width=1 by monotonic_pred/
595 ∀m,n,p:nat. m ≤ n → (n-m)+p = (n+p)-m.
598 |#n #p #abs @False_ind /2 width=3 by absurd/
599 |normalize /3 width=1 by monotonic_pred/
603 theorem minus_plus_m_m: ∀n,m:nat.n = (n+m)-m.
604 /2 width=1 by plus_minus/ qed.
606 theorem plus_minus_m_m: ∀n,m:nat.
608 /2 width=1 by plus_minus/ qed.
610 theorem minus_to_plus :∀n,m,p:nat.
611 m ≤ n → n-m = p → n = m+p.
612 #n #m #p #lemn #eqp (applyS plus_minus_m_m) //
615 theorem plus_to_minus :∀n,m,p:nat.n = m+p → n-m = p.
616 #n #m #p #eqp @sym_eq (applyS (minus_plus_m_m p m))
619 theorem minus_pred_pred : ∀n,m:nat. O < n → O < m →
620 pred n - pred m = n - m.
621 #n #m #posn #posm @(lt_O_n_elim n posn) @(lt_O_n_elim m posm) //.
624 theorem plus_minus_associative: ∀x,y,z. z ≤ y → x + (y - z) = x + y - z.
625 /2 width=1 by plus_minus/ qed.
627 (* More atomic conclusion ***************************************************)
631 theorem le_n_fn: ∀f:nat → nat.
632 increasing f → ∀n:nat. n ≤ f n.
633 #f #incr #n elim n /2 width=3 by le_to_lt_to_lt/
636 theorem monotonic_le_minus_l:
637 ∀p,q,n:nat. q ≤ p → q-n ≤ p-n.
639 [#lePO @(le_n_O_elim ? lePO) //
641 |#Hind * /3 width=1 by monotonic_pred/
645 theorem le_minus_to_plus: ∀n,m,p. n-m ≤ p → n≤ p+m.
646 #n #m #p #lep @transitive_le
647 [|@le_plus_minus_m_m | @monotonic_le_plus_l // ]
650 theorem le_minus_to_plus_r: ∀a,b,c. c ≤ b → a ≤ b - c → a + c ≤ b.
651 #a #b #c #Hlecb #H >(plus_minus_m_m … Hlecb) /2 width=1 by monotonic_le_plus_l/
654 theorem le_plus_to_minus: ∀n,m,p. n ≤ p+m → n-m ≤ p.
655 /2 width=1 by monotonic_le_minus_l/ qed.
657 theorem monotonic_le_minus_r:
658 ∀p,q,n:nat. q ≤ p → n-p ≤ n-q.
659 #p #q #n #lepq @le_plus_to_minus
660 @(transitive_le … (le_plus_minus_m_m ? q)) /2 width=1 by monotonic_le_plus_r/
663 theorem increasing_to_le: ∀f:nat → nat.
664 increasing f → ∀m:nat.∃i.m ≤ f i.
665 #f #incr #m elim m /2 width=2 by ex_intro/
667 @(ex_intro ?? (S a)) /2 width=3 by le_to_lt_to_lt/
670 lemma minus_le: ∀x,y. x - y ≤ x.
671 /2 width=1 by monotonic_le_minus_l/ qed.
675 theorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n<m.
676 #n #m #Hneq #Hle cases (le_to_or_lt_eq ?? Hle) //
677 #Heq @not_le_to_lt /2 width=3 by not_to_not/ qed-.
679 theorem lt_times_n_to_lt_l:
680 ∀n,p,q:nat. p*n < q*n → p < q.
681 #n #p #q #Hlt (elim (decidable_lt p q)) //
682 #nltpq @False_ind @(absurd ? ? (lt_to_not_le ? ? Hlt))
683 applyS monotonic_le_times_r /2 width=1 by not_lt_to_le/
686 theorem lt_times_n_to_lt_r:
687 ∀n,p,q:nat. n*p < n*q → p < q.
688 /2 width=2 by lt_times_n_to_lt_l/ qed-.
690 theorem lt_minus_to_plus: ∀a,b,c. a - b < c → a < c + b.
691 #a #b #c #H @not_le_to_lt
692 @(not_to_not … (lt_to_not_le …H)) /2 width=1 by le_plus_to_minus_r/
695 theorem lt_minus_to_plus_r: ∀a,b,c. a < b - c → a + c < b.
696 #a #b #c #H @not_le_to_lt @(not_to_not … (le_plus_to_minus …))
700 theorem lt_plus_to_minus: ∀n,m,p. m ≤ n → n < p+m → n-m < p.
701 #n #m #p #lenm #H normalize <minus_Sn_m // @le_plus_to_minus //
704 theorem monotonic_lt_minus_l: ∀p,q,n. n ≤ q → q < p → q - n < p - n.
706 @lt_plus_to_minus_r <plus_minus_m_m //
709 (* More compound conclusion *************************************************)
711 lemma discr_minus_x_xy: ∀x,y. x = x - y → x = 0 ∨ y = 0.
712 * /2 width=1/ #x * /2 width=1/ #y normalize #H
713 lapply (minus_le x y) <H -H #H
714 elim (not_le_Sn_n x) #H0 elim (H0 ?) //
717 lemma plus_le_0: ∀x,y. x + y ≤ 0 → x = 0 ∧ y = 0.
718 #x #y #H elim (le_inv_plus_l … H) -H /3 width=1 by conj, plus_minus_associative/
721 (* Still more equalities ****************************************************)
723 theorem eq_minus_O: ∀n,m:nat.
725 #n #m #lenm @(le_n_O_elim (n-m)) /2 width=1 by monotonic_le_minus_r/
728 theorem distributive_times_minus: distributive ? times minus.
730 (cases (decidable_lt b c)) #Hbc
731 [>eq_minus_O [ >eq_minus_O // @monotonic_le_times_r ]
732 /2 width=1 by lt_to_le/
733 |@sym_eq (applyS plus_to_minus) <distributive_times_plus
734 @eq_f (applyS plus_minus_m_m) /2 width=1 by not_lt_to_le/
738 theorem minus_plus: ∀n,m,p. n-m-p = n-(m+p).
740 cases (decidable_le (m+p) n) #Hlt
741 [@plus_to_minus @plus_to_minus <associative_plus
743 |cut (n ≤ m+p) [@(transitive_le … (le_n_Sn …)) @not_le_to_lt //]
744 #H >eq_minus_O /2 width=1 by eq_minus_O, monotonic_le_minus_l/ (* >eq_minus_O // *)
748 theorem minus_minus: ∀n,m,p:nat. p ≤ m → m ≤ n →
751 @sym_eq @plus_to_minus <associative_plus <plus_minus_m_m //
752 <commutative_plus <plus_minus_m_m //
755 lemma minus_minus_associative: ∀x,y,z. z ≤ y → y ≤ x → x - (y - z) = x - y + z.
756 /2 width=1 by minus_minus/ qed.
758 lemma minus_minus_comm: ∀a,b,c. a - b - c = a - c - b.
759 /3 width=1 by monotonic_le_minus_l, le_to_le_to_eq/ qed.
761 lemma minus_le_minus_minus_comm: ∀b,c,a. c ≤ b → a - (b - c) = a + c - b.
762 #b #c #a #H >(plus_minus_m_m b c) in ⊢ (? ? ?%); //
765 lemma minus_minus_m_m: ∀m,n. n ≤ m → m - (m - n) = n.
766 /2 width=1 by minus_le_minus_minus_comm/ qed.
768 lemma minus_plus_plus_l: ∀x,y,h. (x + h) - (y + h) = x - y.
771 lemma plus_minus_plus_plus_l: ∀z,x,y,h. z + (x + h) - (y + h) = z + x - y.
774 (* Stilll more atomic conclusion ********************************************)
778 lemma le_fwd_plus_plus_ge: ∀m1,m2. m2 ≤ m1 → ∀n1,n2. m1 + n1 ≤ m2 + n2 → n1 ≤ n2.
779 #m1 #m2 #H #n1 #n2 >commutative_plus
780 #H elim (le_inv_plus_l … H) -H >commutative_plus <minus_le_minus_minus_comm //
781 #H #_ @(transitive_le … H) /2 width=1/
784 (*********************** boolean arithmetics ********************)
786 include "basics/bool.ma".
790 [ O ⇒ match m with [ O ⇒ true | S q ⇒ false]
791 | S p ⇒ match m with [ O ⇒ false | S q ⇒ eqb p q]
794 theorem eqb_elim : ∀ n,m:nat.∀ P:bool → Prop.
795 (n=m → (P true)) → (n ≠ m → (P false)) → (P (eqb n m)).
797 [#n (cases n) normalize /3/
803 theorem eqb_n_n: ∀n. eqb n n = true.
804 #n (elim n) normalize // qed.
806 theorem eqb_true_to_eq: ∀n,m:nat. eqb n m = true → n = m.
807 #n #m @(eqb_elim n m) // #_ #abs @False_ind /2/ qed.
809 theorem eqb_false_to_not_eq: ∀n,m:nat. eqb n m = false → n ≠ m.
810 #n #m @(eqb_elim n m) /2/ qed.
812 theorem eq_to_eqb_true: ∀n,m:nat.n = m → eqb n m = true.
815 theorem not_eq_to_eqb_false: ∀n,m:nat.
816 n ≠ m → eqb n m = false.
817 #n #m #noteq @eqb_elim// #Heq @False_ind /2/ qed.
827 theorem leb_elim: ∀n,m:nat. ∀P:bool → Prop.
828 (n ≤ m → P true) → (n ≰ m → P false) → P (leb n m).
832 |#n #m #Hind #P #Pt #Pf @Hind
833 [#lenm @Pt @le_S_S // |#nlenm @Pf /2/ ]
837 theorem leb_true_to_le:∀n,m.leb n m = true → n ≤ m.
838 #n #m @leb_elim // #_ #abs @False_ind /2/ qed.
840 theorem leb_false_to_not_le:∀n,m.
841 leb n m = false → n ≰ m.
842 #n #m @leb_elim // #_ #abs @False_ind /2/ qed.
844 theorem le_to_leb_true: ∀n,m. n ≤ m → leb n m = true.
845 #n #m @leb_elim // #H #H1 @False_ind /2/ qed.
847 theorem not_le_to_leb_false: ∀n,m. n ≰ m → leb n m = false.
848 #n #m @leb_elim // #H #H1 @False_ind /2/ qed.
850 theorem lt_to_leb_false: ∀n,m. m < n → leb n m = false.
854 definition min: nat →nat →nat ≝
855 λn.λm. if leb n m then n else m.
857 definition max: nat →nat →nat ≝
858 λn.λm. if leb n m then m else n.
860 lemma commutative_min: commutative ? min.
861 #n #m normalize @leb_elim
862 [@leb_elim normalize /2/
863 |#notle >(le_to_leb_true …) // @(transitive_le ? (S m)) /2/
866 lemma le_minr: ∀i,n,m. i ≤ min n m → i ≤ m.
867 #i #n #m normalize @leb_elim normalize /2/ qed.
869 lemma le_minl: ∀i,n,m. i ≤ min n m → i ≤ n.
872 lemma to_min: ∀i,n,m. i ≤ n → i ≤ m → i ≤ min n m.
873 #i #n #m #lein #leim normalize (cases (leb n m))
876 lemma commutative_max: commutative ? max.
877 #n #m normalize @leb_elim
878 [@leb_elim normalize /2/
879 |#notle >(le_to_leb_true …) // @(transitive_le ? (S m)) /2/
882 lemma le_maxl: ∀i,n,m. max n m ≤ i → n ≤ i.
883 #i #n #m normalize @leb_elim normalize /2/ qed.
885 lemma le_maxr: ∀i,n,m. max n m ≤ i → m ≤ i.
888 lemma to_max: ∀i,n,m. n ≤ i → m ≤ i → max n m ≤ i.
889 #i #n #m #leni #lemi normalize (cases (leb n m))