The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

Pat Castelnau wrote:
> 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?


Benjamin Werner wrote a Coq contribution about ZF set theory. See
http://coq.inria.fr/contribs/zermelo-fraenkel.html
He defines (following Aczel's idea) well-founded sets as an inductive type:

Inductive Ens : Type :=
    sup : forall A : Type, (A -> Ens) -> Ens.

Then he defines all set theoretical operators (including the powerset).
It seems that Replacement requires an axiom, but maybe you won't need it.
So, you probably only have to reuse the same definitions, but making Ens
co-inductive. Equality of sets also becomes co-inductive (and also the
proof that it is an equivalence relation), but then set constructors
should be defined in the same way as Benjamin's.

Hope this helps,

Bruno Barras.

PS: if you happen to formalize set theory with anti-foundation axiom,
then it could make a Coq contrib that other people would be happy to reuse.