From 42f80e6de0618ef919d72557e179072a0c8dc771 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 26 Nov 2007 08:45:42 +0000 Subject: [PATCH] Almost there. --- helm/software/matita/library/nat/chebyshev.ma | 271 ++++++++++++++++++ helm/software/matita/library/nat/log.ma | 18 ++ 2 files changed, 289 insertions(+) diff --git a/helm/software/matita/library/nat/chebyshev.ma b/helm/software/matita/library/nat/chebyshev.ma index c06675d0e..a7b473ec0 100644 --- a/helm/software/matita/library/nat/chebyshev.ma +++ b/helm/software/matita/library/nat/chebyshev.ma @@ -1199,6 +1199,277 @@ apply (trans_le ? (B((S(S O))*n)*A n)) ] 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 diff --git a/helm/software/matita/library/nat/log.ma b/helm/software/matita/library/nat/log.ma index 7f31127b6..04ab67d5b 100644 --- a/helm/software/matita/library/nat/log.ma +++ b/helm/software/matita/library/nat/log.ma @@ -214,6 +214,24 @@ split ] qed. +theorem log_exp1: \forall p,n,m.S O < p \to +log p (exp n m) \le m*S(log p n). +intros.elim m + [simplify in ⊢ (? (? ? %) ?). + rewrite > log_SO + [apply le_O_n + |assumption + ] + |simplify. + apply (trans_le ? (S (log p n+log p (n\sup n1)))) + [apply log_times.assumption + |apply le_S_S. + apply le_plus_r. + assumption + ] + ] +qed. + theorem le_log: \forall p,n,m. S O < p \to O < n \to n \le m \to log p n \le log p m. intros. -- 2.39.2