From 7deb67bf075a845f84d51ac4757a5c69b779487d Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 23 Sep 2005 09:42:12 +0000 Subject: [PATCH] A few changes to factorization and gcd. --- helm/matita/library/nat/factorization.ma | 248 +++++++++++++++-------- helm/matita/library/nat/gcd.ma | 24 +-- helm/matita/library/nat/nat.ma | 2 +- 3 files changed, 169 insertions(+), 105 deletions(-) diff --git a/helm/matita/library/nat/factorization.ma b/helm/matita/library/nat/factorization.ma index c9669e2ba..f9f0289a0 100644 --- a/helm/matita/library/nat/factorization.ma +++ b/helm/matita/library/nat/factorization.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/nat/factorization". -include "nat/log.ma". +include "nat/ord.ma". include "nat/gcd.ma". include "nat/nth_prime.ma". @@ -72,9 +72,9 @@ apply divides_max_prime_factor_n. assumption. qed. -theorem plog_to_lt_max_prime_factor: \forall n,p,q,r. O < n \to +theorem p_ord_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 +(pair nat nat q r) = p_ord n (nth_prime p) \to (S O) < r \to max_prime_factor r < p. intros. rewrite > H1. @@ -90,7 +90,7 @@ intro. cut mod r (nth_prime (max_prime_factor n)) \neq 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 p_ord_aux_to_not_mod_O n n ? q r. apply lt_SO_nth_prime_n.assumption. apply le_n. rewrite < H1.assumption. @@ -99,13 +99,13 @@ apply divides_to_max_prime_factor. assumption.assumption. apply witness r n ((nth_prime p) \sup q). rewrite < sym_times. -apply plog_aux_to_exp n n ? q r. +apply p_ord_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 +theorem p_ord_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 +(pair nat nat q r) = p_ord 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. @@ -113,10 +113,10 @@ elim Hcut.apply le_to_lt_to_lt ? (max_prime_factor n). apply divides_to_max_prime_factor.assumption.assumption. apply witness r n ((nth_prime p) \sup q). rewrite > sym_times. -apply plog_aux_to_exp n n. +apply p_ord_aux_to_exp n n. apply lt_O_nth_prime_n. assumption.assumption. -apply plog_to_lt_max_prime_factor n ? q. +apply p_ord_to_lt_max_prime_factor n ? q. assumption.apply sym_eq.assumption.assumption.assumption. apply le_to_or_lt_eq ? p H1. qed. @@ -136,7 +136,7 @@ let rec factorize_aux p n acc \def match p with [ O \Rightarrow acc | (S p1) \Rightarrow - match plog n (nth_prime p1) with + match p_ord n (nth_prime p1) with [ (pair q r) \Rightarrow factorize_aux p1 r (nf_cons q acc)]]. @@ -148,7 +148,7 @@ definition factorize : nat \to nat_fact_all \def \lambda n:nat. [ 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 + match p_ord (S(S n2)) (nth_prime p) with [ (pair q r) \Rightarrow nfa_proper (factorize_aux p r (nf_last (pred q)))]]]. @@ -165,6 +165,47 @@ match f with | nfa_one \Rightarrow (S O) | (nfa_proper g) \Rightarrow defactorize_aux g O]. +theorem lt_O_defactorize_aux: \forall f:nat_fact.\forall i:nat. +O < defactorize_aux f i. +intro.elim f.simplify. +rewrite > times_n_SO. +apply le_times. +change with O < nth_prime i. +apply lt_O_nth_prime_n. +change with O < exp (nth_prime i) n. +apply lt_O_exp. +apply lt_O_nth_prime_n. +simplify. +rewrite > times_n_SO. +apply le_times. +change with O < exp (nth_prime i) n. +apply lt_O_exp. +apply lt_O_nth_prime_n. +change with O < defactorize_aux n1 (S i). +apply H. +qed. + +theorem lt_SO_defactorize_aux: \forall f:nat_fact.\forall i:nat. +S O < defactorize_aux f i. +intro.elim f.simplify. +rewrite > times_n_SO. +apply le_times. +change with S O < nth_prime i. +apply lt_SO_nth_prime_n. +change with O < exp (nth_prime i) n. +apply lt_O_exp. +apply lt_O_nth_prime_n. +simplify. +rewrite > times_n_SO. +rewrite > sym_times. +apply le_times. +change with O < exp (nth_prime i) n. +apply lt_O_exp. +apply lt_O_nth_prime_n. +change with S O < defactorize_aux n1 (S i). +apply H. +qed. + 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 @@ -175,12 +216,12 @@ 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 +cut \forall q,r.(pair nat nat q r) = (p_ord_aux n1 n1 (nth_prime n)) \to +defactorize_aux match (p_ord_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 Hcut (fst ? ? (p_ord_aux n1 n1 (nth_prime n))) +(snd ? ? (p_ord_aux n1 n1 (nth_prime n))). apply sym_eq.apply eq_pair_fst_snd. intros. rewrite < H3. @@ -198,7 +239,7 @@ apply le_to_or_lt_eq.apply le_O_n. cut (S O) < r \lor (S O) \nlt r. elim Hcut1. right. -apply plog_to_lt_max_prime_factor1 n1 ? q r. +apply p_ord_to_lt_max_prime_factor1 n1 ? q r. assumption.elim H2. elim H5. apply False_ind. @@ -225,7 +266,7 @@ apply le_to_or_lt_eq r (S O). apply not_lt_to_le.assumption. apply decidable_lt (S O) r. rewrite > sym_times. -apply plog_aux_to_exp n1 n1. +apply p_ord_aux_to_exp n1 n1. apply lt_O_nth_prime_n.assumption. qed. @@ -235,17 +276,17 @@ 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 +defactorize (match p_ord (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 +cut \forall q,r.(pair nat nat q r) = (p_ord (S(S m1)) (nth_prime p)) \to +defactorize (match p_ord (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 Hcut (fst ? ? (p_ord (S(S m1)) (nth_prime p))) +(snd ? ? (p_ord (S(S m1)) (nth_prime p))). apply sym_eq.apply eq_pair_fst_snd. intros. rewrite < H. @@ -259,7 +300,7 @@ cut (S (pred q)) = q. rewrite > Hcut2. rewrite > sym_times. apply sym_eq. -apply plog_aux_to_exp (S(S m1)). +apply p_ord_aux_to_exp (S(S m1)). apply lt_O_nth_prime_n. assumption. (* O < q *) @@ -273,7 +314,7 @@ cut (S(S m1)) = r. rewrite > Hcut3 in \vdash (? (? ? %)). change with nth_prime p \divides r \to False. intro. -apply plog_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r. +apply p_ord_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r. apply lt_SO_nth_prime_n. simplify.apply le_S_S.apply le_O_n.apply le_n. assumption. @@ -288,7 +329,7 @@ apply le_to_or_lt_eq.apply le_O_n.assumption. cut (S O) < r \lor S O \nlt r. elim Hcut2. right. -apply plog_to_lt_max_prime_factor1 (S(S m1)) ? q r. +apply p_ord_to_lt_max_prime_factor1 (S(S m1)) ? q r. simplify.apply le_S_S. apply le_O_n. apply le_n. assumption.assumption. @@ -315,7 +356,7 @@ rewrite > Hcut.rewrite < H1.rewrite < times_n_O.reflexivity. apply le_to_or_lt_eq.apply le_O_n. (* prova del cut *) goal 20. -apply plog_aux_to_exp (S(S m1)). +apply p_ord_aux_to_exp (S(S m1)). apply lt_O_nth_prime_n. assumption. (* fine prova cut *) @@ -407,6 +448,41 @@ apply divides_times_to_divides. apply prime_nth_prime.assumption. qed. +lemma not_eq_nf_last_nf_cons: \forall g:nat_fact.\forall n,m,i:nat. +\lnot (defactorize_aux (nf_last n) i= defactorize_aux (nf_cons m g) i). +intros. +change with +exp (nth_prime i) (S n) = defactorize_aux (nf_cons m g) i \to False. +intro. +cut S(max_p g)+i= i. +apply not_le_Sn_n i. +rewrite < Hcut in \vdash (? ? %). +simplify.apply le_S_S. +apply le_plus_n. +apply injective_nth_prime. +(* uffa, perche' semplifica ? *) +change with nth_prime (S(max_p g)+i)= nth_prime i. +apply divides_exp_to_eq ? ? (S n). +apply prime_nth_prime.apply prime_nth_prime. +rewrite > H. +change with divides (nth_prime ((max_p (nf_cons m g))+i)) +(defactorize_aux (nf_cons m g) i). +apply divides_max_p_defactorize. +qed. + +lemma not_eq_nf_cons_O_nf_cons: \forall f,g:nat_fact.\forall n,i:nat. +\lnot (defactorize_aux (nf_cons O f) i= defactorize_aux (nf_cons (S n) g) i). +intros. +simplify.rewrite < plus_n_O. +intro. +apply not_divides_defactorize_aux f i (S i) ?. +simplify.apply le_n. +rewrite > H. +rewrite > assoc_times. +apply witness ? ? ((exp (nth_prime i) n)*(defactorize_aux g (S i))). +reflexivity. +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. @@ -417,46 +493,13 @@ 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 nth_prime (S(max_p n2)+i) \divides defactorize_aux (nf_cons n1 n2) i. -apply divides_max_p_defactorize. -rewrite < H2. -change with -(nth_prime (S(max_p n2)+i) \divides (nth_prime i) \sup (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. +apply False_ind. +apply not_eq_nf_last_nf_cons n2 n n1 i H2. generalize in match H1. elim g. -absurd defactorize_aux (nf_last n2) i = -defactorize_aux (nf_cons n n1) i. +apply False_ind. +apply not_eq_nf_last_nf_cons n1 n2 n i. apply sym_eq. assumption. -absurd nth_prime (S(max_p n1)+i) \divides defactorize_aux (nf_cons n n1) i. -apply divides_max_p_defactorize. -rewrite > H2. -change with -(nth_prime (S(max_p n1)+i) \divides (nth_prime i) \sup (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. @@ -470,24 +513,11 @@ 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. apply le_n. -simplify in H5. -rewrite > plus_n_O (defactorize_aux n1 (S i)). -rewrite > H5. -rewrite > assoc_times. -apply witness ? ? (((nth_prime i) \sup n5)*(defactorize_aux n3 (S i))). -reflexivity. +apply not_eq_nf_cons_O_nf_cons n1 n3 n5 i.assumption. intros. apply False_ind. -apply not_divides_defactorize_aux n3 i (S i). -simplify. apply le_n. -simplify in H4. -rewrite > plus_n_O (defactorize_aux n3 (S i)). -rewrite < H4. -rewrite > assoc_times. -apply witness ? ? (((nth_prime i) \sup n4)*(defactorize_aux n1 (S i))). -reflexivity. +apply not_eq_nf_cons_O_nf_cons n3 n1 n4 i. +apply sym_eq.assumption. intros. cut nf_cons n4 n1 = nf_cons m n3. cut n4=m. @@ -517,13 +547,67 @@ 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. -*) +(* zero - zero *) +reflexivity. +(* zero - one *) +simplify in H1. +apply False_ind. +apply not_eq_O_S O H1. +(* zero - proper *) +simplify in H1. +apply False_ind. +apply not_le_Sn_n O. +rewrite > H1 in \vdash (? ? %). +change with O < defactorize_aux n O. +apply lt_O_defactorize_aux. +generalize in match H. +elim g. +(* one - zero *) +simplify in H1. +apply False_ind. +apply not_eq_O_S O.apply sym_eq. assumption. +(* one - one *) +reflexivity. +(* one - proper *) +simplify in H1. +apply False_ind. +apply not_le_Sn_n (S O). +rewrite > H1 in \vdash (? ? %). +change with (S O) < defactorize_aux n O. +apply lt_SO_defactorize_aux. +generalize in match H.elim g. +(* proper - zero *) +simplify in H1. +apply False_ind. +apply not_le_Sn_n O. +rewrite < H1 in \vdash (? ? %). +change with O < defactorize_aux n O. +apply lt_O_defactorize_aux. +(* proper - one *) +simplify in H1. +apply False_ind. +apply not_le_Sn_n (S O). +rewrite < H1 in \vdash (? ? %). +change with (S O) < defactorize_aux n O. +apply lt_SO_defactorize_aux. +(* proper - proper *) +apply eq_f. +apply injective_defactorize_aux O. +exact H1. +qed. + +theorem factorize_defactorize: +\forall f,g: nat_fact_all. factorize (defactorize f) = f. +intros. +apply injective_defactorize. +(* uffa: perche' semplifica ??? *) +change with defactorize(factorize (defactorize f)) = (defactorize f). +apply defactorize_factorize. +qed. diff --git a/helm/matita/library/nat/gcd.ma b/helm/matita/library/nat/gcd.ma index 8475fc06a..99c97b09a 100644 --- a/helm/matita/library/nat/gcd.ma +++ b/helm/matita/library/nat/gcd.ma @@ -297,6 +297,7 @@ rewrite < H7. apply ex_intro ? ? (a1+a*(div m n1)). apply ex_intro ? ? a. left. +(* clear Hcut2.clear H5.clear H6.clear H. *) rewrite > sym_times. rewrite > distr_times_plus. rewrite > sym_times. @@ -331,28 +332,7 @@ qed. theorem eq_minus_gcd: \forall m,n.\exists a,b.a*n - b*m = (gcd n m) \lor b*m - a*n = (gcd n m). intros. -change with -\exists a,b. -a*n - b*m = -match leb n m with - [ true \Rightarrow - match n with - [ O \Rightarrow m - | (S p) \Rightarrow gcd_aux (S p) m (S p) ] - | false \Rightarrow - match m with - [ O \Rightarrow n - | (S p) \Rightarrow gcd_aux (S p) n (S p) ]] -\lor b*m - a*n = -match leb n m with - [ true \Rightarrow - match n with - [ O \Rightarrow m - | (S p) \Rightarrow gcd_aux (S p) m (S p) ] - | false \Rightarrow - match m with - [ O \Rightarrow n - | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]. +unfold gcd. apply leb_elim n m. apply nat_case1 n. simplify.intros. diff --git a/helm/matita/library/nat/nat.ma b/helm/matita/library/nat/nat.ma index e2bf56542..e36c1beaa 100644 --- a/helm/matita/library/nat/nat.ma +++ b/helm/matita/library/nat/nat.ma @@ -26,7 +26,7 @@ definition pred: nat \to nat \def | (S p) \Rightarrow p ]. theorem pred_Sn : \forall n:nat.n=(pred (S n)). -intros; reflexivity. +intros. reflexivity. qed. theorem injective_S : injective nat nat S. -- 2.39.2