From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 3 Dec 2007 11:39:09 +0000 (+0000)
Subject: Some progress.
X-Git-Tag: make_still_working~5744
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=32d926732ac785220007f1999d8ee868efd12e8c;p=helm.git

Some progress.
---

diff --git a/helm/software/matita/library/nat/chebyshev.ma b/helm/software/matita/library/nat/chebyshev.ma
index a7b473ec0..567e40ef6 100644
--- a/helm/software/matita/library/nat/chebyshev.ma
+++ b/helm/software/matita/library/nat/chebyshev.ma
@@ -1016,6 +1016,34 @@ intro.cases n
   ]
 qed.
 
+theorem lt_SO_to_le_exp_B: \forall n. S O < n \to
+exp (S(S O)) ((S(S O))*n) \le (S(S O)) * n * B ((S(S O))*n).
+intros.
+apply (le_times_to_le (exp (fact n) (S(S O))))
+  [apply lt_O_exp.
+   apply lt_O_fact
+  |rewrite < assoc_times in ⊢ (? ? %).
+   rewrite > sym_times in ⊢ (? ? (? % ?)).
+   rewrite > assoc_times in ⊢ (? ? %).
+   rewrite < eq_fact_B
+    [rewrite < sym_times.
+     apply fact3.
+     apply lt_to_le.assumption
+    |assumption
+    ]
+  ]
+qed.
+
+theorem le_exp_B: \forall n. O < n \to
+exp (S(S O)) ((S(S O))*n) \le (S(S O)) * n * B ((S(S O))*n).
+intros.
+elim H
+  [apply le_n
+  |apply lt_SO_to_le_exp_B.
+   apply le_S_S.assumption
+  ]
+qed.
+
 theorem eq_A_SSO_n: \forall n.O < n \to
 A((S(S O))*n) =
  pi_p (S ((S(S O))*n)) primeb 
@@ -1317,31 +1345,6 @@ intro.elim n
   ]
 qed.
 
-theorem times_exp: 
-\forall n,m,p. exp n p * exp m p = exp (n*m) p.
-intros.elim p
-  [simplify.reflexivity
-  |simplify.
-   rewrite > assoc_times.
-   rewrite < assoc_times in ⊢ (? ? (? ? %) ?).
-   rewrite < sym_times in ⊢ (? ? (? ? (? % ?)) ?).
-   rewrite > assoc_times in ⊢ (? ? (? ? %) ?).
-   rewrite < assoc_times.
-   rewrite < H.
-   reflexivity
-  ]
-qed.
-
-theorem monotonic_exp1: \forall n.
-monotonic nat le (\lambda x.(exp x n)).
-unfold monotonic. intros.
-simplify.elim n
-  [apply le_n
-  |simplify.
-   apply le_times;assumption
-  ]
-qed.
-
 (* a better result *)
 theorem le_A_exp3: \forall n. S O < n \to
 A(n) \le exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * n)).
@@ -1468,6 +1471,89 @@ elim H2
   ]
 qed.
 
