coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Detours in Mathematical Proofs formalized in Coq

From: MailingList Bruno Woltzenlogel Paleo <bruno.wp.mailinglist AT googlemail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Detours in Mathematical Proofs formalized in Coq
Date: Thu, 12 May 2011 12:29:49 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=googlemail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=cyDjEh3AFLpEDZZbpZ7uyzn9KrpgIlxSuhpEov060zsDEdhPRPeZarCxB4K4iHj3D5 ZS7RUB0ecCwpk/e2IP2Wsodv9RDt3qaN2NehJd58+HtLRzquYKpxlMkpvSSE1YWQ1YMf 3koXwyp3B8y4nWXcty8UytoLJea9oVmaLCnEc=

Hi,

I am interested in intuitionistic mathematical proofs formalized in
Coq and satisfying (some of) the following (subjective) requirements:
1) it should be not too complex and not too long.
2) it should use some "mathematically interesting" lemma or auxiliary theorem.
3) obtaining an alternative proof of the same theorem not using the
mentioned auxiliary lemma should, if possible, be "desirable".

If you could point me some examples of Coq proofs satisfying these
requirements, that would be great!

Thanks in advance,
Best regards,

Bruno

--
Bruno Woltzenlogel Paleo
http://www.logic.at/people/bruno/

[Coq-Club] Detours in Mathematical Proofs formalized in Coq, MailingList Bruno Woltzenlogel Paleo
- Re: [Coq-Club] Detours in Mathematical Proofs formalized in Coq, AUGER Cedric
  - Message not available
    - Message not available
      - Re: [Coq-Club] Detours in Mathematical Proofs formalized in Coq, MailingList Bruno Woltzenlogel Paleo