私はまだ 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数を返し、th 番目の移動が有効であることを証明し、ゲーム状態ベクトルの th の空の Squareを置き換えます。Squaren < (#ofMoves gs)nmakeMove gs x nn
自分自身とのいくつかの刺激的なゲームの後、私はもっと素晴らしいものを狙うことにしました. 目標は、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、drawまたは のいずれかongoing) 。
s≤s z≤n有効な動き (パーツ)があることを証明したい。suc nn<=であるため、これは可能なはず#ofMoves gsです。Agdaでこれを機能させる方法がわかりません。