The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

Nice indeed, but again the point of the slides is more of "how much time will it take to an experienced mathematician to complete this proof if he never use a proof assistant before". Georges is an experienced mathematician but he does not fulfill the other requirement :).

P.

Le Wed Nov 26 2014 at 11:30:31 AM, Cyril Cohen <cohen AT crans.org> a écrit :

Hi Coq Club,

On 25/11/2014 17:47, Frédéric Blanqui wrote:
> Hello. Here is a relatively short (150 lines) classical proof of the
> infinity of prime numbers. Best regards, Frédéric.

Eight month ago on the ssreflect mailing list, Georges Gonthier posted a
very short proof based on the ssreflect plugin and mathematical
components libraries. As the archives are public anyway
(https://sympa.inria.fr/sympa/arc/ssreflect/2014-04/msg00003.html), I
take the liberty to copy the code down here:

Lemma dvdn_fact m n : 0 < m <= n -> m %| n`!.
Proof.
case: m => //= m; elim: n => //= n IHn; rewrite ltnS leq_eqVlt.
by case/predU1P=> [-> | /IHn]; [apply: dvdn_mulr | apply: dvdn_mull].
Qed.

Lemma prime_above m : {p | m < p & prime p}.
Proof.
have /pdivP[p pr_p p_dv_m1]: 1 < m`! + 1 by rewrite addn1 ltnS fact_gt0.
exists p => //; rewrite ltnNge; apply: contraL p_dv_m1 => p_le_m.
by rewrite dvdn_addr ?dvdn_fact ?prime_gt0 // gtnNdvd ?prime_gt1.
Qed.

Best,
--
Cyril Cohen