Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] applying a function definition

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] applying a function definition


chronological Thread 
  • From: Paul Tarau <paul.tarau AT gmail.com>
  • To: brandon_m_moore AT yahoo.com
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] applying a function definition
  • Date: Mon, 27 Jun 2011 13:44:10 -0500
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=subject:mime-version:content-type:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to:x-mailer; b=w9787lAdXsh6rby7onY+gB8t3kD0ImXhcPqxsj0kS2bnuc74HesZF/WfaqnJhqWB2X GgWKfM32rWnQTVI3UoI0IEAZjfmaHtVLCNOsAXh0baAuIDJarQjsMvkl+ehu8I5REiqm MVXqAEpcE3UrAVz8x6iJBeeV41KEauWyBVH00=

Thanks a lot - it does work indeed! And this typo proves that humans and not 
Coq are the usual suspects :-)

The most interesting challenge now is to prove that the borrowedS and 
borrowedP successor/predecessor functions are equivalent to sT and pT. 

I was wondering if anyone has seen papers about taking advantage of the 
presence of a bijection between some trickier data type and "nat" to somewhat 
automate the proof of computations or properties borrowed from "nat" using 
the bijection. Or papers about automation of structural recursion 
requirements in the presence of such a bijection.

Paul

On Jun 27, 2011, at 1:27 PM, 
brandon_m_moore AT yahoo.com
 wrote:

> The code seems to work correctly after replacing
> 
> Definition hdT (a:T) : T :=
> match a with
> | E => E
> | C _ y =>y
> end.
> 
> by
> 
> Definition hdT (a:T) : T :=
> match a with
> | E => E
> | C x _ =>x
> end.





Archive powered by MhonArc 2.6.16.

Top of Page