4

我仍在尝试围绕 agda 进行思考，所以我写了一个小井字游戏类型

data Game : Player -> Vec Square 9 -> Set where
 start : Game x ( - ∷ - ∷ - ∷
                  - ∷ - ∷ - ∷
                  - ∷ - ∷ - ∷ [] )
 xturn : {gs : Vec Square 9} -> (n : ℕ) -> Game x gs -> n < (#ofMoves gs) -> Game o (makeMove gs x n )
 oturn : {gs : Vec Square 9} -> (n : ℕ) -> Game o gs -> n < (#ofMoves gs) -> Game x (makeMove gs o n )

这将拥有一个有效的游戏路径。

这里#ofMoves gs将返回空Squares 的数量， n < (#ofMoves gs)将证明n第 th 步是有效的，并makeMove gs x n替换n游戏状态向量中的第 th 个空 Square。

在与自己进行了几场刺激的比赛之后，我决定拍摄更棒的东西。目标是创建一个函数，让 x 玩家和 o 玩家在史诗般的生死战中相互对抗。

--two programs enter, one program leaves
gameMaster : {p : Player } -> {gs : Vec Square 9} --FOR ALL
 -> ({gs : Vec Square 9} -> Game x gs -> (0 < (#ofMoves gs)) -> Game o (makeMove gs x _ )) --take an x player
 -> ({gs : Vec Square 9} -> Game o gs -> (0 < (#ofMoves gs)) -> Game x (makeMove gs o _ )) --take an o player
 -> ( Game p gs)  --Take an initial configuration
 -> GameCondition --return a winner
gameMaster {_} {gs} _ _ game with (gameCondition gs)
... | xWin = xWin
... | oWin = oWin
... | draw = draw
... | ongoing  with #ofMoves gs
... | 0 = draw --TODO: really just prove this state doesn't exist, it will always be covered by gameCondition gs = draw
gameMaster {x} {gs} fx fo game | ongoing | suc nn = gameMaster (fx) (fo) (fx game (s≤s z≤n)) -- x move
gameMaster {o} {gs} fx fo game | ongoing | suc nn = gameMaster (fx) (fo) (fo game (s≤s z≤n)) -- o move

这(0 < (#ofMoves gs))是游戏正在进行的证明的“速记”， 将返回您所期望的游戏状态gameCondition gs（之一xWin，，，或oWin）drawongoing

我想证明有有效的动作（s≤s z≤n部分）。这应该是可能的，因为suc nn<= #ofMoves gs。我不知道如何在 agda 中完成这项工作。

4

2 回答 2

9
于 2013-08-28T17:22:08.643 回答
3

我认为您正在寻找一种名为“检查”或“检查类固醇”的 Agda 技术。它允许您获得从 with 模式匹配中学到的知识的等式证明。我建议您阅读以下邮件中的代码并尝试了解它是如何工作的。关注底部的函数 foo 如何需要记住“fx = z”，并通过在“inspect (hide fx)”和“f x”上进行匹配来做到这一点：

https://lists.chalmers.se/pipermail/agda/2011/003286.html

要在实际代码中使用它，我建议您从 Agda 标准库中导入 Relation.Binary.PropositionalEquality 并使用其版本的检查（表面上与上面的代码不同）。它具有以下示例代码：

f x y with g x | inspect g x
f x y | c z | [ eq ] = ...

注意：“检查类固醇”是检查成语中旧方法的更新版本。

我希望这有帮助...

于 2013-08-28T05:32:07.300 回答