From 25e2e100e1ae3d4291246aeee38e3c61d51f47b2 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 14 Sep 2005 07:48:44 +0000 Subject: [PATCH] factorization.ma --- helm/matita/library/nat/factorization.ma | 530 +++++++++++++++++++++++ 1 file changed, 530 insertions(+) create mode 100644 helm/matita/library/nat/factorization.ma diff --git a/helm/matita/library/nat/factorization.ma b/helm/matita/library/nat/factorization.ma new file mode 100644 index 000000000..30174d770 --- /dev/null +++ b/helm/matita/library/nat/factorization.ma @@ -0,0 +1,530 @@ +(**************************************************************************) +(* ___ *) +(* ||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/factorization". + +include "nat/log.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 (mod n (nth_prime p)) O)). + +(* max_prime_factor is indeed a factor *) +theorem divides_max_prime_factor_n: \forall n:nat. (S O) < n \to +divides (nth_prime (max_prime_factor n)) n. +intros.apply divides_b_true_to_divides. +apply lt_O_nth_prime_n. +apply f_max_true (\lambda p:nat.eqb (mod n (nth_prime p)) O) n. +cut ex nat (\lambda i. nth_prime i = smallest_factor n). +elim Hcut. +apply ex_intro nat ? a. +split. +apply trans_le a (nth_prime a). +apply le_n_fn. +exact lt_nth_prime_n_nth_prime_Sn. +rewrite > H1. apply le_smallest_factor_n. +rewrite > H1. +change with divides_b (smallest_factor n) n = true. +apply divides_to_divides_b_true. +apply trans_lt ? (S O).simplify. apply le_n. +apply lt_SO_smallest_factor.assumption. +apply divides_smallest_factor_n. +apply trans_lt ? (S O). simplify. apply le_n. assumption. +apply prime_to_nth_prime. +apply prime_smallest_factor_n.assumption. +qed. + +theorem divides_to_max_prime_factor : \forall n,m. (S O) < n \to O < m \to divides n m \to +max_prime_factor n \le max_prime_factor m. +intros.change with +(max n (\lambda p:nat.eqb (mod n (nth_prime p)) O)) \le +(max m (\lambda p:nat.eqb (mod m (nth_prime p)) O)). +apply f_m_to_le_max. +apply trans_le ? n. +apply le_max_n.apply divides_to_le.assumption.assumption. +change with divides_b (nth_prime (max_prime_factor n)) m = true. +apply divides_to_divides_b_true. +cut prime (nth_prime (max_prime_factor n)). +apply lt_O_nth_prime_n.apply prime_nth_prime. +cut divides (nth_prime (max_prime_factor n)) n. +apply transitive_divides ? n. +apply divides_max_prime_factor_n. +assumption.assumption. +apply divides_b_true_to_divides. +apply lt_O_nth_prime_n. +apply divides_to_divides_b_true. +apply lt_O_nth_prime_n. +apply divides_max_prime_factor_n. +assumption. +qed. + +theorem plog_to_lt_max_prime_factor: \forall n,p,q,r. O < n \to +p = max_prime_factor n \to +(pair nat nat q r) = plog n (nth_prime p) \to +(S O) < r \to max_prime_factor r < p. +intros. +rewrite > H1. +cut max_prime_factor r \lt max_prime_factor n \lor + max_prime_factor r = max_prime_factor n. +elim Hcut.assumption. +absurd (divides (nth_prime (max_prime_factor n)) r). +rewrite < H4. +apply divides_max_prime_factor_n. +assumption. +change with (divides (nth_prime (max_prime_factor n)) r) \to False. +intro. +cut \not (mod r (nth_prime (max_prime_factor n))) = O. +apply Hcut1.apply divides_to_mod_O. +apply lt_O_nth_prime_n.assumption. +apply plog_aux_to_not_mod_O n n ? q r. +apply lt_SO_nth_prime_n.assumption. +apply le_n. +rewrite < H1.assumption. +apply le_to_or_lt_eq (max_prime_factor r) (max_prime_factor n). +apply divides_to_max_prime_factor. +assumption.assumption. +apply witness r n (exp (nth_prime p) q). +rewrite < sym_times. +apply plog_aux_to_exp n n ? q r. +apply lt_O_nth_prime_n.assumption. +qed. + +theorem plog_to_lt_max_prime_factor1: \forall n,p,q,r. O < n \to +max_prime_factor n \le p \to +(pair nat nat q r) = plog n (nth_prime p) \to +(S O) < r \to max_prime_factor r < p. +intros. +cut max_prime_factor n < p \lor max_prime_factor n = p. +elim Hcut.apply le_to_lt_to_lt ? (max_prime_factor n). +apply divides_to_max_prime_factor.assumption.assumption. +apply witness r n (exp (nth_prime p) q). +rewrite > sym_times. +apply plog_aux_to_exp n n. +apply lt_O_nth_prime_n. +assumption.assumption. +apply plog_to_lt_max_prime_factor n ? q. +assumption.apply sym_eq.assumption.assumption.assumption. +apply le_to_or_lt_eq ? p H1. +qed. + +(* datatypes and functions *) + +inductive nat_fact : Set \def + nf_last : nat \to nat_fact + | nf_cons : nat \to nat_fact \to nat_fact. + +inductive nat_fact_all : Set \def + nfa_zero : nat_fact_all + | nfa_one : nat_fact_all + | nfa_proper : nat_fact \to nat_fact_all. + +let rec factorize_aux p n acc \def + match p with + [ O \Rightarrow acc + | (S p1) \Rightarrow + match plog n (nth_prime p1) with + [ (pair q r) \Rightarrow + factorize_aux p1 r (nf_cons q acc)]]. + +definition factorize : nat \to nat_fact_all \def \lambda n:nat. + match n with + [ O \Rightarrow nfa_zero + | (S n1) \Rightarrow + match n1 with + [ O \Rightarrow nfa_one + | (S n2) \Rightarrow + let p \def (max (S(S n2)) (\lambda p:nat.eqb (mod (S(S n2)) (nth_prime p)) O)) in + match plog (S(S n2)) (nth_prime p) with + [ (pair q r) \Rightarrow + nfa_proper (factorize_aux p r (nf_last (pred q)))]]]. + +let rec defactorize_aux f i \def + match f with + [ (nf_last n) \Rightarrow exp (nth_prime i) (S n) + | (nf_cons n g) \Rightarrow + (exp (nth_prime i) n)*(defactorize_aux g (S i))]. + +definition defactorize : nat_fact_all \to nat \def +\lambda f : nat_fact_all. +match f with +[ nfa_zero \Rightarrow O +| nfa_one \Rightarrow (S O) +| (nfa_proper g) \Rightarrow defactorize_aux g O]. + +theorem defactorize_aux_factorize_aux : +\forall p,n:nat.\forall acc:nat_fact.O < n \to +((n=(S O) \land p=O) \lor max_prime_factor n < p) \to +defactorize_aux (factorize_aux p n acc) O = n*(defactorize_aux acc p). +intro.elim p.simplify. +elim H1.elim H2.rewrite > H3. +rewrite > sym_times. apply times_n_SO. +apply False_ind.apply not_le_Sn_O (max_prime_factor n) H2. +simplify. +(* generalizing the goal: I guess there exists a better way *) +cut \forall q,r.(pair nat nat q r) = (plog_aux n1 n1 (nth_prime n)) \to +defactorize_aux match (plog_aux n1 n1 (nth_prime n)) with +[(pair q r) \Rightarrow (factorize_aux n r (nf_cons q acc))] O = +n1*defactorize_aux acc (S n). +apply Hcut (fst ? ? (plog_aux n1 n1 (nth_prime n))) +(snd ? ? (plog_aux n1 n1 (nth_prime n))). +apply sym_eq.apply eq_pair_fst_snd. +intros. +rewrite < H3. +simplify. +cut n1 = r*(exp (nth_prime n) q). +rewrite > H. +simplify.rewrite < assoc_times. +rewrite < Hcut.reflexivity. +rewrite > sym_times. +apply plog_aux_to_exp n1 n1. +apply lt_O_nth_prime_n.assumption. +cut O < r \lor O = r. +elim Hcut1.assumption.absurd n1 = O. +rewrite > Hcut.rewrite < H4.reflexivity. +simplify. intro.apply not_le_Sn_O O. +rewrite < H5 in \vdash (? ? %).assumption. +apply le_to_or_lt_eq.apply le_O_n. +cut (S O) < r \lor \lnot (S O) < r. +elim Hcut1. +right. +apply plog_to_lt_max_prime_factor1 n1 ? q r. +assumption.elim H2. +elim H5. +apply False_ind. +apply not_eq_O_S n.apply sym_eq.assumption. +apply le_S_S_to_le. +exact H5. +assumption.assumption. +cut r=(S O). +apply nat_case n. +left.split.assumption.reflexivity. +intro.right.rewrite > Hcut2. +simplify.apply le_S_S.apply le_O_n. +cut r \lt (S O) \or r=(S O). +elim Hcut2.absurd O=r. +apply le_n_O_to_eq.apply le_S_S_to_le.exact H5. +simplify.intro. +cut O=n1. +apply not_le_Sn_O O ?. +rewrite > Hcut3 in \vdash (? ? %). +assumption.rewrite > Hcut. +rewrite < H6.reflexivity. +assumption. +apply le_to_or_lt_eq r (S O). +apply not_lt_to_le.assumption. +apply decidable_lt (S O) r. +qed. + +theorem defactorize_factorize: \forall n:nat.defactorize (factorize n) = n. +intro. +apply nat_case n.reflexivity. +intro.apply nat_case m.reflexivity. +intro.change with +let p \def (max (S(S m1)) (\lambda p:nat.eqb (mod (S(S m1)) (nth_prime p)) O)) in +defactorize (match plog (S(S m1)) (nth_prime p) with +[ (pair q r) \Rightarrow + nfa_proper (factorize_aux p r (nf_last (pred q)))])=(S(S m1)). +intro. +(* generalizing the goal; find a better way *) +cut \forall q,r.(pair nat nat q r) = (plog (S(S m1)) (nth_prime p)) \to +defactorize (match plog (S(S m1)) (nth_prime p) with +[ (pair q r) \Rightarrow + nfa_proper (factorize_aux p r (nf_last (pred q)))])=(S(S m1)). +apply Hcut (fst ? ? (plog (S(S m1)) (nth_prime p))) +(snd ? ? (plog (S(S m1)) (nth_prime p))). +apply sym_eq.apply eq_pair_fst_snd. +intros. +rewrite < H. +change with +defactorize_aux (factorize_aux p r (nf_last (pred q))) O = (S(S m1)). +cut (S(S m1)) = (exp (nth_prime p) q)*r. +cut O defactorize_aux_factorize_aux. +change with r*(exp (nth_prime p) (S (pred q))) = (S(S m1)). +cut (S (pred q)) = q. +rewrite > Hcut2. +rewrite > sym_times. +apply sym_eq. +apply plog_aux_to_exp (S(S m1)). +apply lt_O_nth_prime_n. +assumption. +(* O < q *) +apply sym_eq. apply S_pred. +cut O < q \lor O = q. +elim Hcut2.assumption. +absurd divides (nth_prime p) (S (S m1)). +apply divides_max_prime_factor_n (S (S m1)). +simplify.apply le_S_S.apply le_S_S. apply le_O_n. +cut (S(S m1)) = r. +rewrite > Hcut3 in \vdash (? (? ? %)). +change with divides (nth_prime p) r \to False. +intro. +apply plog_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r ? ? ? ?. +apply divides_to_mod_O. +apply lt_O_nth_prime_n. +assumption. +apply lt_SO_nth_prime_n. +simplify.apply le_S_S.apply le_O_n. +apply le_n. +assumption.rewrite > times_n_SO in \vdash (? ? ? %). +rewrite < sym_times. +rewrite > exp_n_O (nth_prime p). +rewrite > H1 in \vdash (? ? ? (? (? ? %) ?)). +assumption. +apply le_to_or_lt_eq.apply le_O_n. +(* O < r *) +cut O < r \lor O = r. +elim Hcut1.assumption. +apply False_ind. +apply not_eq_O_S (S m1). +rewrite > Hcut.rewrite < H1.rewrite < times_n_O.reflexivity. +apply le_to_or_lt_eq.apply le_O_n. +(* prova del cut *) +apply plog_aux_to_exp (S(S m1)). +apply lt_O_nth_prime_n. +assumption. +(* fine prova cut *) +assumption. +(* e adesso l'ultimo goal *) +cut (S O) < r \lor \lnot (S O) < r. +elim Hcut2. +right. +apply plog_to_lt_max_prime_factor1 (S(S m1)) ? q r. +simplify.apply le_S_S. apply le_O_n. +apply le_n. +assumption.assumption. +cut r=(S O). +apply nat_case p. +left.split.assumption.reflexivity. +intro.right.rewrite > Hcut3. +simplify.apply le_S_S.apply le_O_n. +cut r \lt (S O) \or r=(S O). +elim Hcut3.absurd O=r. +apply le_n_O_to_eq.apply le_S_S_to_le.exact H2. +simplify.intro. +apply not_le_Sn_O O ?. +rewrite > H3 in \vdash (? ? %).assumption.assumption. +apply le_to_or_lt_eq r (S O). +apply not_lt_to_le.assumption. +apply decidable_lt (S O) r. +qed. + +let rec max_p f \def +match f with +[ (nf_last n) \Rightarrow O +| (nf_cons n g) \Rightarrow S (max_p g)]. + +let rec max_p_exponent f \def +match f with +[ (nf_last n) \Rightarrow n +| (nf_cons n g) \Rightarrow max_p_exponent g]. + +theorem divides_max_p_defactorize: \forall f:nat_fact.\forall i:nat. +divides (nth_prime ((max_p f)+i)) (defactorize_aux f i). +intro. +elim f.simplify.apply witness ? ? (exp (nth_prime i) n). +reflexivity. +change with +divides (nth_prime (S(max_p n1)+i)) +((exp (nth_prime i) n)*(defactorize_aux n1 (S i))). +elim H (S i). +rewrite > H1. +rewrite < sym_times. +rewrite > assoc_times. +rewrite < plus_n_Sm. +apply witness ? ? (n2*(exp (nth_prime i) n)). +reflexivity. +qed. + +theorem divides_exp_to_divides: +\forall p,n,m:nat. prime p \to +divides p (exp n m) \to divides p n. +intros 3.elim m.simplify in H1. +apply transitive_divides p (S O).assumption. +apply divides_SO_n. +cut divides p n \lor divides p (exp n 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 +divides p (exp q m) \to p = q. +intros. +simplify in H1. +elim H1.apply H4. +apply divides_exp_to_divides p q m. +assumption.assumption. +simplify in H.elim H.assumption. +qed. + +theorem not_divides_defactorize_aux: \forall f:nat_fact. \forall i,j:nat. +i < j \to \not divides (nth_prime i) (defactorize_aux f j). +intro.elim f. +change with +divides (nth_prime i) (exp (nth_prime j) (S n)) \to False. +intro.absurd (nth_prime i) = (nth_prime j). +apply divides_exp_to_eq ? ? (S n). +apply prime_nth_prime.apply prime_nth_prime. +assumption. +change with (nth_prime i) = (nth_prime j) \to False. +intro.cut i = j. +apply not_le_Sn_n i.rewrite > Hcut in \vdash (? ? %).assumption. +apply injective_nth_prime ? ? H2. +change with +divides (nth_prime i) ((exp (nth_prime j) n)*(defactorize_aux n1 (S j))) \to False. +intro. +cut divides (nth_prime i) (exp (nth_prime j) n) +\lor divides (nth_prime i) (defactorize_aux n1 (S j)). +elim Hcut. +absurd (nth_prime i) = (nth_prime j). +apply divides_exp_to_eq ? ? n. +apply prime_nth_prime.apply prime_nth_prime. +assumption. +change with (nth_prime i) = (nth_prime j) \to False. +intro. +cut i = j. +apply not_le_Sn_n i.rewrite > Hcut1 in \vdash (? ? %).assumption. +apply injective_nth_prime ? ? H4. +apply H i (S j) ?. +assumption.apply trans_lt ? j.assumption.simplify.apply le_n. +apply divides_times_to_divides. +apply prime_nth_prime.assumption. +qed. + +theorem eq_defactorize_aux_to_eq: \forall f,g:nat_fact.\forall i:nat. +defactorize_aux f i = defactorize_aux g i \to f = g. +intro. +elim f. +generalize in match H. +elim g. +apply eq_f. +apply inj_S. apply inj_exp_r (nth_prime i). +apply lt_SO_nth_prime_n. +assumption. +absurd defactorize_aux (nf_last n) i = +defactorize_aux (nf_cons n1 n2) i. +rewrite > H2.reflexivity. +absurd divides (nth_prime (S(max_p n2)+i)) (defactorize_aux (nf_cons n1 n2) i). +apply divides_max_p_defactorize. +rewrite < H2. +change with +(divides (nth_prime (S(max_p n2)+i)) (exp (nth_prime i) (S n))) \to False. +intro. +absurd nth_prime (S (max_p n2) + i) = nth_prime i. +apply divides_exp_to_eq ? ? (S n). +apply prime_nth_prime.apply prime_nth_prime.assumption. +change with nth_prime (S (max_p n2) + i) = nth_prime i \to False. +intro.apply not_le_Sn_n i. +cut S(max_p n2)+i= i. +rewrite < Hcut in \vdash (? ? %). +simplify.apply le_S_S. +apply le_plus_n. +apply injective_nth_prime ? ? H4. +generalize in match H1. +elim g. +absurd defactorize_aux (nf_last n2) i = +defactorize_aux (nf_cons n n1) i. +apply sym_eq. assumption. +absurd divides (nth_prime (S(max_p n1)+i)) (defactorize_aux (nf_cons n n1) i). +apply divides_max_p_defactorize. +rewrite > H2. +change with +(divides (nth_prime (S(max_p n1)+i)) (exp (nth_prime i) (S n2))) \to False. +intro. +absurd nth_prime (S (max_p n1) + i) = nth_prime i. +apply divides_exp_to_eq ? ? (S n2). +apply prime_nth_prime.apply prime_nth_prime.assumption. +change with nth_prime (S (max_p n1) + i) = nth_prime i \to False. +intro.apply not_le_Sn_n i. +cut S(max_p n1)+i= i. +rewrite < Hcut in \vdash (? ? %). +simplify.apply le_S_S. +apply le_plus_n. +apply injective_nth_prime ? ? H4. +simplify in H3. +generalize in match H3. +apply nat_elim2 (\lambda n,n2. +(exp (nth_prime i) n)*(defactorize_aux n1 (S i)) = +(exp (nth_prime i) n2)*(defactorize_aux n3 (S i)) \to +nf_cons n n1 = nf_cons n2 n3). +intro. +elim n4. apply eq_f. +apply H n3 (S i). +simplify in H4. +rewrite > plus_n_O. +rewrite > plus_n_O (defactorize_aux n3 (S i)).assumption. +apply False_ind. +apply not_divides_defactorize_aux n1 i (S i) ?. +simplify in H5. +rewrite > plus_n_O (defactorize_aux n1 (S i)). +rewrite > H5. +rewrite > assoc_times. +apply witness ? ? ((exp (nth_prime i) n5)*(defactorize_aux n3 (S i))). +reflexivity. +simplify. apply le_n. +intros. +apply False_ind. +apply not_divides_defactorize_aux n3 i (S i) ?. +simplify in H4. +rewrite > plus_n_O (defactorize_aux n3 (S i)). +rewrite < H4. +rewrite > assoc_times. +apply witness ? ? ((exp (nth_prime i) n4)*(defactorize_aux n1 (S i))). +reflexivity. +simplify. apply le_n. +intros. +cut nf_cons n4 n1 = nf_cons m n3. +cut n4=m. +cut n1=n3. +rewrite > Hcut1.rewrite > Hcut2.reflexivity. +change with +match nf_cons n4 n1 with +[ (nf_last m) \Rightarrow n1 +| (nf_cons m g) \Rightarrow g ] = n3. +rewrite > Hcut.simplify.reflexivity. +change with +match nf_cons n4 n1 with +[ (nf_last m) \Rightarrow m +| (nf_cons m g) \Rightarrow m ] = m. +rewrite > Hcut.simplify.reflexivity. +apply H4.simplify in H5. +apply inj_times_r1 (nth_prime i). +apply lt_O_nth_prime_n. +rewrite < assoc_times.rewrite < assoc_times.assumption. +qed. + +theorem injective_defactorize_aux: \forall i:nat. +injective nat_fact nat (\lambda f.defactorize_aux f i). +change with \forall i:nat.\forall f,g:nat_fact. +defactorize_aux f i = defactorize_aux g i \to f = g. +intros. +apply eq_defactorize_aux_to_eq f g i H. +qed. + +(* +theorem injective_defactorize: +injective nat_fact_all nat defactorize. +change with \forall f,g:nat_fact_all. +defactorize f = defactorize g \to f = g. +intro.elim f. +generalize in match H.elim g. +reflexivity.simplify in H1. +*) + -- 2.39.2