The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hi. It follows easily using Classical:

Lemma goal : ~(exists n, forall p, prime p -> p <=n) ->
             forall n, exists p, prime p /\ p > n.

Proof.
  intros h n. apply NNPP. intro hn. apply h. exists n. intros p hp.
  generalize (not_ex_all_not _ _ hn p); clear hn; intro hn.
  apply not_and_or in hn. destruct hn. tauto. omega.
Qed.

Le 30/11/2014 12:40, Ilmārs Cīrulis a écrit :

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".

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

On Wed, Nov 26, 2014 at 12:40 PM, Enrico Tassi <enrico.tassi AT inria.fr> wrote:
On Wed, Nov 26, 2014 at 09:35:11AM +0100, Carst Tankink wrote:
> In any case, thanks for posting this, Gabriel! It's always good to have
> something on the web to point to when making the point that theorem provers
> need external support (tools/documentation/communities) as well as the tool
> itself.

I fully agree.  Unfortunately the wish-list is so long that it makes me
fear it will take a century to solve all these issues.

But I really want to share the solution to one of them, in particular
how to prove the infinity of primes on top of a "well furnished"
library[1] in a number of lines that compares well with his latex proof:

  https://sympa.inria.fr/sympa/arc/ssreflect/2014-04/msg00000.html

Best,
--
Enrico Tassi
[1] : that Neil could not install, and that is very sad, but still...