coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Re: Codata: problem with guardedness condition?

From: "Nils Anders Danielsson" <nils.anders.danielsson AT gmail.com>
To: "Samuel Bronson" <naesten AT gmail.com>
Cc: coq-club <coq-club AT pauillac.inria.fr>
Subject: [Coq-Club] Re: Codata: problem with guardedness condition?
Date: Mon, 4 Aug 2008 18:43:32 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:to:subject:cc:in-reply-to:mime-version :content-type:content-transfer-encoding:content-disposition :references; b=lVqkusZAixRlJOrwlXhvdu9n0S1piPHG/7nvl3b+zpNR0FLVzmfHsCA7xrur2NzD6d oqny/3Je/0pBSx5zqzn7v4Pz5oOCesb+UanHPEP/gz9mCd9p29vUDmdt21WFm4c7kY0u f+jax1/a4C1oV8IhN3zh4UrT3utzWMy4Li6k0=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Mon, Jun 30, 2008 at 3:23 PM, Samuel Bronson
<naesten AT gmail.com>
wrote:
>
> I'm trying to implement
> http://conal.net/blog/posts/beautiful-differentiation/ but having
> trouble with the guardedness condition -- at least, that's what I
> think it must be.

Yves noted some ways in which to work around your problem. If you want
to try something more lightweight, but less elegant and more ad-hoc
and monolithic, you can read here:

http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=109

The idea is to make your definition guarded by turning the offending
function (addition) into a constructor of a suitable type.

I have not tried this method in Coq, though, so I don't know if it
will work for you. In particular, I use mixed induction and
coinduction.

--
/NAD

[Coq-Club] Re: Codata: problem with guardedness condition?, Nils Anders Danielsson