X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Ffactorial2.ma;h=bb6c72aebccd7092070199095efb69ea6b279fb3;hb=647b419e96770d90a82d7a9e5e8843566a9f93ee;hp=dd3df52d4952bbe5e4c3bfe4efe40df3fa11b653;hpb=32d926732ac785220007f1999d8ee868efd12e8c;p=helm.git diff --git a/helm/software/matita/library/nat/factorial2.ma b/helm/software/matita/library/nat/factorial2.ma index dd3df52d4..bb6c72aeb 100644 --- a/helm/software/matita/library/nat/factorial2.ma +++ b/helm/software/matita/library/nat/factorial2.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/factorial2". - include "nat/exp.ma". include "nat/factorial.ma". @@ -25,20 +23,16 @@ 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 +theorem lt_O_to_fact1: \forall n.O 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 (trans_le ? ((2*(S n1))*(2*(S n1))*(fact (2*n1)))) [apply le_times_l. rewrite > times_SSO. apply le_times_r. @@ -46,6 +40,7 @@ intro.elim n |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. @@ -54,26 +49,42 @@ intro.elim n 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 + 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 @@ -87,7 +98,7 @@ intro.elim n 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)). +(exp 2 (2*n))*(fact n)*(fact n) < fact (S(2*n)). intros.elim H [simplify.apply le_S.apply le_n |rewrite > times_SSO. @@ -142,7 +153,7 @@ 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). +(exp 2 (2*n))*(exp (fact n) 2) \le 2*n*fact (2*n). intros. elim H [simplify.apply le_n @@ -179,6 +190,83 @@ elim H ] 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.