coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] A non well-founded set

From: Pat Castelnau <dfzone-coq AT yahoo.fr>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] A non well-founded set
Date: Sat, 5 Apr 2008 04:23:13 +0000 (GMT)
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.fr; h=X-YMail-OSG:Received:X-Mailer:Date:From:Reply-To:Subject:To:MIME-Version:Content-Type:Content-Transfer-Encoding:Message-ID; b=FLv5rqjzPYVtZ3dL7txtyVEMRsDDbURTufUh3rURje0dAVPSEwvl8y7T+Pi9x8zyMwTwrFAYNUWa+Q3vmI29k2k46Zm31TEmzwUK0StMfhiIeJuv5imuakW1QozPDGOzHDbhFPN3BZ6o7boY+C+BNywCbEgWu5voK0stgw1ynpw=;
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

How can I define the greatest fixpoint of the following operator F:

  F(X) = { f | for any positive integer n, f(n) is a subset of X }

This definition makes sense in the universe of non well-founded sets (in the
sense of Aczel). In Coq syntax, I thought it might be defined by

  CoInductive T : Type :=
    t : (nat->T->Prop)->T.

This is rejected by Coq:

  Error: Non strictly positive occurrence of "T" in "(nat -> T -> Prop) -> T"

How can I define it in Coq?


_____________________________________________________________________________
Envoyez avec Yahoo! Mail. Une boite mail plus intelligente
http://mail.yahoo.fr

[Coq-Club] A non well-founded set, Pat Castelnau
- Re: [Coq-Club] A non well-founded set, Bruno Barras
- <Possible follow-ups>
- Re: [Coq-Club] A non well-founded set, Pat Castelnau