为什么coq互感类型必须具有相同的参数？

下列的亚瑟的建议 https://stackoverflow.com/a/17304209/403875，我改变了我的Fixpoint相互关系Inductive这种关系“建立”游戏之间的不同比较，而不是“深入研究”。

但现在我收到一条全新的错误消息：

Error: Parameters should be syntactically the same for each inductive type.

我认为错误消息表明我需要为所有这些互感定义提供相同的精确参数。

我意识到有一些简单的技巧可以解决这个问题（未使用的虚拟变量、包含所有内容的长函数类型）forall），但我不明白为什么我必须这么做。

有人可以解释这种对互感类型的限制背后的逻辑吗？有没有更优雅的方式来写这个？此限制是否还意味着彼此之间的归纳调用必须全部使用相同的参数（在这种情况下，我不知道有任何黑客可以节省大量的代码重复）？

（所有类型和术语的定义，例如compare_quest、game、g1side等，与我的定义相同第一个问题 https://stackoverflow.com/q/17297165/403875.

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 (next_c : compare_quest) (cbn : combiner) (g1s g2s : side)
    : game -> game -> Prop :=
 | compBoth : forall g1 g2 : game,
    cbn (listGameCompare next_c cbn (g1s g1) g2)
        (gameListCompare next_c cbn g1 (g2s g2)) ->
    innerGCompare next_c cbn g1s g2s g1 g2
with listGameCompare (c : compare_quest) (cbn : combiner) : gamelist -> game -> Prop :=
 | emptylgCompare : cbn_init cbn -> forall g2 : game, listGameCompare c cbn emptylist g2
 | otlgCompare : forall (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) (cbn : combiner) : game -> gamelist -> Prop :=
 | emptyglCompare : cbn_init cbn -> forall g1 : game, gameListCompare c cbn g1 emptylist
 | otglCompare : forall (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).

在 CGT 中，通常有两名玩家（名为Left and Right）轮流玩游戏，最后一步的玩家获胜。每个游戏（意味着游戏中的每个位置）都可以被解读为一组Left的选项和一组Right的选项写为{G_L | G_R}。在比较两个游戏时，他们可以通过四种不同方式中的任何一种进行比较：<, >, =, or ||.

一个游戏是A < B if B严格优于A for Left，无论谁先走。A > B if A比B for Left. A = B如果两个游戏是等价的（从某种意义上说，游戏的总和A + -B是零游戏，所以先走的玩家就输了）。和，A || B如果哪个游戏更适合Left取决于谁先走。

检查两个游戏之间的比较的一种方法如下：

• A <= B如果全部A's Left孩子们是<| B and A <| all of B是对的孩子们。

• A <| B if A有一个右孩子是<= B or if A <= any of B留下了孩子。

• 并且，类似地对于>= and >|.

那么，然后看看哪一对这些关系适用于两个游戏A and B，可以判断是否A < B (A<=B and A<|B), A=B (A<=B and A>=B), A > B (A>=B and A>|B), or A || B (A<|B and A>|B).

这是关于 CGT 的维基文章 http://en.wikipedia.org/wiki/Combinatorial_game_theory.

这个限制很有趣，我以前从来没有遇到过。我看不出有任何理由应该拒绝这段代码。我最好的选择是，当人们设计 Coq 的基础时，这种限制使一些证明变得更容易，并且由于没有多少人对此感到恼火，所以它就保持了这种状态。不过，我可能完全错了；我确实知道参数和参数（即指向箭头右侧的参数）在某些方面的处理方式略有不同。例如，与参数相比，定义归纳类型时施加的宇宙约束对参数的限制较少。

也许这应该转发到 Coq Club 邮件列表？ :)

您不必将所有内容都放在箭头右侧即可使其正常工作。你可以做的一件事就是把除了compare_quest右边的参数。当您使用与在构造函数中定义的类型相同的归纳参数时，您给出的参数不必与标头中给出的参数相同，因此没问题：

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).

不幸的是，尝试评估它会产生一个新错误:(

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".

这个错误在 Coq 中更为常见。它抱怨您正在将定义的类型传递给cbn因为这可能会导致该类型成为left箭头（负面事件），已知这会导致逻辑不一致。

I think你可以通过内联来摆脱这个问题compareCombiner在最后三种类型的构造函数中，这可能需要对代码进行一些重构。再说一次，我很确定一定有更好的方法来定义它，但我不明白你想做什么，所以我的帮助在某种程度上是有限的。

UPDATE：我已经开始撰写一系列有关在 Coq 中形式化某些 CGT 的文章。你可以找到第一个here http://poleiro.info/posts/2013-09-08-an-introduction-to-combinatorial-game-theory.html.