From 173965d294635f861850a850769b1530c73b835f Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 30 Jan 2008 09:13:06 +0000 Subject: [PATCH] Improved approximations --- helm/software/matita/library/nat/chebyshev.ma | 242 +++++++++++------- .../software/matita/library/nat/factorial2.ma | 62 +++-- 2 files changed, 184 insertions(+), 120 deletions(-) diff --git a/helm/software/matita/library/nat/chebyshev.ma b/helm/software/matita/library/nat/chebyshev.ma index 2c705635f..e4ca6587a 100644 --- a/helm/software/matita/library/nat/chebyshev.ma +++ b/helm/software/matita/library/nat/chebyshev.ma @@ -1058,7 +1058,7 @@ cut ((S(S O)) < (S ((S(S(S(S O))))*n))) qed. theorem le_fact_A:\forall n.S O < n \to -fact ((S(S O))*n) \le exp (fact n) (S(S O)) * A ((S(S O))*n). +fact (2*n) \le exp (fact n) 2 * A (2*n). intros. rewrite > eq_fact_B [apply le_times_r. @@ -1068,7 +1068,7 @@ rewrite > eq_fact_B qed. theorem lt_SO_to_le_B_exp: \forall n.S O < n \to -B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n). +B (2*n) \le exp 2 (pred (2*n)). intros. apply (le_times_to_le (exp (fact n) (S(S O)))) [apply lt_O_exp. @@ -1084,11 +1084,11 @@ apply (le_times_to_le (exp (fact n) (S(S O)))) qed. theorem le_B_exp: \forall n. -B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n). +B (2*n) \le exp 2 (pred (2*n)). intro.cases n [apply le_n |cases n1 - [simplify.apply le_S.apply le_S.apply le_n + [simplify.apply le_n |apply lt_SO_to_le_B_exp. apply le_S_S.apply lt_O_S. ] @@ -1295,32 +1295,94 @@ intros.cases n qed. theorem le_A_exp: \forall n. -A((S(S O))*n) \le (exp (S(S O)) ((S(S O)*n)))*A n. +A(2*n) \le (exp 2 (pred (2*n)))*A n. intro. -apply (trans_le ? (B((S(S O))*n)*A n)) +apply (trans_le ? (B(2*n)*A n)) [apply le_A_BA |apply le_times_l. apply le_B_exp ] qed. +theorem times_SSO_pred: \forall n. 2*(pred n) \le pred (2*n). +intro.cases n + [apply le_n + |simplify.apply le_plus_r. + apply le_n_Sn + ] +qed. + +theorem le_S_times_SSO: \forall n. O < n \to S n \le 2*n. +intros. +elim H + [apply le_n + |rewrite > times_SSO. + apply le_S_S. + apply (trans_le ? (2*n1)) + [assumption + |apply le_n_Sn + ] + ] +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))). +A(exp 2 n) \le (exp 2 ((2*(exp 2 n)-(S(S 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))) + [simplify.apply le_n + |change in ⊢ (? % ?) with (A(2*(exp 2 n1))). + apply (trans_le ? ((exp 2 (pred(2*(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 (trans_le ? ((2)\sup(pred (2*(2)\sup(n1)))*(2)\sup(2*(2)\sup(n1)-S (S n1)))) [apply le_times_r. assumption |rewrite < exp_plus_times. - simplify.rewrite < plus_n_O in ⊢ (? ? (? ? (? ? %))). - apply le_n + apply le_exp + [apply lt_O_S + |cut (S(S n1) \le 2*(exp 2 n1)) + [apply le_S_S_to_le. + change in ⊢ (? % ?) with (S(pred (2*(2)\sup(n1)))+(2*(2)\sup(n1)-S (S n1))). + rewrite < S_pred + [rewrite > eq_minus_S_pred in ⊢ (? ? %). + rewrite < S_pred + [rewrite < eq_minus_plus_plus_minus + [rewrite > plus_n_O in ⊢ (? (? (? ? %) ?) ?). + apply le_n + |assumption + ] + |apply lt_to_lt_O_minus. + apply (lt_to_le_to_lt ? (2*(S(S n1)))) + [rewrite > times_n_SO in ⊢ (? % ?). + rewrite > sym_times. + apply lt_times_l1 + [apply lt_O_S + |apply le_n + ] + |apply le_times_r. + assumption + ] + ] + |unfold.rewrite > times_n_SO in ⊢ (? % ?). + apply le_times + [apply le_n_Sn + |apply lt_O_exp. + apply lt_O_S + ] + ] + |elim n1 + [apply le_n + |apply (trans_le ? (2*(S(S n2)))) + [apply le_S_times_SSO. + apply lt_O_S + |apply le_times_r. + assumption + ] + ] + ] + ] ] ] ] -qed. +qed. theorem monotonic_A: monotonic nat le A. unfold.intros. @@ -1358,7 +1420,8 @@ elim H ] ] 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. @@ -1380,6 +1443,7 @@ apply (trans_le ? (A (exp (S(S O)) (S(log (S(S O)) n))))) ] ] qed. +*) (* example *) theorem A_SO: A (S O) = S O. @@ -1415,9 +1479,10 @@ intro.elim n ] 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)). +A(n) \le exp (pred n) (2*(exp 2 (2 * n)). intro. apply (nat_elim1 n). intros. @@ -1536,13 +1601,14 @@ elim H2 apply False_ind. apply (lt_to_not_le ? ? H1). rewrite > H3. - apply le_n + apply le_ ] ] qed. +*) theorem le_A_exp4: \forall n. S O < n \to -A(n) \le exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * (pred n))). +A(n) \le (pred n)*exp 2 ((2 * n) -3). intro. apply (nat_elim1 n). intros. @@ -1550,10 +1616,9 @@ 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 (trans_le ? (exp 2 (pred(2*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))*(pred a))))) + |apply (trans_le ? (2\sup(pred(2*a))*((pred a)*2\sup((2*a)-3)))) [apply le_times_r. apply H [rewrite > H3. @@ -1565,56 +1630,35 @@ elim H2 ] |assumption ] - |rewrite > sym_times. + |rewrite < H3. + rewrite < assoc_times. + rewrite > sym_times in ⊢ (? (? % ?) ?). 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))*(pred m)))) - [rewrite > assoc_times. - apply le_times_r. - rewrite < exp_plus_times. + apply le_times + [rewrite > H3. + elim a[apply le_n|simplify.apply le_plus_n_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. - rewrite < plus_n_O; - apply le_S_S_to_le; - rewrite > plus_n_Sm in \vdash (? ? %); - rewrite < S_pred; - [change in \vdash (? % ?) with ((S (pred a + pred a)) + m); - apply le_plus_l; - apply le_S_S_to_le; - rewrite < S_pred; - [rewrite > plus_n_Sm;rewrite > sym_plus; - rewrite > plus_n_Sm; - rewrite > H3;simplify in \vdash (? ? %); - rewrite < plus_n_O;rewrite < S_pred; - [apply le_n - |apply lt_to_le;assumption] - |apply lt_to_le;assumption] - |apply lt_to_le;assumption]] - |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 + |apply (trans_le ? (m+(m-3))) + [apply le_plus_l. + cases m[apply le_n|apply le_n_Sn] + |simplify.rewrite < plus_n_O. + rewrite > eq_minus_plus_plus_minus + [apply le_n + |rewrite > H3. + apply (trans_le ? (2*2)) + [simplify.apply (le_n_Sn 3) + |apply le_times_r.assumption + ] + ] + ] ] ] ] ] - |rewrite < H4 in H3. - simplify in H3. - rewrite > H3. - simplify. - apply le_S_S.apply le_S_S.apply le_O_n + |rewrite > H3.rewrite < H4.simplify. + apply le_S_S.apply lt_O_S |apply not_lt_to_le.intro. apply (lt_to_not_le ? ? H1). rewrite > H3. @@ -1629,41 +1673,44 @@ elim H2 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 (trans_le ? ((exp 2 (pred(2*(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))*a)))) + |apply (trans_le ? ((2\sup(pred (2*S a)))*(a*(exp 2 ((2*(S a))-3))))) [apply le_times_r. - apply (trans_le ? ? ? (H (S a) ? ?)); + apply H [rewrite > H3. apply le_S_S. - simplify. - rewrite > plus_n_SO. - apply le_plus_r. - rewrite < plus_n_O. + apply le_S_times_SSO. assumption |apply le_S_S.assumption - |simplify in ⊢ (? (? (? % ?) ?) ?); - apply le_times_r;apply le_exp; - [apply le_S;apply le_n - |apply le_times_r;simplify;apply le_n] ] - |rewrite > sym_times. - rewrite > assoc_times. - rewrite < exp_plus_times. - rewrite > H3; - change in ⊢ (? ? (? (? % ?) ?)) with ((S (S O))*a); - rewrite < times_exp; - rewrite < sym_times in \vdash (? ? (? % ?)); - rewrite > assoc_times; - apply le_times_r; - rewrite < times_n_Sm in ⊢ (? (? ? (? ? %)) ?); - rewrite > sym_plus in \vdash (? (? ? %) ?); - rewrite > assoc_plus in \vdash (? (? ? %) ?); - rewrite > exp_plus_times;apply le_times_r; - rewrite < distr_times_plus in ⊢ (? (? ? %) ?); - simplify in ⊢ (? ? (? ? (? ? %)));rewrite < plus_n_O; - apply le_n + |rewrite > H3. + change in ⊢ (? ? (? % ?)) with (2*a). + rewrite > times_SSO. + change in ⊢ (? (? (? ? %) ?) ?) with (S(2*a)). + rewrite > minus_Sn_m + [change in ⊢ (? (? ? (? ? %)) ?) with (2*(exp 2 (S(2*a)-3))). + rewrite < assoc_times in ⊢ (? (? ? %) ?). + rewrite < assoc_times. + rewrite > sym_times in ⊢ (? (? % ?) ?). + rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?). + rewrite > assoc_times. + apply le_times_r. + rewrite < exp_plus_times. + apply le_exp + [apply lt_O_S + |rewrite < eq_minus_plus_plus_minus + [rewrite > plus_n_O in ⊢ (? (? (? ? %) ?) ?). + apply le_n + |apply le_S_S. + apply O_lt_const_to_le_times_const. + assumption + ] + ] + |apply le_S_S. + apply O_lt_const_to_le_times_const. + assumption + ] ] ] ] @@ -1778,21 +1825,20 @@ rewrite < (eq_log_exp (S(S O))) in ⊢ (? % ?) 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)) * (pred n))). +exp n (prim n) \le exp (pred n) 2*(exp 2 (2*(2*n-3))). intros. -apply (trans_le ? (exp (A n) (S(S O)))) +apply (trans_le ? (exp (A n) 2)) [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)) * (pred n)))) (S(S O)))) + |apply (trans_le ? (exp ((pred n)*(exp 2 (2*n - 3))) 2)) [apply monotonic_exp1. apply le_A_exp4. assumption |rewrite < times_exp. rewrite > exp_exp_times. - rewrite > exp_exp_times. - rewrite > sym_times in ⊢ (? (? ? (? ? %)) ?). - rewrite < assoc_times in ⊢ (? (? ? (? ? %)) ?). + apply le_times_r. + rewrite > sym_times. apply le_n ] ] diff --git a/helm/software/matita/library/nat/factorial2.ma b/helm/software/matita/library/nat/factorial2.ma index dd3df52d4..1d375df88 100644 --- a/helm/software/matita/library/nat/factorial2.ma +++ b/helm/software/matita/library/nat/factorial2.ma @@ -25,20 +25,21 @@ 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)). +alias num (instance 0) = "natural number". +lemma times_SSO: \forall n.2*(S n) = S(S(2*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 +47,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 +56,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 -- 2.39.2