From 9e028235daa0abea353d06b4226d4c6698ede3d4 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 19 Nov 2007 11:55:54 +0000 Subject: [PATCH] Towards chebyshev. --- matita/library/nat/chebyshev.ma | 1680 ++++++++++++++++++++++++++ matita/library/nat/compare.ma | 17 + matita/library/nat/div_and_mod.ma | 25 + matita/library/nat/euler_theorem.ma | 2 - matita/library/nat/exp.ma | 23 +- matita/library/nat/factorial2.ma | 177 +++ matita/library/nat/factorization.ma | 53 +- matita/library/nat/gcd.ma | 28 +- matita/library/nat/generic_iter_p.ma | 118 +- matita/library/nat/le_arith.ma | 12 + matita/library/nat/log.ma | 274 +++++ matita/library/nat/lt_arith.ma | 95 ++ matita/library/nat/minimization.ma | 149 +++ matita/library/nat/ord.ma | 161 ++- matita/library/nat/orders.ma | 10 + matita/library/nat/pi_p.ma | 395 ++++++ matita/library/nat/primes.ma | 34 +- 17 files changed, 3214 insertions(+), 39 deletions(-) create mode 100644 matita/library/nat/chebyshev.ma create mode 100644 matita/library/nat/factorial2.ma create mode 100644 matita/library/nat/log.ma create mode 100644 matita/library/nat/pi_p.ma diff --git a/matita/library/nat/chebyshev.ma b/matita/library/nat/chebyshev.ma new file mode 100644 index 000000000..f980d4458 --- /dev/null +++ b/matita/library/nat/chebyshev.ma @@ -0,0 +1,1680 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/nat/chebishev". + +include "nat/log.ma". +include "nat/pi_p.ma". +include "nat/factorization.ma". +include "nat/factorial2.ma". + +definition prim: nat \to nat \def +\lambda n. sigma_p (S n) primeb (\lambda p.(S O)). + +definition A: nat \to nat \def +\lambda n. pi_p (S n) primeb (\lambda p.exp p (log p n)). + +theorem le_Al1: \forall n. +A n \le pi_p (S n) primeb (\lambda p.n). +intro.unfold A. +cases n + [simplify.apply le_n + |apply le_pi_p. + intros. + apply le_exp_log. + apply lt_O_S + ] +qed. + +theorem le_Al: \forall n. +A n \le exp n (prim n). +intro.unfold prim. +rewrite < exp_sigma_p. +apply le_Al1. +qed. + +theorem leA_r2: \forall n. +exp n (prim n) \le A n * A n. +intro.unfold prim. +elim (le_to_or_lt_eq ? ? (le_O_n n)) + [rewrite < (exp_sigma_p (S n) n primeb). + unfold A. + rewrite < times_pi_p. + apply le_pi_p. + intros. + rewrite < exp_plus_times. + apply (trans_le ? (exp i (S(log i n)))) + [apply lt_to_le. + apply lt_exp_log. + apply prime_to_lt_SO. + apply primeb_true_to_prime. + assumption + |apply le_exp + [apply prime_to_lt_O. + apply primeb_true_to_prime. + assumption + |rewrite > plus_n_O. + simplify. + rewrite > plus_n_Sm. + apply le_plus_r. + apply lt_O_log + [assumption + |apply le_S_S_to_le. + apply H1 + ] + ] + ] + |rewrite < H. apply le_n + ] +qed. + +definition A': nat \to nat \def +\lambda n. pi_p (S n) primeb + (\lambda p.(pi_p (log p n) (\lambda i.true) (\lambda i.p))). + +theorem eq_A_A': \forall n.A n = A' n. +intro.unfold A.unfold A'. +apply eq_pi_p + [intros.reflexivity + |intros. + apply (trans_eq ? ? (exp x (sigma_p (log x n) (λi:nat.true) (λi:nat.(S O))))) + [apply eq_f.apply sym_eq.apply sigma_p_true + |apply sym_eq.apply exp_sigma_p + ] + ] +qed. + +theorem eq_pi_p_primeb_divides_b: \forall n,m. +pi_p n (\lambda p.primeb p \land divides_b p m) (\lambda p.exp p (ord m p)) += pi_p n primeb (\lambda p.exp p (ord m p)). +intro. +elim n + [reflexivity + |apply (bool_elim ? (primeb n1));intro + [rewrite > true_to_pi_p_Sn in ⊢ (? ? ? %) + [apply (bool_elim ? (divides_b n1 m));intro + [rewrite > true_to_pi_p_Sn + [apply eq_f. + apply H + |apply true_to_true_to_andb_true;assumption + ] + |rewrite > false_to_pi_p_Sn + [rewrite > not_divides_to_ord_O + [simplify in ⊢ (? ? ? (? % ?)). + rewrite > sym_times. + rewrite < times_n_SO. + apply H + |apply primeb_true_to_prime.assumption + |apply divides_b_false_to_not_divides. + assumption + ] + |rewrite > H1.rewrite > H2.reflexivity + ] + ] + |assumption + ] + |rewrite > false_to_pi_p_Sn + [rewrite > false_to_pi_p_Sn + [apply H + |assumption + ] + |rewrite > H1.reflexivity + ] + ] + ] +qed. + +theorem lt_max_to_pi_p_primeb: \forall q,m. O < m \to max m (\lambda i.primeb i \land divides_b i m) < q \to +m = pi_p q (\lambda i.primeb i \land divides_b i m) (\lambda p.exp p (ord m p)). +intro.elim q + [apply False_ind. + apply (not_le_Sn_O ? H1) + |apply (bool_elim ? (primeb n∧divides_b n m));intro + [rewrite > true_to_pi_p_Sn + [rewrite > (exp_ord n m) in ⊢ (? ? % ?) + [apply eq_f. + rewrite > (H (ord_rem m n)) + [apply eq_pi_p1 + [intros. + apply (bool_elim ? (primeb x));intro + [simplify. + apply (bool_elim ? (divides_b x (ord_rem m n)));intro + [apply sym_eq. + apply divides_to_divides_b_true + [apply prime_to_lt_O. + apply primeb_true_to_prime. + assumption + |apply (trans_divides ? (ord_rem m n)) + [apply divides_b_true_to_divides. + assumption + |apply divides_ord_rem + [apply (trans_lt ? x) + [apply prime_to_lt_SO. + apply primeb_true_to_prime. + assumption + |assumption + ] + |assumption + ] + ] + ] + |apply sym_eq. + apply not_divides_to_divides_b_false + [apply prime_to_lt_O. + apply primeb_true_to_prime. + assumption + |apply ord_O_to_not_divides + [assumption + |apply primeb_true_to_prime. + assumption + |rewrite < (ord_ord_rem n) + [apply not_divides_to_ord_O + [apply primeb_true_to_prime. + assumption + |apply divides_b_false_to_not_divides. + assumption + ] + |assumption + |apply primeb_true_to_prime. + apply (andb_true_true ? ? H3) + |apply primeb_true_to_prime. + assumption + |assumption + ] + ] + ] + ] + |reflexivity + ] + |intros. + apply eq_f. + apply ord_ord_rem + [assumption + |apply primeb_true_to_prime. + apply (andb_true_true ? ? H3) + |apply primeb_true_to_prime. + apply (andb_true_true ? ? H5) + |assumption + ] + ] + |apply lt_O_ord_rem + [apply prime_to_lt_SO. + apply primeb_true_to_prime. + apply (andb_true_true ? ? H3) + |assumption + ] + |apply not_eq_to_le_to_lt + [elim (exists_max_forall_false (λi:nat.primeb i∧divides_b i (ord_rem m n)) (ord_rem m n)) + [elim H4. + intro.rewrite > H7 in H6.simplify in H6. + apply (not_divides_ord_rem m n) + [assumption + |apply prime_to_lt_SO. + apply primeb_true_to_prime. + apply (andb_true_true ? ? H3) + |apply divides_b_true_to_divides. + apply (andb_true_true_r ? ? H6) + ] + |elim H4.rewrite > H6. + apply lt_to_not_eq. + apply prime_to_lt_O. + apply primeb_true_to_prime. + apply (andb_true_true ? ? H3) + ] + |apply (trans_le ? (max m (λi:nat.primeb i∧divides_b i (ord_rem m n)))) + [apply le_to_le_max. + apply divides_to_le + [assumption + |apply divides_ord_rem + [apply prime_to_lt_SO. + apply primeb_true_to_prime. + apply (andb_true_true ? ? H3) + |assumption + ] + ] + |apply (trans_le ? (max m (λi:nat.primeb i∧divides_b i m))) + [apply le_max_f_max_g. + intros. + apply (bool_elim ? (primeb i));intro + [simplify. + apply divides_to_divides_b_true + [apply prime_to_lt_O. + apply primeb_true_to_prime. + assumption + |apply (trans_divides ? (ord_rem m n)) + [apply divides_b_true_to_divides. + apply (andb_true_true_r ? ? H5) + |apply divides_ord_rem + [apply prime_to_lt_SO. + apply primeb_true_to_prime. + apply (andb_true_true ? ? H3) + |assumption + ] + ] + ] + |rewrite > H6 in H5. + assumption + ] + |apply le_S_S_to_le. + assumption + ] + ] + ] + ] + |apply prime_to_lt_SO. + apply primeb_true_to_prime. + apply (andb_true_true ? ? H3) + |assumption + ] + |assumption + ] + |elim (le_to_or_lt_eq ? ? H1) + [rewrite > false_to_pi_p_Sn + [apply H + [assumption + |apply false_to_lt_max + [apply (lt_to_le_to_lt ? (max m (λi:nat.primeb i∧divides_b i m))) + [apply lt_to_le. + apply lt_SO_max_prime. + assumption + |apply le_S_S_to_le. + assumption + ] + |assumption + |apply le_S_S_to_le. + assumption + ] + ] + |assumption + ] + |rewrite < H4. + rewrite < (pi_p_false (λp:nat.p\sup(ord (S O) p)) (S n) ) in ⊢ (? ? % ?). + apply eq_pi_p + [intros. + apply (bool_elim ? (primeb x));intro + [apply sym_eq. + change with (divides_b x (S O) =false). + apply not_divides_to_divides_b_false + [apply prime_to_lt_O. + apply primeb_true_to_prime. + assumption + |intro. + apply (le_to_not_lt x (S O)) + [apply divides_to_le + [apply lt_O_S.assumption + |assumption + ] + |elim (primeb_true_to_prime ? H6). + assumption + ] + ] + |reflexivity + ] + |intros.reflexivity + ] + ] + ] + ] +qed. + +theorem pi_p_primeb_divides_b: \forall n. O < n \to +n = pi_p (S n) (\lambda i.primeb i \land divides_b i n) (\lambda p.exp p (ord n p)). +intros. +apply lt_max_to_pi_p_primeb + [assumption + |apply le_S_S. + apply le_max_n + ] +qed. + +theorem pi_p_primeb: \forall n. O < n \to +n = pi_p (S n) primeb (\lambda p.exp p (ord n p)). +intros. +rewrite < eq_pi_p_primeb_divides_b. +apply pi_p_primeb_divides_b. +assumption. +qed. + +theorem le_ord_log: \forall n,p. O < n \to S O < p \to +ord n p \le log p n. +intros. +rewrite > (exp_ord p) in ⊢ (? ? (? ? %)) + [rewrite > log_exp + [apply le_plus_n_r + |assumption + |apply lt_O_ord_rem;assumption + ] + |assumption + |assumption + ] +qed. + +theorem sigma_p_divides_b: +\forall m,n,p. O < n \to prime p \to \lnot divides p n \to +m = sigma_p m (λi:nat.divides_b (p\sup (S i)) ((exp p m)*n)) (λx:nat.S O). +intro.elim m + [reflexivity + |simplify in ⊢ (? ? ? (? % ? ?)). + rewrite > true_to_sigma_p_Sn + [rewrite > sym_plus.rewrite < plus_n_SO. + apply eq_f. + rewrite > (H n1 p H1 H2 H3) in ⊢ (? ? % ?). + apply eq_sigma_p1 + [intros. + apply (bool_elim ? (divides_b (p\sup(S x)) (p\sup n*n1)));intro + [apply sym_eq. + apply divides_to_divides_b_true + [apply lt_O_exp. + apply prime_to_lt_O. + assumption + |apply (witness ? ? ((exp p (n - x))*n1)). + rewrite < assoc_times. + rewrite < exp_plus_times. + apply eq_f2 + [apply eq_f.simplify. + apply eq_f. + rewrite > sym_plus. + apply plus_minus_m_m. + apply lt_to_le.assumption + |reflexivity + ] + ] + |apply sym_eq. + apply False_ind. + apply (divides_b_false_to_not_divides ? ? H5). + apply (witness ? ? ((exp p (n - S x))*n1)). + rewrite < assoc_times. + rewrite < exp_plus_times. + apply eq_f2 + [apply eq_f. + rewrite > sym_plus. + apply plus_minus_m_m. + assumption + |reflexivity + ] + ] + |intros.reflexivity + ] + |apply divides_to_divides_b_true + [apply lt_O_exp. + apply prime_to_lt_O.assumption + |apply (witness ? ? n1).reflexivity + ] + ] + ] +qed. + +theorem sigma_p_divides_b1: +\forall m,n,p,k. O < n \to prime p \to \lnot divides p n \to m \le k \to +m = sigma_p k (λi:nat.divides_b (p\sup (S i)) ((exp p m)*n)) (λx:nat.S O). +intros. +lapply (prime_to_lt_SO ? H1) as H4. +lapply (prime_to_lt_O ? H1) as H5. +rewrite > (false_to_eq_sigma_p m k) + [apply sigma_p_divides_b;assumption + |assumption + |intros. + apply not_divides_to_divides_b_false + [apply lt_O_exp.assumption + |intro.apply (le_to_not_lt ? ? H6). + unfold lt. + rewrite < (ord_exp p) + [rewrite > (plus_n_O m). + rewrite < (not_divides_to_ord_O ? ? H1 H2). + rewrite < (ord_exp p ? H4) in ⊢ (? ? (? % ?)). + rewrite < ord_times + [apply divides_to_le_ord + [apply lt_O_exp.assumption + |rewrite > (times_n_O O). + apply lt_times + [apply lt_O_exp.assumption + |assumption + ] + |assumption + |assumption + ] + |apply lt_O_exp.assumption + |assumption + |assumption + ] + |assumption + ] + ] + ] +qed. + +theorem eq_ord_sigma_p: +\forall n,m,x. O < n \to prime x \to +exp x m \le n \to n < exp x (S m) \to +ord n x=sigma_p m (λi:nat.divides_b (x\sup (S i)) n) (λx:nat.S O). +intros. +lapply (prime_to_lt_SO ? H1). +rewrite > (exp_ord x n) in ⊢ (? ? ? (? ? (λi:?.? ? %) ?)) + [apply sigma_p_divides_b1 + [apply lt_O_ord_rem;assumption + |assumption + |apply not_divides_ord_rem;assumption + |apply lt_S_to_le. + apply (le_to_lt_to_lt ? (log x n)) + [apply le_ord_log;assumption + |apply (lt_exp_to_lt x) + [assumption + |apply (le_to_lt_to_lt ? n ? ? H3). + apply le_exp_log. + assumption + ] + ] + ] + |assumption + |assumption + ] +qed. + +theorem pi_p_primeb1: \forall n. O < n \to +n = pi_p (S n) primeb + (\lambda p.(pi_p (log p n) + (\lambda i.divides_b (exp p (S i)) n) (\lambda i.p))). +intros. +rewrite > (pi_p_primeb n H) in ⊢ (? ? % ?). +apply eq_pi_p1 + [intros.reflexivity + |intros. + rewrite > exp_sigma_p. + apply eq_f. + apply eq_ord_sigma_p + [assumption + |apply primeb_true_to_prime. + assumption + |apply le_exp_log.assumption + |apply lt_exp_log. + apply prime_to_lt_SO. + apply primeb_true_to_prime. + assumption + ] + ] +qed. + +theorem eq_fact_pi_p:\forall n. fact n = +pi_p (S n) (\lambda i.leb (S O) i) (\lambda i.i). +intro.elim n + [reflexivity + |change with ((S n1)*n1! = pi_p (S (S n1)) (λi:nat.leb (S O) i) (λi:nat.i)). + rewrite > true_to_pi_p_Sn + [apply eq_f.assumption + |reflexivity + ] + ] +qed. + +theorem eq_sigma_p_div: \forall n,q.O < q \to +sigma_p (S n) (λm:nat.leb (S O) m∧divides_b q m) (λx:nat.S O) +=n/q. +intros. +apply (div_mod_spec_to_eq n q ? (n \mod q) ? (n \mod q)) + [apply div_mod_spec_intro + [apply lt_mod_m_m.assumption + |elim n + [simplify.elim q;reflexivity + |elim (or_div_mod1 n1 q) + [elim H2.clear H2. + rewrite > divides_to_mod_O + [rewrite < plus_n_O. + rewrite > true_to_sigma_p_Sn + [rewrite > H4 in ⊢ (? ? % ?). + apply eq_f2 + [rewrite < sym_plus. + rewrite < plus_n_SO. + apply eq_f. + apply (div_mod_spec_to_eq n1 q (div n1 q) (mod n1 q) ? (mod n1 q)) + [apply div_mod_spec_div_mod. + assumption + |apply div_mod_spec_intro + [apply lt_mod_m_m.assumption + |assumption + ] + ] + |reflexivity + ] + |apply true_to_true_to_andb_true + [reflexivity + |apply divides_to_divides_b_true;assumption + ] + ] + |assumption + |assumption + ] + |elim H2.clear H2. + rewrite > false_to_sigma_p_Sn + [rewrite > mod_S + [rewrite < plus_n_Sm. + apply eq_f. + assumption + |assumption + |elim (le_to_or_lt_eq (S (mod n1 q)) q) + [assumption + |apply False_ind. + apply H3. + apply (witness ? ? (S(div n1 q))). + rewrite < times_n_Sm. + rewrite < sym_plus. + rewrite < H2 in ⊢ (? ? ? (? ? %)). + rewrite > sym_times. + assumption + |apply lt_mod_m_m. + assumption + ] + ] + |rewrite > not_divides_to_divides_b_false + [rewrite < andb_sym in ⊢ (? ? % ?).reflexivity + |assumption + |assumption + ] + ] + |assumption + ] + ] + ] + |apply div_mod_spec_div_mod. + assumption + ] +qed. + +theorem fact_pi_p: \forall n. fact n = +pi_p (S n) primeb + (\lambda p.(pi_p (log p n) + (\lambda i.true) (\lambda i.(exp p (n /(exp p (S i))))))). +intros. +rewrite > eq_fact_pi_p. +apply (trans_eq ? ? + (pi_p (S n) (λi:nat.leb (S O) i) + (λn.pi_p (S n) primeb + (\lambda p.(pi_p (log p n) + (\lambda i.divides_b (exp p (S i)) n) (\lambda i.p)))))) + [apply eq_pi_p1;intros + [reflexivity + |apply pi_p_primeb1. + apply leb_true_to_le.assumption + ] + |apply (trans_eq ? ? + (pi_p (S n) (λi:nat.leb (S O) i) + (λn:nat + .pi_p (S n) (\lambda p.primeb p\land leb p n) + (λp:nat.pi_p (log p n) (λi:nat.divides_b ((p)\sup(S i)) n) (λi:nat.p))))) + [apply eq_pi_p1 + [intros.reflexivity + |intros.apply eq_pi_p1 + [intros.elim (primeb x1) + [simplify.apply sym_eq. + apply le_to_leb_true. + apply le_S_S_to_le. + assumption + |reflexivity + ] + |intros.reflexivity + ] + ] + |apply (trans_eq ? ? + (pi_p (S n) (λi:nat.leb (S O) i) + (λm:nat + .pi_p (S n) (λp:nat.primeb p∧leb p m) + (λp:nat.pi_p (log p m) (λi:nat.divides_b ((p)\sup(S i)) m) (λi:nat.p))))) + [apply eq_pi_p1 + [intros.reflexivity + |intros. + apply sym_eq. + apply false_to_eq_pi_p + [assumption + |intros.rewrite > lt_to_leb_false + [elim primeb;reflexivity|assumption] + ] + ] + |(* make a general theorem *) + apply (trans_eq ? ? + (pi_p (S n) primeb + (λp:nat + .pi_p (S n) (λm.leb p m) + (λm:nat.pi_p (log p m) (λi:nat.divides_b ((p)\sup(S i)) m) (λi:nat.p))) + )) + [apply pi_p_pi_p1. + intros. + apply (bool_elim ? (primeb y \land leb y x));intros + [rewrite > (le_to_leb_true (S O) x) + [reflexivity + |apply (trans_le ? y) + [apply prime_to_lt_O. + apply primeb_true_to_prime. + apply (andb_true_true ? ? H2) + |apply leb_true_to_le. + apply (andb_true_true_r ? ? H2) + ] + ] + |elim (leb (S O) x);reflexivity + ] + |apply eq_pi_p1 + [intros.reflexivity + |intros. + apply (trans_eq ? ? + (pi_p (S n) (λm:nat.leb x m) + (λm:nat.pi_p (log x n) (λi:nat.divides_b (x\sup(S i)) m) (λi:nat.x)))) + [apply eq_pi_p1 + [intros.reflexivity + |intros. + apply sym_eq. + apply false_to_eq_pi_p + [apply le_log + [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 + ] + |intros. + apply not_divides_to_divides_b_false + [apply lt_O_exp. + apply prime_to_lt_O. + apply primeb_true_to_prime. + assumption + |intro. + apply (lt_to_not_le x1 (exp x (S i))) + [apply (lt_to_le_to_lt ? (exp x (S(log x x1)))) + [apply lt_exp_log. + apply prime_to_lt_SO. + apply primeb_true_to_prime. + assumption + |apply le_exp + [apply prime_to_lt_O. + apply primeb_true_to_prime. + assumption + |apply le_S_S. + assumption + ] + ] + |apply divides_to_le + [apply (lt_to_le_to_lt ? x) + [apply prime_to_lt_O. + apply primeb_true_to_prime. + assumption + |apply leb_true_to_le. + assumption + ] + |assumption + ] + ] + ] + ] + ] + |apply + (trans_eq ? ? + (pi_p (log x n) (λi:nat.true) + (λi:nat.pi_p (S n) (λm:nat.leb x m \land divides_b (x\sup(S i)) m) (λm:nat.x)))) + [apply (pi_p_pi_p1 (\lambda m,i.x)). + intros. + reflexivity + |apply eq_pi_p1 + [intros.reflexivity + |intros. + rewrite > exp_sigma_p. + apply eq_f. + apply (trans_eq ? ? + (sigma_p (S n) (λm:nat.leb (S O) m∧divides_b (x\sup(S x1)) m) (λx:nat.S O))) + [apply eq_sigma_p1 + [intros. + apply (bool_elim ? (divides_b (x\sup(S x1)) x2));intro + [apply (bool_elim ? (leb x x2));intro + [rewrite > le_to_leb_true + [reflexivity + |apply (trans_le ? x) + [apply prime_to_lt_O. + apply primeb_true_to_prime. + assumption + |apply leb_true_to_le. + assumption + ] + ] + |rewrite > lt_to_leb_false + [reflexivity + |apply not_le_to_lt.intro. + apply (leb_false_to_not_le ? ? H6). + apply (trans_le ? (exp x (S x1))) + [rewrite > times_n_SO in ⊢ (? % ?). + change with (exp x (S O) \le exp x (S x1)). + apply le_exp + [apply prime_to_lt_O. + apply primeb_true_to_prime. + assumption + |apply le_S_S.apply le_O_n. + ] + |apply divides_to_le + [assumption + |apply divides_b_true_to_divides. + assumption + ] + ] + ] + ] + |rewrite < andb_sym. + rewrite < andb_sym in ⊢ (? ? ? %). + reflexivity + ] + |intros.reflexivity + ] + |apply eq_sigma_p_div. + apply lt_O_exp. + apply prime_to_lt_O. + apply primeb_true_to_prime. + assumption + ] + ] + ] + ] + ] + ] + ] + ] + ] +qed. + +(* odd n is just mod n (S(S O)) +let rec odd n \def + match n with + [ O \Rightarrow O + | S m \Rightarrow (S O) - odd m + ]. + +theorem le_odd_SO: \forall n. odd n \le S O. +intro.elim n + [apply le_O_n + |simplify.cases (odd n1) + [simplify.apply le_n. + |apply le_O_n + ] + ] +qed. + +theorem SSO_odd: \forall n. n = (n/(S(S O)))*(S(S O)) + odd n. +intro.elim n + [apply (lt_O_n_elim ? H). + intro.simplify.reflexivity + | +*) + +theorem fact_pi_p2: \forall n. fact ((S(S O))*n) = +pi_p (S ((S(S O))*n)) primeb + (\lambda p.(pi_p (log p ((S(S O))*n)) + (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))*(exp p (mod ((S(S O))*n /(exp p (S i))) (S(S O)))))))). +intros.rewrite > fact_pi_p. +apply eq_pi_p1 + [intros.reflexivity + |intros.apply eq_pi_p + [intros.reflexivity + |intros. + rewrite < exp_plus_times. + apply eq_f. + rewrite > sym_times in ⊢ (? ? ? (? % ?)). + apply SSO_mod. + apply lt_O_exp. + apply prime_to_lt_O. + apply primeb_true_to_prime. + assumption + ] + ] +qed. + +theorem fact_pi_p3: \forall n. fact ((S(S O))*n) = +pi_p (S ((S(S O))*n)) primeb + (\lambda p.(pi_p (log p ((S(S O))*n)) + (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))* +pi_p (S ((S(S O))*n)) primeb + (\lambda p.(pi_p (log p ((S(S O))*n)) + (\lambda i.true) (\lambda i.(exp p (mod ((S(S O))*n /(exp p (S i))) (S(S O))))))). +intros. +rewrite < times_pi_p. +rewrite > fact_pi_p2. +apply eq_pi_p;intros + [reflexivity + |apply times_pi_p + ] +qed. + +theorem pi_p_primeb4: \forall n. S O < n \to +pi_p (S ((S(S O))*n)) primeb + (\lambda p.(pi_p (log p ((S(S O))*n)) + (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))) += +pi_p (S n) primeb + (\lambda p.(pi_p (log p (S(S O)*n)) + (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))). +intros. +apply or_false_eq_SO_to_eq_pi_p + [apply le_S_S. + apply le_times_n. + apply lt_O_S + |intros. + right. + rewrite > log_i_SSOn + [change with (i\sup((S(S O))*(n/i\sup(S O)))*(S O) = S O). + rewrite < times_n_SO. + rewrite > eq_div_O + [reflexivity + |simplify.rewrite < times_n_SO.assumption + ] + |assumption + |assumption + |apply le_S_S_to_le.assumption + ] + ] +qed. + +theorem pi_p_primeb5: \forall n. S O < n \to +pi_p (S ((S(S O))*n)) primeb + (\lambda p.(pi_p (log p ((S(S O))*n)) + (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))) += +pi_p (S n) primeb + (\lambda p.(pi_p (log p n) + (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))). +intros. +rewrite > (pi_p_primeb4 ? H). +apply eq_pi_p1;intros + [reflexivity + |apply or_false_eq_SO_to_eq_pi_p + [apply le_log + [apply prime_to_lt_SO. + apply primeb_true_to_prime. + assumption + |apply lt_to_le.assumption + |apply le_times_n. + apply lt_O_S + ] + |intros.right. + rewrite > eq_div_O + [simplify.reflexivity + |apply (lt_to_le_to_lt ? (exp x (S(log x n)))) + [apply lt_exp_log. + apply prime_to_lt_SO. + apply primeb_true_to_prime. + assumption + |apply le_exp + [apply prime_to_lt_O. + apply primeb_true_to_prime. + assumption + |apply le_S_S. + assumption + ] + ] + ] + ] + ] +qed. + +theorem exp_fact_SSO: \forall n. +exp (fact n) (S(S O)) += +pi_p (S n) primeb + (\lambda p.(pi_p (log p n) + (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))). +intros. +rewrite > fact_pi_p. +rewrite < exp_pi_p. +apply eq_pi_p;intros + [reflexivity + |apply sym_eq. + apply exp_times_pi_p + ] +qed. + +definition B \def +\lambda n. +pi_p (S n) primeb + (\lambda p.(pi_p (log p n) + (\lambda i.true) (\lambda i.(exp p (mod (n /(exp p (S i))) (S(S O))))))). + +theorem eq_fact_B:\forall n.S O < n \to +fact ((S(S O))*n) = exp (fact n) (S(S O)) * B((S(S O))*n). +intros. unfold B. +rewrite > fact_pi_p3. +apply eq_f2 + [apply sym_eq. + rewrite > pi_p_primeb5 + [apply exp_fact_SSO + |assumption + ] + |reflexivity + ] +qed. + +theorem le_B_A: \forall n. B n \le A n. +intro.unfold B. +rewrite > eq_A_A'. +unfold A'. +apply le_pi_p.intros. +apply le_pi_p.intros. +rewrite > exp_n_SO in ⊢ (? ? %). +apply le_exp + [apply prime_to_lt_O. + apply primeb_true_to_prime. + assumption + |apply le_S_S_to_le. + apply lt_mod_m_m. + apply lt_O_S + ] +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). +intros. +rewrite > eq_fact_B + [apply le_times_r. + apply le_B_A + |assumption + ] +qed. + +theorem le_B_exp: \forall n.S O < n \to +B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n). +intros. +apply (le_times_to_le (exp (fact n) (S(S O)))) + [apply lt_O_exp. + apply lt_O_fact + |rewrite < eq_fact_B + [rewrite < sym_times in ⊢ (? ? %). + rewrite > exp_SSO. + rewrite < assoc_times. + apply fact1 + |assumption + ] + ] +qed. + +theorem le_A_SSO_A: \forall n. +A((S(S O))*n) \le + pi_p (S ((S(S O))*n)) primeb (λp:nat.p)*A n. +unfold A.intros. +cut (pi_p (S n) primeb (λp:nat.(exp p (log p n))) = pi_p (S ((S(S O))*n)) primeb (λp:nat.(p)\sup(log p n))) + [rewrite > Hcut. + rewrite < times_pi_p. + apply le_pi_p.intros. + lapply (prime_to_lt_SO ? (primeb_true_to_prime ? H1)) as H2. + change with (i\sup(log i ((S(S O))*n))≤i\sup(S(log i n))). + apply le_exp + [apply lt_to_le.assumption + |apply (trans_le ? (log i (i*n))) + [apply le_log + [assumption + |apply not_le_to_lt.intro. + apply (lt_to_not_le ? ? H). + apply (trans_le ? (S O)) + [apply le_S_S.assumption + |apply lt_to_le.assumption + ] + |apply le_times_l. + assumption + ] + |rewrite > exp_n_SO in ⊢ (? (? ? (? % ?)) ?). + rewrite > log_exp + [apply le_n + |assumption + |apply not_le_to_lt.intro. + apply (lt_to_not_le ? ? H). + apply (le_n_O_elim ? H3). + apply lt_to_le. + assumption + ] + ] + ] + |apply sym_eq. + apply or_false_eq_SO_to_eq_pi_p + [apply le_S_S. + apply le_times_n. + apply lt_O_S + |intros.right. + change with (exp i (log i n) = (exp i O)). + apply eq_f. + apply antisymmetric_le + [cut (O < n) + [apply le_S_S_to_le. + apply (lt_exp_to_lt i) + [apply (le_to_lt_to_lt ? n);assumption + |apply (le_to_lt_to_lt ? n) + [apply le_exp_log. + assumption + |rewrite < exp_n_SO. + assumption + ] + ] + |apply not_le_to_lt.intro. + apply (lt_to_not_le ? ? H1). + generalize in match H. + apply (le_n_O_elim ? H2). + intro.assumption + ] + |apply le_O_n + ] + ] + ] +qed. + +(* so far so good + +theorem le_A_BA: \forall n. +A((S(S O))*n) \le B((S(S O))*n)*A n. +(* + [simplify.reflexivity + |rewrite > times_SSO. + rewrite > times_SSO. + unfold A. +apply (trans_le ? ((pi_p (S ((S(S O))*n)) primeb (λp:nat.p))*A n)) + [apply le_A_SSO_A + |apply le_times_l. + unfold B. + apply le_pi_p.intros. +*) +intro.unfold A.unfold B. +cut (pi_p (S n) primeb (λp:nat.(exp p (log p n))) = pi_p (S ((S(S O))*n)) primeb (λp:nat.(p)\sup(log p n))) + [rewrite > Hcut. + rewrite < times_pi_p. + apply le_pi_p.intros. + apply le_trans i. + + + change with (i\sup(log i ((S(S O))*n))≤i\sup(S(log i n))). + apply le_exp + [apply prime_to_lt_O. + apply primeb_true_to_prime. + assumption + |apply (trans_le ? (log i (i*n))) + [apply le_log + [apply prime_to_lt_SO. + apply primeb_true_to_prime. + assumption + |apply not_le_to_lt.intro. + apply (lt_to_not_le ? ? H). + apply (trans_le ? (S O)) + [apply le_S_S.assumption + |apply prime_to_lt_O. + apply primeb_true_to_prime. + assumption + ] + |apply le_times_l. + apply prime_to_lt_SO. + apply primeb_true_to_prime. + assumption + ] + |rewrite > exp_n_SO in ⊢ (? (? ? (? % ?)) ?). + rewrite > log_exp + [apply le_n + |apply prime_to_lt_SO. + apply primeb_true_to_prime. + assumption + |apply not_le_to_lt.intro. + apply (lt_to_not_le ? ? H). + apply (le_n_O_elim ? H2). + apply prime_to_lt_O. + apply primeb_true_to_prime. + assumption + ] + ] + ] + |apply sym_eq. + apply or_false_eq_SO_to_eq_pi_p + [apply le_S_S. + apply le_times_n. + apply lt_O_S + |intros.right. + change with (exp i (log i n) = (exp i O)). + apply eq_f. + apply antisymmetric_le + [cut (O < n) + [apply le_S_S_to_le. + apply (lt_exp_to_lt i) + [apply (le_to_lt_to_lt ? n);assumption + |apply (le_to_lt_to_lt ? n) + [apply le_exp_log. + assumption + |rewrite < exp_n_SO. + assumption + ] + ] + |apply not_le_to_lt.intro. + apply (lt_to_not_le ? ? H1). + generalize in match H. + apply (le_n_O_elim ? H2). + intro.assumption + ] + |apply le_O_n + ] + ] + ] +qed. + + +unfold A.unfold B. +rewrite > eq_A_A'.rewrite > eq_A_A'. +unfold A'.unfold B. + +(* 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 + diff --git a/matita/library/nat/compare.ma b/matita/library/nat/compare.ma index 78dc50318..b002d78cc 100644 --- a/matita/library/nat/compare.ma +++ b/matita/library/nat/compare.ma @@ -126,6 +126,23 @@ apply nat_elim2; intros; simplify ] qed. +theorem leb_true_to_le:\forall n,m. +leb n m = true \to (n \le m). +intros 2. +apply leb_elim + [intros.assumption + |intros.destruct H1. + ] +qed. + +theorem leb_false_to_not_le:\forall n,m. +leb n m = false \to \lnot (n \le m). +intros 2. +apply leb_elim + [intros.destruct H1 + |intros.assumption + ] +qed. (* theorem decidable_le: \forall n,m. n \leq m \lor n \nleq m. intros. diff --git a/matita/library/nat/div_and_mod.ma b/matita/library/nat/div_and_mod.ma index f7f2883d5..0323b18fb 100644 --- a/matita/library/nat/div_and_mod.ma +++ b/matita/library/nat/div_and_mod.ma @@ -325,6 +325,31 @@ rewrite > (div_mod m n) in \vdash (? ? %) ] qed. +theorem or_div_mod: \forall n,q. O < q \to +((S (n \mod q)=q) \land S n = (S (div n q)) * q \lor +((S (n \mod q) sym_plus. + rewrite < H1 in ⊢ (? ? ? (? ? %)). + rewrite < plus_n_Sm. + apply eq_f. + apply div_mod. + assumption + ] + ] +qed. + (* injectivity *) theorem injective_times_r: \forall n:nat.injective nat nat (\lambda m:nat.(S n)*m). change with (\forall n,p,q:nat.(S n)*p = (S n)*q \to p=q). diff --git a/matita/library/nat/euler_theorem.ma b/matita/library/nat/euler_theorem.ma index ab7d8242e..1e5988b35 100644 --- a/matita/library/nat/euler_theorem.ma +++ b/matita/library/nat/euler_theorem.ma @@ -55,7 +55,6 @@ intro.apply (nat_case n) qed. *) - (*this obvious property is useful because simplify, sometimes, "simplifies too much", and doesn't allow to obtain this simple result. *) @@ -136,7 +135,6 @@ elim (m) ] qed. - lemma totient_card: \forall n. totient n = card n (\lambda i.eqb (gcd i n) (S O)). intros. diff --git a/matita/library/nat/exp.ma b/matita/library/nat/exp.ma index 193478c0f..49efe8525 100644 --- a/matita/library/nat/exp.ma +++ b/matita/library/nat/exp.ma @@ -40,6 +40,12 @@ theorem exp_n_SO : \forall n:nat. n = n \sup (S O). intro.simplify.rewrite < times_n_SO.reflexivity. qed. +theorem exp_SSO: \forall n. exp n (S(S O)) = n*n. +intro.simplify. +rewrite < times_n_SO. +reflexivity. +qed. + theorem exp_exp_times : \forall n,p,q:nat. (n \sup p) \sup q = n \sup (p * q). intros. @@ -164,7 +170,22 @@ apply nat_elim2;intros ] qed. - +theorem lt_exp_to_lt: +\forall a,n,m. S O < a \to exp a n < exp a m \to n < m. +intros. +elim (le_to_or_lt_eq n m) + [assumption + |apply False_ind. + apply (lt_to_not_eq ? ? H1). + rewrite < H2. + reflexivity + |apply (le_exp_to_le a) + [assumption + |apply lt_to_le. + assumption + ] + ] +qed. diff --git a/matita/library/nat/factorial2.ma b/matita/library/nat/factorial2.ma new file mode 100644 index 000000000..4f3631cdb --- /dev/null +++ b/matita/library/nat/factorial2.ma @@ -0,0 +1,177 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/nat/factorial2". + +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. + +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 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 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 diff --git a/matita/library/nat/factorization.ma b/matita/library/nat/factorization.ma index 14696ca28..8c50d1d7d 100644 --- a/matita/library/nat/factorization.ma +++ b/matita/library/nat/factorization.ma @@ -15,14 +15,32 @@ set "baseuri" "cic:/matita/nat/factorization". include "nat/ord.ma". -include "nat/gcd.ma". -include "nat/nth_prime.ma". (* the following factorization algorithm looks for the largest prime factor. *) definition max_prime_factor \def \lambda n:nat. (max n (\lambda p:nat.eqb (n \mod (nth_prime p)) O)). +theorem lt_SO_max_prime: \forall m. S O < m \to +S O < max m (λi:nat.primeb i∧divides_b i m). +intros. +apply (lt_to_le_to_lt ? (smallest_factor m)) + [apply lt_SO_smallest_factor.assumption + |apply f_m_to_le_max + [apply le_smallest_factor_n + |apply true_to_true_to_andb_true + [apply prime_to_primeb_true. + apply prime_smallest_factor_n. + assumption + |apply divides_to_divides_b_true + [apply lt_O_smallest_factor.apply lt_to_le.assumption + |apply divides_smallest_factor_n. + apply lt_to_le.assumption + ] + ] + ] + ] +qed. (* max_prime_factor is indeed a factor *) theorem divides_max_prime_factor_n: \forall n:nat. (S O) < n @@ -40,7 +58,6 @@ cut (\exists i. nth_prime i = smallest_factor n); | rewrite > H1; apply le_smallest_factor_n; ] | rewrite > H1; - (*CSC: simplify here does something nasty! *) change with (divides_b (smallest_factor n) n = true); apply divides_to_divides_b_true; [ apply (trans_lt ? (S O)); @@ -356,7 +373,7 @@ theorem defactorize_factorize: \forall n:nat.defactorize (factorize n) = n. intro. apply (nat_case n).reflexivity. intro.apply (nat_case m).reflexivity. -intro.(*CSC: simplify here does something really nasty *) +intro. change with (let p \def (max (S(S m1)) (\lambda p:nat.eqb ((S(S m1)) \mod (nth_prime p)) O)) in defactorize (match p_ord (S(S m1)) (nth_prime p) with @@ -377,7 +394,6 @@ simplify. cut ((S(S m1)) = (nth_prime p) \sup q *r). cut (O defactorize_aux_factorize_aux. -(*CSC: simplify here does something really nasty *) change with (r*(nth_prime p) \sup (S (pred q)) = (S(S m1))). cut ((S (pred q)) = q). rewrite > Hcut2. @@ -395,7 +411,6 @@ apply (divides_max_prime_factor_n (S (S m1))). unfold lt.apply le_S_S.apply le_S_S. apply le_O_n. cut ((S(S m1)) = r). rewrite > Hcut3 in \vdash (? (? ? %)). -(*CSC: simplify here does something really nasty *) change with (nth_prime p \divides r \to False). intro. apply (p_ord_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r). @@ -472,30 +487,6 @@ apply (witness ? ? (n2* (nth_prime i) \sup n)). reflexivity. qed. -theorem divides_exp_to_divides: -\forall p,n,m:nat. prime p \to -p \divides n \sup m \to p \divides n. -intros 3.elim m.simplify in H1. -apply (transitive_divides p (S O)).assumption. -apply divides_SO_n. -cut (p \divides n \lor p \divides n \sup n1). -elim Hcut.assumption. -apply H.assumption.assumption. -apply divides_times_to_divides.assumption. -exact H2. -qed. - -theorem divides_exp_to_eq: -\forall p,q,m:nat. prime p \to prime q \to -p \divides q \sup m \to p = q. -intros. -unfold prime in H1. -elim H1.apply H4. -apply (divides_exp_to_divides p q m). -assumption.assumption. -unfold prime in H.elim H.assumption. -qed. - lemma eq_p_max: \forall n,p,r:nat. O < n \to O < r \to r = (S O) \lor (max r (\lambda p:nat.eqb (r \mod (nth_prime p)) O)) < p \to @@ -762,7 +753,7 @@ exact H1. qed. theorem factorize_defactorize: -\forall f,g: nat_fact_all. factorize (defactorize f) = f. +\forall f: nat_fact_all. factorize (defactorize f) = f. intros. apply injective_defactorize. apply defactorize_factorize. diff --git a/matita/library/nat/gcd.ma b/matita/library/nat/gcd.ma index ded9d4843..9bbce8144 100644 --- a/matita/library/nat/gcd.ma +++ b/matita/library/nat/gcd.ma @@ -749,6 +749,7 @@ apply gcd_O_to_eq_O.apply sym_eq.assumption. apply le_to_or_lt_eq.apply le_O_n. qed. +(* primes and divides *) theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to n \divides p*q \to n \divides p \lor n \divides q. intros. @@ -802,6 +803,30 @@ cut (n \divides p \lor n \ndivides p) ] qed. +theorem divides_exp_to_divides: +\forall p,n,m:nat. prime p \to +p \divides n \sup m \to p \divides n. +intros 3.elim m.simplify in H1. +apply (transitive_divides p (S O)).assumption. +apply divides_SO_n. +cut (p \divides n \lor p \divides n \sup n1). +elim Hcut.assumption. +apply H.assumption.assumption. +apply divides_times_to_divides.assumption. +exact H2. +qed. + +theorem divides_exp_to_eq: +\forall p,q,m:nat. prime p \to prime q \to +p \divides q \sup m \to p = q. +intros. +unfold prime in H1. +elim H1.apply H4. +apply (divides_exp_to_divides p q m). +assumption.assumption. +unfold prime in H.elim H.assumption. +qed. + theorem eq_gcd_times_SO: \forall m,n,p:nat. O < n \to O < p \to gcd m n = (S O) \to gcd m p = (S O) \to gcd m (n*p) = (S O). intros. @@ -877,4 +902,5 @@ cut (n \divides p \lor n \ndivides p) |apply (decidable_divides n p). assumption. ] -qed. \ No newline at end of file +qed. + diff --git a/matita/library/nat/generic_iter_p.ma b/matita/library/nat/generic_iter_p.ma index 3a9adc231..249957f1b 100644 --- a/matita/library/nat/generic_iter_p.ma +++ b/matita/library/nat/generic_iter_p.ma @@ -205,6 +205,47 @@ elim H ] qed. +(* a therem slightly more general than the previous one *) +theorem or_false_eq_baseA_to_eq_iter_p_gen: \forall A:Type. \forall n,m:nat.\forall p:nat \to bool. +\forall g: nat \to A. \forall baseA:A. \forall plusA: A \to A \to A. +(\forall a. plusA baseA a = a) \to +n \le m \to (\forall i:nat. n \le i \to i < m \to p i = false \lor g i = baseA) +\to iter_p_gen m p A g baseA plusA = iter_p_gen n p A g baseA plusA. +intros 9. +elim H1 +[reflexivity +|apply (bool_elim ? (p n1));intro + [elim (H4 n1) + [apply False_ind. + apply not_eq_true_false. + rewrite < H5. + rewrite < H6. + reflexivity + |rewrite > true_to_iter_p_gen_Sn + [rewrite > H6. + rewrite > H. + apply H3.intros. + apply H4 + [assumption + |apply le_S.assumption + ] + |assumption + ] + |assumption + |apply le_n + ] + |rewrite > false_to_iter_p_gen_Sn + [apply H3.intros. + apply H4 + [assumption + |apply le_S.assumption + ] + |assumption + ] + ] +] +qed. + theorem iter_p_gen2 : \forall n,m:nat. \forall p1,p2:nat \to bool. @@ -1631,7 +1672,82 @@ apply (trans_eq ? ? ] qed. - +theorem iter_p_gen_iter_p_gen: +\forall A:Type. +\forall baseA: A. +\forall plusA: A \to A \to A. +(symmetric A plusA) \to +(associative A plusA) \to +(\forall a:A.(plusA a baseA) = a)\to +\forall g: nat \to nat \to A. +\forall n,m. +\forall p11,p21:nat \to bool. +\forall p12,p22:nat \to nat \to bool. +(\forall x,y. x < n \to y < m \to + (p11 x \land p12 x y) = (p21 y \land p22 y x)) \to +iter_p_gen n p11 A + (\lambda x:nat.iter_p_gen m (p12 x) A (\lambda y. g x y) baseA plusA) + baseA plusA = +iter_p_gen m p21 A + (\lambda y:nat.iter_p_gen n (p22 y) A (\lambda x. g x y) baseA plusA ) + baseA plusA. +intros. +apply (iter_p_gen_2_eq A baseA plusA H H1 H2 (\lambda x,y. g x y) (\lambda x,y.y) (\lambda x,y.x) (\lambda x,y.y) (\lambda x,y.x) + n m m n p11 p21 p12 p22) + [intros.split + [split + [split + [split + [split + [apply (andb_true_true ? (p12 j i)). + rewrite > H3 + [rewrite > H6.rewrite > H7.reflexivity + |assumption + |assumption + ] + |apply (andb_true_true_r (p11 j)). + rewrite > H3 + [rewrite > H6.rewrite > H7.reflexivity + |assumption + |assumption + ] + ] + |reflexivity + ] + |reflexivity + ] + |assumption + ] + |assumption + ] + |intros.split + [split + [split + [split + [split + [apply (andb_true_true ? (p22 j i)). + rewrite < H3 + [rewrite > H6.rewrite > H7.reflexivity + |assumption + |assumption + ] + |apply (andb_true_true_r (p21 j)). + rewrite < H3 + [rewrite > H6.rewrite > H7.reflexivity + |assumption + |assumption + ] + ] + |reflexivity + ] + |reflexivity + ] + |assumption + ] + |assumption + ] + ] +qed. diff --git a/matita/library/nat/le_arith.ma b/matita/library/nat/le_arith.ma index 6ad389346..f391c85a9 100644 --- a/matita/library/nat/le_arith.ma +++ b/matita/library/nat/le_arith.ma @@ -146,6 +146,18 @@ apply nat_elim2;intros ] qed. +theorem le_S_times_SSO: \forall n,m.O < m \to +n \le m \to S n \le (S(S O))*m. +intros. +simplify. +rewrite > plus_n_O. +simplify.rewrite > plus_n_Sm. +apply le_plus + [assumption + |rewrite < plus_n_O. + assumption + ] +qed. (*0 and times *) theorem O_lt_const_to_le_times_const: \forall a,c:nat. O \lt c \to a \le a*c. diff --git a/matita/library/nat/log.ma b/matita/library/nat/log.ma new file mode 100644 index 000000000..53b124531 --- /dev/null +++ b/matita/library/nat/log.ma @@ -0,0 +1,274 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/nat/log". + +include "datatypes/constructors.ma". +include "nat/minimization.ma". +include "nat/relevant_equations.ma". +include "nat/primes.ma". + +definition log \def \lambda p,n. +max n (\lambda x.leb (exp p x) n). + +theorem le_exp_log: \forall p,n. O < n \to +exp p (log p 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 log_SO: \forall n. S O < n \to log n (S O) = O. +intros. +apply sym_eq.apply le_n_O_to_eq. +apply (le_exp_to_le n) + [assumption + |simplify in ⊢ (? ? %). + apply le_exp_log. + apply le_n + ] +qed. + +theorem lt_log_n_n: \forall p, n. S O < p \to O < n \to log p n < n. +intros. +cut (log p n \le n) + [elim (le_to_or_lt_eq ? ? Hcut) + [assumption + |absurd (exp p n \le n) + [rewrite < H2 in ⊢ (? (? ? %) ?). + apply le_exp_log. + assumption + |apply lt_to_not_le. + apply lt_m_exp_nm. + assumption + ] + ] + |unfold log.apply le_max_n + ] +qed. + +theorem lt_O_log: \forall p,n. O < n \to p \le n \to O < log p n. +intros. +unfold log. +apply not_lt_to_le. +intro. +apply (leb_false_to_not_le ? ? ? H1). +rewrite > (exp_n_SO p). +apply (lt_max_to_false ? ? ? H2). +assumption. +qed. + +theorem le_log_n_n: \forall p,n. S O < p \to log p n \le n. +intros. +cases n + [apply le_n + |apply lt_to_le. + apply lt_log_n_n + [assumption|apply lt_O_S] + ] +qed. + +theorem lt_exp_log: \forall p,n. S O < p \to n < exp p (S (log p n)). +intros.cases n + [simplify.rewrite < times_n_SO.apply lt_to_le.assumption + |apply not_le_to_lt. + apply leb_false_to_not_le. + apply (lt_max_to_false ? (S n1) (S (log p (S n1)))) + [apply le_S_S.apply le_n + |apply lt_log_n_n + [assumption|apply lt_O_S] + ] + ] +qed. + +theorem log_times1: \forall p,n,m. S O < p \to O < n \to O < m \to +log p (n*m) \le S(log p n+log p 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 p (S(log p n)))*(exp p (S(log p m))))) + [apply lt_times;apply lt_exp_log;assumption + |rewrite < exp_plus_times. + apply le_exp + [apply lt_to_le.assumption + |simplify. + rewrite < plus_n_Sm. + assumption + ] + ] + ] +qed. + +theorem log_times: \forall p,n,m.S O < p \to log p (n*m) \le S(log p n+log p m). +intros. +cases n + [apply le_O_n + |cases m + [rewrite < times_n_O. + apply le_O_n + |apply log_times1 + [assumption + |apply lt_O_S + |apply lt_O_S + ] + ] + ] +qed. + +theorem log_exp: \forall p,n,m.S O < p \to O < m \to +log p ((exp p n)*m)=n+log p 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. + assumption + |simplify. + rewrite > assoc_times. + apply (trans_le ? ((S(S O))*(p\sup n1*m))) + [apply le_S_times_SSO + [rewrite > (times_n_O O) in ⊢ (? % ?). + apply lt_times + [apply lt_O_exp. + apply lt_to_le. + assumption + |assumption + ] + |assumption + ] + |apply le_times + [assumption + |apply le_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 p n)*(exp p (S(log p m))))) + [apply lt_times_r1 + [apply lt_O_exp.apply lt_to_le.assumption + |apply lt_exp_log.assumption + ] + |rewrite < exp_plus_times. + apply le_exp + [apply lt_to_le.assumption + |rewrite < plus_n_Sm. + 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. +apply le_S_S_to_le. +apply (lt_exp_to_lt p) + [assumption + |apply (le_to_lt_to_lt ? n) + [apply le_exp_log. + assumption + |apply (le_to_lt_to_lt ? m) + [assumption + |apply lt_exp_log. + assumption + ] + ] + ] +qed. + +theorem log_n_n: \forall n. S O < n \to log n n = S O. +intros. +rewrite > exp_n_SO in ⊢ (? ? (? ? %) ?). +rewrite > times_n_SO in ⊢ (? ? (? ? %) ?). +rewrite > log_exp + [rewrite > log_SO + [reflexivity + |assumption + ] + |assumption + |apply le_n + ] +qed. + +theorem log_i_SSOn: \forall n,i. S O < n \to n < i \to i \le ((S(S O))*n) \to +log i ((S(S O))*n) = S O. +intros. +apply antisymmetric_le + [apply not_lt_to_le.intro. + apply (lt_to_not_le ((S(S O)) * n) (exp i (S(S O)))) + [rewrite > exp_SSO. + apply lt_times + [apply (le_to_lt_to_lt ? n);assumption + |assumption + ] + |apply (trans_le ? (exp i (log i ((S(S O))*n)))) + [apply le_exp + [apply (ltn_to_ltO ? ? H1) + |assumption + ] + |apply le_exp_log. + rewrite > (times_n_O O) in ⊢ (? % ?). + apply lt_times + [apply lt_O_S + |apply lt_to_le.assumption + ] + ] + ] + |apply (trans_le ? (log i i)) + [rewrite < (log_n_n i) in ⊢ (? % ?) + [apply le_log + [apply (trans_lt ? n);assumption + |apply (ltn_to_ltO ? ? H1) + |apply le_n + ] + |apply (trans_lt ? n);assumption + ] + |apply le_log + [apply (trans_lt ? n);assumption + |apply (ltn_to_ltO ? ? H1) + |assumption + ] + ] + ] +qed. diff --git a/matita/library/nat/lt_arith.ma b/matita/library/nat/lt_arith.ma index a568ca408..623f30295 100644 --- a/matita/library/nat/lt_arith.ma +++ b/matita/library/nat/lt_arith.ma @@ -239,6 +239,27 @@ apply (nat_case n) ] qed. +theorem le_times_to_le_div: \forall a,b,c:nat. +O \lt b \to (b*c) \le a \to c \le (a /b). +intros. +apply lt_S_to_le. +apply (lt_times_n_to_lt b) + [assumption + |rewrite > sym_times. + apply (le_to_lt_to_lt ? a) + [assumption + |simplify. + rewrite > sym_plus. + rewrite > (div_mod a b) in ⊢ (? % ?) + [apply lt_plus_r. + apply lt_mod_m_m. + assumption + |assumption + ] + ] + ] +qed. + theorem nat_compare_times_l : \forall n,p,q:nat. nat_compare p q = nat_compare ((S n) * p) ((S n) * q). intros.apply nat_compare_elim.intro. @@ -320,7 +341,81 @@ apply (trans_lt ? (S O)). unfold lt. apply le_n.assumption. qed. +theorem eq_div_div_div_times: \forall n,m,q. O < n \to O < m \to +q/n/m = q/(n*m). +intros. +apply (div_mod_spec_to_eq q (n*m) ? (q\mod n+n*(q/n\mod m)) ? (mod q (n*m))) + [apply div_mod_spec_intro + [apply (lt_to_le_to_lt ? (n*(S (q/n\mod m)))) + [rewrite < times_n_Sm. + apply lt_plus_l. + apply lt_mod_m_m. + assumption + |apply le_times_r. + apply lt_mod_m_m. + assumption + ] + |rewrite > sym_times in ⊢ (? ? ? (? (? ? %) ?)). + rewrite < assoc_times. + rewrite > (eq_times_div_minus_mod ? ? H1). + rewrite > sym_times. + rewrite > distributive_times_minus. + rewrite > sym_times. + rewrite > (eq_times_div_minus_mod ? ? H). + rewrite < sym_plus in ⊢ (? ? ? (? ? %)). + rewrite < assoc_plus. + rewrite < plus_minus_m_m + [rewrite < plus_minus_m_m + [reflexivity + |apply (eq_plus_to_le ? ? ((q/n)*n)). + rewrite < sym_plus. + apply div_mod. + assumption + ] + |apply (trans_le ? (n*(q/n))) + [apply le_times_r. + apply (eq_plus_to_le ? ? ((q/n)/m*m)). + rewrite < sym_plus. + apply div_mod. + assumption + |rewrite > sym_times. + rewrite > eq_times_div_minus_mod + [apply le_n + |assumption + ] + ] + ] + ] + |apply div_mod_spec_div_mod. + rewrite > (times_n_O O). + apply lt_times;assumption + ] +qed. + +theorem eq_div_div_div_div: \forall n,m,q. O < n \to O < m \to +q/n/m = q/m/n. +intros. +apply (trans_eq ? ? (q/(n*m))) + [apply eq_div_div_div_times;assumption + |rewrite > sym_times. + apply sym_eq. + apply eq_div_div_div_times;assumption + ] +qed. +theorem SSO_mod: \forall n,m. O < m \to (S(S O))*n/m = (n/m)*(S(S O)) + mod ((S(S O))*n/m) (S(S O)). +intros. +rewrite < (lt_O_to_div_times n (S(S O))) in ⊢ (? ? ? (? (? (? % ?) ?) ?)) + [rewrite > eq_div_div_div_div + [rewrite > sym_times in ⊢ (? ? ? (? (? (? (? % ?) ?) ?) ?)). + apply div_mod. + apply lt_O_S + |apply lt_O_S + |assumption + ] + |apply lt_O_S + ] +qed. (* Forall a,b : N. 0 < b \to b * (a/b) <= a < b * (a/b +1) *) (* The theorem is shown in two different parts: *) diff --git a/matita/library/nat/minimization.ma b/matita/library/nat/minimization.ma index 8b4b83c2f..22d5030dd 100644 --- a/matita/library/nat/minimization.ma +++ b/matita/library/nat/minimization.ma @@ -72,6 +72,76 @@ intro.simplify.rewrite < H3. rewrite > H2.simplify.apply le_n. qed. +theorem max_f_g: \forall f,g,n. (\forall i. i \le n \to f i = g i) \to +max n f = max n g. +intros 3. +elim n + [simplify. + rewrite > (H O) + [reflexivity + |apply le_n + ] + |simplify. + rewrite > H + [rewrite > H1 + [reflexivity + |apply le_n + ] + |intros. + apply H1. + apply le_S. + assumption + ] + ] +qed. + +theorem le_max_f_max_g: \forall f,g,n. (\forall i. i \le n \to f i = true \to g i =true) \to +max n f \le max n g. +intros 3. +elim n + [simplify. + elim (f O);apply le_O_n + |simplify. + apply (bool_elim ? (f (S n1)));intro + [rewrite > (H1 (S n1) ? H2) + [apply le_n + |apply le_n + ] + |cases (g(S n1)) + [simplify. + apply le_S. + apply le_max_n + |simplify. + apply H. + intros. + apply H1 + [apply le_S.assumption + |assumption + ] + ] + ] + ] +qed. + + +theorem max_O : \forall f:nat \to bool. \forall n:nat. +(\forall i:nat. le i n \to f i = false) \to max n f = O. +intros 2.elim n + [simplify.rewrite > H + [reflexivity + |apply le_O_n + ] + |simplify.rewrite > H1 + [simplify.apply H. + intros. + apply H1. + apply le_S. + assumption + |apply le_n + ] + ] +qed. + theorem f_max_true : \forall f:nat \to bool. \forall n:nat. (\exists i:nat. le i n \land f i = true) \to f (max n f) = true. intros 2. @@ -95,6 +165,73 @@ rewrite < H2.rewrite < H7.rewrite > H6. reflexivity. reflexivity. qed. +theorem exists_forall_le:\forall f,n. +(\exists i. i \le n \land f i = true) \lor +(\forall i. i \le n \to f i = false). +intros. +elim n + [apply (bool_elim ? (f O));intro + [left.apply (ex_intro ? ? O). + split[apply le_n|assumption] + |right.intros. + apply (le_n_O_elim ? H1). + assumption + ] + |elim H + [elim H1.elim H2. + left.apply (ex_intro ? ? a). + split[apply le_S.assumption|assumption] + |apply (bool_elim ? (f (S n1)));intro + [left.apply (ex_intro ? ? (S n1)). + split[apply le_n|assumption] + |right.intros. + elim (le_to_or_lt_eq ? ? H3) + [apply H1. + apply le_S_S_to_le. + apply H4 + |rewrite > H4. + assumption + ] + ] + ] + ] +qed. + +theorem exists_max_forall_false:\forall f,n. +((\exists i. i \le n \land f i = true) \land (f (max n f) = true))\lor +((\forall i. i \le n \to f i = false) \land (max n f) = O). +intros. +elim (exists_forall_le f n) + [left.split + [assumption + |apply f_max_true.assumption + ] + |right.split + [assumption + |apply max_O.assumption + ] + ] +qed. + +theorem false_to_lt_max: \forall f,n,m.O < n \to +f n = false \to max m f \le n \to max m f < n. +intros. +elim (le_to_or_lt_eq ? ? H2) + [assumption + |elim (exists_max_forall_false f m) + [elim H4. + apply False_ind. + apply not_eq_true_false. + rewrite < H6. + rewrite > H3. + assumption + |elim H4. + rewrite > H6. + assumption + ] + ] +qed. + theorem lt_max_to_false : \forall f:nat \to bool. \forall n,m:nat. (max n f) < m \to m \leq n \to f m = false. intros 2. @@ -114,6 +251,18 @@ apply le_S_S_to_le.assumption. intro.rewrite > H7.assumption. 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. + definition max_spec \def \lambda f:nat \to bool.\lambda n,m: nat. m \le n \land (f m)=true \land (\forall i. m < i \to i \le n \to (f i = false)). diff --git a/matita/library/nat/ord.ma b/matita/library/nat/ord.ma index 340e33a86..335550d0d 100644 --- a/matita/library/nat/ord.ma +++ b/matita/library/nat/ord.ma @@ -17,6 +17,7 @@ set "baseuri" "cic:/matita/nat/ord". include "datatypes/constructors.ma". include "nat/exp.ma". include "nat/nth_prime.ma". +include "nat/gcd.ma". (* for some properties of divides *) include "nat/relevant_equations.ma". (* required by autobatch paramod *) let rec p_ord_aux p n m \def @@ -429,7 +430,165 @@ elim (le_to_or_lt_eq O (ord_rem n p)) ] qed. -(* p_ord_inv is the inverse of ord *) +(* properties of ord e ord_rem *) + +theorem ord_times: \forall p,m,n.O (p_ord_times ? ? ? (ord m p) (ord_rem m p) (ord n p) (ord_rem n p)) + [reflexivity + |assumption + |assumption + |assumption + |unfold ord.unfold ord_rem.apply eq_pair_fst_snd + |unfold ord.unfold ord_rem.apply eq_pair_fst_snd + ] +qed. + +theorem ord_exp: \forall p,m.S O < p \to +ord (exp p m) p = m. +intros. +unfold ord. +rewrite > (p_ord_exp1 p (exp p m) m (S O)) + [reflexivity + |apply lt_to_le.assumption + |intro.apply (lt_to_not_le ? ? H). + apply divides_to_le + [apply lt_O_S + |assumption + ] + |apply times_n_SO + ] +qed. + +theorem not_divides_to_ord_O: +\forall p,m. prime p \to \lnot (divides p m) \to +ord m p = O. +intros.unfold ord. +rewrite > (p_ord_exp1 p m O m) + [reflexivity + |apply prime_to_lt_O.assumption + |assumption + |simplify.apply plus_n_O + ] +qed. + +theorem ord_O_to_not_divides: +\forall p,m. O < m \to prime p \to ord m p = O \to +\lnot (divides p m). +intros. +lapply (p_ord_to_exp1 p m (ord m p) (ord_rem m p)) + [elim Hletin. + rewrite > H4. + rewrite > H2. + rewrite > sym_times. + rewrite < times_n_SO. + assumption + |apply prime_to_lt_SO.assumption + |assumption + |unfold ord.unfold ord_rem.apply eq_pair_fst_snd + ] +qed. + +theorem divides_to_not_ord_O: +\forall p,m. O < m \to prime p \to divides p m \to +\lnot(ord m p = O). +intros.intro. +apply (ord_O_to_not_divides ? ? H H1 H3). +assumption. +qed. + +theorem not_ord_O_to_divides: +\forall p,m. O < m \to prime p \to \lnot (ord m p = O) \to +divides p m. +intros. +rewrite > (exp_ord p) in ⊢ (? ? %) + [apply (trans_divides ? (exp p (ord m p))) + [generalize in match H2. + cases (ord m p);intro + [apply False_ind.apply H3.reflexivity + |simplify.autobatch + ] + |autobatch + ] + |apply prime_to_lt_SO. + assumption + |assumption + ] +qed. + +theorem not_divides_ord_rem: \forall m,p.O< m \to S O < p \to +\lnot (divides p (ord_rem m p)). +intros. +elim (p_ord_to_exp1 p m (ord m p) (ord_rem m p)) + [assumption + |assumption + |assumption + |unfold ord.unfold ord_rem.apply eq_pair_fst_snd + ] +qed. + +theorem ord_ord_rem: \forall p,q,m. O < m \to +prime p \to prime q \to +q < p \to ord (ord_rem m p) q = ord m q. +intros. +rewrite > (exp_ord p) in ⊢ (? ? ? (? % ?)) + [rewrite > ord_times + [rewrite > not_divides_to_ord_O in ⊢ (? ? ? (? % ?)) + [reflexivity + |assumption + |intro. + apply (lt_to_not_eq ? ? H3). + apply (divides_exp_to_eq ? ? ? H2 H1 H4) + ] + |apply lt_O_exp. + apply (ltn_to_ltO ? ? H3) + |apply lt_O_ord_rem + [elim H1.assumption + |assumption + + ] + |assumption + ] + |elim H1.assumption + |assumption + ] +qed. + +theorem lt_ord_rem: \forall n,m. prime n \to O < m \to +divides n m \to ord_rem m n < m. +intros. +elim (le_to_or_lt_eq (ord_rem m n) m) + [assumption + |apply False_ind. + apply (ord_O_to_not_divides ? ? H1 H ? H2). + apply (inj_exp_r n) + [apply prime_to_lt_SO.assumption + |apply (inj_times_l1 m) + [assumption + |rewrite > sym_times in ⊢ (? ? ? %). + rewrite < times_n_SO. + rewrite < H3 in ⊢ (? ? (? ? %) ?). + apply sym_eq. + apply exp_ord + [apply prime_to_lt_SO.assumption + |assumption + ] + ] + ] + |apply divides_to_le + [assumption + |apply divides_ord_rem + [apply prime_to_lt_SO.assumption + |assumption + ] + ] + ] +qed. + +(* p_ord_inv is used to encode the pair ord and rem into + a single natural number. *) + definition p_ord_inv \def \lambda p,m,x. match p_ord x p with diff --git a/matita/library/nat/orders.ma b/matita/library/nat/orders.ma index caecbe063..799f8bf7c 100644 --- a/matita/library/nat/orders.ma +++ b/matita/library/nat/orders.ma @@ -325,6 +325,16 @@ intros.apply (le_to_lt_to_lt O n). apply le_O_n.assumption. qed. +theorem lt_SO_n_to_lt_O_pred_n: \forall n:nat. +(S O) \lt n \to O \lt (pred n). +intros. +apply (ltn_to_ltO (pred (S O)) (pred n) ?). + apply (lt_pred (S O) n); + [ apply (lt_O_S O) + | assumption + ] +qed. + theorem lt_O_n_elim: \forall n:nat. lt O n \to \forall P:nat\to Prop. (\forall m:nat.P (S m)) \to P n. intro.elim n.apply False_ind.exact (not_le_Sn_O O H). diff --git a/matita/library/nat/pi_p.ma b/matita/library/nat/pi_p.ma new file mode 100644 index 000000000..e649f5f19 --- /dev/null +++ b/matita/library/nat/pi_p.ma @@ -0,0 +1,395 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/nat/pi_p". + +include "nat/primes.ma". +(* include "nat/ord.ma". *) +include "nat/generic_iter_p.ma". +(* include "nat/count.ma". necessary just to use bool_to_nat and bool_to_nat_andb*) +include "nat/iteration2.ma". + +(* pi_p on nautral numbers is a specialization of iter_p_gen *) +definition pi_p: nat \to (nat \to bool) \to (nat \to nat) \to nat \def +\lambda n, p, g. (iter_p_gen n p nat g (S O) times). + +theorem true_to_pi_p_Sn: +\forall n:nat. \forall p:nat \to bool. \forall g:nat \to nat. +p n = true \to pi_p (S n) p g = (g n)*(pi_p n p g). +intros. +unfold pi_p. +apply true_to_iter_p_gen_Sn. +assumption. +qed. + +theorem false_to_pi_p_Sn: +\forall n:nat. \forall p:nat \to bool. \forall g:nat \to nat. +p n = false \to pi_p (S n) p g = pi_p n p g. +intros. +unfold pi_p. +apply false_to_iter_p_gen_Sn. +assumption. +qed. + +theorem eq_pi_p: \forall p1,p2:nat \to bool. +\forall g1,g2: nat \to nat.\forall n. +(\forall x. x < n \to p1 x = p2 x) \to +(\forall x. x < n \to g1 x = g2 x) \to +pi_p n p1 g1 = pi_p n p2 g2. +intros. +unfold pi_p. +apply eq_iter_p_gen; +assumption. +qed. + +theorem eq_pi_p1: \forall p1,p2:nat \to bool. +\forall g1,g2: nat \to nat.\forall n. +(\forall x. x < n \to p1 x = p2 x) \to +(\forall x. x < n \to p1 x = true \to g1 x = g2 x) \to +pi_p n p1 g1 = pi_p n p2 g2. +intros. +unfold pi_p. +apply eq_iter_p_gen1; +assumption. +qed. + +theorem pi_p_false: +\forall g: nat \to nat.\forall n.pi_p n (\lambda x.false) g = S O. +intros. +unfold pi_p. +apply iter_p_gen_false. +qed. + +theorem pi_p_times: \forall n,k:nat.\forall p:nat \to bool. +\forall g: nat \to nat. +pi_p (k+n) p g += pi_p k (\lambda x.p (x+n)) (\lambda x.g (x+n)) * pi_p n p g. +intros. +unfold pi_p. +apply (iter_p_gen_plusA nat n k p g (S O) times) +[ apply sym_times. +| intros. + apply sym_eq. + apply times_n_SO +| apply associative_times +] +qed. + +theorem false_to_eq_pi_p: \forall n,m:nat.n \le m \to +\forall p:nat \to bool. +\forall g: nat \to nat. (\forall i:nat. n \le i \to i < m \to +p i = false) \to pi_p m p g = pi_p n p g. +intros. +unfold pi_p. +apply (false_to_eq_iter_p_gen); +assumption. +qed. + +theorem or_false_eq_SO_to_eq_pi_p: +\forall n,m:nat.\forall p:nat \to bool. +\forall g: nat \to nat. +n \le m \to (\forall i:nat. n \le i \to i < m \to p i = false \lor g i = S O) +\to pi_p m p g = pi_p n p g. +intros. +unfold pi_p. +apply or_false_eq_baseA_to_eq_iter_p_gen + [intros.simplify.rewrite < plus_n_O.reflexivity + |assumption + |assumption + ] +qed. + +theorem pi_p2 : +\forall n,m:nat. +\forall p1,p2:nat \to bool. +\forall g: nat \to nat \to nat. +pi_p (n*m) + (\lambda x.andb (p1 (div x m)) (p2 (mod x m))) + (\lambda x.g (div x m) (mod x m)) = +pi_p n p1 + (\lambda x.pi_p m p2 (g x)). +intros. +unfold pi_p. +apply (iter_p_gen2 n m p1 p2 nat g (S O) times) +[ apply sym_times +| apply associative_times +| intros. + apply sym_eq. + apply times_n_SO +] +qed. + +theorem pi_p2' : +\forall n,m:nat. +\forall p1:nat \to bool. +\forall p2:nat \to nat \to bool. +\forall g: nat \to nat \to nat. +pi_p (n*m) + (\lambda x.andb (p1 (div x m)) (p2 (div x m) (mod x m))) + (\lambda x.g (div x m) (mod x m)) = +pi_p n p1 + (\lambda x.pi_p m (p2 x) (g x)). +intros. +unfold pi_p. +apply (iter_p_gen2' n m p1 p2 nat g (S O) times) +[ apply sym_times +| apply associative_times +| intros. + apply sym_eq. + apply times_n_SO +] +qed. + +lemma pi_p_gi: \forall g: nat \to nat. +\forall n,i.\forall p:nat \to bool.i < n \to p i = true \to +pi_p n p g = g i * pi_p n (\lambda x. andb (p x) (notb (eqb x i))) g. +intros. +unfold pi_p. +apply (iter_p_gen_gi) +[ apply sym_times +| apply associative_times +| intros. + apply sym_eq. + apply times_n_SO +| assumption +| assumption +] +qed. + +theorem eq_pi_p_gh: +\forall g,h,h1: nat \to nat.\forall n,n1. +\forall p1,p2:nat \to bool. +(\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to +(\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to +(\forall i. i < n \to p1 i = true \to h i < n1) \to +(\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to +(\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to +(\forall j. j < n1 \to p2 j = true \to h1 j < n) \to +pi_p n p1 (\lambda x.g(h x)) = pi_p n1 p2 g. +intros. +unfold pi_p. +apply (eq_iter_p_gen_gh nat (S O) times ? ? ? g h h1 n n1 p1 p2) +[ apply sym_times +| apply associative_times +| intros. + apply sym_eq. + apply times_n_SO +| assumption +| assumption +| assumption +| assumption +| assumption +| assumption +] +qed. + +(* monotonicity *) +theorem le_pi_p: +\forall n:nat. \forall p:nat \to bool. \forall g1,g2:nat \to nat. +(\forall i. i < n \to p i = true \to g1 i \le g2 i ) \to +pi_p n p g1 \le pi_p n p g2. +intros. +generalize in match H. +elim n + [apply le_n. + |apply (bool_elim ? (p n1));intros + [rewrite > true_to_pi_p_Sn + [rewrite > true_to_pi_p_Sn in ⊢ (? ? %) + [apply le_times + [apply H2[apply le_n|assumption] + |apply H1. + intros. + apply H2[apply le_S.assumption|assumption] + ] + |assumption + ] + |assumption + ] + |rewrite > false_to_pi_p_Sn + [rewrite > false_to_pi_p_Sn in ⊢ (? ? %) + [apply H1. + intros. + apply H2[apply le_S.assumption|assumption] + |assumption + ] + |assumption + ] + ] + ] +qed. + +theorem exp_sigma_p: \forall n,a,p. +pi_p n p (\lambda x.a) = (exp a (sigma_p n p (\lambda x.S O))). +intros. +elim n + [reflexivity + |apply (bool_elim ? (p n1)) + [intro. + rewrite > true_to_pi_p_Sn + [rewrite > true_to_sigma_p_Sn + [simplify. + rewrite > H. + reflexivity. + |assumption + ] + |assumption + ] + |intro. + rewrite > false_to_pi_p_Sn + [rewrite > false_to_sigma_p_Sn + [simplify.assumption + |assumption + ] + |assumption + ] + ] + ] +qed. + +theorem times_pi_p: \forall n,p,f,g. +pi_p n p (\lambda x.f x*g x) = pi_p n p f * pi_p n p g. +intros. +elim n + [simplify.reflexivity + |apply (bool_elim ? (p n1)) + [intro. + rewrite > true_to_pi_p_Sn + [rewrite > true_to_pi_p_Sn + [rewrite > true_to_pi_p_Sn + [rewrite > H.autobatch + |assumption + ] + |assumption + ] + |assumption + ] + |intro. + rewrite > false_to_pi_p_Sn + [rewrite > false_to_pi_p_Sn + [rewrite > false_to_pi_p_Sn;assumption + |assumption + ] + |assumption + ] + ] + ] +qed. + +theorem pi_p_SO: \forall n,p. +pi_p n p (\lambda i.S O) = S O. +intros.elim n + [reflexivity + |simplify.elim (p n1) + [simplify.rewrite < plus_n_O.assumption + |simplify.assumption + ] + ] +qed. + +theorem exp_pi_p: \forall n,m,p,f. +pi_p n p (\lambda x.exp (f x) m) = exp (pi_p n p f) m. +intros. +elim m + [simplify.apply pi_p_SO + |simplify. + rewrite > times_pi_p. + rewrite < H. + reflexivity + ] +qed. + +theorem exp_times_pi_p: \forall n,m,k,p,f. +pi_p n p (\lambda x.exp k (m*(f x))) = +exp (pi_p n p (\lambda x.exp k (f x))) m. +intros. +apply (trans_eq ? ? (pi_p n p (\lambda x.(exp (exp k (f x)) m)))) + [apply eq_pi_p;intros + [reflexivity + |apply sym_eq.rewrite > sym_times. + apply exp_exp_times + ] + |apply exp_pi_p + ] +qed. + + +theorem pi_p_knm: +\forall g: nat \to nat. +\forall h2:nat \to nat \to nat. +\forall h11,h12:nat \to nat. +\forall k,n,m. +\forall p1,p21:nat \to bool. +\forall p22:nat \to nat \to bool. +(\forall x. x < k \to p1 x = true \to +p21 (h11 x) = true \land p22 (h11 x) (h12 x) = true +\land h2 (h11 x) (h12 x) = x +\land (h11 x) < n \land (h12 x) < m) \to +(\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to +p1 (h2 i j) = true \land +h11 (h2 i j) = i \land h12 (h2 i j) = j +\land h2 i j < k) \to +pi_p k p1 g = +pi_p n p21 (\lambda x:nat.pi_p m (p22 x) (\lambda y. g (h2 x y))). +intros. +unfold pi_p.unfold pi_p. +apply (iter_p_gen_knm nat (S O) times sym_times assoc_times ? ? ? h11 h12) + [intros.apply sym_eq.apply times_n_SO. + |assumption + |assumption + ] +qed. + +theorem pi_p_pi_p: +\forall g: nat \to nat \to nat. +\forall h11,h12,h21,h22: nat \to nat \to nat. +\forall n1,m1,n2,m2. +\forall p11,p21:nat \to bool. +\forall p12,p22:nat \to nat \to bool. +(\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to +p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true +\land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j +\land h11 i j < n1 \land h12 i j < m1) \to +(\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to +p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true +\land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j +\land (h21 i j) < n2 \land (h22 i j) < m2) \to +pi_p n1 p11 + (\lambda x:nat .pi_p m1 (p12 x) (\lambda y. g x y)) = +pi_p n2 p21 + (\lambda x:nat .pi_p m2 (p22 x) (\lambda y. g (h11 x y) (h12 x y))). +intros. +unfold pi_p.unfold pi_p. +apply (iter_p_gen_2_eq ? ? ? sym_times assoc_times ? ? ? ? h21 h22) + [intros.apply sym_eq.apply times_n_SO. + |assumption + |assumption + ] +qed. + +theorem pi_p_pi_p1: +\forall g: nat \to nat \to nat. +\forall n,m. +\forall p11,p21:nat \to bool. +\forall p12,p22:nat \to nat \to bool. +(\forall x,y. x < n \to y < m \to + (p11 x \land p12 x y) = (p21 y \land p22 y x)) \to +pi_p n p11 (\lambda x:nat.pi_p m (p12 x) (\lambda y. g x y)) = +pi_p m p21 (\lambda y:nat.pi_p n (p22 y) (\lambda x. g x y)). +intros. +unfold pi_p.unfold pi_p. +apply (iter_p_gen_iter_p_gen ? ? ? sym_times assoc_times) + [intros.apply sym_eq.apply times_n_SO. + |assumption + ] +qed. \ No newline at end of file diff --git a/matita/library/nat/primes.ma b/matita/library/nat/primes.ma index 6885a9847..ec7118980 100644 --- a/matita/library/nat/primes.ma +++ b/matita/library/nat/primes.ma @@ -190,8 +190,33 @@ rewrite > H2.rewrite < H3. simplify.exact (not_le_Sn_n O). qed. - -(*divides and div*) +(*a variant of or_div_mod *) +theorem or_div_mod1: \forall n,q. O < q \to +(divides q (S n)) \land S n = (S (div n q)) * q \lor +(\lnot (divides q (S n)) \land S n= (div n q) * q + S (n\mod q)). +intros.elim (or_div_mod n q H);elim H1 + [left.split + [apply (witness ? ? (S (n/q))). + rewrite > sym_times.assumption + |assumption + ] + |right.split + [intro. + apply (not_eq_O_S (n \mod q)). + (* come faccio a fare unfold nelleipotesi ? *) + cut ((S n) \mod q = O) + [rewrite < Hcut. + apply (div_mod_spec_to_eq2 (S n) q (div (S n) q) (mod (S n) q) (div n q) (S (mod n q))) + [apply div_mod_spec_div_mod. + assumption + |apply div_mod_spec_intro;assumption + ] + |apply divides_to_mod_O;assumption + ] + |assumption + ] + ] +qed. theorem divides_to_div: \forall n,m.divides n m \to m/n*n = m. intro. @@ -490,6 +515,11 @@ theorem prime_to_lt_O: \forall p. prime p \to O < p. intros.elim H.apply lt_to_le.assumption. qed. +theorem prime_to_lt_SO: \forall p. prime p \to S O < p. +intros.elim H. +assumption. +qed. + (* smallest factor *) definition smallest_factor : nat \to nat \def \lambda n:nat. -- 2.39.2