X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fnat.ma;h=6b3a1a19bf7b730af3e90aacec9d36b48a3d0289;hb=1cd2f9aa6e0aee9eb4939b39c985b6ad6605092b;hp=dc0af3a6b14663ef1e6d4e269a8b9031129894f4;hpb=16a95f57b09ae92ea24ab2addd02c1d0be80f109;p=helm.git

diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index dc0af3a6b..6b3a1a19b 100644
--- a/matita/matita/lib/arithmetics/nat.ma
+++ b/matita/matita/lib/arithmetics/nat.ma
@@ -151,6 +151,9 @@ theorem associative_times: associative nat times.
 lemma times_times: ∀x,y,z. x*(y*z) = y*(x*z).
 // qed. 
 
+theorem times_n_1 : ∀n:nat. n = n * 1.
+#n // qed.
+
 (* ci servono questi risultati? 
 theorem times_O_to_O: ∀n,m:nat.n*m=O → n=O ∨ m=O.
 napply nat_elim2 /2/ 
@@ -322,6 +325,10 @@ theorem lt_O_n_elim: ∀n:nat. O < n →
 #n (elim n) // #abs @False_ind /2/
 qed.
 
+theorem S_pred: ∀n. 0 < n → S(pred n) = n.
+#n #posn (cases posn) //
+qed.
+
 (*
 theorem lt_pred: \forall n,m. 
   O < n \to n < m \to pred n < pred m. 
@@ -332,11 +339,6 @@ apply nat_elim2
   ]
 qed.
 
-theorem S_pred: \forall n:nat.lt O n \to eq nat n (S (pred n)).
-intro.elim n.apply False_ind.exact (not_le_Sn_O O H).
-apply eq_f.apply pred_Sn.
-qed.
-
 theorem le_pred_to_le:
  ∀n,m. O < m → pred n ≤ pred m → n ≤ m.
 intros 2
@@ -453,58 +455,46 @@ cut (∀q:nat. q ≤ n → P q) /2/
 qed.
 
 (* some properties of functions *)
-(*
-definition increasing \def \lambda f:nat \to nat. 
-\forall n:nat. f n < f (S n).
-
-theorem increasing_to_monotonic: \forall f:nat \to nat.
-increasing f \to monotonic nat lt f.
-unfold monotonic.unfold lt.unfold increasing.unfold lt.intros.elim H1.apply H.
-apply (trans_le ? (f n1)).
-assumption.apply (trans_le ? (S (f n1))).
-apply le_n_Sn.
-apply H.
+
+definition increasing ≝ λf:nat → nat. ∀n:nat. f n < f (S n).
+
+theorem increasing_to_monotonic: ∀f:nat → nat.
+  increasing f → monotonic nat lt f.
+#f #incr #n #m #ltnm (elim ltnm) /2/
 qed.
 
-theorem le_n_fn: \forall f:nat \to nat. (increasing f) 
-\to \forall n:nat. n \le (f n).
-intros.elim n.
-apply le_O_n.
-apply (trans_le ? (S (f n1))).
-apply le_S_S.apply H1.
-simplify in H. unfold increasing in H.unfold lt in H.apply H.
+theorem le_n_fn: ∀f:nat → nat. 
+  increasing f → ∀n:nat. n ≤ f n.
+#f #incr #n (elim n) /2/
 qed.
 
-theorem increasing_to_le: \forall f:nat \to nat. (increasing f) 
-\to \forall m:nat. \exists i. m \le (f i).
-intros.elim m.
-apply (ex_intro ? ? O).apply le_O_n.
-elim H1.
-apply (ex_intro ? ? (S a)).
-apply (trans_le ? (S (f a))).
-apply le_S_S.assumption.
-simplify in H.unfold increasing in H.unfold lt in H.
-apply H.
+theorem increasing_to_le: ∀f:nat → nat. 
+  increasing f → ∀m:nat.∃i.m ≤ f i.
+#f #incr #m (elim m) /2/#n * #a #lenfa
+@(ex_intro ?? (S a)) /2/
 qed.
 
-theorem increasing_to_le2: \forall f:nat \to nat. (increasing f) 
-\to \forall m:nat. (f O) \le m \to 
-\exists i. (f i) \le m \land m <(f (S i)).
-intros.elim H1.
-apply (ex_intro ? ? O).
-split.apply le_n.apply H.
-elim H3.elim H4.
-cut ((S n1) < (f (S a)) \lor (S n1) = (f (S a))).
-elim Hcut.
-apply (ex_intro ? ? a).
-split.apply le_S. assumption.assumption.
-apply (ex_intro ? ? (S a)).
-split.rewrite < H7.apply le_n.
-rewrite > H7.
-apply H.
-apply le_to_or_lt_eq.apply H6.
+theorem increasing_to_le2: ∀f:nat → nat. increasing f → 
+  ∀m:nat. f 0 ≤ m → ∃i. f i ≤ m ∧ m < f (S i).
+#f #incr #m #lem (elim lem)
+  [@(ex_intro ? ? O) /2/
+  |#n #len * #a * #len #ltnr (cases(le_to_or_lt_eq … ltnr)) #H
+    [@(ex_intro ? ? a) % /2/ 
+    |@(ex_intro ? ? (S a)) % //
+    ]
+  ]
+qed.
+
+theorem increasing_to_injective: ∀f:nat → nat.
+  increasing f → injective nat nat f.
+#f #incr #n #m cases(decidable_le n m)
+  [#lenm cases(le_to_or_lt_eq … lenm) //
+   #lenm #eqf @False_ind @(absurd … eqf) @lt_to_not_eq 
+   @increasing_to_monotonic //
+  |#nlenm #eqf @False_ind @(absurd … eqf) @sym_not_eq 
+   @lt_to_not_eq @increasing_to_monotonic /2/
+  ]
 qed.
-*)
 
 (*********************** monotonicity ***************************)
 theorem monotonic_le_plus_r: 
@@ -693,8 +683,8 @@ simplify.rewrite < plus_n_O.rewrite < plus_n_O.assumption.
 apply lt_plus.assumption.assumption.
 qed. *)
 
