我正在尝试定义game组合游戏的归纳型。我想要一个比较方法来判断两个游戏是否相同lessOrEq, greatOrEq, lessOrConf or greatOrConf。然后我可以检查两个游戏是否相等（如果它们都是）lessOrEq and greatOrEq.
但是当我尝试定义用于进行此检查的相互递归方法时，我得到：
错误：无法猜测递减参数fix.
我认为这是因为每次递归调用时只有一个游戏或另一个游戏的大小会减小（但不是两者都会减小）。我如何向 Coq 表明这一点？
这是我的代码。失败的部分是相互递归定义gameCompare, innerGCompare, listGameCompare, gameListCompare.
Inductive game : Set :=
| gameCons : gamelist -> gamelist -> game
with gamelist : Set :=
| emptylist : gamelist
| listCons : game -> gamelist -> gamelist.
Definition side :=
game -> gamelist.
Definition leftSide (g : game) : gamelist :=
match g with
| gameCons gll glr => gll
end.
Definition rightSide (g : game) : gamelist :=
match g with
| gameCons gll glr => glr
end.
Inductive compare_quest : Set :=
| lessOrEq : compare_quest
| greatOrEq : compare_quest
| lessOrConf : compare_quest
| greatOrConf : compare_quest.
Definition g1side (c : compare_quest) : side :=
match c with
| lessOrEq => leftSide
| greatOrEq => rightSide
| lessOrConf => rightSide
| greatOrConf => leftSide
end.
Definition g2side (c : compare_quest) : side :=
match c with
| lessOrEq => rightSide
| greatOrEq => leftSide
| lessOrConf => leftSide
| greatOrConf => rightSide
end.
Definition combiner :=
Prop -> Prop -> Prop.
Definition compareCombiner (c : compare_quest) : combiner :=
match c with
| lessOrEq => and
| greatOrEq => and
| lessOrConf => or
| greatOrConf => or
end.
Definition nextCompare (c : compare_quest) : compare_quest :=
match c with
| lessOrEq => lessOrConf
| greatOrEq => greatOrConf
| lessOrConf => lessOrEq
| greatOrConf => greatOrEq
end.
Definition cbn_init (cbn : combiner) : Prop :=
~ (cbn False True).
Fixpoint gameCompare (c : compare_quest) (g1 : game) (g2 : game) : Prop :=
innerGCompare (nextCompare c) (compareCombiner c) g1 (g1side c g1) g2 (g2side c g2)
with innerGCompare (next_c : compare_quest) (cbn : combiner)
(g1 : game) (g1s : gamelist) (g2 : game) (g2s : gamelist) : Prop :=
cbn (listGameCompare next_c cbn g1s g2) (gameListCompare next_c cbn g1 g2s)
with listGameCompare (c : compare_quest) (cbn : combiner) (g1s : gamelist) (g2 : game) : Prop :=
match g1s with
| emptylist => cbn_init cbn
| listCons g1s_car g1s_cdr => cbn (gameCompare c g1s_car g2) (listGameCompare c cbn g1s_cdr g2)
end
with gameListCompare (c : compare_quest) (cbn : combiner) (g1 : game) (g2s : gamelist) : Prop :=
match g2s with
| emptylist => cbn_init cbn
| listCons g2s_car g2s_cdr => cbn (gameCompare c g1 g2s_car) (gameListCompare c cbn g1 g2s_cdr)
end.
Definition game_eq (g1 : game) (g2 : game) : Prop :=
(gameCompare lessOrEq g1 g2) /\ (gameCompare greatOrEq g1 g2).
您可能可以采取多种措施来解决此问题。我无法真正理解您的代码想要做什么，所以也许有比我要提到的更有效的方法。
你可以做的一件事就是定义gameCompare作为（可能是相互的）归纳关系而不是函数。我不知道你对 Coq 有多熟悉，所以我不会详细解释这一点，因为答案会太大，但是在定义诸如以下概念时，归纳关系比函数提供了更大的灵活性gameCompare。有关如何定义归纳关系的更多信息，可以查看Benjamin Pierce的书软件基础.
这种方法的一个缺点是，与函数不同，归纳关系并不真正计算任何东西。这使得它们有时更难使用。特别是，您不能像简化函数调用那样简化归纳命题。
另一种可能更容易应用于您的问题的方法是向函数添加一个“时间”数字参数，该参数随着每次递归调用而减少。这使得函数很容易终止。然后，为了使其工作，您只需确保使用足够大的“时间”参数进行初始调用。以下是如何执行此操作的示例：
Fixpoint gameSize (g : game) : nat :=
match g with
| gameCons gl1 gl2 => 1 + gameListSize gl1 + gameListSize gl2
end
with gameListSize (gl : gamelist) : nat :=
match gl with
| emptylist => 1
| listCons g gl => 1 + gameSize g + gameListSize gl
end.
Definition gameCompareTime (g1 g2 : game) : nat :=
gameSize g1 + gameSize g2.
Fixpoint gameCompareAux (time : nat) (c : compare_quest) (g1 : game) (g2 : game) : Prop :=
match time with
| O => True
| S time =>
compareCombiner c
(listGameCompare time
(nextCompare c)
(compareCombiner c)
(g1side c g1)
g2)
(gameListCompare time
(nextCompare c)
(compareCombiner c)
g1
(g2side c g2))
end
with listGameCompare (time : nat) (c : compare_quest) (cbn : combiner) (g1s : gamelist) (g2 : game) : Prop :=
match time with
| 0 => True
| S time =>
match g1s with
| emptylist => cbn_init cbn
| listCons g1s_car g1s_cdr => cbn (gameCompareAux time c g1s_car g2) (listGameCompare time c cbn g1s_cdr g2)
end
end
with gameListCompare (time : nat) (c : compare_quest) (cbn : combiner) (g1 : game) (g2s : gamelist) : Prop :=
match time with
| 0 => True
| S time =>
match g2s with
| emptylist => cbn_init cbn
| listCons g2s_car g2s_cdr => cbn (gameCompareAux time c g1 g2s_car) (gameListCompare time c cbn g1 g2s_cdr)
end
end.
Definition gameCompare c g1 g2 :=
gameCompareAux (gameCompareTime g1 g2) c g1 g2.
Definition game_eq (g1 : game) (g2 : game) : Prop :=
(gameCompare lessOrEq g1 g2) /\ (gameCompare greatOrEq g1 g2).
The gameCompareTime函数计算两个游戏的大小总和，这似乎是调用树深度的合理界限gameCompareAux。请注意，我已经内联了innerGCompare，因为这使得边界更容易计算。当时间结束时（即模式匹配的 0 分支），我们返回一个任意值（True，在本例中），因为我们将给函数足够的时间让它在到达这种情况之前完成。
这种方法的优点是相对容易实现。缺点是证明任何关于gameCompare需要你推理gameCompareAux并明确终止时间，这可能非常繁琐。
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
