Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] proof techniques

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] proof techniques


chronological Thread 
  • 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/



Archive powered by MhonArc 2.6.16.

Top of Page