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.
]
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
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 *)
]
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
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
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.
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
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
]
|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).
projects / helm.git / commitdiff