This restriction is very interesting, and I had never encountered it before. I don't see any reasons for why this piece of code should be rejected. My best bet is that when people were designing the foundations of Coq this restriction made some of the proofs easier, and since not many people were annoyed by it, it just remained that way. I could be completely wrong, though; I do know that parameters and arguments (i.e., the ones that go to the right of the arrow) are treated slightly differently for some things. For instance, the universe constraints imposed when defining inductive types are less restrictive with parameters when compared to arguments.
Perhaps this should be forwarded to the Coq Club mailing list? :)
You don't have to put everything to the right of the arrow to get this to work. One thing you can do is to put everything but the compare_quest
parameter to the right. When you use an inductive of the same type you're defining in a constructor, the parameter you give doesn't have to be the same as the one you give on the header, so that's OK:
Inductive gameCompare (c : compare_quest) : game -> game -> Prop :=
| igc : forall g1 g2 : game,
innerGCompare (nextCompare c) (compareCombiner c) (g1side c) (g2side c) g1 g2 ->
gameCompare c g1 g2
with innerGCompare (c : compare_quest) : combiner -> side -> side ->
game -> game -> Prop :=
| compBoth : forall cbn g1s g2s (g1 g2 : game),
cbn (listGameCompare c cbn (g1s g1) g2)
(gameListCompare c cbn g1 (g2s g2)) ->
innerGCompare c cbn g1s g2s g1 g2
with listGameCompare (c : compare_quest) : combiner -> gamelist -> game -> Prop :=
| emptylgCompare : forall cbn, cbn_init cbn -> forall g2 : game, listGameCompare c cbn emptylist g2
| otlgCompare : forall cbn (g1_cdr : gamelist) (g1_car g2 : game),
(cbn (listGameCompare c cbn g1_cdr g2) (gameCompare c g1_car g2)) ->
listGameCompare c cbn (listCons g1_car g1_cdr) g2
with gameListCompare (c : compare_quest) : combiner -> game -> gamelist -> Prop :=
| emptyglCompare : forall cbn, cbn_init cbn -> forall g1 : game, gameListCompare c cbn g1 emptylist
| otglCompare : forall cbn (g1 g2_car : game) (g2_cdr : gamelist),
(cbn (gameListCompare c cbn g1 g2_cdr) (gameCompare c g1 g2_car)) ->
gameListCompare c cbn g1 (listCons g2_car g2_cdr).
Unfortunately, trying to evaluate this gives a new error :(
Error: Non strictly positive occurrence of "listGameCompare" in
"forall (cbn : Prop -> Prop -> Prop) (g1s g2s : game -> gamelist)
(g1 g2 : game),
cbn (listGameCompare c cbn (g1s g1) g2) (gameListCompare c cbn g1 (g2s g2)) ->
innerGCompare c cbn g1s g2s g1 g2".
This error is much more common in Coq. It is complaining that you are passing the type you are defining as an argument to cbn
because that could result in that type being to the left of an arrow (a negative occurrence), which is known to lead to logical inconsistencies.
I think you can get rid of this problem by inlining compareCombiner
in the constructors of last three types, which may require some refactoring of your code. Again, I'm pretty sure that there must be a better way of defining this, but I don't understand what you're trying to do very well, so my help is somewhat limited there.
UPDATE: I've started a series of articles about formalizing some of CGT in Coq. You can find the first one here.