2

我正在尝试game为组合游戏定义归纳类型。我想要一个比较方法来判断两个游戏是lessOrEq、greatOrEq还是。然后我可以检查两个游戏是否相等，如果它们都是和。lessOrConfgreatOrConflessOrEqgreatOrEq

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

错误：无法猜测 的递减参数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).
4

2 回答 2

3

您可能可以做几件事来解决这个问题。我无法真正理解您的代码试图做什么，所以也许有比我要提到的更有效的方法来做到这一点。

您可以做的一件事是定义gameCompare为​​（可能是相互的）归纳关系而不是函数。我不知道你对 Coq 有多熟悉，所以我不会详细解释这一点，因为答案会变得太大，但是在定义诸如gameCompare. 有关如何定义归纳关系的更多信息，您可以查看 Benjamin Pierce 的书Software Foundations。

这种方法的一个缺点是，与函数不同，归纳关系并不真正计算任何东西。这使得它们有时更难使用。特别是，您不能像简化函数调用那样简化归纳命题。

另一种可能更容易应用于您的问题的方法是向您的函数添加一个“时间”数字参数，该参数随着每次递归调用而减少。这使得函数可以简单地终止。然后，要使其工作，您只需确保使用足够大的“时间”参数进行初始调用。这是一个如何执行此操作的示例：

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。请注意，我已经 inlined innerGCompare，因为这使得边界更容易计算。当时间结束时（即模式匹配的 0 分支），我们返回一个任意值（True在本例中为 ），因为我们将给函数足够的时间让它在到达该情况之前完成。

这种方法的优点是相对容易实现。缺点是证明任何事情gameCompare都需要你明确地推理gameCompareAux和终止时间，这可能非常繁琐。

于 2013-06-25T17:52:57.383 回答
1

指示函数递减参数的一种方法是使用描述该函数域的临时谓词。

Inductive gameCompareDom : compare_quest ->  game -> game -> Prop :=
  | gameCompareDom1 : forall c g1 g2, innerGCompareDom (nextCompare c) (compareCombiner c) g1 (g1side c g1) g2 (g2side c g2) -> gameCompareDom c g1 g2

with innerGCompareDom : compare_quest -> combiner -> game -> gamelist -> game -> gamelist -> Prop :=
  | innerGCompareDom1 : forall next_c cbn g1 g1s g2 g2s, listGameCompareDom next_c cbn g1s g2 -> gameListCompareDom next_c cbn g1 g2s -> innerGCompareDom next_c cbn g1 g1s g2 g2s

with listGameCompareDom : compare_quest -> combiner -> gamelist -> game -> Prop :=
  | listGameCompareDom1 : forall c cbn g1s g2, g1s = emptylist -> listGameCompareDom c cbn g1s g2
  | listGameCompareDom2 : forall c cbn g1s g2 g1s_car g1s_cdr, g1s = listCons g1s_car g1s_cdr -> gameCompareDom c g1s_car g2 -> listGameCompareDom c cbn g1s_cdr g2 -> listGameCompareDom c cbn g1s g2

with gameListCompareDom : compare_quest -> combiner -> game -> gamelist -> Prop :=
  | gameListCompareDom1 : forall c cbn g1 g2s, g2s = emptylist -> gameListCompareDom c cbn g1 g2s
  | gameListCompareDom2 : forall c cbn g1 g2s g2s_car g2s_cdr, g2s = listCons g2s_car g2s_cdr -> gameCompareDom c g1 g2s_car -> gameListCompareDom c cbn g1 g2s_cdr -> gameListCompareDom c cbn g1 g2s.

有了一些反演引理和证明你的函数是完全的，你可以像这样定义函数：

Lemma gameCompareDom1Inv : forall c g1 g2, gameCompareDom c g1 g2 ->
  innerGCompareDom (nextCompare c) (compareCombiner c) g1 (g1side c g1) g2 (g2side c g2).

Lemma innerGCompareDom1Inv1 : forall next_c cbn g1 g1s g2 g2s,
  innerGCompareDom next_c cbn g1 g1s g2 g2s ->
  listGameCompareDom next_c cbn g1s g2.

Lemma innerGCompareDom1Inv2 : forall next_c cbn g1 g1s g2 g2s,
  innerGCompareDom next_c cbn g1 g1s g2 g2s ->
  gameListCompareDom next_c cbn g1 g2s.

Lemma listGameCompareDom2Inv1 : forall c cbn g1s g2 g1s_car g1s_cdr,
  listGameCompareDom c cbn g1s g2 -> g1s = listCons g1s_car g1s_cdr ->
  gameCompareDom c g1s_car g2.

Lemma listGameCompareDom2Inv2 : forall c cbn g1s g2 g1s_car g1s_cdr,
  listGameCompareDom c cbn g1s g2 -> g1s = listCons g1s_car g1s_cdr ->
  listGameCompareDom c cbn g1s_cdr g2.

Lemma gameListCompareDom2Inv1 : forall c cbn g1 g2s g2s_car g2s_cdr,
  gameListCompareDom c cbn g1 g2s -> g2s = listCons g2s_car g2s_cdr ->
  gameCompareDom c g1 g2s_car.

