[apply prime_to_lt_SO.
apply primeb_true_to_prime.
assumption
- |apply (lt_to_le_to_lt ? x)
- [apply prime_to_lt_O.
- apply primeb_true_to_prime.
- assumption
- |apply leb_true_to_le.
- assumption
- ]
|apply le_S_S_to_le.
assumption
]
[apply prime_to_lt_SO.
apply primeb_true_to_prime.
assumption
- |apply lt_to_le.assumption
|apply le_times_n.
apply lt_O_S
]
[apply prime_to_lt_SO.
apply primeb_true_to_prime.
assumption
- |assumption
|simplify.
apply le_plus_n_r
]
[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
]
]
[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 ⊢ (? ? %).
]
qed.
-
-(* da spostare *)
-theorem times_exp: \forall n,m,p.exp n p * exp m p = exp (n*m) p.
-intros.elim p
- [reflexivity
- |simplify.autobatch
- ]
-qed.
-
-theorem le_exp_log: \forall p,n. O < n \to
-exp p (
-log n) \le n.
-intros.
-apply leb_true_to_le.
-unfold log.
-apply (f_max_true (\lambda x.leb (exp p x) n)).
-apply (ex_intro ? ? O).
-split
- [apply le_O_n
- |apply le_to_leb_true.simplify.assumption
- ]
-qed.
-
-theorem lt_log_n_n: \forall n. O < n \to log n < n.
-intros.
-cut (log n \le n)
- [elim (le_to_or_lt_eq ? ? Hcut)
- [assumption
- |absurd (exp (S(S O)) n \le n)
- [rewrite < H1 in ⊢ (? (? ? %) ?).
- apply le_exp_log.
- assumption
- |apply lt_to_not_le.
- apply lt_m_exp_nm.
- apply le_n
- ]
- ]
- |unfold log.apply le_max_n
- ]
-qed.
-
-theorem le_log_n_n: \forall n. log n \le n.
-intro.
-cases n
- [apply le_n
- |apply lt_to_le.
- apply lt_log_n_n.
- apply lt_O_S
- ]
-qed.
-
-theorem lt_exp_log: \forall n. n < exp (S(S O)) (S (log n)).
-intro.cases n
- [simplify.apply le_S.apply le_n
- |apply not_le_to_lt.
- apply leb_false_to_not_le.
- apply (lt_max_to_false ? (S n1) (S (log (S n1))))
- [apply le_S_S.apply le_n
- |apply lt_log_n_n.apply lt_O_S
- ]
- ]
-qed.
-
-theorem f_false_to_le_max: \forall f,n,p. (∃i:nat.i≤n∧f i=true) \to
-(\forall m. p < m \to f m = false)
-\to max n f \le p.
-intros.
-apply not_lt_to_le.intro.
-apply not_eq_true_false.
-rewrite < (H1 ? H2).
-apply sym_eq.
-apply f_max_true.
-assumption.
-qed.
-
-theorem log_times1: \forall n,m. O < n \to O < m \to
-log (n*m) \le S(log n+log m).
-intros.
-unfold in ⊢ (? (% ?) ?).
-apply f_false_to_le_max
- [apply (ex_intro ? ? O).
- split
- [apply le_O_n
- |apply le_to_leb_true.
- simplify.
- rewrite > times_n_SO.
- apply le_times;assumption
- ]
- |intros.
- apply lt_to_leb_false.
- apply (lt_to_le_to_lt ? ((exp (S(S O)) (S(log n)))*(exp (S(S O)) (S(log m)))))
- [apply lt_times;apply lt_exp_log
- |rewrite < exp_plus_times.
- apply le_exp
- [apply lt_O_S
- |simplify.
- rewrite < plus_n_Sm.
- assumption
- ]
- ]
- ]
-qed.
-
-theorem log_times: \forall n,m.log (n*m) \le S(log n+log m).
-intros.
-cases n
- [apply le_O_n
- |cases m
- [rewrite < times_n_O.
- apply le_O_n
- |apply log_times1;apply lt_O_S
- ]
- ]
-qed.
-
-theorem log_exp: \forall n,m.O < m \to
-log ((exp (S(S O)) n)*m)=n+log m.
-intros.
-unfold log in ⊢ (? ? (% ?) ?).
-apply max_spec_to_max.
-unfold max_spec.
-split
- [split
- [elim n
- [simplify.
- rewrite < plus_n_O.
- apply le_log_n_n
- |simplify.
- rewrite < plus_n_O.
- rewrite > times_plus_l.
- apply (trans_le ? (S((S(S O))\sup(n1)*m)))
- [apply le_S_S.assumption
- |apply (lt_O_n_elim ((S(S O))\sup(n1)*m))
- [rewrite > (times_n_O O) in ⊢ (? % ?).
- apply lt_times
- [apply lt_O_exp.
- apply lt_O_S
- |assumption
- ]
- |intro.simplify.apply le_S_S.
- apply le_plus_n
- ]
- ]
- ]
- |simplify.
- apply le_to_leb_true.
- rewrite > exp_plus_times.
- apply le_times_r.
- apply le_exp_log.
- assumption
- ]
- |intros.
- simplify.
- apply lt_to_leb_false.
- apply (lt_to_le_to_lt ? ((exp (S(S O)) n)*(exp (S(S O)) (S(log m)))))
- [apply lt_times_r1
- [apply lt_O_exp.apply lt_O_S
- |apply lt_exp_log.
- ]
- |rewrite < exp_plus_times.
- apply le_exp
- [apply lt_O_S
- |rewrite < plus_n_Sm.
- assumption
- ]
- ]
- ]
-qed.
-
-theorem log_SSO: \forall n. O < n \to
-log ((S(S O))*n) = S (log n).
-intros.
-change with (log ((exp (S(S O)) (S O))*n)=S (log n)).
-rewrite > log_exp.reflexivity.assumption.
-qed.
-
-theorem or_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.apply times_n_O
- |elim H.elim H1
- [apply (ex_intro ? ? a).right.apply eq_f.assumption
- |apply (ex_intro ? ? (S a)).left.
- rewrite > H2.simplify.
- rewrite < plus_n_O.
- rewrite < plus_n_Sm.
- reflexivity
- ]
- ]
-qed.
-
-theorem lt_O_to_or_eq_S: \forall n.O < n \to \exists m.m < n \land
-((n = (S(S O))*m) \lor (n = S((S(S O))*m))).
-intros.
-elim (or_eq_S n).
-elim H1
- [apply (ex_intro ? ? a).split
- [rewrite > H2.
- rewrite > times_n_SO in ⊢ (? % ?).
- rewrite > sym_times.
- apply lt_times_l1
- [apply (divides_to_lt_O a n ? ?)
- [assumption
- |apply (witness a n (S (S O))).
- rewrite > sym_times.
- assumption
- ]
- |apply le_n
- ]
- |left.assumption
- ]
- |apply (ex_intro ? ? a).split
- [rewrite > H2.
- apply (le_to_lt_to_lt ? ((S(S O))*a))
- [rewrite > times_n_SO in ⊢ (? % ?).
- rewrite > sym_times.
- apply le_times_l.
- apply le_n_Sn
- |apply le_n
- ]
- |right.assumption
- ]
- ]
-qed.
-
-theorem factS: \forall n. fact (S n) = (S n)*(fact n).
-intro.simplify.reflexivity.
-qed.
-
-theorem exp_S: \forall n,m. exp m (S n) = m*exp m n.
-intros.reflexivity.
-qed.
-
-lemma times_SSO: \forall n.(S(S O))*(S n) = S(S((S(S O))*n)).
-intro.simplify.rewrite < plus_n_Sm.reflexivity.
-qed.
-
-theorem fact1: \forall n.
-fact ((S(S O))*n) \le (exp (S(S O)) ((S(S O))*n))*(fact n)*(fact n).
-intro.elim n
- [rewrite < times_n_O.apply le_n
- |rewrite > times_SSO.
- rewrite > factS.
- rewrite > factS.
- rewrite < assoc_times.
- rewrite > factS.
- apply (trans_le ? (((S(S O))*(S n1))*((S(S O))*(S n1))*(fact (((S(S O))*n1)))))
- [apply le_times_l.
- rewrite > times_SSO.
- apply le_times_r.
- apply le_n_Sn
- |rewrite > assoc_times.
- rewrite > assoc_times.
- rewrite > assoc_times in ⊢ (? ? %).
- rewrite > exp_S.
- rewrite > assoc_times in ⊢ (? ? %).
- apply le_times_r.
- rewrite < assoc_times.
- rewrite < assoc_times.
- rewrite < sym_times in ⊢ (? (? (? % ?) ?) ?).
- rewrite > assoc_times.
- rewrite > assoc_times.
- rewrite > exp_S.
- rewrite > assoc_times in ⊢ (? ? %).
- apply le_times_r.
- rewrite > sym_times in ⊢ (? ? %).
- rewrite > assoc_times in ⊢ (? ? %).
- rewrite > assoc_times in ⊢ (? ? %).
- apply le_times_r.
- rewrite < assoc_times in ⊢ (? ? %).
- rewrite < assoc_times in ⊢ (? ? %).
- rewrite < sym_times in ⊢ (? ? (? (? % ?) ?)).
- rewrite > assoc_times in ⊢ (? ? %).
- rewrite > assoc_times in ⊢ (? ? %).
- apply le_times_r.
- rewrite > sym_times in ⊢ (? ? (? ? %)).
- rewrite > sym_times in ⊢ (? ? %).
- assumption
- ]
- ]
-qed.
-
-theorem monotonic_log: monotonic nat le log.
-unfold monotonic.intros.
-elim (le_to_or_lt_eq ? ? H) 0
- [cases x;intro
- [apply le_O_n
- |apply lt_S_to_le.
- apply (lt_exp_to_lt (S(S O)))
- [apply le_n
- |apply (le_to_lt_to_lt ? (S n))
- [apply le_exp_log.
- apply lt_O_S
- |apply (trans_lt ? y)
- [assumption
- |apply lt_exp_log
- ]
- ]
- ]
- ]
- |intro.rewrite < H1.apply le_n
- ]
-qed.
-
-theorem lt_O_fact: \forall n. O < fact n.
-intro.elim n
- [simplify.apply lt_O_S
- |rewrite > factS.
- rewrite > (times_n_O O).
- apply lt_times
- [apply lt_O_S
- |assumption
- ]
- ]
-qed.
-
-theorem fact2: \forall n.O < n \to
-(exp (S(S O)) ((S(S O))*n))*(fact n)*(fact n) < fact (S((S(S O))*n)).
-intros.elim H
- [simplify.apply le_S.apply le_n
- |rewrite > times_SSO.
- rewrite > factS.
- rewrite > factS.
- rewrite < assoc_times.
- rewrite > factS.
- rewrite < times_SSO in ⊢ (? ? %).
- apply (trans_lt ? (((S(S O))*S n1)*((S(S O))*S n1*(S ((S(S O))*n1))!)))
- [rewrite > assoc_times in ⊢ (? ? %).
- rewrite > exp_S.
- rewrite > assoc_times.
- rewrite > assoc_times.
- rewrite > assoc_times.
- apply lt_times_r.
- rewrite > exp_S.
- rewrite > assoc_times.
- rewrite > sym_times in ⊢ (? ? %).
- rewrite > assoc_times in ⊢ (? ? %).
- rewrite > assoc_times in ⊢ (? ? %).
- apply lt_times_r.
- rewrite > sym_times.
- rewrite > assoc_times.
- rewrite > assoc_times.
- apply lt_times_r.
- rewrite < assoc_times.
- rewrite < assoc_times.
- rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?).
- rewrite > assoc_times.
- rewrite > assoc_times.
- rewrite > sym_times in ⊢ (? ? %).
- apply lt_times_r.
- rewrite < assoc_times.
- rewrite < sym_times.
- rewrite < assoc_times.
- assumption
- |apply lt_times_l1
- [rewrite > (times_n_O O) in ⊢ (? % ?).
- apply lt_times
- [rewrite > (times_n_O O) in ⊢ (? % ?).
- apply lt_times
- [apply lt_O_S
- |apply lt_O_S
- ]
- |apply lt_O_fact
- ]
- |apply le_n
- ]
- ]
- ]
-qed.
-
-theorem lt_O_log: \forall n. S O < n \to O < log n.
-intros.elim H
- [simplify.apply lt_O_S
- |apply (lt_to_le_to_lt ? (log n1))
- [assumption
- |apply monotonic_log.
- apply le_n_Sn
- ]
- ]
-qed.
-
-theorem log_fact_SSSO: log (fact (S(S(S O)))) = S (S O).
-reflexivity.
-qed.
-
-lemma exp_SSO_SSO: exp (S(S O)) (S(S O)) = S(S(S(S O))).
-reflexivity.
-qed.
-(*
-theorem log_fact_SSSSO: log (fact (S(S(S(S O))))) = S(S(S(S O))).
-reflexivity.
-qed.
-*)
-theorem log_fact_SSSSSO: log (fact (S(S(S(S(S O)))))) = S(S(S(S O))).
-reflexivity.
-qed.
-
-theorem bof_bof: \forall n.(S(S(S(S O)))) < n \to
-n \le (S(S(S(S(S(S(S(S O)))))))) \to log (fact n) < n*log n - n.
-intros.
-elim H
- [rewrite > factS in ⊢ (? (? %) ?).
- rewrite > factS in ⊢ (? (? (? ? %)) ?).
- rewrite < assoc_times in ⊢ (? (? %) ?).
- rewrite < sym_times in ⊢ (? (? (? % ?)) ?).
- rewrite > assoc_times in ⊢ (? (? %) ?).
- change with (exp (S(S O)) (S(S O))) in ⊢ (? (? (? % ?)) ?).
-
-theorem bof: \forall n.(S(S(S(S O))))) < n \to log (fact n) < n*log n - n.
-intro.apply (nat_elim1 n).
-intros.
-elim (lt_O_to_or_eq_S m)
- [elim H2.clear H2.
- elim H4.clear H4.
- rewrite > H2.
- apply (le_to_lt_to_lt ? (log ((exp (S(S O)) ((S(S O))*a))*(fact a)*(fact a))))
- [apply monotonic_log.
- apply fact1
- |rewrite > assoc_times in ⊢ (? (? %) ?).
- rewrite > log_exp.
- apply (le_to_lt_to_lt ? ((S(S O))*a+S(log a!+log a!)))
- [apply le_plus_r.
- apply log_times
- |rewrite > plus_n_Sm.
- rewrite > log_SSO.
- rewrite < times_n_Sm.
- apply (le_to_lt_to_lt ? ((S(S O))*a+(log a!+(a*log a-a))))
- [apply le_plus_r.
- apply le_plus_r.
- apply H.assumption
- |apply (lt_to_le_to_lt ? ((S(S O))*a+((a*log a-a)+(a*log a-a))))
- [apply lt_plus_r.
- apply lt_plus_l.
- apply H.
- assumption.
- |rewrite > times_SSO_n.
- rewrite > distr_times_minus.
- rewrite > sym_plus.
- rewrite > plus_minus
- [rewrite > sym_plus.
- rewrite < assoc_times.
- apply le_n
- |rewrite < assoc_times.
- rewrite > times_n_SO in ⊢ (? % ?).
- apply le_times
- [apply le_n
- |apply lt_O_log.
- apply (lt_times_n_to_lt_r (S(S O)))
- [apply lt_O_S
- |rewrite < times_n_SO.
- rewrite < H2.
- assumption
- ]
- ]
- ]
- ]
-
- .
- ]
- |
- rewrite < eq_plus_minus_minus_plus.
-
- rewrite > assoc_plus.
- apply lt_plus_r.
- rewrite > plus_n_O in ⊢ (? (? (? ? (? ? %))) ?).
- change with
- (S((S(S O))*a+((S(S O))*log a!)) < (S(S O))*a*log ((S(S O))*a)-(S(S O))*a+k*log ((S(S O))*a)).
- apply (trans_lt ? (S ((S(S O))*a+(S(S O))*(a*log a-a+k*log a))))
- [apply le_S_S.
- apply lt_plus_r.
- apply lt_times_r.
- apply H.
- assumption
- |
-
-theorem stirling: \forall n,k.k \le n \to
-log (fact n) < n*log n - n + k*log n.
-intro.
-apply (nat_elim1 n).
-intros.
-elim (lt_O_to_or_eq_S m)
- [elim H2.clear H2.
- elim H4.clear H4.
- rewrite > H2.
- apply (le_to_lt_to_lt ? (log ((exp (S(S O)) ((S(S O))*a))*(fact a)*(fact a))))
- [apply monotonic_log.
- apply fact1
- |rewrite > assoc_times in ⊢ (? (? %) ?).
- rewrite > log_exp.
- apply (le_to_lt_to_lt ? ((S(S O))*a+S(log a!+log a!)))
- [apply le_plus_r.
- apply log_times
- |rewrite < plus_n_Sm.
- rewrite > plus_n_O in ⊢ (? (? (? ? (? ? %))) ?).
- change with
- (S((S(S O))*a+((S(S O))*log a!)) < (S(S O))*a*log ((S(S O))*a)-(S(S O))*a+k*log ((S(S O))*a)).
- apply (trans_lt ? (S ((S(S O))*a+(S(S O))*(a*log a-a+k*log a))))
- [apply le_S_S.
- apply lt_plus_r.
- apply lt_times_r.
- apply H.
- assumption
- |
-
- [
-
- a*log a-a+k*log a
-
-*)
\ No newline at end of file
projects / helm.git / blobdiff