theory Pratt_Certificate imports Complex_Main "../Lehmer/Lehmer" begin section {* Pratt's Primality Certificates *} text_raw {* \label{sec:pratt} *} text {* This work formalizes Pratt's proof system as described in his article ``Every Prime has a Succinct Certificate''\cite{pratt1975certificate}. The proof system makes use of two types of predicates: \begin{itemize} \item $\text{Prime}(p)$: $p$ is a prime number \item $(p, a, x)$: @{text "∀q ∈ prime_factors(x). [a^((p - 1) div q) ≠ 1] (mod p)"} \end{itemize} We represent these predicates with the following datatype: *} datatype pratt = Prime nat | Triple nat nat nat text {* Pratt describes an inference system consisting of the axiom $(p, a, 1)$ and the following inference rules: \begin{itemize} \item R1: If we know that $(p, a, x)$ and @{text "[a^((p - 1) div q) ≠ 1] (mod p)"} hold for some prime number $q$ we can conclude $(p, a, qx)$ from that. \item R2: If we know that $(p, a, p - 1)$ and @{text "[a^(p - 1) = 1] (mod p)"} hold, we can infer $\text{Prime}(p)$. \end{itemize} Both rules follow from Lehmer's theorem as we will show later on. A list of predicates (i.e., values of type @{type pratt}) is a \emph{certificate}, if it is built according to the inference system described above. I.e., a list @{term "x # xs :: pratt list"} is a certificate if @{term "xs :: pratt list"} is a certificate and @{term "x :: pratt"} is either an axiom or all preconditions of @{term "x :: pratt"} occur in @{term "xs :: pratt list"}. We call a certificate @{term "xs :: pratt list"} a \emph{certificate for @{term p}}, if @{term "Prime p"} occurs in @{term "xs :: pratt list"}. The function @{text valid_cert} checks whether a list is a certificate. *} fun valid_cert :: "pratt list => bool" where "valid_cert [] = True" | R2: "valid_cert (Prime p#xs) <-> 1 < p ∧ valid_cert xs ∧ (∃ a . [a^(p - 1) = 1] (mod p) ∧ Triple p a (p - 1) ∈ set xs)" | R1: "valid_cert (Triple p a x # xs) <-> 0 < x ∧ valid_cert xs ∧ (x=1 ∨ (∃q y. x = q * y ∧ Prime q ∈ set xs ∧ Triple p a y ∈ set xs ∧ [a^((p - 1) div q) ≠ 1] (mod p)))" text {* We define a function @{term size_cert} to measure the size of a certificate, assuming a binary encoding of numbers. We will use this to show that there is a certificate for a prime number $p$ such that the size of the certificate is polynomially bounded in the size of the binary representation of $p$. *} fun size_pratt :: "pratt => real" where "size_pratt (Prime p) = log 2 p" | "size_pratt (Triple p a x) = log 2 p + log 2 a + log 2 x" fun size_cert :: "pratt list => real" where "size_cert [] = 0" | "size_cert (x # xs) = 1 + size_pratt x + size_cert xs" section {* Soundness *} text {* In Section \ref{sec:pratt} we introduced the predicates $\text{Prime}(p)$ and $(p, a, x)$. In this section we show that for a certificate every predicate occuring in this certificate holds. In particular, if $\text{Prime}(p)$ occurs in a certificate, $p$ is prime. *} lemma prime_factors_one[simp]: shows "prime_factors (Suc 0) = {}" by (auto simp add:prime_factors_altdef2_nat) lemma prime_factors_prime: fixes p :: nat assumes "prime p" shows "prime_factors p = {p}" proof have "0 < p" using assms by auto then show "{p} ⊆ prime_factors p" using assms by (auto simp add:prime_factors_altdef2_nat) { fix q assume "q ∈ prime_factors p" then have "q dvd p" "prime q" using `0<p` by (auto simp add:prime_factors_altdef2_nat) with assms have "q=p" by (auto simp: prime_nat_def) } then show "prime_factors p ⊆ {p}" by auto qed theorem pratt_sound: assumes 1: "valid_cert c" assumes 2: "t ∈ set c" shows "(t = Prime p --> prime p) ∧ (t = Triple p a x --> ((∀ q ∈ prime_factors x . [a^((p - 1) div q) ≠ 1] (mod p)) ∧ 0<x))" using assms proof (induction c arbitrary: p a x t) case Nil then show ?case by force next case (Cons y ys) { assume "y=Triple p a x" "x=1" then have "(∀ q ∈ prime_factors x . [a^((p - 1) div q) ≠ 1] (mod p)) ∧ 0<x" by simp } moreover { assume x_y: "y=Triple p a x" "x~=1" hence "x>0" using Cons.prems by auto obtain q z where "x=q*z" "Prime q ∈ set ys ∧ Triple p a z ∈ set ys" and cong:"[a^((p - 1) div q) ≠ 1] (mod p)" using Cons.prems x_y by auto then have factors_IH:"(∀ r ∈ prime_factors z . [a^((p - 1) div r) ≠ 1] (mod p))" "prime q" "z>0" using Cons.IH Cons.prems `x>0` `y=Triple p a x` by force+ then have "prime_factors x = prime_factors z ∪ {q}" using `x =q*z` `x>0` by (simp add:prime_factors_product_nat prime_factors_prime) then have "(∀ q ∈ prime_factors x . [a^((p - 1) div q) ≠ 1] (mod p)) ∧ 0 < x" using factors_IH cong by (simp add: `x>0`) } ultimately have y_Triple:"y=Triple p a x ==> (∀ q ∈ prime_factors x . [a^((p - 1) div q) ≠ 1] (mod p)) ∧ 0<x" by linarith { assume y: "y=Prime p" "p>2" then obtain a where a:"[a^(p - 1) = 1] (mod p)" "Triple p a (p - 1) ∈ set ys" using Cons.prems by auto then have Bier:"(∀q∈prime_factors (p - 1). [a^((p - 1) div q) ≠ 1] (mod p))" using Cons.IH Cons.prems(1) by (simp add:y(1)) then have "prime p" using lehmers_theorem[OF _ _a(1)] `p>2` by fastforce } moreover { assume "y=Prime p" "p=2" hence "prime p" by simp } moreover { assume "y=Prime p" then have "p>1" using Cons.prems by simp } ultimately have y_Prime:"y = Prime p ==> prime p" by linarith show ?case proof (cases "t ∈ set ys") case True show ?thesis using Cons.IH[OF _ True] Cons.prems(1) by (cases y) auto next case False thus ?thesis using Cons.prems(2) y_Prime y_Triple by force qed qed section {* Completeness *} text {* In this section we show completeness of Pratt's proof system, i.e., we show that for every prime number $p$ there exists a certificate for $p$. We also give an upper bound for the size of a minimal certificate The prove we give is constructive. We assume that we have certificates for all prime factors of $p - 1$ and use these to build a certificate for $p$ from that. It is important to note that certificates can be concatenated. *} lemma valid_cert_appendI: assumes "valid_cert r" assumes "valid_cert s" shows "valid_cert (r @ s)" using assms proof (induction r) case (Cons y ys) then show ?case by (cases y) auto qed simp lemma valid_cert_concatI: "(∀x ∈ set xs . valid_cert x) ==> valid_cert (concat xs)" by (induction xs) (auto simp add: valid_cert_appendI) lemma size_pratt_le: fixes d::real assumes "∀ x ∈ set c. size_pratt x ≤ d" shows "size_cert c ≤ length c * (1 + d)" using assms by (induction c) (simp_all add: real_of_nat_def algebra_simps) fun build_fpc :: "nat => nat => nat => nat list => pratt list" where "build_fpc p a r [] = [Triple p a r]" | "build_fpc p a r (y # ys) = Triple p a r # build_fpc p a (r div y) ys" text {* The function @{term build_fpc} helps us to construct a certificate for $p$ from the certificates for the prime factors of $p - 1$. Called as @{term "build_fpc p a (p - 1) qs"} where $@{term "qs"} = q_1 \ldots q_n$ is prime decomposition of $p - 1$ such that $q_1 \cdot \dotsb \cdot q_n = @{term "p - 1 :: nat"}$, it returns the following list of predicates: \[ (p,a,p-1), (p,a,\frac{p - 1}{q_1}), (p,a,\frac{p - 1}{q_1 q_2}), \ldots, (p,a,\frac{p-1}{q_1 \ldots q_n}) = (p,a,1) \] I.e., if there is an appropriate $a$ and and a certificate @{term rs} for all prime factors of $p$, then we can construct a certificate for $p$ as @{term [display] "Prime p # build_fpc p a (p - 1) qs @ rs"} *} definition "listprod ≡ λxs. foldr (op *) xs 1" lemma listprod_Nil[simp]: "listprod [] = 1" by (simp add: listprod_def) lemma listprod_Cons[simp]: "listprod (x # xs) = x * listprod xs" by (simp add: listprod_def) text {* The following lemma shows that @{text "build_fpc"} extends a certificate that satisfies the preconditions described before to a correct certificate. *} lemma correct_fpc: assumes "valid_cert xs" assumes "listprod qs = r" "r ≠ 0" assumes "∀ q ∈ set qs . Prime q ∈ set xs" assumes "∀ q ∈ set qs . [a^((p - 1) div q) ≠ 1] (mod p)" shows "valid_cert (build_fpc p a r qs @ xs)" using assms proof (induction qs arbitrary: r) case Nil thus ?case by auto next case (Cons y ys) have "listprod ys = r div y" using Cons.prems by auto then have T_in: "Triple p a (listprod ys) ∈ set (build_fpc p a (r div y) ys @ xs)" by (cases ys) auto have "valid_cert (build_fpc p a (r div y) ys @ xs)" using Cons.prems by (intro Cons.IH) auto then have "valid_cert (Triple p a r # build_fpc p a (r div y) ys @ xs)" using `r ≠ 0` T_in Cons.prems by auto then show ?case by simp qed lemma length_fpc: "length (build_fpc p a r qs) = length qs + 1" by (induction qs arbitrary: r) auto lemma div_gt_0: fixes m n :: nat assumes "m ≤ n" "0 < m" shows "0 < n div m" proof - have "0 < m div m" using `0 < m` div_self by auto also have "m div m ≤ n div m" using `m ≤ n` by (rule div_le_mono) finally show ?thesis . qed lemma size_pratt_fpc: assumes "a ≤ p" "r ≤ p" "0 < a" "0 < r" "0 < p" "listprod qs = r" shows "∀x ∈ set (build_fpc p a r qs) . size_pratt x ≤ 3 * log 2 p" using assms proof (induction qs arbitrary: r) case Nil then have "log 2 a ≤ log 2 p" "log 2 r ≤ log 2 p" by auto then show ?case by simp next case (Cons q qs) then have "log 2 a ≤ log 2 p" "log 2 r ≤ log 2 p" by auto then have "log 2 a + log 2 r ≤ 2 * log 2 p" by arith moreover have "r div q > 0" using Cons.prems by (fastforce intro: div_gt_0) moreover hence "listprod qs = r div q" using Cons.prems(6) by auto moreover have "r div q ≤ p" using `r≤p` div_le_dividend[of r q] by linarith ultimately show ?case using Cons by simp qed lemma concat_set: assumes "∀ q ∈ qs . ∃ c ∈ set cs . Prime q ∈ set c" shows "∀ q ∈ qs . Prime q ∈ set (concat cs)" using assms by (induction cs) auto lemma p_in_prime_factorsE: fixes n :: nat assumes "p ∈ prime_factors n" "0 < n" obtains "2 ≤ p" "p ≤ n" "p dvd n" "prime p" proof from assms show "prime p" by auto then show "2 ≤ p" by (auto dest: prime_gt_1_nat) from assms show "p dvd n" by (intro prime_factors_dvd_nat) then show "p ≤ n" using `0 < n` by (rule dvd_imp_le) qed lemma prime_factors_list_prime: fixes n :: nat assumes "prime n" shows "∃ qs. prime_factors n = set qs ∧ listprod qs = n ∧ length qs = 1" proof - have "prime_factors n = set [n]" using prime_factors_prime assms by force thus ?thesis by fastforce qed lemma prime_factors_list: fixes n :: nat assumes "3 < n" "¬ prime n" shows "∃ qs. prime_factors n = set qs ∧ listprod qs = n ∧ length qs ≥ 2" using assms proof (induction n rule: less_induct) case (less n) obtain p where "p ∈ prime_factors n" using `n > 3` prime_factors_elem by force then have p':"2 ≤ p" "p ≤ n" "p dvd n" "prime p" using `3 < n` by (auto elim: p_in_prime_factorsE) { assume "n div p > 3" "¬ prime (n div p)" then obtain qs where "prime_factors (n div p) = set qs" "listprod qs = (n div p)" "length qs ≥ 2" using p' by atomize_elim (auto intro: less simp: div_gt_0) moreover have "prime_factors (p * (n div p)) = insert p (prime_factors (n div p))" using `3 < n` `2 ≤ p` `p ≤ n` `prime p` by (auto simp: prime_factors_product_nat div_gt_0 prime_factors_prime) ultimately have "prime_factors n = set (p # qs)" "listprod (p # qs) = n" "length (p#qs) ≥ 2" using `p dvd n` by (simp_all add: dvd_mult_div_cancel) hence ?case by blast } moreover { assume "prime (n div p)" then obtain qs where "prime_factors (n div p) = set qs" "listprod qs = (n div p)" "length qs = 1" using prime_factors_list_prime by blast moreover have "prime_factors (p * (n div p)) = insert p (prime_factors (n div p))" using `3 < n` `2 ≤ p` `p ≤ n` `prime p` by (auto simp: prime_factors_product_nat div_gt_0 prime_factors_prime) ultimately have "prime_factors n = set (p # qs)" "listprod (p # qs) = n" "length (p#qs) ≥ 2" using `p dvd n` by (simp_all add: dvd_mult_div_cancel) hence ?case by blast } note case_prime = this moreover { assume "n div p = 1" hence "n = p" using `n>3` using One_leq_div[OF `p dvd n`] p'(2) by force hence ?case using `prime p` `¬ prime n` by auto } moreover { assume "n div p = 2" hence ?case using case_prime by force } moreover { assume "n div p = 3" hence ?case using p' case_prime by force } ultimately show ?case using p' div_gt_0[of p n] case_prime by fastforce qed lemma listprod_ge: fixes xs::"nat list" assumes "∀ x ∈ set xs . x ≥ 1" shows "listprod xs ≥ 1" using assms by (induction xs) auto lemma listsum_log: fixes b::real fixes xs::"nat list" assumes b: "b > 0" "b ≠ 1" assumes xs:"∀ x ∈ set xs . x ≥ b" shows "(∑x\<leftarrow>xs. log b x) = log b (listprod xs)" using assms proof (induction xs) case Nil thus ?case by simp next case (Cons y ys) have "real (listprod ys) > 0" using listprod_ge Cons.prems by fastforce thus ?case using log_mult[OF Cons.prems(1-2)] Cons by force qed lemma concat_length_le: fixes g :: "nat => real" assumes "∀ x ∈ set xs . real (length (f x)) ≤ g x" shows "length (concat (map f xs)) ≤ (∑x\<leftarrow>xs. g x)" using assms by (induction xs) force+ (* XXX move *) lemma powr_realpow_numeral: "0 < x ==> x powr (numeral n :: real) = x^(numeral n)" unfolding real_of_nat_numeral[symmetric] by (rule powr_realpow) lemma prime_gt_3_impl_p_minus_one_not_prime: fixes p::nat assumes "prime p" "p>3" shows "¬ prime (p - 1)" proof assume "prime (p - 1)" have "¬ even p" using assms by (simp add: prime_odd_nat) hence "2 dvd (p - 1)" by presburger hence "2 ∈ prime_factors (p - 1)" using `p>3` by (auto simp: prime_factors_altdef2_nat) thus False using prime_factors_prime `p>3` `prime (p - 1)` by auto qed text {* We now prove that Pratt's proof system is complete and derive upper bounds for the length and the size of the entries of a minimal certificate. *} theorem pratt_complete': assumes "prime p" shows "∃c. Prime p ∈ set c ∧ valid_cert c ∧ length c ≤ 6*log 2 p - 4 ∧ (∀ x ∈ set c. size_pratt x ≤ 3 * log 2 p)" using assms proof (induction p rule: less_induct) case (less p) { assume [simp]: "p = 2" have "Prime p ∈ set [Prime 2, Triple 2 1 1]" by simp then have ?case by fastforce } moreover { assume [simp]: "p = 3" let ?cert = "[Prime 3, Triple 3 2 2, Triple 3 2 1, Prime 2, Triple 2 1 1]" have "length ?cert ≤ 6*log 2 p - 4 <-> 2 powr 9 ≤ 2 powr (log 2 p * 6)" by auto also have "… <-> True" by (simp add: powr_powr[symmetric] powr_realpow_numeral) finally have ?case by (intro exI[where x="?cert"]) (simp add: cong_nat_def) } moreover { assume "p > 3" have "∀q ∈ prime_factors (p - 1) . q < p" using `prime p` by (fastforce elim: p_in_prime_factorsE) hence factor_certs:"∀q ∈ prime_factors (p - 1) . (∃c . ((Prime q ∈ set c) ∧ (valid_cert c) ∧ length c ≤ 6*log 2 q - 4) ∧ (∀ x ∈ set c. size_pratt x ≤ 3 * log 2 q))" by (auto intro: less.IH) obtain a where a:"[a^(p - 1) = 1] (mod p) ∧ (∀ q. q ∈ prime_factors (p - 1) --> [a^((p - 1) div q) ≠ 1] (mod p))" and a_size: "a > 0" "a < p" using converse_lehmer[OF `prime p`] by blast have "¬ prime (p - 1)" using `p>3` prime_gt_3_impl_p_minus_one_not_prime `prime p` by auto have "p ≠ 4" using `prime p` by auto hence "p - 1 > 3" using `p > 3` by auto then obtain qs where prod_qs_eq:"listprod qs = p - 1" and qs_eq:"set qs = prime_factors (p - 1)" and qs_length_eq: "length qs ≥ 2" using prime_factors_list[OF _ `¬ prime (p - 1)`] by auto obtain f where f:"∀q ∈ prime_factors (p - 1) . ∃ c. f q = c ∧ ((Prime q ∈ set c) ∧ (valid_cert c) ∧ length c ≤ 6*log 2 q - 4) ∧ (∀ x ∈ set c. size_pratt x ≤ 3 * log 2 q)" using factor_certs by metis let ?cs = "map f qs" have cs: "∀q ∈ prime_factors (p - 1) . (∃c ∈ set ?cs . (Prime q ∈ set c) ∧ (valid_cert c) ∧ length c ≤ 6*log 2 q - 4 ∧ (∀ x ∈ set c. size_pratt x ≤ 3 * log 2 q))" using f qs_eq by auto have cs_cert_size: "∀c ∈ set ?cs . ∀ x ∈ set c. size_pratt x ≤ 3 * log 2 p" proof fix c assume "c ∈ set (map f qs)" then obtain q where "c = f q" and "q ∈ set qs" by auto hence *:"∀ x ∈ set c. size_pratt x ≤ 3 * log 2 q" using f qs_eq by blast have "q < p" "q > 0" using `∀q ∈ prime_factors (p - 1) . q < p` `q ∈ set qs` qs_eq by fast+ show "∀ x ∈ set c. size_pratt x ≤ 3 * log 2 p" proof fix x assume "x ∈ set c" hence "size_pratt x ≤ 3 * log 2 q" using * by fastforce also have "… ≤ 3 * log 2 p" using `q < p` `q > 0` `p > 3` by simp finally show "size_pratt x ≤ 3 * log 2 p" . qed qed have cs_valid_all: "∀c ∈ set ?cs . valid_cert c" using f qs_eq by fastforce have "∀x ∈ set (build_fpc p a (p - 1) qs). size_pratt x ≤ 3 * log 2 p" using cs_cert_size a_size `p > 3` prod_qs_eq by (intro size_pratt_fpc) auto hence "∀x ∈ set (build_fpc p a (p - 1) qs @ concat ?cs) . size_pratt x ≤ 3 * log 2 p" using cs_cert_size by auto moreover have "Triple p a (p - 1) ∈ set (build_fpc p a (p - 1) qs @ concat ?cs)" by (cases qs) auto moreover have "valid_cert ((build_fpc p a (p - 1) qs)@ concat ?cs)" proof (rule correct_fpc) show "valid_cert (concat ?cs)" using cs_valid_all by (auto simp: valid_cert_concatI) show "listprod qs = p - 1" by (rule prod_qs_eq) show "p - 1 ≠ 0" using prime_gt_1_nat[OF `prime p`] by arith show "∀ q ∈ set qs . Prime q ∈ set (concat ?cs)" using concat_set[of "prime_factors (p - 1)"] cs qs_eq by blast show "∀ q ∈ set qs . [a^((p - 1) div q) ≠ 1] (mod p)" using qs_eq a by auto qed moreover { let ?k = "length qs" have qs_ge_2:"∀q ∈ set qs . q ≥ 2" using qs_eq by (simp add: prime_factors_prime_nat prime_ge_2_nat) have "∀x∈set qs. real (length (f x)) ≤ 6 * log 2 (real x) - 4" using f qs_eq by blast hence "length (concat ?cs) ≤ (∑q\<leftarrow>qs. 6*log 2 q - 4)" using concat_length_le by fast hence "length (Prime p # ((build_fpc p a (p - 1) qs)@ concat ?cs)) ≤ ((∑q\<leftarrow>(map real qs). 6*log 2 q - 4) + ?k + 2)" by (simp add: o_def length_fpc) also have "… = (6*(∑q\<leftarrow>(map real qs). log 2 q) + (-4 * real ?k) + ?k + 2)" by (simp add: o_def listsum_subtractf listsum_triv real_of_nat_def listsum_const_mult) also have "… ≤ 6*log 2 (p - 1) - 4" using `?k≥2` prod_qs_eq listsum_log[of 2 qs] qs_ge_2 by force also have "… ≤ 6*log 2 p - 4" using log_le_cancel_iff[of 2 "p - 1" p] `p>3` by force ultimately have "length (Prime p # ((build_fpc p a (p - 1) qs)@ concat ?cs)) ≤ 6*log 2 p - 4" by linarith } ultimately obtain c where c:"Triple p a (p - 1) ∈ set c" "valid_cert c" "length (Prime p #c) ≤ 6*log 2 p - 4" "(∀ x ∈ set c. size_pratt x ≤ 3 * log 2 p)" by blast hence "Prime p ∈ set (Prime p # c)" "valid_cert (Prime p # c)" "(∀ x ∈ set (Prime p # c). size_pratt x ≤ 3 * log 2 p)" using a `prime p` by auto hence ?case using c by blast } moreover have "p≥2" using less by (simp add: prime_ge_2_nat) ultimately show ?case using less by fastforce qed text {* We now recapitulate our results. A number $p$ is prime if and only if there is a certificate for $p$. Moreover, for a prime $p$ there always is a certificate whose size is polynomially bounded in the logarithm of $p$. *} corollary pratt: "prime p <-> (∃c. Prime p ∈ set c ∧ valid_cert c)" using pratt_complete' pratt_sound(1) by blast corollary pratt_size: assumes "prime p" shows "∃c. Prime p ∈ set c ∧ valid_cert c ∧ size_cert c ≤ (6 * log 2 p - 4) * (1 + 3 * log 2 p)" proof - obtain c where c: "Prime p ∈ set c" "valid_cert c" and len: "length c ≤ 6*log 2 p - 4" and "(∀ x ∈ set c. size_pratt x ≤ 3 * log 2 p)" using pratt_complete' assms by blast hence "size_cert c ≤ length c * (1 + 3 * log 2 p)" by (simp add: size_pratt_le) also have "… ≤ (6*log 2 p - 4) * (1 + 3 * log 2 p)" using len by simp finally show ?thesis using c by blast qed end