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

Question

关注 Arthur's suggestion ，我换了我的Fixpoint相互的关系 Inductive关系“建立”了游戏之间的不同比较，而不是“深入研究”。

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

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

我认为错误消息是说我需要为所有这些互归纳定义提供相同的确切参数。

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

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

(compare_quest、game、g1side 等所有类型和术语的定义与我在 first question 中的定义没有变化。

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 children 是<| B和 A <|全部B是对的 child 。

A <| B如果 A有一个右 child 是 <= B或者如果 A <=任何 B留下了 child 。

并且，对于 >= 也类似和 >| .

那么，通过查看哪一对关系适用于两个游戏 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 )。

这是 wiki article on CGT .

Answer 1

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

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

你不必把所有东西都放在箭头的右边来让它工作。你可以做的一件事就是把除了 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 的文章。您可以找到第一个 here .