繼Arthur's suggestion之後,我改變了我的Fixpoint
關係,這個關係是「建立」遊戲之間的不同比較而不是「鑽取」的相互關係Inductive
。爲什麼coq互感類型具有相同的參數?
但現在我接受了一個全新的錯誤消息:
Error: Parameters should be syntactically the same for each inductive type.
我認爲錯誤消息是說,我需要所有這些互感的定義完全相同的參數。
我知道有一些簡單的黑客可以解決這個問題(未使用的虛擬變量,包含forall
中的所有內容的長功能類型),但我不明白爲什麼我必須這樣做。
有人可以解釋這種限制在互感類型背後的邏輯嗎?有沒有更優雅的寫法呢?這個限制是否也意味着彼此的歸納調用都必須使用相同的參數(在這種情況下,我不知道任何黑客是否可以省去大量代碼重複)?
(所有類型和諸如compare_quest,遊戲,g1side等的定義是從什麼人在我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).
在CGT,一般兩名球員(名爲Left
和Right
)輪流玩一個讓玩家做出最後一招的遊戲,每場比賽(意思是遊戲中的每一個位置)都可以被看作是一組Left
的選項和一組Right
的選項,寫作{G_L | G_R}
。比較兩款遊戲,他們可以用四種不同的方式進行比較:<
,>
,=
或||
。
遊戲是A < B
如果B
嚴格優於A
的Left
,無論誰先走。 A > B
如果A
好於B
對於Left
。 A = B
如果這兩個遊戲是相同的(在遊戲總和A + -B
是一個零遊戲,以便首先失敗的玩家)。並且,A || B
如果哪個遊戲更適合Left
取決於誰先走。檢查兩場比賽之間的比較
的一種方法如下:
A <= B
如果所有A
的的Left
孩子<| 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
(A>=B
和A>|B
) ,或A || B
(A<|B
和A>|B
)。
謝謝,這很好。 我看到了問題,我知道如何擺脫它(雖然不是沒有一些代碼重複)。 我已經添加了對比較兩個CGT遊戲意味着什麼的描述。如果你有任何其他想法。再次感謝 – dspyz
哇,這個CGT的東西真酷!感謝您對此進行更詳細的解釋。我已經發布了一個[gist](https://gist.github.com/arthuraa/5882759)在Coq中開發一些,也許這對你有幫助! –