Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] From inductive predicates to induction principles

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] From inductive predicates to induction principles


chronological Thread 
  • From: Julien Forest <forest AT ensiie.fr>
  • To: Fr�d�ric Peschanski <Frederic.Peschanski AT lip6.fr>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] From inductive predicates to induction principles
  • Date: Mon, 9 Jun 2008 12:21:49 +0200
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=date:from:to:cc:subject:message-id:in-reply-to:references :organization:x-mailer:mime-version:content-type :content-transfer-encoding:sender; b=Ofz13utzscW2OId7vmg84R0g8kk7BHR+MNlqInFlvqUvSVZdZxFsW+AITwZuFHElrk 649TbE2iLbP9VJYou9lDIoaZxQHC4Iqfyv2halyV96i2f9wQKyV1IkK3IbxIHVGhNeAz d6OY0Ys9yaN3zXlIoEemgQBoXLvqjI7JeJqB8=
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
  • Organization: CNAM
On Mon, 09 Jun 2008 11:00:19 +0200
Frédéric Peschanski 
<Frederic.Peschanski AT lip6.fr>
 wrote:

> Thank you Julien,
> that was exactly what I was looking for.
> 
> You did not make any mistake, only the last element
> of nil is term  (for termination) ;-).
> 
> Is there somewhere a tutorial documentation on functional induction ?
> (cocorico would be a nice place for such a tutorial ...).
> 
> Cheers,
> Frederic.
> 
> 
> Julien Forest a écrit :
> > Dear Frederic, 
> > you can use Function (to create principles) and functionnal induction (to 
> > use them).
> > I've done the proofs using this technique (I needed to define hd, last 
> > and length and 
> > I hope I didn't do any mistake) 
> > (* I hope that this might help you. 
> >    Best regards 
> >    Julien Forest.
> > *)
> >   
Dear Frederic, 
Function is a part of Coq since v8.1. The documentation about it is in the 
standard coq documentation.
J.



Archive powered by MhonArc 2.6.16.

Top of Page