5

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,一般兩名球員(名爲LeftRight )輪流玩一個讓玩家做出最後一招的遊戲,每場比賽(意思是遊戲中的每一個位置)都可以被看作是一組Left的選項和一組Right的選項,寫作{G_L | G_R}。比較兩款遊戲,他們可以用四種不同的方式進行比較:<,>=||

遊戲是A < B如果B嚴格優於ALeft,無論誰先走。 A > B如果A好於B對於LeftA = B如果這兩個遊戲是相同的(在遊戲總和A + -B是一個零遊戲,以便首先失敗的玩家)。並且,A || B如果哪個遊戲更適合Left取決於誰先走。檢查兩場比賽之間的比較

的一種方法如下:

  • A <= B如果所有A的的Left孩子<| BA <|所有B的沒錯兒。

  • A <| B如果A有右孩子是<= B或者A <=任何B的左孩子。和>=>|類似。

因此,然後通過觀察其對這些關係的適用於兩場比賽AB,這是可能的,以確定是否A < BA<=BA<|B),A=BA<=BA>=BA > BA>=BA>|B) ,或A || BA<|BA>|B)。

這是wiki article on CGT

回答

2

這個限制是非常有趣的,我從來沒有遇到過它。我沒有看到爲什麼這段代碼應該被拒絕的原因。我最好的選擇是,當人們設計Coq的基礎時,這個限制使得一些證明更容易,並且由於沒有很多人被它煩惱,它仍然是這樣。儘管如此,我可能完全錯了。我知道參數和參數(即箭頭右側的那些參數和參數)對於某些事物的處理略有不同。例如,定義歸納類型時施加的宇宙約束與參數相比,參數的限制性較小。

也許這應該轉發到Coq俱樂部郵件列表? :)

您不必將所有內容都放在箭頭的右側以使其起作用。你可以做的一件事是把除compare_quest參數之外的所有東西都放在右邊。當你使用你在構造函數中定義相同類型的感應,你給的參數並不一定是一樣的,你給出的報頭中的一個,所以這是確定:

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 (c : compare_quest) : combiner -> side -> side -> 
    game -> game -> Prop := 
| compBoth : forall cbn g1s g2s (g1 g2 : game), 
    cbn (listGameCompare c cbn (g1s g1) g2) 
     (gameListCompare c cbn g1 (g2s g2)) -> 
    innerGCompare c cbn g1s g2s g1 g2 

with listGameCompare (c : compare_quest) : combiner -> gamelist -> game -> Prop := 
| emptylgCompare : forall cbn, cbn_init cbn -> forall g2 : game, listGameCompare c cbn emptylist g2 
| otlgCompare : forall cbn (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) : combiner -> game -> gamelist -> Prop := 
| emptyglCompare : forall cbn, cbn_init cbn -> forall g1 : game, gameListCompare c cbn g1 emptylist 
| otglCompare : forall cbn (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). 

不幸,試圖評價這給了一個新的錯誤:(

Error: Non strictly positive occurrence of "listGameCompare" in 
"forall (cbn : Prop -> Prop -> Prop) (g1s g2s : game -> gamelist) 
    (g1 g2 : game), 
    cbn (listGameCompare c cbn (g1s g1) g2) (gameListCompare c cbn g1 (g2s g2)) -> 
    innerGCompare c cbn g1s g2s g1 g2". 

此錯誤是在勒柯克更爲常見,它是抱怨,你是通過你定義爲參數的類型cbn,因爲這可能導致在類型爲左側的箭頭(否定事件),這已知會導致邏輯i nconsistencies。

認爲您可以通過在最後三種類型的構造函數中內聯compareCombiner來解決此問題,這可能需要重構代碼。再說一次,我很確定必須有更好的方式來定義這一點,但我不明白你要做的很好,所以我的幫助在這裏有所限制。

UPDATE:我已經開始了一系列關於在Coq中正式化CGT的文章。你可以找到第一個here

+0

謝謝,這很好。 我看到了問題,我知道如何擺脫它(雖然不是沒有一些代碼重複)。 我已經添加了對比較兩個CGT遊戲意味着什麼的描述。如果你有任何其他想法。再次感謝 – dspyz

+2

哇,這個CGT的東西真酷!感謝您對此進行更詳細的解釋。我已經發布了一個[gist](https://gist.github.com/arthuraa/5882759)在Coq中開發一些,也許這對你有幫助! –

相關問題