- lambda_delta: programmed renaming to lambdadelta

[helm.git] / matita / matita / lib / arithmetics / nat.ma

diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index 56482a0428e6e434a880d23d9f4dcd9f042e0c9c..e80380217218b13d13dc41a247c8bf503cb4bff8 100644 (file)
--- a/matita/matita/lib/arithmetics/nat.ma
+++ b/matita/matita/lib/arithmetics/nat.ma
@@ -1,4 +1,4 @@
-  (*
+(*
     ||M||  This file is part of HELM, an Hypertextual, Electronic        
     ||A||  Library of Mathematics, developed at the Computer Science     
     ||T||  Department of the University of Bologna, Italy.                     
@@ -132,7 +132,7 @@ theorem assoc_plus1: ∀a,b,c. c + (b + a) = b + c + a.
 theorem injective_plus_r: ∀n:nat.injective nat nat (λm.n+m).
 #n (elim n) normalize /3/ qed.
 
-theorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m.
+theorem injective_plus_l: ∀n:nat.injective nat nat (λm.m+n). 
 /2/ qed.
 
 theorem times_Sn_m: ∀n,m:nat. m+n*m = S n*m.
@@ -184,8 +184,14 @@ theorem minus_Sn_n: ∀n:nat. S 0 = (S n)-n.
 theorem eq_minus_S_pred: ∀n,m. n - (S m) = pred(n -m).
 @nat_elim2 normalize // qed.
 
+lemma plus_plus_comm_23: ∀x,y,z. x + y + z = x + z + y.
+// qed.
+
 (* Negated equalities *******************************************************)
 
+theorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m.
+/2/ qed.
+
 theorem not_eq_O_S : ∀n:nat. 0 ≠ S n.
 #n @nmk #eqOS (change with (not_zero O)) >eqOS // qed.
 
@@ -236,7 +242,7 @@ theorem monotonic_le_plus_l:
 theorem le_plus: ∀n1,n2,m1,m2:nat. n1 ≤ n2  → m1 ≤ m2 
 → n1 + m1 ≤ n2 + m2.
 #n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1+m2))
-/2/ qed-.
+/2/ qed.
 
 theorem le_plus_n :∀n,m:nat. m ≤ n + m.
 /2/ qed. 
@@ -293,6 +299,16 @@ theorem le_plus_to_minus_r: ∀a,b,c. a + b ≤ c → a ≤ c -b.
 #a #b #c #H @(le_plus_to_le_r … b) /2/
 qed.
 
+lemma lt_to_le: ∀x,y. x < y → x ≤ y.
+/2 width=2/ qed.
+
+lemma inv_eq_minus_O: ∀x,y. x - y = 0 → x ≤ y.
+// qed-.
+
+lemma le_x_times_x: ∀x. x ≤ x * x.
+#x elim x -x //
+qed.
+
 (* lt *)
 
 theorem transitive_lt: transitive nat lt.
@@ -368,6 +384,13 @@ theorem lt_plus_to_minus_r: ∀a,b,c. a + b < c → a < c - b.
 #a #b #c #H @le_plus_to_minus_r //
 qed.
 
+lemma lt_plus_Sn_r: ∀a,x,n. a < a + x + (S n).
+/2 width=1/ qed.
+
+theorem lt_S_S_to_lt: ∀n,m:nat. S n < S m → n < m.
+(* demo *)
+/2/ qed-.
+
 (* not le, lt *)
 
 theorem not_le_Sn_O: ∀ n:nat. S n ≰ 0.
@@ -389,14 +412,14 @@ theorem not_le_to_lt: ∀n,m. n ≰ m → m < n.
 @nat_elim2 #n
  [#abs @False_ind /2/
  |/2/
- |#m #Hind #HnotleSS @le_S_S /3/
+ |#m #Hind #HnotleSS @le_S_S @Hind /2/ 
  ]
 qed.
 
 (* not lt, le *)
 
 theorem not_lt_to_le: ∀n,m:nat. n ≮ m → m ≤ n.
-/4/ qed.
+#n #m #H @le_S_S_to_le @not_le_to_lt /2/ qed.
 
 theorem le_to_not_lt: ∀n,m:nat. n ≤ m → m ≮ n.
 #n #m #H @lt_to_not_le /2/ (* /3/ *) qed.
@@ -427,8 +450,26 @@ theorem increasing_to_le2: ∀f:nat → nat. increasing f →
   ]
 qed.
 
+lemma le_inv_plus_l: ∀x,y,z. x + y ≤ z → x ≤ z - y ∧ y ≤ z.
+/3/ qed-.
+
+lemma lt_inv_plus_l: ∀x,y,z. x + y < z → x < z ∧ y < z - x.
+/3/ qed-.
+
+lemma lt_or_ge: ∀m,n. m < n ∨ n ≤ m.
+#m #n elim (decidable_lt m n) /2/ /3/
+qed-.
+
+lemma le_or_ge: ∀m,n. m ≤ n ∨ n ≤ m.
+#m #n elim (decidable_le m n) /2/ /4/
+qed-.
+
 (* More general conclusion **************************************************)
 
+theorem nat_ind_plus: ∀R:predicate nat.
+                      R 0 → (∀n. R n → R (n + 1)) → ∀n. R n.
+/3 by nat_ind/ qed-.
+
 theorem lt_O_n_elim: ∀n:nat. 0 < n → 
   ∀P:nat → Prop.(∀m:nat.P (S m)) → P n.
 #n (elim n) // #abs @False_ind /2/ @absurd
@@ -454,6 +495,31 @@ cut (∀q:nat. q ≤ n → P q) /2/
  ]
 qed.
 
