The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2014-12-01 11:40 GMT+01:00 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.

I guess that means you use excluded middle axiom. I am not sure that the initial question allowed use of an extra axiom.
I am almost certain that the proof scheme I gave is axiom free in the logic of Coq.

 

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

--

.../Sedrikov\...