+theorem eq_sigma_pi_SO_n: \forall n.
+sigma_p n (\lambda i.true) (\lambda i.S O) = n.
+intro.elim n
+  [reflexivity
+  |rewrite > true_to_sigma_p_Sn
+    [rewrite > H.reflexivity
+    |reflexivity
+    ]
+  ]
+qed.
+
+theorem leA_prim: \forall n.
+exp n (prim n) \le A n * pi_p (S n) primeb (λp:nat.p).
+intro.
+unfold prim.
+rewrite < (exp_sigma_p (S n) n primeb).
+unfold A.
+rewrite < times_pi_p.
+apply le_pi_p.
+intros.
+rewrite > sym_times.
+change in ⊢ (? ? %) with (exp i (S (log i n))).
+apply lt_to_le.
+apply lt_exp_log.
+apply prime_to_lt_SO.
+apply primeb_true_to_prime.
+assumption.
+qed.
+
+
+(* the inequalities *)
+theorem le_exp_priml: \forall n. O < n \to
+exp (S(S O)) ((S(S O))*n) \le exp ((S(S O))*n) (S(prim ((S(S O))*n))).
+intros.
+apply (trans_le ? ((((S(S O))*n*(B ((S(S O))*n))))))
+  [apply le_exp_B.assumption
+  |change in ⊢ (? ? %) with ((((S(S O))*n))*(((S(S O))*n))\sup (prim ((S(S O))*n))).
+   apply le_times_r.
+   apply (trans_le ? (A ((S(S O))*n)))
+    [apply le_B_A
+    |apply le_Al
+    ]
+  ]
+qed.
+
+theorem le_priml: \forall n. O < n \to
+(S(S O))*n \le (S (log (S(S O)) ((S(S O))*n)))*S(prim ((S(S O))*n)).
+intros.
+rewrite < (eq_log_exp (S(S O))) in ⊢ (? % ?)
+  [apply (trans_le ? ((log (S(S O)) (exp ((S(S O))*n) (S(prim ((S(S O))*n)))))))
+    [apply le_log
+      [apply le_n
+      |apply lt_O_exp.apply lt_O_S
+      |apply le_exp_priml.assumption
+      ]
+    |rewrite > sym_times in ⊢ (? ? %). 
+     apply log_exp1.
+     apply le_n
+    ]
+  |apply le_n
+  ]
+qed.
+
+theorem le_exp_primr: \forall n. S O < n \to
+exp n (prim n) \le exp (pred n) ((S(S O))*(S(S O)))*(exp (S(S O)) ((S(S O))*(S(S O)) * n)).
+intros.
+apply (trans_le ? (exp (A n) (S(S O))))
+  [change in ⊢ (? ? %) with ((A n)*((A n)*(S O))).
+   rewrite < times_n_SO.
+   apply leA_r2
+  |apply (trans_le ? (exp (exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * n))) (S(S O))))
+    [apply monotonic_exp1.
+     apply le_A_exp3.
+     assumption
+    |rewrite < times_exp.
+     rewrite > exp_exp_times.
+     rewrite > exp_exp_times.
+     rewrite > sym_times in ⊢ (? (? ? (? ? %)) ?).
+     rewrite < assoc_times in ⊢ (? (? ? (? ? %)) ?).
+     apply le_n
+    ]
+  ]
+qed.
 
 
 (* da spostare *)
diff --git a/helm/software/matita/library/nat/div_and_mod.ma b/helm/software/matita/library/nat/div_and_mod.ma
index 0323b18fb..523f74314 100644
--- a/helm/software/matita/library/nat/div_and_mod.ma
+++ b/helm/software/matita/library/nat/div_and_mod.ma
@@ -223,6 +223,7 @@ apply (div_mod_spec_to_eq2 (q*m+r) m ((q*m+r)/ m) ((q*m+r) \mod m) q r)
   |apply div_mod_spec_intro[assumption|reflexivity]
   ]
 qed.
+
 (* some properties of div and mod *)
 theorem div_times: \forall n,m:nat. ((S n)*m) / (S n) = m.
 intros.
@@ -312,19 +313,6 @@ rewrite > (div_mod ? (S O)) in \vdash (? ? ? %)
   ]
 qed.
 
-theorem le_div: \forall n,m. O < n \to m/n \le m.
-intros.
-rewrite > (div_mod m n) in \vdash (? ? %)
-  [apply (trans_le ? (m/n*n))
-    [rewrite > times_n_SO in \vdash (? % ?).
-     apply le_times
-      [apply le_n|assumption]
-    |apply le_plus_n_r
-    ]
-  |assumption
-  ]
-qed.
-
 theorem or_div_mod: \forall n,q. O < q \to
 ((S (n \mod q)=q) \land S n = (S (div n q)) * q \lor
 ((S (n \mod q)<q) \land S n= (div n q) * q + S (n\mod q))).
@@ -395,6 +383,7 @@ qed.
 variant inj_times_l1:\forall n. O < n \to \forall p,q:nat.p*n = q*n \to p=q
 \def lt_O_to_injective_times_l.
 
+      
 (* n_divides computes the pair (div,mod) *)
 
 (* p is just an upper bound, acc is an accumulator *)