-theorem monotonic_lt_times_l: 
-  ∀c:nat. O < c → monotonic nat lt (λt.(t*c)).
+theorem monotonic_lt_times_r: 
+  ∀c:nat. O < c → monotonic nat lt (λt.(c*t)).
 #c #posc #n #m #ltnm
 (elim ltnm) normalize
   [/2/ 
@@ -702,9 +692,10 @@ theorem monotonic_lt_times_l:
   ]
 qed.
 
-theorem monotonic_lt_times_r: 
-  ∀c:nat. O < c → monotonic nat lt (λt.(c*t)).
-/2/ qed.
+theorem monotonic_lt_times_l: 
+  ∀c:nat. O < c → monotonic nat lt (λt.(t*c)).
+/2/
+qed.
 
 theorem lt_to_le_to_lt_times: 
 ∀n,m,p,q:nat. n < m → p ≤ q → O < q → n*p < m*q.
@@ -856,6 +847,7 @@ pred n - pred m = n - m.
 #n #m #posn #posm @(lt_O_n_elim n posn) @(lt_O_n_elim m posm) //.
 qed.
 
+
 (*
 
 theorem le_SO_minus: \forall n,m:nat.S n \leq m \to S O \leq m-n.
@@ -921,9 +913,35 @@ theorem le_minus_to_plus: ∀n,m,p. n-m ≤ p → n≤ p+m.
   [|@le_plus_minus_m_m | @monotonic_le_plus_l // ]
 qed.
 
+theorem le_minus_to_plus_r: ∀a,b,c. c ≤ b → a ≤ b - c → a + c ≤ b.
+#a #b #c #Hlecb #H >(plus_minus_m_m … Hlecb) /2/
+qed.
+
 theorem le_plus_to_minus: ∀n,m,p. n ≤ p+m → n-m ≤ p.
 #n #m #p #lep /2/ qed.
 
+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.
+
+theorem lt_minus_to_plus: ∀a,b,c. a - b < c → a < c + b.
+#a #b #c #H @not_le_to_lt 
+@(not_to_not … (lt_to_not_le …H)) /2/
+qed.
+
+theorem lt_minus_to_plus_r: ∀a,b,c. a < b - c → a + c < b.
+#a #b #c #H @not_le_to_lt @(not_to_not … (le_plus_to_minus …))
+@lt_to_not_le //
+qed.
+
+theorem lt_plus_to_minus: ∀n,m,p. m ≤ n → n < p+m → n-m < p.
+#n #m #p #lenm #H normalize <minus_Sn_m // @le_plus_to_minus //
+qed.
+
+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. 
+
 theorem monotonic_le_minus_r: 
 ∀p,q,n:nat. q ≤ p → n-p ≤ n-q.
 #p #q #n #lepq @le_plus_to_minus
@@ -938,11 +956,33 @@ 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/ >eq_minus_O // 
   @monotonic_le_times_r /2/
- |@sym_eq (applyS plus_to_minus) <(distributive_times_plus …) 
- (* STRANO *)
-  @(eq_f …b) (applyS plus_minus_m_m) /2/
+ |@sym_eq (applyS plus_to_minus) <distributive_times_plus 
+  @eq_f (applyS plus_minus_m_m) /2/
+qed.
+
+theorem minus_plus: ∀n,m,p. n-m-p = n -(m+p).
+#n #m #p 
+cases (decidable_le (m+p) n) #Hlt
+  [@plus_to_minus @plus_to_minus <associative_plus
+   @minus_to_plus //
+  |cut (n ≤ m+p) [@(transitive_le … (le_n_Sn …)) @not_le_to_lt //]
+   #H >eq_minus_O /2/ >eq_minus_O // 
+  ]
+qed.
+
+(*
+theorem plus_minus: ∀n,m,p. p ≤ m → (n+m)-p = n +(m-p).
+#n #m #p #lepm @plus_to_minus >(commutative_plus p)
+>associative_plus <plus_minus_m_m //
+qed.  *)
+
+theorem minus_minus: ∀n,m,p:nat. p ≤ m → m ≤ n →
+  p+(n-m) = n-(m-p).
+#n #m #p #lepm #lemn
+@sym_eq @plus_to_minus <associative_plus <plus_minus_m_m //
+<commutative_plus <plus_minus_m_m //
 qed.
 
 (*********************** boolean arithmetics ********************)