# Theory Pratt_Certificate

theory Pratt_Certificate
imports Lehmer
theory Pratt_Certificateimports  Complex_Main  Lehmerbeginsection {* 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 nattext {*  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 autoqedtheorem 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 assmsproof (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 auto    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  qedqedsection {* 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 assmsproof (induction r)  case (Cons y ys) then show ?case by (cases y) autoqed simplemma 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 assmsproof (induction qs arbitrary: r)  case Nil thus ?case by autonext  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 simpqedlemma length_fpc:  "length (build_fpc p a r qs) = length qs + 1" by (induction qs arbitrary: r) autolemma 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 .qedlemma 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 assmsproof (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 simpnext  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 simpqedlemma 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) autolemma 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)qedlemma 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 fastforceqedlemma 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 assmsproof (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 fastforceqedlemma listprod_ge:  fixes xs::"nat list"  assumes "∀ x ∈ set xs . x ≥ 1"  shows "listprod xs ≥ 1" using assms by (induction xs) autolemma 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 assmsproof (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 forceqedlemma 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 autoqedtext {*  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 assmsproof (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 fastforceqedtext {*  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 blastcorollary 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 blastqedend