The Coq mailing list

[AUGER C�dric <Cedric.Auger AT lri.fr>]

Le Mon, 21 Dec 2009 11:54:58 +0100,
Andrea Poles 
<evilpuchu AT gmail.com>
 a écrit :

> Hi all, we have modified the coq-implementation of the Euclid's
> theorem (for primes).
> The following code is supposed to be right:
> 
>   1 Require Import Wf_nat.
>   2 Require Import Coq.Program.Equality.
>   3
>   4
>   5 Variable Pn1 : nat.
>   6 Definition Divides (n m: nat) : Prop := exists q : nat, m = n * q.
>   7 Definition Prime (n : nat) : Prop :=
>   8   n > 1 /\ (forall q : nat, Divides q n -> q = 1 \/ q = n).
>   9
>  10 Fixpoint fact (n:nat) : nat :=
>  11   match n with
>  12     | O => 1
>  13     | S n => S n * fact n
>  14   end.
>  15 Definition Bound := forall (Pn:nat) , Prime(Pn) ->
>  16            (exists x:nat , (gt x Pn) /\ x < fact(Pn)+1
>  17                         /\ Prime(x)).
>  18
>  19 Hypothesis  hyp: Prime Pn1.
>  20
>  21 Theorem Euclide : forall (y:nat) ,
>  22        (exists x:nat , Prime(x) /\ (gt x y)).
>  23 intros.
>  24 elim y.
>  25 exists Pn1.
>  26 split.
>  27 apply hyp.
> 
> Now, we have to demonstrate that primes are infinitely, using the
> above "rules"... and the Euclid's theorem of course!
> Any idea?
> 
> Thank you all!
> 

if you don't want to use excluded middle, you need to build a successor
(not necessarily immediate successor), which can be quite tricky;
else you can prove:
>  21 Theorem Euclide : forall (y:nat) ,
>  22        (forall x:nat , Prime(x) -> gt x y -> False) -> False.
which is probably easier.

But I think the real point is to add lemmas, such as:
forall x, (forall y, gt x y -> Prime y -> Divides y x -> False) ->
Prime x.

forall x, exists (l : list nat), forall y, gt x y -> Prime y -> In y l

also define a list_prod function and prove that

forall (l : list nat), (forall x, In x l -> x<>0) ->
 forall y, In y l -> gt (S (list_prod l)) y

forall l x, In x l -> Divides x (S (list_prod l)) -> False

After having proved that, the proof shouldn't be too hard...
(But proving all that can consume a lot of time)
This is not the only proof of infinity of primes number I know,
but it is the easiest.

I think that googling can also be useful, as I am pretty sure someone
has already done it (do not restrict search to coq, try also other
proof assistants to have more results).

By the way, do not hesitate to define your own Prop inductives, they
can be prettier and easier than using _ /\ _ or _ \/ _ or exists _, _;
for instance, Divides can be rewritten as:
>   6    Record Divides (n m : nat) : Prop :=
>   6bis Div { quo : nat;
>   6ter       div_spe : m = n * quo }.

it can be handful, as a proof term of Divides 2 6 can simply be
({| quo := 3;
    div_spe := refl_equal 6|} : Divides 2 6)
 (with 8.3 version I hope (sorry I don't have installed it on my
 computer))

or at least:
"Div 2 6 3 (refl_equal 6)"
(checked)

which is less awful than 
   (ex_intro _ 3 (refl_equal 6) : Divides 2 6)
or (ex_intro (fun q => 6 = 2 * q) 3 (refl_equal 6))

and notations, such as 
Notation "[ x | y ]" := (Divides x y).

which allows proofs like:

Goal [2|6].
split with 3.
split.
Qed. (* very implicit *)

Goal [2|6].
apply Div with (quo := 3).
reflexivity.
Qed. (* very explicit *)

(there is no real gain with exists definition in the first case, but
the second case is clear in comparison to:
exists 3.
reflexivity.)

First time I read your post, I didn't see your fact function, and
suggested you list_prod; I think list_prod is easier, but what I said
should be adaptable to your fact function.

About records vs exists, and, or, for Prime, you can consider:

Record Prime (n : nat) : Prop :=
{ one_is_not_prime : n > 1;
  no_other_prime_factor : forall q : nat, q<>1 -> gt n q ->
                          Divides q n -> False
}.