# Theory Pratt_Certificate

theory Pratt_Certificate
imports Lehmer
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) = {}"

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
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"}
*}

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

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