diff --git a/helm/software/matita/library/nat/div_and_mod_diseq.ma b/helm/software/matita/library/nat/div_and_mod_diseq.ma
new file mode 100644
index 000000000..53c59de35
--- /dev/null
+++ b/helm/software/matita/library/nat/div_and_mod_diseq.ma
@@ -0,0 +1,308 @@
+(**************************************************************************)
+(*       ___	                                                          *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        Matita is distributed under the terms of the          *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/nat/div_and_mod_diseq".
+
+include "nat/lt_arith.ma".
+
+(* the proof that 
+     n \mod m < m, 
+   called lt_mod_m_m, is in div_and_mod.
+Other inequalities are also in lt_arith.ma.  
+*)
+
+theorem lt_div_S: \forall n,m. O < m \to 
+n < S(n / m)*m.
+intros.
+change with (n < m +(n/m)*m).
+rewrite > sym_plus.
+rewrite > (div_mod n m H) in ⊢ (? % ?).
+apply lt_plus_r.
+apply lt_mod_m_m.
+assumption.
+qed.
+
+theorem le_div: \forall n,m. O < n \to m/n \le m.
+intros.
+rewrite > (div_mod m n) in \vdash (? ? %)
+  [apply (trans_le ? (m/n*n))
+    [rewrite > times_n_SO in \vdash (? % ?).
+     apply le_times
+      [apply le_n|assumption]
+    |apply le_plus_n_r
+    ]
+  |assumption
+  ]
+qed.
+
+theorem le_plus_mod: \forall m,n,q. O < q \to
+(m+n) \mod q \le m \mod q + n \mod q .
+intros.
+elim (decidable_le q (m \mod q + n \mod q))
+  [apply not_lt_to_le.intro.
+   apply (le_to_not_lt q q)
+    [apply le_n
+    |apply (le_to_lt_to_lt ? (m\mod q+n\mod q))
+      [assumption
+      |apply (trans_lt ? ((m+n)\mod q))
+        [assumption
+        |apply lt_mod_m_m.assumption
+        ]
+      ]
+    ]
+  |cut ((m+n)\mod q = m\mod q+n\mod q)
+    [rewrite < Hcut.apply le_n
+    |apply (div_mod_spec_to_eq2 (m+n) q ((m+n)/q) ((m+n) \mod q) (m/q + n/q))
+      [apply div_mod_spec_div_mod.
+       assumption
+      |apply div_mod_spec_intro
+        [apply not_le_to_lt.assumption
+        |rewrite > (div_mod n q H) in ⊢ (? ? (? ? %) ?).
+         rewrite < assoc_plus.
+         rewrite < assoc_plus in ⊢ (? ? ? %).
+         apply eq_f2
+          [rewrite > (div_mod m q) in ⊢ (? ? (? % ?) ?)
+            [rewrite > sym_times in ⊢ (? ? ? (? % ?)).
+             rewrite > distr_times_plus.
+             rewrite > sym_times in ⊢ (? ? ? (? (? % ?) ?)).
+             rewrite > assoc_plus.
+             rewrite > assoc_plus in ⊢ (? ? ? %).
+             apply eq_f.
+             rewrite > sym_plus.
+             rewrite > sym_times.
+             reflexivity
+            |assumption
+            ]
+          |reflexivity
+          ]
+        ]
+      ]
+    ]
+  ]
+qed.
+
+theorem le_plus_div: \forall m,n,q. O < q \to
+m/q + n/q \le (m+n)/q.
+intros.
+apply (le_times_to_le q)
+  [assumption
+  |rewrite > distr_times_plus.
+   rewrite > sym_times.
+   rewrite > sym_times in ⊢ (? (? ? %) ?).
+   rewrite > sym_times in ⊢ (? ? %).
+   apply (le_plus_to_le ((m+n) \mod q)).
+   rewrite > sym_plus in ⊢ (? ? %).
+   rewrite < (div_mod ? ? H).
+   rewrite > (div_mod n q H) in ⊢ (? ? (? ? %)).
+   rewrite < assoc_plus.
+   rewrite > sym_plus in ⊢ (? ? (? ? %)).
+   rewrite < assoc_plus in ⊢ (? ? %).
+   apply le_plus_l.
+   rewrite > (div_mod m q H) in ⊢ (? ? (? % ?)).
+   rewrite > assoc_plus.
+   rewrite > sym_plus.
+   apply le_plus_r.
+   apply le_plus_mod.
+   assumption
+  ]
+qed.
+
+theorem le_times_to_le_div: \forall a,b,c:nat.
+O \lt b \to (b*c) \le a \to c \le (a /b).
+intros.
+apply lt_S_to_le.
+apply (lt_times_n_to_lt b)
+  [assumption
+  |rewrite > sym_times.
+   apply (le_to_lt_to_lt ? a)
+    [assumption
+    |simplify.
+     rewrite > sym_plus.
+     rewrite > (div_mod a b) in ⊢ (? % ?)
+      [apply lt_plus_r.
+       apply lt_mod_m_m.
+       assumption
+      |assumption
+      ]
+    ]
+  ]
+qed.
+
+theorem le_times_to_le_div2: \forall m,n,q. O < q \to 
+n \le m*q \to n/q \le m.
+intros.
+apply (le_times_to_le q ? ? H).
+rewrite > sym_times.
+rewrite > sym_times in ⊢ (? ? %).
+apply (le_plus_to_le (n \mod q)).
+rewrite > sym_plus.
+rewrite < div_mod
+  [apply (trans_le ? (m*q))
+    [assumption
+    |apply le_plus_n
+    ]
+  |assumption
+  ]
+qed.
+
+(* da spostare *)
+theorem lt_m_nm: \forall n,m. O < m \to S O < n \to 
+m < n*m.
+intros.
+elim H1
+  [simplify.rewrite < plus_n_O.
+   rewrite > plus_n_O in ⊢ (? % ?).
+   apply lt_plus_r.assumption
+  |simplify.
+   rewrite > plus_n_O in ⊢ (? % ?).
+   rewrite > sym_plus.
+   apply lt_plus
+    [assumption
+    |assumption
+    ]
+  ]
+qed.
+
+theorem lt_times_to_lt: \forall i,n,m. O < i \to
+i * n < i * m \to n < m.
+intros.
+apply not_le_to_lt.intro.
+apply (lt_to_not_le ? ? H1).
+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.
+intros.
+apply (lt_times_to_lt q ? ? H).
+rewrite > sym_times.
+rewrite > sym_times in ⊢ (? ? %).
+apply (le_plus_to_le (n \mod q)).
+rewrite < plus_n_Sm. 
+rewrite > sym_plus.
+rewrite < div_mod
+  [apply (trans_le ? (m*q))
+    [assumption
+    |apply le_plus_n
+    ]
+  |assumption
+  ]
+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
+  ]
+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
+    ]
+  ]
+qed.
+
+theorem le_div_S_S_div: \forall n,m. O < m \to
+(S n)/m \le S (n /m).
+intros.
+apply le_times_to_le_div2
+  [assumption
+  |simplify.
+   rewrite > (div_mod n m H) in ⊢ (? (? %) ?).
+   rewrite > plus_n_Sm.
+   rewrite > sym_plus.
+   apply le_plus_l.
+   apply lt_mod_m_m.
+   assumption.
+  ]
+qed.
+
+theorem le_times_div_div_times: \forall a,n,m.O < m \to 
+a*(n/m) \le a*n/m. 
+intros.
+apply le_times_to_le_div
+  [assumption
+  |rewrite > sym_times.
+   rewrite > assoc_times.
+   apply le_times_r.
+   rewrite > (div_mod n m H) in ⊢ (? ? %).
+   apply le_plus_n_r.
+  ]
+qed.
+
+theorem monotonic_div: \forall n.O < n \to
+monotonic nat le (\lambda m.div m n).
+unfold monotonic.simplify.intros.
+apply le_times_to_le_div
+  [assumption
+  |apply (trans_le ? x)
+    [rewrite > sym_times.
+     rewrite > (div_mod x n H) in ⊢ (? ? %).
+     apply le_plus_n_r
+    |assumption
+    ]
+  ]
+qed.
+ 
+theorem le_div_times_m: \forall a,i,m. O < i \to O < m \to
+(a * (m / i)) / m \le a / i.
+intros.
+apply (trans_le ? ((a*m/i)/m))
+  [apply monotonic_div
+    [assumption
+    |apply le_times_div_div_times.
+     assumption
+    ]
+  |rewrite > eq_div_div_div_times
+    [rewrite > sym_times in ⊢ (? (? ? %) ?).
+     rewrite < eq_div_div_div_times
+      [apply monotonic_div
+        [assumption
+        |rewrite > lt_O_to_div_times
+          [apply le_n
+          |assumption
+          ]
+        ]
+      |assumption
+      |assumption
+      ]
+    |assumption
+    |assumption
+    ]
+  ]
+qed.
+       
diff --git a/helm/software/matita/library/nat/exp.ma b/helm/software/matita/library/nat/exp.ma
index 49efe8525..74a3be71f 100644
--- a/helm/software/matita/library/nat/exp.ma
+++ b/helm/software/matita/library/nat/exp.ma
@@ -187,6 +187,30 @@ elim (le_to_or_lt_eq n m)
   ]
 qed.
      
