The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

I'm looking for  a constructive proof that runs reasonably fast.

Ideally, the statement should say that given a list of primes, there (constructively) exists  a prime not in the list.

By reasonably fast, I mean that it should take only a few seconds to (vm_)compute the answer for small inputs like [2,5,7].

It would great if someone posted  complete .v file(s), along with a description of the dependencies.

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Mon, Dec 1, 2014 at 7:17 AM, Enrico Tassi <enrico.tassi AT inria.fr> wrote:

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