Lemma gameListCompareDom2Inv2 : forall c cbn g1 g2s g2s_car g2s_cdr,
  gameListCompareDom c cbn g1 g2s -> g2s = listCons g2s_car g2s_cdr ->
  gameListCompareDom c cbn g1 g2s_cdr.

Fixpoint gameCompareAux (c : compare_quest) (g1 : game) (g2 : game) (H1 : gameCompareDom c g1 g2) : Prop :=
  innerGCompareAux (nextCompare c) (compareCombiner c) g1 (g1side c g1) g2 (g2side c g2) (gameCompareDom1Inv _ _ _ H1)

with innerGCompareAux (next_c : compare_quest) (cbn : combiner) (g1 : game) (g1s : gamelist) (g2 : game) (g2s : gamelist) (H1 : innerGCompareDom next_c cbn g1 g1s g2 g2s) : Prop :=
  cbn (listGameCompareAux next_c cbn g1s g2 (innerGCompareDom1Inv1 _ _ _ _ _ _ H1)) (gameListCompareAux next_c cbn g1 g2s (innerGCompareDom1Inv2 _ _ _ _ _ _ H1))

with listGameCompareAux (c : compare_quest) (cbn : combiner) (g1s : gamelist) (g2 : game) (H1 : listGameCompareDom c cbn g1s g2) : Prop :=
  match g1s as gl1 return g1s = gl1 -> Prop with
  | emptylist                => fun H2 => cbn_init cbn
  | listCons g1s_car g1s_cdr => fun H2 => cbn (gameCompareAux c g1s_car g2 (listGameCompareDom2Inv1 _ _ _ _ _ _ H1 H2)) (listGameCompareAux c cbn g1s_cdr g2 (listGameCompareDom2Inv2 _ _ _ _ _ _ H1 H2))
  end eq_refl

with gameListCompareAux (c : compare_quest) (cbn : combiner) (g1 : game) (g2s : gamelist) (H1 : gameListCompareDom c cbn g1 g2s) : Prop :=
  match g2s as gl1 return g2s = gl1 -> Prop with
  | emptylist                => fun H2 => cbn_init cbn
  | listCons g2s_car g2s_cdr => fun H2 => cbn (gameCompareAux c g1 g2s_car (gameListCompareDom2Inv1 _ _ _ _ _ _ H1 H2)) (gameListCompareAux c cbn g1 g2s_cdr (gameListCompareDom2Inv2 _ _ _ _ _ _ H1 H2))
  end eq_refl.

Lemma gameCompareTot : forall c g1 g2, gameCompareDom c g1 g2.

Lemma innerGCompareTot : forall next_c cbn g1 g1s g2 g2s,
  innerGCompareDom next_c cbn g1 g1s g2 g2s.

Lemma listGameCompareTot : forall g2 g1s c cbn,
  listGameCompareDom c cbn g1s g2.

Lemma gameListCompareTot : forall g1 g2s c cbn,
  gameListCompareDom c cbn g1 g2s.

Definition gameCompare (c : compare_quest) (g1 : game) (g2 : game) : Prop :=
  gameCompareAux c g1 g2 (gameCompareTot _ _ _).

Definition innerGCompare (next_c : compare_quest) (cbn : combiner) (g1 : game) (g1s : gamelist) (g2 : game) (g2s : gamelist) : Prop :=
  innerGCompareAux next_c cbn g1 g1s g2 g2s (innerGCompareTot _ _ _ _ _ _).

Definition listGameCompare (c : compare_quest) (cbn : combiner) (g1s : gamelist) (g2 : game) : Prop :=
  listGameCompareAux c cbn g1s g2 (listGameCompareTot _ _ _ _).

Definition gameListCompare (c : compare_quest) (cbn : combiner) (g1 : game) (g2s : gamelist) : Prop :=
  gameListCompareAux c cbn g1 g2s (gameListCompareTot _ _ _ _).

反演引理的证明必须以Defined.代替结尾，Qed.以便它们的内容是透明的并且可用于计算。他们也不能引用任何不透明的定理。

之后，您应该能够通过诉诸证明无关公理来定义以下等式引理：

Lemma gameCompareEq : forall c g1 g2, gameCompare c g1 g2 =
  innerGCompare (nextCompare c) (compareCombiner c) g1 (g1side c g1) g2 (g2side c g2).

Lemma innerGCompareEq : forall next_c cbn g1 g1s g2 g2s, innerGCompare next_c cbn g1 g1s g2 g2s =
  cbn (listGameCompare next_c cbn g1s g2) (gameListCompare next_c cbn g1 g2s).

Lemma listGameCompareEq : forall c cbn g1s g2, listGameCompare c cbn g1s g2 =
  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.

Lemma gameListCompareEq : forall c cbn g1 g2s, gameListCompare c cbn g1 g2s =
  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.

您可以Extraction Inline在辅助功能上使用，以便您的主要功能在提取时看起来像您期望的那样。但这不适用于这里，因为您的函数返回Props 而不是bools。

在这里全面发展。

于 2013-07-16T14:08:28.317 回答