From 5e50ef5a9b00a18778c0eb728f7fc909c0b0f729 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 10 Dec 2007 10:11:13 +0000
Subject: [PATCH] Restructuring.

---
 .../matita/library/nat/div_and_mod_diseq.ma   | 51 ++++++++---------
 .../matita/library/nat/generic_iter_p.ma      | 56 +++++++++++--------
 .../software/matita/library/nat/iteration2.ma | 14 +++++
 helm/software/matita/library/nat/lt_arith.ma  | 11 ++++
 helm/software/matita/library/nat/neper.ma     | 17 +++++-
 5 files changed, 97 insertions(+), 52 deletions(-)

diff --git a/helm/software/matita/library/nat/div_and_mod_diseq.ma b/helm/software/matita/library/nat/div_and_mod_diseq.ma
index 4977df660..299897a38 100644
--- a/helm/software/matita/library/nat/div_and_mod_diseq.ma
+++ b/helm/software/matita/library/nat/div_and_mod_diseq.ma
@@ -183,10 +183,9 @@ apply le_times_r.
 assumption.
 qed.
    
-theorem lt_times_to_lt_div: \forall m,n,q. O < q \to 
-n < m*q \to n/q < m.
+theorem lt_times_to_lt_div: \forall m,n,q. n < m*q \to n/q < m.
 intros.
-apply (lt_times_to_lt q ? ? H).
+apply (lt_times_to_lt q ? ? (lt_times_to_lt_O ? ? ? H)).
 rewrite > sym_times.
 rewrite > sym_times in ⊢ (? ? %).
 apply (le_plus_to_le (n \mod q)).
@@ -197,42 +196,38 @@ rewrite < div_mod
     [assumption
     |apply le_plus_n
     ]
-  |assumption
+  |apply (lt_times_to_lt_O ? ? ? H)
   ]
 qed.
 
 theorem lt_div: \forall n,m. O < m \to S O < n \to m/n < m.
 intros.
-apply lt_times_to_lt_div
-  [apply lt_to_le. assumption
-  |rewrite > sym_times.
-   apply lt_m_nm;assumption
-  ]
+apply lt_times_to_lt_div.
+rewrite < sym_times.
+apply lt_m_nm;assumption.
 qed. 
   
 theorem le_div_plus_S: \forall m,n,q. O < q \to
 (m+n)/q \le S(m/q + n/q).
 intros.
 apply le_S_S_to_le.
-apply lt_times_to_lt_div
-  [assumption
-  |change in ⊢ (? ? %) with (q + (q + (m/q+n/q)*q)).
-   rewrite > sym_times.
-   rewrite > distr_times_plus.
-   rewrite > sym_times.
-   rewrite < assoc_plus in ⊢ (? ? (? ? %)).
-   rewrite < assoc_plus.
-   rewrite > sym_plus in ⊢ (? ? (? % ?)).
-   rewrite > assoc_plus.
-   apply lt_plus
-    [change with (m < S(m/q)*q).
-     apply lt_div_S.
-     assumption
-    |rewrite > sym_times.
-     change with (n < S(n/q)*q).
-     apply lt_div_S.
-     assumption
-    ]
+apply lt_times_to_lt_div.
+change in ⊢ (? ? %) with (q + (q + (m/q+n/q)*q)).
+rewrite > sym_times.
+rewrite > distr_times_plus.
+rewrite > sym_times.
+rewrite < assoc_plus in ⊢ (? ? (? ? %)).
+rewrite < assoc_plus.
+rewrite > sym_plus in ⊢ (? ? (? % ?)).
+rewrite > assoc_plus.
+apply lt_plus
+  [change with (m < S(m/q)*q).
+   apply lt_div_S.
+   assumption
+  |rewrite > sym_times.
+   change with (n < S(n/q)*q).
+   apply lt_div_S.
+   assumption
   ]
 qed.
 
diff --git a/helm/software/matita/library/nat/generic_iter_p.ma b/helm/software/matita/library/nat/generic_iter_p.ma
index 249957f1b..f89c32f87 100644
--- a/helm/software/matita/library/nat/generic_iter_p.ma
+++ b/helm/software/matita/library/nat/generic_iter_p.ma
@@ -14,6 +14,7 @@
 
 set "baseuri" "cic:/matita/nat/generic_iter_p".
 
+include "nat/div_and_mod_diseq.ma".
 include "nat/primes.ma".
 include "nat/ord.ma".
 
@@ -47,8 +48,6 @@ rewrite > H.
 reflexivity.
 qed.
 
-
-
 theorem false_to_iter_p_gen_Sn: 
 \forall n:nat. \forall p:nat \to bool. \forall A:Type. \forall g:nat \to A.
 \forall baseA:A. \forall plusA: A \to A \to A.
@@ -59,7 +58,6 @@ rewrite > H.
 reflexivity.
 qed.
 
-
 theorem eq_iter_p_gen: \forall p1,p2:nat \to bool. \forall A:Type.
 \forall g1,g2: nat \to A. \forall baseA: A. 
 \forall plusA: A \to A \to A. \forall n:nat.
@@ -708,9 +706,38 @@ elim n
 ]
 qed.
 
