The Coq mailing list

["Flavio L. C. de Moura" <flaviomoura AT unb.br>]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Yes, you are right. An the point is that I can't see how to adapt my
paper proof to Coq. The paper proof is as follows:

We need an auxiliary lemma (already proved in Coq):

Lemma 1 : forall (x i k:Z), 0 < k < i -> (i|x) -> ~(i|(x+k)).

Since i is prime, if it divides a product of consecutive numbers, say
(n-i+1)(n-i+2)...(n-1) then it divides exactly one of the numbers
(n-i+1), (n-i+2), ..., (n-1). So there exists 1 <= j < i such that i |
(n-i+j). By Lemma 1, we conclude that ~(i|n) by taking k = i-j. Qed.

So, the problem is the number j because I believe that its existence is
not enough to build a proof in Coq. It is necessary to have a way to
build j, isn't it?

Cheers,
Flávio.




Em 22-05-2010 17:01, Taral escreveu:
> On Sat, May 22, 2010 at 7:36 PM, Flavio L. C. de Moura
>Â <flaviomoura AT unb.br>
>  wrote:
>> I am afraid this theorem cannot be proved in Coq because in a certain
>> sense we cannot find the exact k such that i divides (n-i+k) (1<=k<i)...
>> is that true? Any comments is very welcome!
> 
> The first step in creating a coq proof is being able to prove your
> statement to yourself and understanding how the proof works. If you
> can't prove it at a high level, then (in my experience) coq will not
> help you.
> 
> So... how would you prove this statement of yours on paper?
> 

-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.15 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iEYEARECAAYFAkv4R/oACgkQJ9M3XSenoWhWlACfY6V5y3b/apJrXkmwcIhnZxVC
8rUAn0C/05b9wYSmSkR9JD1Sj0zjrTdv
=rQKe
-----END PGP SIGNATURE-----