5

在Arthur 的建议下，我将我的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 < BifB绝对比Afor好Left，不管谁先走。A > BifA比Bfor好Left。A = B如果两个游戏是等价的（从某种意义上说，游戏的总和A + -B是零游戏，所以先走的玩家输了）。而且，A || B如果哪个游戏更适合Left取决于谁先走。

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

  • A <= B如果所有A的Left孩子都是<| B并且A <|所有的孩子都是B正确的孩子。

  • A <| BifA有一个右孩子，<= B或者如果A <=有任何一个B左孩子。

  • 并且，同样对于>=和>|。

因此，然后通过查看这对关系中的哪一对适用于两个游戏Aand B，可以确定是A < B( A<=Band A<|B)、A=B( A<=Band A>=B)、A > B( A>=Band A>|B) 还是A || B( A<|Band A>|B)。

这是关于 CGT 的 wiki 文章。

4

1 回答 1

2

这个限制很有趣，我以前从未遇到过。我看不出应该拒绝这段代码的任何原因。我最好的选择是，当人们设计 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 的文章。你可以在这里找到第一个。

于 2013-06-26T15:50:49.813 回答