Even if the error is not localized, it was not a good idea to make the unification...

[helm.git] / helm / software / matita / library / nat / chebyshev.ma

diff --git a/helm/software/matita/library/nat/chebyshev.ma b/helm/software/matita/library/nat/chebyshev.ma
index c06675d0e2d3db98e1019496b3ed94887609fba5..567e40ef6bad13927c6098602f9efb7f2bdc7c98 100644 (file)
--- 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 
@@ -1199,6 +1227,335 @@ apply (trans_le ? (B((S(S O))*n)*A n))
   ]
 qed.
 
+theorem le_A_exp1: \forall n.
+A(exp (S(S O)) n) \le (exp (S(S O)) ((S(S O))*(exp (S(S O)) n))).
+intro.elim n
+  [simplify.apply le_S_S.apply le_O_n
+  |change with (A ((S(S O))*((S(S O)))\sup n1)≤ ((S(S O)))\sup((S(S O))*((S(S O))\sup(S n1)))).
+   apply (trans_le ? ((exp (S(S O)) ((S(S O)*(exp (S(S O)) n1))))*A (exp (S(S O)) n1)))
+    [apply le_A_exp
+    |apply (trans_le ? ((S(S O))\sup((S(S O))*((S(S O)))\sup(n1))*(S(S O))\sup((S(S O))*((S(S O)))\sup(n1))))
+      [apply le_times_r.
+       assumption
+      |rewrite < exp_plus_times.
+       simplify.rewrite < plus_n_O in ⊢ (? ? (? ? (? ? %))).
+       apply le_n
+      ]
+    ]
+  ]
+qed.  
+
+theorem monotonic_A: monotonic nat le A.
+unfold.intros.
+elim H
+  [apply le_n
+  |apply (trans_le ? (A n1))
+    [assumption
+    |unfold A.
+     cut (pi_p (S n1) primeb (λp:nat.(p)\sup(log p n1))
+          ≤pi_p (S n1) primeb (λp:nat.(p)\sup(log p (S n1))))
+      [apply (bool_elim ? (primeb (S n1)));intro
+        [rewrite > (true_to_pi_p_Sn ? ? ? H3).
+         rewrite > times_n_SO in ⊢ (? % ?).
+         rewrite > sym_times.
+         apply le_times
+          [apply lt_O_exp.apply lt_O_S
+          |assumption
+          ]
+        |rewrite > (false_to_pi_p_Sn ? ? ? H3).
+         assumption
+        ]
+      |apply le_pi_p.intros.
+       apply le_exp
+        [apply prime_to_lt_O.
+         apply primeb_true_to_prime.
+         assumption
+        |apply le_log
+          [apply prime_to_lt_SO.
+           apply primeb_true_to_prime.
+           assumption
+          |apply (lt_to_le_to_lt ? i)
+            [apply prime_to_lt_O.
+             apply primeb_true_to_prime.
+             assumption
+            |apply le_S_S_to_le.
+             assumption
+            ]
+          |apply le_S.apply le_n
+          ]
+        ]
+      ]
+    ]
+  ]
+qed.
+ 
+theorem le_A_exp2: \forall n. O < n \to
+A(n) \le (exp (S(S O)) ((S(S O)) * (S(S O)) * n)).
+intros.
+apply (trans_le ? (A (exp (S(S O)) (S(log (S(S O)) n)))))
+  [apply monotonic_A.
+   apply lt_to_le.
+   apply lt_exp_log.
+   apply le_n
+  |apply (trans_le ? ((exp (S(S O)) ((S(S O))*(exp (S(S O)) (S(log (S(S O)) n)))))))
+    [apply le_A_exp1
+    |apply le_exp
+      [apply lt_O_S
+      |rewrite > assoc_times.apply le_times_r.
+       change with ((S(S O))*((S(S O))\sup(log (S(S O)) n))≤(S(S O))*n).
+       apply le_times_r.
+       apply le_exp_log.
+       assumption
+      ]
+    ]
+  ]
+qed.
+
+(* example *)
+theorem A_SO: A (S O) = S O.
+reflexivity.
+qed.
+
+theorem A_SSO: A (S(S O)) = S (S O).
+reflexivity.
+qed.
+
+theorem A_SSSO: A (S(S(S O))) = S(S(S(S(S(S O))))).
+reflexivity.
+qed.
+
+theorem A_SSSSO: A (S(S(S(S O)))) = S(S(S(S(S(S(S(S(S(S(S(S O))))))))))).
+reflexivity.
+qed.
+
+(* da spostare *)
+theorem or_eq_eq_S: \forall n.\exists m. 
+n = (S(S O))*m \lor n = S ((S(S O))*m).
+intro.elim n
+  [apply (ex_intro ? ? O).
+   left.reflexivity
+  |elim H.elim H1
+    [apply (ex_intro ? ? a).
+     right.apply eq_f.assumption
+    |apply (ex_intro ? ? (S a)).
+     left.rewrite > H2.
+     apply sym_eq.
+     apply times_SSO
+    ]
+  ]
+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)).
+intro.
+apply (nat_elim1 n).
+intros.
+elim (or_eq_eq_S m).
+elim H2
+  [elim (le_to_or_lt_eq (S O) a)
+    [rewrite > H3 in ⊢ (? % ?).
+     apply (trans_le ? ((exp (S(S O)) ((S(S O)*a)))*A a))
+      [apply le_A_exp
+      |apply (trans_le ? (((S(S O)))\sup((S(S O))*a)*
+         ((pred a)\sup((S(S O)))*((S(S O)))\sup((S(S O))*a))))
+        [apply le_times_r.
+         apply H
+          [rewrite > H3.
+           rewrite > times_n_SO in ⊢ (? % ?).
+           rewrite > sym_times.
+           apply lt_times_l1
+            [apply lt_to_le.assumption
+            |apply le_n
+            ]
+          |assumption
+          ]
+        |rewrite > sym_times.
+         rewrite > assoc_times.
+         rewrite < exp_plus_times.
+         apply (trans_le ? 
+          (pred a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
+          [rewrite > assoc_times.
+           apply le_times_r.
+           rewrite < exp_plus_times.
+           apply le_exp
+            [apply lt_O_S
+            |rewrite < H3.
+             simplify.
+             rewrite < plus_n_O.
+             apply le_S.apply le_S.
+             apply le_n
+            ]
+          |apply le_times_l.
+           rewrite > times_exp.
+           apply monotonic_exp1.
+           rewrite > H3.
+           rewrite > sym_times.
+           cases a
+            [apply le_n
+            |simplify.
+             rewrite < plus_n_Sm.
+             apply le_S.
+             apply le_n
+            ]
+          ]
+        ]
+      ]
+    |rewrite < H4 in H3.
+     simplify in H3.
+     rewrite > H3.
+     simplify.
+     apply le_S_S.apply le_S_S.apply le_O_n
+    |apply not_lt_to_le.intro.
+     apply (lt_to_not_le ? ? H1).
+     rewrite > H3.
+     apply (le_n_O_elim a)
+      [apply le_S_S_to_le.assumption
+      |apply le_O_n
+      ]
+    ]
+  |elim (le_to_or_lt_eq O a (le_O_n ?))
+    [apply (trans_le ? (A ((S(S O))*(S a))))
+      [apply monotonic_A.
+       rewrite > H3.
+       rewrite > times_SSO.
+       apply le_n_Sn
+      |apply (trans_le ? ((exp (S(S O)) ((S(S O)*(S a))))*A (S a)))
+        [apply le_A_exp
+        |apply (trans_le ? (((S(S O)))\sup((S(S O))*S a)*
+           (a\sup((S(S O)))*((S(S O)))\sup((S(S O))*(S a)))))
+          [apply le_times_r.
+           apply H
+            [rewrite > H3.
+             apply le_S_S.
+             simplify.
+             rewrite > plus_n_SO.
+             apply le_plus_r.
+             rewrite < plus_n_O.
+             assumption
+            |apply le_S_S.assumption
+            ]
+          |rewrite > sym_times.
+           rewrite > assoc_times.
+           rewrite < exp_plus_times.
+           apply (trans_le ? 
+            (a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
+            [rewrite > assoc_times.
+             apply le_times_r.
+             rewrite < exp_plus_times.
+             apply le_exp
+              [apply lt_O_S
+              |rewrite > times_SSO.
+               rewrite < H3.
+               simplify.
+               rewrite < plus_n_Sm.
+               rewrite < plus_n_O.
+               apply le_n
+              ]
+            |apply le_times_l.
+             rewrite > times_exp.
+             apply monotonic_exp1.
+             rewrite > H3.
+             rewrite > sym_times.
+             apply le_n
+            ]
+          ]
+        ]
+      ]
+    |rewrite < H4 in H3.simplify in H3.
+     apply False_ind.
+     apply (lt_to_not_le ? ? H1).
+     rewrite > H3.
+     apply le_n
+    ]
+  ]
+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 *)
 theorem times_exp: \forall n,m,p.exp n p * exp m p = exp (n*m) p.
 intros.elim p