]
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.
+
+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)).
+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.
+
+
+
(* da spostare *)
theorem times_exp: \forall n,m,p.exp n p * exp m p = exp (n*m) p.
intros.elim p
projects / helm.git / commitdiff