为什么coq互感类型具有相同的参数？ [英] Why must coq mutually inductive types have the same parameters?

问题描述

根据 Arthur的建议，我将我的 Fixpoint 关系更改为

但是，这种关系是建立游戏之间的不同比较的相互现在我收到一个全新的错误消息：

 错误：每个感应类型的参数在句法上应该相同。 
  

我认为错误消息说我需要所有这些互感定义。

我意识到有一些简单的hack来解决这个问题（未使用的虚拟变量，长函数类型， forall ），但我不明白为什么我应该。

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

（所有类型和术语（例如compare_quest，game，g1side等）的定义与其第一个问题。

 感应游戏比较（c：compare_quest）：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  - >游戏 - > 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（g1g2_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  

>和右）轮流玩一个游戏，玩家做最后一步的胜利。每个游戏（意味着游戏中的每个位置）可以被看作一组左的选项和一组右的选项写为 {G_L | G_R} 。当比较两个游戏时，他们可以以四种不同的方式比较：< ，> ， = 或 || 。

游戏 A< B 如果 B 严格优于 A / code>，无论谁先走。 A>如果 比 B code>。 A = B 如果两个游戏是等价的（在游戏的总和 A + -B 零游戏，所以首先失败的玩家）。和， A || B 如果哪个游戏更适合左取决于谁先走。

检查两个游戏之间的比较如下：

• A <= B 如果所有 A 的左子 B 和 A< | 所有 B




• A< | B 如果 A 有一个正确的孩子是< = B c $ c> A <= 任何 B 的左孩子。




• 同样，对于> = 和 code>。




那么，看看哪一对关系适用于两个游戏 code>和 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的wiki文章。

解决方案

这个限制是非常有趣的，我从来没有遇到过。我没有看到为什么这段代码应该被拒绝的任何原因。我最好的打赌是，当人们设计Coq的基础时，这个限制使一些证明更容易，并且由于没有很多人被它恼怒，它只是保持这种方式。我可能完全错了，我知道参数和参数（即，在箭头的右边）被处理略有不同的一些事情。例如，定义归纳类型时所应用的Universe约束与参数相比，对参数的限制较小。

也许这应该转发到Coq俱乐部的邮件列表？ ：）

您不必将所有内容放在箭头右侧即可使用。你可以做的一件事是把除了 compare_quest 参数的所有东西放在右边。当你使用在构造函数中定义的相同类型的归纳类型时，你给出的参数不一定与在头上给出的参数相同，所以没关系：

  Inductive gameCompare（c：compare_quest）：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  - >侧 - >侧 - > 
 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  - >游戏 - > 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  - >游戏 - > gamelist  - > prop：= 
 | emptyglCompare：forall cbn，cbn_init cbn  - > forall g1：game，gameListCompare c cbn g1 emptylist 
 | otglCompare：forall cbn（g1g2_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）。 
  

不幸的是，试图对此进行评估会产生一个新错误：（

 错误：
中的listGameCompare非严格为正的出现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 在最后三种类型的构造函数中，这可能需要一些重构你的代码再次，我很确定必须有一个更好的方式来定义这个，但我不明白

更新：我已经开始了一系列的文章正式化一些CGT在Coq。您可以找到第一个这里 a>。

Following Arthur's suggestion, I changed my Fixpoint relation to a mutual Inductive relation which "builds up" the different comparisons between games rather than "drilling down".

But now I am receiving an entirely new error message:

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

I think the error message is saying that I need the same exact parameters for all of these mutual inductive definitions.

I realize there are simple hacks to get around this (unused dummy variables, long functional types with everything inside the forall), but I don't see why I should have to.

Can somebody explain the logic behind this restriction on mutual inductive types ? Is there a more elegant way to write this ? Does this restriction also imply that the inductive calls to each other must all use the same parameters (in which case I don't know of any hacks save hideous amounts of code duplication) ?

(The definitions of all the types and terms such as compare_quest, game, g1side etc. are unchanged from what they were in my 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).

In CGT, generally two players (named Left and Right) take turns playing a game where the player to make the last move wins. Each game (meaning each position in a game) can be read as a set of Left's options and a set of Right's options written as {G_L | G_R}. When comparing two games, they can compare in any of four different ways: <, >, =, or ||.

A game is A < B if B is strictly better than A for Left, regardless of who goes first. A > B if A is better than B for Left. A = B if the two games are equivalent (in the sense that the sum of games A + -B is a zero-game so that the player who goes first loses). And, A || B if which game is better for Left depends who goes first.

One way to check the comparison between two games is as follows:

• A <= B if all of A's Left children are <| B and A <| all of B's right children.

• A <| B if A has a right child which is <= B or if A <= any of B's left children.

• And, similarly for >= and >|.

So, then by seeing which pair of these relations apply to two games A and B, it's possible to determine whether 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).

Here's the wiki article on CGT.

解决方案

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.

这篇关于为什么coq互感类型具有相同的参数？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！