theory Pratt_Certificate

imports

Complex_Main

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 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

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