The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Sun, Nov 30, 2014 at 01:40:18PM +0200, Ilmārs Cīrulis wrote:
> Probably a bit offtopic.
> 
> It was easy to prove "(exists n, forall p, prime p -> p <=n) -> False".
> But I had a problems proving "(forall n, exists p, prime p /\ p > n".

That is exactly what the proof Cyril and myself pointed to shows.

 Lemma prime_above m : {p | m < p & prime p}.

Here we have a sigma-type in Type (denoted with {x | P x}) instead of Prop
(denoted with exists), hence we really construct the witness.

> Do you have any hints? (Also, what does that SSReflect proof do?)

The proof uses some facts from the math comp library, namely  

   Lemma pdivP n : n > 1 → {p | prime p & p %| n}.  (* %| means divides *)
   Lemma gtnNdvd n d : 0 < n → n < d → (d %| n) = false.

The theories used are mostly here:

  http://ssr.msr-inria.inria.fr/doc/mathcomp-1.5/MathComp.prime.html
  http://ssr.msr-inria.inria.fr/doc/mathcomp-1.5/MathComp.div.html

I guess you want to look at the pdiv function, that is the one computing
the witness.  Its correctness is not proved directly, but is rather a
consequence of the correctness of the algorithm producing a prime
decomposition (pdiv just picks the smallest item in the decomposition).

Best,
-- 
Enrico Tassi