Skip to content

Instantly share code, notes, and snippets.

@phadej
Created July 17, 2014 21:29
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save phadej/c26dbe6a32b1600d31db to your computer and use it in GitHub Desktop.
Save phadej/c26dbe6a32b1600d31db to your computer and use it in GitHub Desktop.
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