-   
+theorem times_exp: 
+\forall n,m,p. exp n p * exp m p = exp (n*m) p.
+intros.elim p
+  [simplify.reflexivity
+  |simplify.
+   rewrite > assoc_times.
+   rewrite < assoc_times in ⊢ (? ? (? ? %) ?).
+   rewrite < sym_times in ⊢ (? ? (? ? (? % ?)) ?).
+   rewrite > assoc_times in ⊢ (? ? (? ? %) ?).
+   rewrite < assoc_times.
+   rewrite < H.
+   reflexivity
+  ]
+qed.
+
+theorem monotonic_exp1: \forall n.
+monotonic nat le (\lambda x.(exp x n)).
+unfold monotonic. intros.
+simplify.elim n
+  [apply le_n
+  |simplify.
+   apply le_times;assumption
+  ]
+qed.
+  
    
    
\ No newline at end of file
diff --git a/helm/software/matita/library/nat/factorial2.ma b/helm/software/matita/library/nat/factorial2.ma
index 4f3631cdb..dd3df52d4 100644
--- a/helm/software/matita/library/nat/factorial2.ma
+++ b/helm/software/matita/library/nat/factorial2.ma
@@ -140,6 +140,45 @@ intros.elim H
   ]
 qed.
 
+(* a slightly better result *)
+theorem fact3: \forall n.O < n \to
+(exp (S(S O)) ((S(S O))*n))*(exp (fact n) (S(S O))) \le (S(S O))*n*fact ((S(S O))*n).
+intros.
+elim H
+  [simplify.apply le_n
+  |rewrite > times_SSO.
+   rewrite > factS.
+   rewrite < times_exp.
+   change in ⊢ (? (? % ?) ?) with ((S(S O))*((S(S O))*(exp (S(S O)) ((S(S O))*n1)))).
+   rewrite > assoc_times.
+   rewrite > assoc_times in ⊢ (? (? ? %) ?).
+   rewrite < assoc_times in ⊢ (? (? ? (? ? %)) ?).
+   rewrite < sym_times in ⊢ (? (? ? (? ? (? % ?))) ?).
+   rewrite > assoc_times in ⊢ (? (? ? (? ? %)) ?).
+   apply (trans_le ? (((S(S O))*((S(S O))*((S n1)\sup((S(S O)))*((S(S O))*n1*((S(S O))*n1)!))))))
+    [apply le_times_r.
+     apply le_times_r.
+     apply le_times_r.
+     assumption
+    |rewrite > factS.
+     rewrite > factS.
+     rewrite < times_SSO.
+     rewrite > assoc_times in ⊢ (? ? %). 
+     apply le_times_r.
+     rewrite < assoc_times.
+     change in ⊢ (? (? (? ? %) ?) ?) with ((S n1)*((S n1)*(S O))).
+     rewrite < assoc_times in ⊢ (? (? % ?) ?).
+     rewrite < times_n_SO.
+     rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?).
+     rewrite < assoc_times in ⊢ (? ? %).
+     rewrite < assoc_times in ⊢ (? ? (? % ?)).
+     apply le_times_r.
+     apply le_times_l.
+     apply le_S.apply le_n
+    ]
+  ]
+qed.
+
 (*
 theorem stirling: \forall n,k.k \le n \to
 log (fact n) < n*log n - n + k*log n.
diff --git a/helm/software/matita/library/nat/log.ma b/helm/software/matita/library/nat/log.ma
index 04ab67d5b..d96fb28c2 100644
--- a/helm/software/matita/library/nat/log.ma
+++ b/helm/software/matita/library/nat/log.ma
@@ -214,6 +214,20 @@ split
   ]
 qed.
 
