X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Flibrary%2Fnat%2Ffactorial2.ma;fp=matita%2Flibrary%2Fnat%2Ffactorial2.ma;h=bcd228d0801a12f197312637ef7515236b4ba511;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/matita/library/nat/factorial2.ma b/matita/library/nat/factorial2.ma new file mode 100644 index 000000000..bcd228d08 --- /dev/null +++ b/matita/library/nat/factorial2.ma @@ -0,0 +1,304 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "nat/exp.ma". +include "nat/factorial.ma". + +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. + +theorem lt_O_to_fact1: \forall n.O times_SSO. + rewrite > factS. + rewrite > factS. + rewrite < assoc_times. + rewrite > factS. + apply (trans_le ? ((2*(S n1))*(2*(S n1))*(fact (2*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 ⊢ (? ? %). + change in ⊢ (? ? (? (? ? %) ?)) with (S(2*n1)). + 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 > S_pred in ⊢ (? ? (? (? ? %) ?)) + [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 + |unfold.rewrite > times_n_SO in ⊢ (? % ?). + apply le_times + [apply le_n_Sn + |assumption + ] + ] + ] + ] +qed. + +theorem fact1: \forall n. +fact (2*n) \le (exp 2 (pred (2*n)))*(fact n)*(fact n). +intro.cases n + [apply le_n + |apply lt_O_to_fact1. + apply lt_O_S + ] +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. + +(* 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 le_fact_10: fact (2*5) \le (exp 2 ((2*5)-2))*(fact 5)*(fact 5). +simplify in \vdash (? (? %) ?). +rewrite > factS in \vdash (? % ?). +rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash(? % ?). +rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash (? % ?). +rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash (? % ?). +rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash (? % ?). +apply le_times_l. +apply leb_true_to_le.reflexivity. +qed. + +theorem ab_times_cd: \forall a,b,c,d.(a*b)*(c*d)=(a*c)*(b*d). +intros. +rewrite > assoc_times. +rewrite > assoc_times. +apply eq_f. +rewrite < assoc_times. +rewrite < assoc_times. +rewrite > sym_times in \vdash (? ? (? % ?) ?). +reflexivity. +qed. + +(* an even better result *) +theorem lt_SSSSO_to_fact: \forall n.4 times_SSO. + change in \vdash (? ? (? (? (? ? %) ?) ?)) with (2*n1 - O); + rewrite < minus_n_O. + rewrite > factS. + rewrite > factS. + rewrite < assoc_times. + rewrite > factS. + apply (trans_le ? ((2*(S n1))*(2*(S n1))*(fact (2*n1)))) + [apply le_times_l. + rewrite > times_SSO. + apply le_times_r. + apply le_n_Sn + |apply (trans_le ? (2*S n1*(2*S n1)*(2\sup(2*n1-2)*n1!*n1!))) + [apply le_times_r.assumption + |rewrite > assoc_times. + rewrite > ab_times_cd in \vdash (? (? ? %) ?). + rewrite < assoc_times. + apply le_times_l. + rewrite < assoc_times in \vdash (? (? ? %) ?). + rewrite > ab_times_cd. + apply le_times_l. + rewrite < exp_S. + rewrite < exp_S. + apply le_exp + [apply lt_O_S + |rewrite > eq_minus_S_pred. + rewrite < S_pred + [rewrite > eq_minus_S_pred. + rewrite < S_pred + [rewrite < minus_n_O. + apply le_n + |elim H1;simplify + [apply lt_O_S + |apply lt_O_S + ] + ] + |elim H1;simplify + [apply lt_O_S + |rewrite < plus_n_Sm. + rewrite < minus_n_O. + apply lt_O_S + ] + ] + ] + ] + ] + ] +qed. + + +(* +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