The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

You might want to check if your definitions can be expressed using induction-recursion:

http://en.wikipedia.org/wiki/Induction-recursion_(type_theory)

Basically, you can try to see of the mutual inductive predicates that have to be negated can be defined using recursion, instead of induction.

If you can find a valid inductive-recursive formulation, read further, else ignore the rest of the email.

Unlike Agda, Coq does NOT support induction-recursion.

If you want to stick to Coq, you can follow the following technique to convert you mutually inductive recursive definition to a mutually inductive one in Coq: 

http://www.cs.ru.nl/~venanzio/publications/induction_recursion.ps

Since you are defining the predicates in Prop, you would (most probably) NOT run into universe inconsistency issues during the conversion.

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Tue, May 20, 2014 at 2:51 PM, Andrew Kent <andmkent AT indiana.edu> wrote:

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