From: Andrea Asperti Date: Fri, 12 Oct 2007 11:13:57 +0000 (+0000) Subject: More restructuring in moebius.ma X-Git-Tag: make_still_working~5986 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d8b17e4c77989c669c9db3847bd6b9e7c236e2c3;p=helm.git More restructuring in moebius.ma --- diff --git a/helm/software/matita/library/Z/moebius.ma b/helm/software/matita/library/Z/moebius.ma index d2c3765c3..1eb358521 100644 --- a/helm/software/matita/library/Z/moebius.ma +++ b/helm/software/matita/library/Z/moebius.ma @@ -62,33 +62,6 @@ simplify.reflexivity. qed. *) -theorem not_divides_to_p_ord_O: \forall n,i. -Not (divides (nth_prime i) n) \to p_ord n (nth_prime i) = -pair nat nat O n. -intros. -apply p_ord_exp1 - [apply lt_O_nth_prime_n - |assumption - |autobatch - ] -qed. - -theorem p_ord_O_to_not_divides: \forall n,i,r. -O < n \to -p_ord n (nth_prime i) = pair nat nat O r -\to Not (divides (nth_prime i) n). -intros. -lapply (p_ord_to_exp1 ? ? ? ? ? ? H1) - [apply lt_SO_nth_prime_n - |assumption - |elim Hletin. - simplify in H3. - rewrite > H3. - rewrite < plus_n_O. - assumption - ] -qed. - theorem not_divides_to_eq_moebius_aux: \forall n,p,p1.p \le p1 \to (\forall i. p \le i \to i \le p1 \to Not (divides (nth_prime i) n)) \to moebius_aux p n = moebius_aux p1 n. @@ -143,39 +116,6 @@ elim p ] qed. -theorem p_ord_to_not_eq_O : \forall n,p,q,r. - (S O) < n \to - p_ord n (nth_prime p) = pair nat nat q r \to - Not (r=O). -intros. -unfold.intro. -cut (O < n) - [lapply (p_ord_to_exp1 ? ? ? ? ? ? H1) - [apply lt_SO_nth_prime_n. - |assumption - |elim Hletin. - apply (lt_to_not_eq ? ? Hcut). - rewrite > H4. - rewrite > H2. - apply times_n_O - ] - |apply (trans_lt ? (S O))[apply lt_O_S|assumption] - ] -qed. - -theorem max_prime_factor_to_not_p_ord_O : \forall n,p,r. - (S O) < n \to - p = max_prime_factor n \to - p_ord n (nth_prime p) \neq pair nat nat O r. -intros.unfold Not.intro. -apply (p_ord_O_to_not_divides ? ? ? ? H2) - [apply (trans_lt ? (S O))[apply lt_O_S|assumption] - |rewrite > H1. - apply divides_max_prime_factor_n. - assumption - ] -qed. - theorem p_ord_SO_SO_to_moebius : \forall n,p. (S O) < n \to p = max_prime_factor n \to @@ -260,115 +200,6 @@ rewrite > H2.simplify. reflexivity. 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 -p = max_prime_factor (r*(nth_prime p)\sup n). -intros. -apply sym_eq. -unfold max_prime_factor. -apply max_spec_to_max. -split - [split - [rewrite > times_n_SO in \vdash (? % ?). - rewrite > sym_times. - apply le_times - [assumption - |apply lt_to_le. - apply (lt_to_le_to_lt ? (nth_prime p)) - [apply lt_n_nth_prime_n - |rewrite > exp_n_SO in \vdash (? % ?). - apply le_exp - [apply lt_O_nth_prime_n - |assumption - ] - ] - ] - |apply eq_to_eqb_true. - apply divides_to_mod_O - [apply lt_O_nth_prime_n - |apply (lt_O_n_elim ? H). - intro. - apply (witness ? ? (r*(nth_prime p \sup m))). - rewrite < assoc_times. - rewrite < sym_times in \vdash (? ? ? (? % ?)). - rewrite > exp_n_SO in \vdash (? ? ? (? (? ? %) ?)). - rewrite > assoc_times. - rewrite < exp_plus_times. - reflexivity - ] - ] - |intros. - apply not_eq_to_eqb_false. - unfold Not.intro. - lapply (mod_O_to_divides ? ? ? H5) - [apply lt_O_nth_prime_n - |cut (Not (divides (nth_prime i) ((nth_prime p)\sup n))) - [elim H2 - [rewrite > H6 in Hletin. - simplify in Hletin. - rewrite < plus_n_O in Hletin. - apply Hcut.assumption - |elim (divides_times_to_divides ? ? ? ? Hletin) - [apply (lt_to_not_le ? ? H3). - apply lt_to_le. - apply (le_to_lt_to_lt ? ? ? ? H6). - apply f_m_to_le_max - [apply (trans_le ? (nth_prime i)) - [apply lt_to_le. - apply lt_n_nth_prime_n - |apply divides_to_le[assumption|assumption] - ] - |apply eq_to_eqb_true. - apply divides_to_mod_O - [apply lt_O_nth_prime_n|assumption] - ] - |apply prime_nth_prime - |apply Hcut.assumption - ] - ] - |unfold Not.intro. - apply (lt_to_not_eq ? ? H3). - apply sym_eq. - elim (prime_nth_prime p). - apply injective_nth_prime. - apply H8 - [apply (divides_exp_to_divides ? ? ? ? H6). - apply prime_nth_prime. - |apply lt_SO_nth_prime_n - ] - ] - ] - ] -qed. - -lemma lt_max_prime_factor_to_not_divides: \forall n,p:nat. -O < n \to n=S O \lor max_prime_factor n < p \to -(nth_prime p \ndivides n). -intros.unfold Not.intro. -elim H1 - [rewrite > H3 in H2. - apply (le_to_not_lt (nth_prime p) (S O)) - [apply divides_to_le[apply le_n|assumption] - |apply lt_SO_nth_prime_n - ] - |apply (not_le_Sn_n p). - change with (p < p). - apply (le_to_lt_to_lt ? ? ? ? H3). - unfold max_prime_factor. - apply f_m_to_le_max - [apply (trans_le ? (nth_prime p)) - [apply lt_to_le. - apply lt_n_nth_prime_n - |apply divides_to_le;assumption - ] - |apply eq_to_eqb_true. - apply divides_to_mod_O - [apply lt_O_nth_prime_n|assumption] - ] - ] -qed. - theorem moebius_exp: \forall p,q,r:nat. O < r \to r = (S O) \lor (max_prime_factor r) < p \to (* r = (S O) \lor (max r (\lambda p:nat.eqb (r \mod (nth_prime p)) O)) < p \to *) diff --git a/helm/software/matita/library/nat/factorization.ma b/helm/software/matita/library/nat/factorization.ma index 0bd8e2478..14696ca28 100644 --- a/helm/software/matita/library/nat/factorization.ma +++ b/helm/software/matita/library/nat/factorization.ma @@ -101,6 +101,19 @@ elim (le_to_or_lt_eq ? ? H) ] qed. +theorem max_prime_factor_to_not_p_ord_O : \forall n,p,r. + (S O) < n \to + p = max_prime_factor n \to + p_ord n (nth_prime p) \neq pair nat nat O r. +intros.unfold Not.intro. +apply (p_ord_O_to_not_divides ? ? ? ? H2) + [apply (trans_lt ? (S O))[apply lt_O_S|assumption] + |rewrite > H1. + apply divides_max_prime_factor_n. + assumption + ] +qed. + 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) = p_ord n (nth_prime p) \to @@ -164,6 +177,33 @@ assumption.apply sym_eq.assumption.assumption.assumption. apply (le_to_or_lt_eq ? p H1). qed. +lemma lt_max_prime_factor_to_not_divides: \forall n,p:nat. +O < n \to n=S O \lor max_prime_factor n < p \to +(nth_prime p \ndivides n). +intros.unfold Not.intro. +elim H1 + [rewrite > H3 in H2. + apply (le_to_not_lt (nth_prime p) (S O)) + [apply divides_to_le[apply le_n|assumption] + |apply lt_SO_nth_prime_n + ] + |apply (not_le_Sn_n p). + change with (p < p). + apply (le_to_lt_to_lt ? ? ? ? H3). + unfold max_prime_factor. + apply f_m_to_le_max + [apply (trans_le ? (nth_prime p)) + [apply lt_to_le. + apply lt_n_nth_prime_n + |apply divides_to_le;assumption + ] + |apply eq_to_eqb_true. + apply divides_to_mod_O + [apply lt_O_nth_prime_n|assumption] + ] + ] +qed. + (* datatypes and functions *) inductive nat_fact : Set \def @@ -456,6 +496,88 @@ 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 +p = max_prime_factor (r*(nth_prime p)\sup n). +intros. +apply sym_eq. +unfold max_prime_factor. +apply max_spec_to_max. +split + [split + [rewrite > times_n_SO in \vdash (? % ?). + rewrite > sym_times. + apply le_times + [assumption + |apply lt_to_le. + apply (lt_to_le_to_lt ? (nth_prime p)) + [apply lt_n_nth_prime_n + |rewrite > exp_n_SO in \vdash (? % ?). + apply le_exp + [apply lt_O_nth_prime_n + |assumption + ] + ] + ] + |apply eq_to_eqb_true. + apply divides_to_mod_O + [apply lt_O_nth_prime_n + |apply (lt_O_n_elim ? H). + intro. + apply (witness ? ? (r*(nth_prime p \sup m))). + rewrite < assoc_times. + rewrite < sym_times in \vdash (? ? ? (? % ?)). + rewrite > exp_n_SO in \vdash (? ? ? (? (? ? %) ?)). + rewrite > assoc_times. + rewrite < exp_plus_times. + reflexivity + ] + ] + |intros. + apply not_eq_to_eqb_false. + unfold Not.intro. + lapply (mod_O_to_divides ? ? ? H5) + [apply lt_O_nth_prime_n + |cut (Not (divides (nth_prime i) ((nth_prime p)\sup n))) + [elim H2 + [rewrite > H6 in Hletin. + simplify in Hletin. + rewrite < plus_n_O in Hletin. + apply Hcut.assumption + |elim (divides_times_to_divides ? ? ? ? Hletin) + [apply (lt_to_not_le ? ? H3). + apply lt_to_le. + apply (le_to_lt_to_lt ? ? ? ? H6). + apply f_m_to_le_max + [apply (trans_le ? (nth_prime i)) + [apply lt_to_le. + apply lt_n_nth_prime_n + |apply divides_to_le[assumption|assumption] + ] + |apply eq_to_eqb_true. + apply divides_to_mod_O + [apply lt_O_nth_prime_n|assumption] + ] + |apply prime_nth_prime + |apply Hcut.assumption + ] + ] + |unfold Not.intro. + apply (lt_to_not_eq ? ? H3). + apply sym_eq. + elim (prime_nth_prime p). + apply injective_nth_prime. + apply H8 + [apply (divides_exp_to_divides ? ? ? ? H6). + apply prime_nth_prime. + |apply lt_SO_nth_prime_n + ] + ] + ] + ] +qed. + theorem not_divides_defactorize_aux: \forall f:nat_fact. \forall i,j:nat. i < j \to nth_prime i \ndivides defactorize_aux f j. intro.elim f. diff --git a/helm/software/matita/library/nat/ord.ma b/helm/software/matita/library/nat/ord.ma index 4fd2fd282..5895b3bcd 100644 --- a/helm/software/matita/library/nat/ord.ma +++ b/helm/software/matita/library/nat/ord.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/nat/ord". include "datatypes/constructors.ma". include "nat/exp.ma". -include "nat/gcd.ma". +include "nat/nth_prime.ma". include "nat/relevant_equations.ma". (* required by autobatch paramod *) let rec p_ord_aux p n m \def @@ -240,6 +240,7 @@ rewrite < times_n_SO. apply exp_n_SO. qed. +(* p_ord and divides *) theorem divides_to_p_ord: \forall p,a,b,c,d,n,m:nat. O < n \to O < m \to prime p \to divides n m \to p_ord n p = pair ? ? a b \to @@ -313,7 +314,55 @@ cut (S O < p) ] |elim H2.assumption ] -qed. +qed. + +(* p_ord and primes *) +theorem not_divides_to_p_ord_O: \forall n,i. +Not (divides (nth_prime i) n) \to p_ord n (nth_prime i) = +pair nat nat O n. +intros. +apply p_ord_exp1 + [apply lt_O_nth_prime_n + |assumption + |autobatch + ] +qed. + +theorem p_ord_O_to_not_divides: \forall n,i,r. +O < n \to +p_ord n (nth_prime i) = pair nat nat O r +\to Not (divides (nth_prime i) n). +intros. +lapply (p_ord_to_exp1 ? ? ? ? ? ? H1) + [apply lt_SO_nth_prime_n + |assumption + |elim Hletin. + simplify in H3. + rewrite > H3. + rewrite < plus_n_O. + assumption + ] +qed. + +theorem p_ord_to_not_eq_O : \forall n,p,q,r. + (S O) < n \to + p_ord n (nth_prime p) = pair nat nat q r \to + Not (r=O). +intros. +unfold.intro. +cut (O < n) + [lapply (p_ord_to_exp1 ? ? ? ? ? ? H1) + [apply lt_SO_nth_prime_n. + |assumption + |elim Hletin. + apply (lt_to_not_eq ? ? Hcut). + rewrite > H4. + rewrite > H2. + apply times_n_O + ] + |apply (trans_lt ? (S O))[apply lt_O_S|assumption] + ] +qed. definition ord :nat \to nat \to nat \def \lambda n,p. fst ? ? (p_ord n p).