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

Question

按照亚瑟的建议,我改变了我的Fixpoint关系,Inductive建立了一种"建立"游戏之间不同比较而不是"向下钻取" 的相互关系.

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

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

我认为错误信息是说我需要所有这些互感定义的相同精确参数.

我意识到有一些简单的黑客来解决这个问题(未使用的虚拟变量,包含所有内容的长函数类型forall),但我不明白为什么我应该这样做.

有人可以解释这种对互感类型的限制背后的逻辑吗？是否有更优雅的方式来写这个？这种限制是否也意味着相互之间的归纳调用必须都使用相同的参数(在这种情况下,我不知道任何黑客可以保存大量的代码重复)？

(所有类型和术语的定义,例如compare_quest,game,g1side等,与我在第一个问题中的定义相同.

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和Right)轮流玩游戏,其中最后一步的玩家获胜.每个游戏(意味着游戏中的每个位置)都可以被视为一组Left选项和一组Right写的选项{G_L | G_R}.:当比较两个游戏,他们可以在任何的四种不同的方式比较<,>,=,或||.

游戏即是A < B,如果B严格优于A对Left,不管谁先走.A > B如果A是优于B对Left.A = B如果这两场比赛是相同的(从某种意义上说,比赛的总和A + -B是零游戏,以便首先输掉比赛的球员).并且,A || B如果哪个游戏更好,Left取决于谁先行.

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

• A <= B如果所有A的Left孩子都是<| B和A <|所有的B孩子一样.

• A <| B如果A有一个合适的孩子这是<= B,或者A <=任何B的留守儿童.

• 而且,同样的>=和>|.

所以,后来通过观察其对这些关系的适用于两场比赛A和B,这是可能的,以确定是否A < B(A<=B和A<|B), A=B(A<=B和A>=B), A > B(A>=B和A>|B),或A || B(A<|B和A>|B).

这是关于CGT的维基文章.

Answer 1

这个限制很有趣，我以前从来没有遇到过。我看不出有任何理由应该拒绝这段代码。我最好的选择是，当人们设计 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因为这可能会导致该类型位于箭头的左侧（负数出现），众所周知，这会导致逻辑不一致。

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

更新：我已经开始写一系列关于在 Coq 中形式化一些 CGT 的文章。您可以在这里找到第一个。