Correct phrasing for recursive data structure

Stream: general

[Patrick Stevens]

Here's what a Pratt certificate of primality looks like (this is not quite the form that would slot into LucasPrimality.lean, which uses ZMod in a way that appears to foil norm_num entirely):

structure PrattPrimeCertificate (n : ℕ) where
  base: ℕ
  h_base : (base ^ (n - 1)) % n = 1
  sub_one_factors : List ℕ
  all_prime : ∀ x ∈ sub_one_factors, x.Prime
  are_factors : (n - 1) = List.foldl (fun x y => x * y) 1 sub_one_factors
  are_cert : ∀ x ∈ sub_one_factors, (base ^ ((n - 1) / x)) % n ≠ 1

There are several possible options for how the "all_prime" field is expressed, though. Above, I've picked a pretty flexible one which doesn't have any recursion - but it's also not at all amenable to serialisation, and it's always a bit annoying to construct foralls. A more "natural" format from a programming point of view might instead have sub_one_factors be a list of (k, multiplicity, PrattPrimeCertificate(k)), and then store a proof that this is indeed a factorisation of n-1 much as I currently do in are_factors. That way, we entirely separate any idea of a proof of primality away from the data. There's still a degree of freedom about whether to bundle the (base ^ (n - 1) / k) % n ≠ 1 into that list, though: putting it into the list means sub_one_factors is no longer easy to serialise as data, but taking it out of the list means we have to bundle a separate proof quantifying over every factor at once.

What would people's intuitions be on the "easiest" way to express the above (especially given that I imagine a primary use-case for Pratt certificates would be interfacing with external primality provers)? Would you bite the bullet and store recursive copies of the struct in the all_prime list (which I guess means you need well-foundedness proofs for any operation on a PrattPrimeCertificate)? Would you somehow completely unbundle all the proofs so that there's a proof-free datatype which can be freely exchanged with external provers, and then attach some kind of proof object to it? Something else I haven't considered?

[Patrick Stevens]

(I feel like Conor McBride would have a beautiful elegant answer that was somehow perfectly ergonomic.)

[Yury G. Kudryashov]

docs#List.Forall unfolds to Ands. You can construct each Prime _ in this And from PrattPrimeCertificate without adding this requirement to the structure itself.

[Yury G. Kudryashov]

We also have docs#List.prod which is defeq to the List.foldl you use in are_factors

[Yury G. Kudryashov]

Of course, you need a theorem

proof_wanted PrattPrimeCerticifate.prime {n : Nat} (hn : PrattPrimeCertificate n) : n.Prime

to construct each Prime in the long And.

[Markus Himmel]

Hi @Patrick Stevens, I have a formalization of Pratt certificates which you might be interested in (warning: unpolished code): https://github.com/leanprover-community/mathlib4/blob/6439ce3f194a2acd309af6831d753e560c46bcf6/Mathlib/NumberTheory/LucasPrimality.lean#L74 I chose the following approach: the proof-carrying PrattCertificate only has "one level" of depth and just takes Nat.Prime arguments for the factors of n-1. However, there is also an UnverifiedPrattCertificate, which contains recursive unverified pratt certificates down to a fixed list of known primes. The unverified pratt certificate is just the data (i.e., the witnesses and the factorization), without any proofs, and this would lend itself well to serialization, though that isn't implemented. The pratt tactic currently consists of two parts, the first generates an UnverifiedPrattCertificate and the second part turns an UnverifiedPrattCertificate into a PrattCertificate, failing if the data is not valid.

[Patrick Stevens]

Thanks Markus, that looks pretty good ergonomically to me! How did you choose the structure of split - was that just a lucky guess at something that would be easy to use, or did you have some heuristic that told you it would work well, or what?

[Markus Himmel]

This decision was partly inspired by the norm_num implementation of exponentiation (see file#Tactic/NormNum/Pow), where the computation/proof is structured as a binary tree in order to avoid deep recursion. I noticed that a similar approach could be useful to break down dealing with the prime factors of p-1 into smaller steps without having to deal with lists, and it worked out quite well.