Created
July 17, 2014 21:29
-
-
Save phadej/c26dbe6a32b1600d31db to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module TicTacToe where | |
open import Prelude | |
open import Data.List | |
-- TicTacToe it is! | |
-- There is two players | |
data Player : Set where | |
X O : Player | |
-- And the game goes on 3 × 3 grid | |
Position : Set | |
Position = Fin 3 × Fin 3 | |
-- Fin 3 equality is decidable | |
EqFin3 : Eq (Fin 3) | |
EqFin3 = EqFin | |
-- So is Position | |
EqPosition : Eq Position | |
EqPosition = EqPair {{EqA = EqFin3}} {{EqB = EqFin3}} | |
-- Move is a pair of player and position | |
Move : Set | |
Move = Player × Position | |
-- RawGame is a (unrestricted) list of moves | |
RawGame : Set | |
RawGame = List Move | |
-- To certify our game we start to define semantics | |
-- Game is player in turns and player alterate | |
otherPlayer : Player → Player | |
otherPlayer X = O | |
otherPlayer O = X | |
-- We define a relation is position is already marked | |
_pos∈_ : Position → RawGame → Set | |
p pos∈ ps = Any (λ x → p ≡ snd x) ps | |
-- ... and it's negation | |
_pos∉_ : Position → RawGame → Set | |
p pos∉ ps = ¬ (p pos∈ ps) | |
-- Both relations are decidable! | |
proof : ∀ {p} → ¬ p pos∈ [] | |
proof () | |
dec-pos∈-no : ∀ {p q player state} → ¬ (p ≡ q) → ¬ p pos∈ state → ¬ p pos∈ ((player , q) ∷ state) | |
dec-pos∈-no inn₁ inn₂ (zero pf) = inn₁ pf | |
dec-pos∈-no inn₁ inn₂ (suc pf) = inn₂ pf | |
dec-pos∈-∷ : ∀ {p q player state} → Dec (p ≡ q) → Dec (p pos∈ state) → Dec (p pos∈ ((player , q) ∷ state)) | |
dec-pos∈-∷ (yes refl) _ = yes (zero refl) | |
dec-pos∈-∷ _ (yes pf) = yes (suc pf) | |
dec-pos∈-∷ (no inn₁) (no inn₂) = no (λ pf → dec-pos∈-no inn₁ inn₂ pf) | |
_dec-pos∈_ : (p : Position) → (s : RawGame) → Dec (p pos∈ s) | |
p dec-pos∈ [] = no proof | |
p dec-pos∈ ((player , q) ∷ s) = dec-pos∈-∷ (p == q) (p dec-pos∈ s) | |
_dec-pos∉_ : (p : Position) → (s : RawGame) → Dec (p pos∉ s) | |
p dec-pos∉ s with p dec-pos∈ s | |
p dec-pos∉ s | yes x = no (λ z → z x) | |
p dec-pos∉ s | no x = yes x | |
-- So now we can express well formed game. | |
-- Type which is indexed by raw game state and next player in turn | |
-- So, the game is either | |
-- * empty game, next player is X | |
-- * or for every position player and raw state, such that position is not in state ... | |
-- | |
-- So we get a game which contains only good moves | |
-- | |
-- Exercise: extend it to contain winning condition | |
data Game : RawGame → Player → Set where | |
[] : Game [] X | |
_∷_ : ∀ {position player state} (pf : position pos∉ state) → Game state player → Game ((player , position) ∷ state) (otherPlayer player) | |
-- We will make proof obligation easy by defining proofs by reflection | |
dec-pos∉-fast : (p : Position) → (s : RawGame) → Set | |
dec-pos∉-fast p s with p dec-pos∉ s | |
dec-pos∉-fast p s | yes x = ⊤ | |
dec-pos∉-fast p s | no x = ⊥ | |
solve-position : {p : Position} {s : RawGame} {pf : dec-pos∉-fast p s} → p pos∉ s | |
solve-position {p} {s} {pf} with p dec-pos∉ s | |
solve-position | yes x = x | |
solve-position {pf = pf} | no x = λ _ → pf | |
-- Test solve-position: | |
test : (zero , zero) pos∉ [] | |
test = solve-position | |
-- This doesn't work! | |
-- test2 : (zero , zero) pos∉ ((X , zero , zero) ∷ []) | |
-- test2 = solve-position | |
-- And the DEMO | |
-- Sample game, we play it in types! | |
sampleGame : Game ((_ , zero , zero) ∷ (_ , suc zero , suc zero) ∷ []) _ | |
sampleGame = solve-position ∷ solve-position ∷ [] | |
-- But now we can reason about well formed TicTacToe games! | |
-- Though I don't have any ideas what you can show about it :S | |
gameLength : ∀ {s p} → Game s p → Nat | |
gameLength [] = zero | |
gameLength (pf ∷ g) = suc (gameLength g) | |
-- And eventually we could proof something like: | |
-- though here we should probably use some kind of reflection (again) | |
-- or modify Game to have UniqueList of moves... | |
gameLengthMax9 : ∀ {s p} → (g : Game s p) → LessNat (gameLength g) 9 | |
gameLengthMax9 g = {!!} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment