coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] a claim about prime numbers

From: Taral <taralx AT gmail.com>
To: "Flavio L. C. de Moura" <flaviomoura AT unb.br>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] a claim about prime numbers
Date: Sat, 22 May 2010 21:01:18 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; b=p6vn7J0GyPgYOsSti0roBuUIphP4DvjrKQVtMXwlLuRk2ELWCBlKnjO+O3eMkDAjHe QAF8sRZpSr1mDFcysbHsDwCg27hMXW41pMJvJEU1DWb4dulHIxfsEAa4hjEa3kEjON7V iDHbYPdvlXiQ0xR6cA8QVXFYiHEqs/zeprBhU=

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?

--
Taral
<taralx AT gmail.com>
"Please let me know if there's any further trouble I can give you."
-- Unknown

[Coq-Club] a claim about prime numbers, Flavio L. C. de Moura
- Re: [Coq-Club] a claim about prime numbers, Taral
  - Re: [Coq-Club] a claim about prime numbers, Flavio L. C. de Moura
    - Re: [Coq-Club] a claim about prime numbers, St�phane Lescuyer
- Re: [Coq-Club] a claim about prime numbers, Stéphane Glondu
- [Coq-Club] Re: a claim about prime numbers, Adam Megacz