+fact f_ind_aux: ∀A. ∀f:A→ℕ. ∀P:predicate A.
+                (∀n. (∀a. f a < n → P a) → ∀a. f a = n → P a) →
+                ∀n,a. f a = n → P a.
+#A #f #P #H #n @(nat_elim1 … n) -n #n /3 width=3/ (**) (* auto slow (34s) without #n *)
+qed-.
+
+lemma f_ind: ∀A. ∀f:A→ℕ. ∀P:predicate A.
+             (∀n. (∀a. f a < n → P a) → ∀a. f a = n → P a) → ∀a. P a.
+#A #f #P #H #a
+@(f_ind_aux … H) -H [2: // | skip ]
+qed-.
+
+fact f2_ind_aux: ∀A1,A2. ∀f:A1→A2→ℕ. ∀P:relation2 A1 A2.
+                 (∀n. (∀a1,a2. f a1 a2 < n → P a1 a2) → ∀a1,a2. f a1 a2 = n → P a1 a2) →
+                 ∀n,a1,a2. f a1 a2 = n → P a1 a2.
+#A1 #A2 #f #P #H #n @(nat_elim1 … n) -n #n /3 width=3/ (**) (* auto slow (34s) without #n *)
+qed-.
+
+lemma f2_ind: ∀A1,A2. ∀f:A1→A2→ℕ. ∀P:relation2 A1 A2.
+              (∀n. (∀a1,a2. f a1 a2 < n → P a1 a2) → ∀a1,a2. f a1 a2 = n → P a1 a2) →
+              ∀a1,a2. P a1 a2.
+#A1 #A2 #f #P #H #a1 #a2
+@(f2_ind_aux … H) -H [2: // | skip ]
+qed-. 
+
 (* More negated equalities **************************************************)
 
 theorem lt_to_not_eq : ∀n,m:nat. n < m → n ≠ m.
@@ -465,7 +531,7 @@ theorem le_n_O_to_eq : ∀n:nat. n ≤ 0 → 0=n.
 #n (cases n) // #a  #abs @False_ind /2/ qed.
 
 theorem le_to_le_to_eq: ∀n,m. n ≤ m → m ≤ n → n = m.
-@nat_elim2 /4/
+@nat_elim2 /4 by le_n_O_to_eq, monotonic_pred, eq_f, sym_eq/
 qed. 
 
 theorem increasing_to_injective: ∀f:nat → nat.
@@ -519,6 +585,9 @@ pred n - pred m = n - m.
 #n #m #posn #posm @(lt_O_n_elim n posn) @(lt_O_n_elim m posm) //.
 qed.
 
+theorem plus_minus_commutative: ∀x,y,z. z ≤ y → x + (y - z) = x + y - z.
+/2 by plus_minus/ qed.
+
 (* More atomic conclusion ***************************************************)
 
 (* le *)
@@ -561,11 +630,19 @@ theorem increasing_to_le: ∀f:nat → nat.
 @(ex_intro ?? (S a)) /2/
 qed.
 
+(* thus is le_plus
+lemma le_plus_compatible: ∀x1,x2,y1,y2. x1 ≤ y1 → x2 ≤ y2 → x1 + x2 ≤ y1 + y2.
+#x1 #y1 #x2 #y2 #H1 #H2 /2/ @le_plus // /2/ /3 by le_minus_to_plus, monotonic_le_plus_r, transitive_le/ qed.
+*)
+
+lemma minus_le: ∀x,y. x - y ≤ x.
+/2 width=1/ qed.
+
 (* lt *)
 
 theorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n<m.
 #n #m #Hneq #Hle cases (le_to_or_lt_eq ?? Hle) //
-#Heq /3/ qed-.
+#Heq @not_le_to_lt /2/ qed-.
 
 theorem lt_times_n_to_lt_l: 
 ∀n,p,q:nat. p*n < q*n → p < q.
@@ -597,6 +674,14 @@ theorem monotonic_lt_minus_l: ∀p,q,n. n ≤ q → q < p → q - n < p - n.
 @lt_plus_to_minus_r <plus_minus_m_m //
 qed.
 
+(* More compound conclusion *************************************************)
+
+lemma discr_minus_x_xy: ∀x,y. x = x - y → x = 0 ∨ y = 0.
+* /2 width=1/ #x * /2 width=1/ #y normalize #H 
+lapply (minus_le x y) <H -H #H
+elim (not_le_Sn_n x) #H0 elim (H0 ?) //
+qed-.
+
 (* Still more equalities ****************************************************)
 
 theorem eq_minus_O: ∀n,m:nat.
@@ -607,7 +692,7 @@ qed.
 theorem distributive_times_minus: distributive ? times minus.
 #a #b #c
 (cases (decidable_lt b c)) #Hbc
- [> eq_minus_O /2/ >eq_minus_O // 
+ [> eq_minus_O [2:/2/] >eq_minus_O // 
   @monotonic_le_times_r /2/
  |@sym_eq (applyS plus_to_minus) <distributive_times_plus 
   @eq_f (applyS plus_minus_m_m) /2/
@@ -630,7 +715,31 @@ theorem minus_minus: ∀n,m,p:nat. p ≤ m → m ≤ n →
 <commutative_plus <plus_minus_m_m //
 qed.
 
+lemma minus_minus_comm: ∀a,b,c. a - b - c = a - c - b.
+/3 by monotonic_le_minus_l, le_to_le_to_eq/ qed.
+
+lemma minus_le_minus_minus_comm: ∀b,c,a. c ≤ b → a - (b - c) = a + c - b.
+#b #c #a #H >(plus_minus_m_m b c) in ⊢ (? ? ?%); //
+qed.
+
+lemma minus_minus_m_m: ∀m,n. n ≤ m → m - (m - n) = n.
+/2 width=1/ qed.
+
+lemma minus_plus_plus_l: ∀x,y,h. (x + h) - (y + h) = x - y.
+// qed.
+
+(* Stilll more atomic conclusion ********************************************)
+
+(* le *)
+
+lemma le_fwd_plus_plus_ge: ∀m1,m2. m2 ≤ m1 → ∀n1,n2. m1 + n1 ≤ m2 + n2 → n1 ≤ n2.
+#m1 #m2 #H #n1 #n2 >commutative_plus
+#H elim (le_inv_plus_l … H) -H >commutative_plus <minus_le_minus_minus_comm //
+#H #_ @(transitive_le … H) /2 width=1/
+qed-. 
+
 (*********************** boolean arithmetics ********************) 
+
 include "basics/bool.ma".
 
 let rec eqb n m ≝ 
@@ -700,10 +809,10 @@ theorem lt_to_leb_false: ∀n,m. m < n → leb n m = false.
 
 (* min e max *)
 definition min: nat →nat →nat ≝
-λn.λm. if_then_else ? (leb n m) n m.
+λn.λm. if leb n m then n else m.
 
 definition max: nat →nat →nat ≝
-λn.λm. if_then_else ? (leb n m) m n.
+λn.λm. if leb n m then m else n.
 
 lemma commutative_min: commutative ? min.
 #n #m normalize @leb_elim 
@@ -736,4 +845,3 @@ lemma le_maxr: ∀i,n,m. max n m ≤ i → m ≤ i.
 lemma to_max: ∀i,n,m. n ≤ i → m ≤ i → max n m ≤ i.
 #i #n #m #leni #lemi normalize (cases (leb n m)) 
 normalize // qed.
-