如何指示两个同系感应类型的大小减小 [英] How to indicate decreasing in size of two coq inductive types

问题描述

我想为组合游戏定义游戏归纳类型。我想要一个比较方法，它告诉两个游戏是lessOrEqgreatOrEqlessOrConfgreatOrConf。然后我可以检查两个游戏是否相等，如果他们都是lessOrEq和greatOrEq。

I'm trying to define the "game" inductive type for combinatorial games. I want a comparison method which tells if two games are "lessOrEq" "greatOrEq" "lessOrConf" "greatOrConf". Then I can check if two games are equal if they are both "lessOrEq" and "greatOrEq".

但是当我尝试定义相互递归的方法进行此检查，我得到：

But when I try defining the mutually recursive methods for making this check, I get:

错误：无法猜测修复的参数减少。

Error: Cannot guess decreasing argument of fix.

我认为这是因为只有一个游戏或其他游戏在每次递归调用（但不是两个）减少。如何向coq指示此内容？

I think this is because only one game or the other decreases in size with each recursive call (but not both). How can I indicate this to coq?

这是我的代码。失败的部分是gameCompare，innerGCompare，listGameCompare，gameListCompare的相互递归定义。

Here's my code. The part that fails is the mutually recursive definition of "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).

推荐答案

问题。我真的不明白你的代码想要做什么，所以也许有更有效的方式来做这件事我要提的。

There are probably several things you can do to solve this problem. I couldn't really understand what your code is trying to do, so maybe there are more efficient ways of doing this than the ones I'm about to mention.

一个你可以做的是将 gameCompare 定义为一个（可能相互）的归纳关系，而不是一个函数。我不知道你是如何熟悉Coq，所以我不会解释这个详细，因为答案会变得太大，但归纳关系给你比函数更大的灵活性定义概念如 gameCompare 。有关如何定义归纳关系的更多信息，您可以查看Benjamin Pierce的书软件基础。

One thing you can do is to define gameCompare as a (possibly mutually) inductive relation instead of a function. I don't know how familiar you are with Coq, so I won't explain this in detail because the answer will get too big, but inductive relations give you much greater flexibility than functions when defining concepts such as gameCompare. For more information on how to define inductive relations, you can check Benjamin Pierce's book Software Foundations.

这种方法的一个缺点是，与函数不同，归纳关系不会真正计算任何东西。这使得他们有时更难使用。特别是，你不能简化归纳式命题，就像你可以简化一个函数调用。

One drawback of this approach is that inductive relations, unlike functions, don't really compute anything. This makes them sometimes harder to use. In particular, you can't simplify an inductive proposition like you can simplify a function call.

另一种可能更容易应用于你的问题的方法是添加每个递归调用减少的函数的时间数字参数。这使得功能简单地终止。然后，为了使它工作，你只需要确保你做一个足够大的时间参数的初始调用。下面是一个如何做到这一点的示例：

Another approach, which might be easier to apply to your problem, is to add a "time" number parameter to your functions that decreases with every recursive call. This makes the functions trivially terminating. Then, to make it work, you just have to make sure that you do your initial call with a big enough "time" parameter. Here's an example of how you can do this:

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).

gameCompareTime 函数计算两个游戏的大小，这似乎是在 gameCompareAux 的调用树的深度上的合理约束。注意，我已经内联 innerGCompare ，因为这使得边界更容易计算。当时间结束时（即模式匹配的0分支），我们返回一个任意值（在这种情况下 True ），

The gameCompareTime function computes the sum of the sizes of both games, which seems like a reasonable bound on the depth of the call tree of gameCompareAux. Notice that I've inlined innerGCompare, since that makes the bound a little bit easier to compute. When the time ends (i.e., the 0 branch on the pattern matching), we return an arbitrary value (True, in this case), because we will have given the function enough time for it to finish before reaching that case.

这种方法的优点是它相对容易实现。缺点是，证明 gameCompare 的任何东西都需要你明确地解释 gameCompareAux 和终止时间，这可以是非常fiddly。

The advantage of this approach is that it is relatively easy to implement. The drawback is that proving anything about gameCompare will require you to reason about gameCompareAux and the termination time explicitly, which can be very fiddly.

这篇关于如何指示两个同系感应类型的大小减小的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！