The Coq mailing list

["Andrew Kent" <andmkent AT indiana.edu>]

I’m trying to represent a theory in Coq which has several mutually dependent
definitions.

Some of the judgments in this theory call for the negation of other properties
on which they depend, which my representation (initially) was going to model
like this:

Inductive A : ... -> Prop :=
... (inductive constructors for A) ...

with B : ... -> Prop :=
... (inductive constructors for B) ...

with C : ... -> Prop :=
...
| c :
        forall x y z,
                B x y ->
                ~ A x y z ->
                C x y z
...

However, this of course is not allowed since the "~ A x y" is a non-strictly
positive occurrence of A and A is still not fully defined at this point in the
program.

I have thought of trying to define an explicit "notA" Prop which attempts to
represent the complement of A... but this seems unideal and makes things even
more complex. Does anyone have any suggestions for how a mutually-dependent
theory which uses negation in this fashion might be best represented in Coq?

Thanks,
Andrew