[bgregoir]

Adds Pocklington's primality criterion with computable certificates. It is a port of coqprime's Pocklington.v; names follow mathcomp where an equivalent exists.

Stacked on #1238 (ZModP); followed by #1237 (ChaChaPoly: 2^130 - 5 is prime and the Poly1305 proofs).

theories/algebra/IntDiv.ec (generic modular arithmetic, moved here following review)

• modzXm; the multiplicative order on integers mulorder a n with mulorder_spec, mulorder_gt0, expz_mulorder, mulorder_dvdz, mulorder_dvd_pred (named mulorder to avoid a clash with Group.order);
• pdivP (an integer > 1 has a prime divisor) and primePns (characterisation of non-primes by a prime divisor p with p^2 <= n);
• reduction rules for computing, kept out of the default database: modular exponentiation by squaring powmod (powmod0, powmodE) in the hint database powmod, and Euclid's algorithm gcdE : gcd a b = if b = 0 then |a| else gcd b (a %% b) in the hint database gcd. They are used as cbv delta hint +powmod +gcd; plain cbv is unchanged.

theories/algebra/Pocklington.ec (new)

• pocklington: if N - 1 = F1 * R1 and, for every prime p | F1, some a satisfies a^(N-1) = 1 mod N and gcd(a^((N-1)/p) - 1, N) = 1, then every prime divisor of N is 1 mod F1; pocklington_prime concludes prime N when N < F1^2. Unlike coqprime, the combination of the prime factors of F1 goes through gcd/Gauss instead of prime powers, and there is no 1 < a hypothesis;
• computable corollary pock_certif : pock_check N c => all (fun pa => prime pa.1) c => prime N, where the certificate c lists pairs (p, a) whose p multiply to F1; pock_check is decided by cbv delta hint +powmod +gcd.

No new axioms. All of stdlib and examples check.

[fdupress]

This would probably be best as 3 separate PRs (stacked):

1. the ZModP change;
2. Pocklington's criterion and computable primality check;
3. the finalization of the ChaCha+Poly proofs.

We can probably merge as a single PR but it would be good to have the commits rebased into the above so each is meaningful in isolation.

[fdupress]

Should this entire section move to IntDiv or a related theory on modular arithmetic without the algebra?

[bgregoir]

I am agree with you, I will do that

[bgregoir]

done

[fdupress]

Same, does this belong in IntDiv?

[fdupress]

Or perhaps all of the generic, but computable stuff should be in a ComputableIntDiv theory?

[bgregoir]

In fact, I think the best solution is to add reduction lemma in database that can be used when needed.