coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] proof techniques
- Date: Fri, 17 Feb 2012 18:36:39 +0100
On Fri, Feb 17, 2012 at 06:26:02PM +0100, Daniel Schepler wrote:
> On Friday, February 17, 2012 07:19:42 AM Daniel de Rauglaudre wrote:
> > I discovered interesting proof techniques while using Coq:
> > 1. think before
> > 2. don't try to prove false theorems
> [...]
>
> Let us know if you find a sure-fire way of detecting false theorems
> beforehand for #2. That would save us all a lot of work. :)
Well, you can apply #1 on the statement of the theorem and, sometimes,
it works.
--
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/
- [Coq-Club] proof techniques, Daniel de Rauglaudre
- Re: [Coq-Club] proof techniques, Daniel Schepler
- Message not available
- Re: [Coq-Club] proof techniques, Daniel de Rauglaudre
Archive powered by MhonArc 2.6.16.