+theorem eq_log_exp: \forall p,n.S O < p \to
+log p (exp p n)=n.
+intros.
+rewrite > times_n_SO in ⊢ (? ? (? ? %) ?).
+rewrite > log_exp
+  [rewrite > log_SO
+    [rewrite < plus_n_O.reflexivity
+    |assumption
+    ]
+  |assumption
+  |apply le_n
+  ]
+qed.
+
 theorem log_exp1: \forall p,n,m.S O < p \to
 log p (exp n m) \le m*S(log p n).
 intros.elim m
diff --git a/helm/software/matita/library/nat/lt_arith.ma b/helm/software/matita/library/nat/lt_arith.ma
index 623f30295..d8422a4dd 100644
--- a/helm/software/matita/library/nat/lt_arith.ma
+++ b/helm/software/matita/library/nat/lt_arith.ma
@@ -239,26 +239,7 @@ apply (nat_case n)
   ]
 qed.
 
-theorem le_times_to_le_div: \forall a,b,c:nat.
-O \lt b \to (b*c) \le a \to c \le (a /b).
-intros.
-apply lt_S_to_le.
-apply (lt_times_n_to_lt b)
-  [assumption
-  |rewrite > sym_times.
-   apply (le_to_lt_to_lt ? a)
-    [assumption
-    |simplify.
-     rewrite > sym_plus.
-     rewrite > (div_mod a b) in ⊢ (? % ?)
-      [apply lt_plus_r.
-       apply lt_mod_m_m.
-       assumption
-      |assumption
-      ]
-    ]
-  ]
-qed.
+
 
 theorem nat_compare_times_l : \forall n,p,q:nat. 
 nat_compare p q = nat_compare ((S n) * p) ((S n) * q).