(* PrattCertificate.m *)
Off[General::spell1];
AssumedPrimeBound::usage = "AssumedPrimeBound is an option to PrattCertificate that causes primes under this bound to be deemed prime without need of certification.";
PrattCertificate::usage = "PrattCertificate[p] returns a Pratt certificate of p's primality, where p is assumed to have returned True under PrimeQ.";
Tree::usage = "Tree is an option to PrattCertificate that requests that the certificate be returned in the form of a tree.";
PrimeQTest::usage = "PrimeQTest is an option to PrattCertificate that asks the PrimeQ test on the input to be performed. Setting this to False saves time in situations where it is known that the input passes this test.";
CertificateTreeForm::usage = "CertificateTreeForm[data, level, indent] takes a Pratt certificate in the list-form returned by PrattCertificate and turns it into a gridbox in the form of a tree.";
ShowWitnesses::usage = "ShowWitnesses is an option to PrattCertify that causes a list of the witnesses used to be returned along with the certificate.";
SetAttributes[PrattCertificate, Listable]
(* The level is included only to distinguish the top of the recursion for purposes of calling CertificateTreeForm at the right time only. *)
PrattCertificate::noprim = "`` is not prime.";
PrattCertificate::notree = "The tree format will not work when the ShowWitnesses option is turned on";
PrattCertificate::nowitn = "The request for witnesses works only if the AssumedPrimeBound is set to its default, 2.";
Options[PrattCertificate] = {Tree -> False,
PrimeQTest -> True, AssumedPrimeBound -> 2,
HighlightFirstLevel -> True,
ShowWitnesses -> False, Show2s -> True, FontSize -> 12};
PrattCertificate[2, level_Integer:0, opts___] := 2
PrattCertificate[p_Integer, level_Integer:0, opts___Rule] :=
Module[{w = 2, primes, treeQ, skipQ, specBound, show2Q},
{treeQ, skipQ, specBound, witQ, show2Q,fs, hfl} =
{Tree, PrimeQTest, AssumedPrimeBound,
ShowWitnesses, Show2s, FontSize, HighlightFirstLevel} /.
{opts} /. Options[PrattCertificate];
input = HoldForm[PrattCertificate[p, opts]];
If[specBound > 2 && witQ,
Message[PrattCertificate::nowitn]; Return[input]];
If[treeQ && witQ,
Message[PrattCertificate::notree]; Return[input]];
witF = If[witQ && level == 0,
{#, Flatten[# //.{a_, b_, c_} :> {b,c}]} &,
Identity];
If[p <= specBound, Return[p]];
If[!skipQ && !PrimeQ[p],
Message[PrattCertificate::noprim, p];
Return[input]];
primes = Map[First, FactorInteger[p - 1]];
If[level==0,
elim2sfcn[d_] := If[show2Q,d,
DeleteCases[d, _List?(Union[Characters[#[[1]]]]=={"\""," ","2"}&),\[Infinity]]]];
While[ JacobiSymbol[w, p] == 1 ||
PowerMod[w, p-1, p] != 1 ||
(temp = False;
Do[If[PowerMod[w, (p - 1)/primes[[i]], p] == 1,
temp = True; Break[]],
{i, Length[primes]}]; temp), w++];
out = elim2sfcn @ witF[If[treeQ && level == 0,
CertificateTreeForm[#,0,0]&,
Identity][
{p, w, PrattCertificate[primes, 1,
PrimeQTest -> False, opts]}//.
{2, x__} :> {If[treeQ && level == 0,List,Identity][2], x}]];
out //. If[hfl, {s_String?(coun[#]=={weight[out]}&)}:>{StyleBox[s, FontWeight->Plain,
FontColor->RGBColor[1,0,0]]}, {}]] /; p > 2
indentFcn[ind_, x_] := Table[" ", {ind}] <> ToString[x]
CertificateTreeForm[m_Integer, indent_, level_] :=
If[level==0, TableForm, Identity][{indentFcn[indent,m]}];
CertificateTreeForm[{m_Integer}, indent_, level_] :=
If[level==0, TableForm, Identity][{indentFcn[indent,m]}];
CertificateTreeForm[{{m_Integer}, other__}, indent_, level_] :=
Prepend[Apply[Join,
Map[CertificateTreeForm[#, indent, level+1]&, {other}]],
indentFcn[indent, m]]
CertificateTreeForm[{p_, w_Integer, other_}, indent_, level_] :=
If[level == 0,
DisplayForm[StyleBox[GridBox[List /@ ToString /@ MakeBoxes /@ #,
ColumnAlignments->Left,GridFrame->1,
GridFrameMargins -> {{1,1}, {1.5,1.5}},
RowSpacings->0.6],
FontFamily->Courier, FontSize->fs, FontWeight->Plain,Background->GrayLevel[0.9]]]&, Identity][
Prepend[
Flatten[CertificateTreeForm[#,
indent+1+Length[IntegerDigits[p]], level+1]& /@ other,1],
indentFcn[indent, p] <> " \[Rule] " <> ToString[w]]]
coun[s_] := First@Rest@Position[Characters[s], _?(# != " "&)]
weight[d_] := First[Rest[Flatten[(d /.
(x_String :> coun[x]))[[1,1,1]]]]]