-
-(* da spostare *)
-
+theorem eq_iter_p_gen_pred: 
+\forall A:Type.
+\forall baseA: A.
+\forall plusA: A \to A \to A.
+\forall n,p,g.
+p O = true \to
+(symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a  baseA) = a) \to
+iter_p_gen (S n) (\lambda i.p (pred i)) A (\lambda i.g(pred i)) baseA plusA = 
+plusA (iter_p_gen n p A g baseA plusA) (g O).
+intros.
+elim n
+  [rewrite > true_to_iter_p_gen_Sn
+    [simplify.apply H1
+    |assumption
+    ]
+  |apply (bool_elim ? (p n1));intro
+    [rewrite > true_to_iter_p_gen_Sn
+      [rewrite > true_to_iter_p_gen_Sn in ⊢ (? ? ? %)
+        [rewrite > H2 in ⊢ (? ? ? %).
+         apply eq_f.assumption
+        |assumption
+        ]
+      |assumption
+      ]
+    |rewrite > false_to_iter_p_gen_Sn
+      [rewrite > false_to_iter_p_gen_Sn in ⊢ (? ? ? %);assumption
+      |assumption
+      ]
+    ]
+  ]
+qed.
+    
 definition p_ord_times \def
 \lambda p,m,x.
   match p_ord x p with
@@ -749,23 +776,6 @@ elim (le_to_or_lt_eq O ? (le_O_n m))
   ]
 qed.
 
-(* lemmino da postare *)
-theorem lt_times_to_lt_div: \forall i,n,m. i < n*m \to i/m < n.
-intros.
-cut (O < m)
-  [apply (lt_times_n_to_lt m)
-    [assumption
-    |apply (le_to_lt_to_lt ? i)
-      [rewrite > (div_mod i m) in \vdash (? ? %).
-       apply le_plus_n_r.
-       assumption
-      |assumption
-      ]
-    ]
-  |apply (lt_times_to_lt_O ? ? ? H)
-  ]
-qed.
-
 theorem iter_p_gen_knm:
 \forall A:Type.
 \forall baseA: A.
diff --git a/helm/software/matita/library/nat/iteration2.ma b/helm/software/matita/library/nat/iteration2.ma
index ea306f455..c5236ff4a 100644
--- a/helm/software/matita/library/nat/iteration2.ma
+++ b/helm/software/matita/library/nat/iteration2.ma
@@ -191,6 +191,20 @@ apply (eq_iter_p_gen_gh nat O plus ? ? ? g h h1 n n1 p1 p2)
 ]
 qed.
 
+theorem eq_sigma_p_pred: 
+\forall n,p,g. p O = true \to
+sigma_p (S n) (\lambda i.p (pred i)) (\lambda i.g(pred i)) = 
+plus (sigma_p n p g) (g O).
+intros.
+unfold sigma_p.
+apply eq_iter_p_gen_pred
+  [assumption
+  |apply symmetricIntPlus
+  |apply associative_plus
+  |intros.apply sym_eq.apply plus_n_O
+  ]
+qed.
+
 (* monotonicity *)
 theorem le_sigma_p: 
 \forall n:nat. \forall p:nat \to bool. \forall g1,g2:nat \to nat.
diff --git a/helm/software/matita/library/nat/lt_arith.ma b/helm/software/matita/library/nat/lt_arith.ma
index d8422a4dd..b4c31c526 100644
--- a/helm/software/matita/library/nat/lt_arith.ma
+++ b/helm/software/matita/library/nat/lt_arith.ma
@@ -118,6 +118,17 @@ apply (nat_case1 a)
 ]
 qed.
 
+lemma lt_times_to_lt_O: \forall i,n,m:nat. i < n*m \to O < m.
+intros.
+elim (le_to_or_lt_eq O ? (le_O_n m))
+  [assumption
+  |apply False_ind.
+   rewrite < H1 in H.
+   rewrite < times_n_O in H.
+   apply (not_le_Sn_O ? H)
+  ]
+qed.
+
 (* times *)
 theorem monotonic_lt_times_r: 
 \forall n:nat.monotonic nat lt (\lambda m.(S n)*m).
diff --git a/helm/software/matita/library/nat/neper.ma b/helm/software/matita/library/nat/neper.ma
index f3db405d4..4b90420c8 100644
--- a/helm/software/matita/library/nat/neper.ma
+++ b/helm/software/matita/library/nat/neper.ma
@@ -195,7 +195,22 @@ apply lt_sigma_p
   ]
 qed.
        
-   
+theorem le_exp_Sn_n_SSSO: \forall n. (exp (S n) n) \le (S(S(S O))).
+intro.  
+apply (trans_le ? (sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!)))
+  [apply le_exp_sigma_p_exp
+  |apply (trans_le ? (sigma_p (S n) (\lambda i.true) (\lambda i.(exp n n)/(exp (S(S O)) i))))
+    [apply le_sigma_p.intros.
+     apply le_times_to_le_div
+      [apply lt_O_exp.
+       apply lt_O_S
+      |apply (trans_le ? ((S(S O))\sup i* n \sup n/i!))
+        [apply le_times_div_div_times.
+         apply lt_O_fact
+        |apply le_times_to_le_div2
+          [apply lt_O_fact
+          |rewrite < sym_times.
+           apply le_times_r.
     
 
    
-- 
2.39.2