module Fun where
open import Data.Nat
open import Data.Empty
open import Data.Product
open import Data.Sum
open import Data.List
open import Data.Unit
open import Relation.Binary.PropositionalEquality hiding (inspect; [_])
open import Relation.Nullary
data Direction : Set where
up : Direction
down : Direction
left : Direction
right : Direction
leftOf : Direction → Direction
leftOf up = left
leftOf left = down
leftOf down = right
leftOf right = up
rightOf : Direction → Direction
rightOf up = right
rightOf right = down
rightOf down = left
rightOf left = up
data Color : Set where
red : Color
blue : Color
yellow : Color
green : Color
colorEq? : (x y : Color) → Dec (x ≡ y)
colorEq? green green = yes refl
colorEq? yellow yellow = yes refl
colorEq? blue blue = yes refl
colorEq? red red = yes refl
colorEq? green red = no (λ ())
colorEq? green blue = no (λ ())
colorEq? green yellow = no (λ ())
colorEq? red blue = no (λ ())
colorEq? red green = no (λ ())
colorEq? red yellow = no (λ ())
colorEq? yellow red = no (λ ())
colorEq? yellow green = no (λ ())
colorEq? yellow blue = no (λ ())
colorEq? blue yellow = no (λ ())
colorEq? blue red = no (λ ())
colorEq? blue green = no (λ ())
data Cell : Set where
blank : Cell
accept : Cell
branch : Direction → Color → Color → Cell
path : Direction → Cell
write : Direction → Color → Cell
module GameBoard where
data Row : ℕ → Set where
row-cons : ∀ {n} → Cell → Row n → Row (suc n)
row-nil : Row zero
data GameBoard (w : ℕ) : ℕ → Set where
game : GameBoard w (zero)
_∥_ : ∀ {h} → GameBoard w h → Row w → GameBoard w (suc h)
∣ = row-nil
▢_ = λ {n} → row-cons {n} blank
a_ = λ {n} → row-cons {n} accept
⇑_ = λ {n} → row-cons {n} (path up)
⇓_ = λ {n} → row-cons {n} (path down)
⇐_ = λ {n} → row-cons {n} (path left)
⇒_ = λ {n} → row-cons {n} (path right)
infixl 2 _∥_
getR : ∀ {w} → Row w → ℕ → Cell
getR (row-nil) v = blank
getR (row-cons c r) zero = c
getR (row-cons c r) (suc n) = getR r n
get : ∀ {n m} → GameBoard n m → ℕ → ℕ → Cell
get game x n = blank
get (bd ∥ r) x zero = getR r x
get (bd ∥ r) x (suc n) = get bd x n
module State where
Tape : Set
Tape = List Color
data RobotState : Set where
state : ℕ → ℕ → Tape → RobotState
accept : RobotState
reject : RobotState
moveState : Direction → RobotState → RobotState
moveState _ reject = reject
moveState _ accept = accept
moveState down (state x (suc n) t) = state x n t
moveState down (state x zero t) = reject
moveState left (state (suc n) y t) = state n y t
moveState left (state zero y t) = reject
moveState up (state x y t) = state x (suc y) t
moveState right (state x y t) = state (suc x) y t
open GameBoard
open State
module Game {n m : ℕ}(g : GameBoard n m) where
δ : RobotState → RobotState
δ accept = accept
δ reject = reject
δ (state x y t) with get g x y
δ (state x y t) | blank = reject
δ (state x y t) | accept = accept
δ (state x y t) | path d = moveState d (state x y t)
δ (state x y []) | (branch d l r) = moveState d (state x y [])
δ (state x y (h ∷ t)) | (branch d l r) with colorEq? h l
... | yes p = moveState (leftOf d) (state x y t)
... | no p with colorEq? h r
... | yes p' = moveState (rightOf d) (state x y t)
... | no p' = moveState d (state x y t)
δ (state x y t) | (write d c) = moveState d (state x y (t ++ [ c ]))
δ⟨_⟩ : ℕ → RobotState → RobotState
δ⟨ zero ⟩ s = s
δ⟨ suc n ⟩ s = δ⟨ n ⟩ (δ s)
module LTL where
StatePred : Set₁
StatePred = RobotState → Set
withY : (ℕ → Set) → StatePred
withY p (state x y t) = p y
withY _ _ = ⊥
withX : (ℕ → Set) → StatePred
withX p (state x y t) = p x
withX _ _ = ⊥
withTape : (Tape → Set) → StatePred
withTape p (state x y t) = p t
withTape _ _ = ⊥
◯_ : StatePred → StatePred
◯_ p s = p (δ s)
_u_ : StatePred → StatePred → StatePred
_u_ p₁ p₂ s = Σ[ n ∶ ℕ ] ( (∀ {x : ℕ}{t : x < n} → p₁ (δ⟨ x ⟩ s)) × (p₂ (δ⟨ n ⟩ s)))
⋄_ : StatePred → StatePred
⋄_ p s = Σ[ n ∶ ℕ ] p (δ⟨ n ⟩ s)
□_ : StatePred → StatePred
□_ p s = ∀ {n : ℕ} → p (δ⟨ n ⟩ s)
_∧_ : StatePred → StatePred → StatePred
(p₁ ∧ p₂) s = (p₁ s × p₂ s)
_∨_ : StatePred → StatePred → StatePred
(p₁ ∨ p₂) s = (p₁ s ⊎ p₂ s)
not_ : StatePred → StatePred
not_ p s = ¬ (p s)
_⟶_ : StatePred → StatePred → StatePred
(p₁ ⟶ p₂) s = p₁ s → p₂ s
infixr 6 _⟶_
inBoard : StatePred
inBoard = withY (λ y → y < m) ∧ withX (λ x → x < n)
accepts : StatePred
accepts = _≡_ accept
rejects : StatePred
rejects = _≡_ reject
open LTL public
allStartStates : StatePred → Set
allStartStates p = ∀ {x y} {t} → p (state x y t)
module Example1 where
testBoard : GameBoard 3 3
testBoard = game ∥ ▢ ▢ ▢ ∣
∥ ▢ ▢ ▢ ∣
∥ ▢ ▢ ▢ ∣
open Game (testBoard)
row-blank : ∀ {x} → getR (▢ ▢ ▢ ∣) x ≡ blank
row-blank {0} = refl
row-blank {1} = refl
row-blank {2} = refl
row-blank {suc (suc (suc n))} = refl
board-blank : ∀ {x y} → get testBoard x y ≡ blank
board-blank {x} {suc (suc (suc n))} = refl
board-blank {x} {2} = row-blank {x}
board-blank {x} {1} = row-blank {x}
board-blank {x} {0} = row-blank {x}
one-step-reject : ∀ {x y : ℕ} {t : Tape} → δ (state x y t) ≡ reject
one-step-reject {x} {y} {t} rewrite board-blank {x} {y} = refl
simpleProof : allStartStates (⋄ rejects)
simpleProof {x} {y} {t} = 1 , sym( one-step-reject {x}{y}{t})
module Example2 where
testBoard : GameBoard 3 3
testBoard = game ∥ ▢ ⇓ ▢ ∣
∥ ▢ ⇓ ▢ ∣
∥ ▢ a ▢ ∣
open Game (testBoard)
accepts-prf : allStartStates (withX (_≡_ 1) ∧ withY (λ y → y < 3) ⟶ ⋄ accepts)
accepts-prf {y = 0} (refl , _) = 1 , refl
accepts-prf {y = 1} (refl , _) = 2 , refl
accepts-prf {y = 2} (refl , _) = 3 , refl
accepts-prf {y = suc (suc (suc n))} (refl , s≤s (s≤s (s≤s ())))