Я пытаюсь определить индуктивный тип game для комбинаторных игр. Мне нужен метод сравнения, который показывает, являются ли две игры lessOrEq, greatOrEq, lessOrConf или greatOrConf. Затем я могу проверить, равны ли две игры, если они обе равны lessOrEq и 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).
