Div3DFA

Div3DFA.agda

module Div3DFA where

open import Prelude
open import Data.Bool
open import Data.Nat
open import Data.Nat.Order.Base
open import Data.Nat.DivMod
open import Data.Nat.DivMod.Base
open import Data.List
open import Data.Reflects

-- State

data State : 𝒰 where
  S0 S1 S2 : State
  
_==ˢ_ : State → State → Bool
S0 ==ˢ S0 = true
S1 ==ˢ S1 = true
S2 ==ˢ S2 = true
_ ==ˢ _   = false

module StateCode where
  Code-State : State → State → 𝒰
  Code-State S0 S0 = ⊤
  Code-State S1 S1 = ⊤
  Code-State S2 S2 = ⊤
  Code-State _  _  = ⊥

  code-state-refl : (s : State) → Code-State s s
  code-state-refl S0 = tt
  code-state-refl S1 = tt
  code-state-refl S2 = tt

  encode-state : ∀ {s₁ s₂ : State} → s₁ ＝ s₂ → Code-State s₁ s₂
  encode-state {s₁} e = subst (Code-State s₁) e (code-state-refl s₁)

S0≠S1 : S0 ≠ S1
S0≠S1 = StateCode.encode-state

S0≠S2 : S0 ≠ S2
S0≠S2 = StateCode.encode-state

S1≠S2 : S1 ≠ S2
S1≠S2 = StateCode.encode-state

-- State equality is decidable and its decision procedure is the boolean test
instance 
  Reflects-State : ∀ {s₁ s₂} → Reflects (s₁ ＝ s₂) (s₁ ==ˢ s₂)
  Reflects-State {s₁ = S0} {s₂ = S0} = ofʸ refl
  Reflects-State {s₁ = S0} {s₂ = S1} = ofⁿ S0≠S1
  Reflects-State {s₁ = S0} {s₂ = S2} = ofⁿ S0≠S2
  Reflects-State {s₁ = S1} {s₂ = S0} = ofⁿ (S0≠S1 ∘ _⁻¹)
  Reflects-State {s₁ = S1} {s₂ = S1} = ofʸ refl
  Reflects-State {s₁ = S1} {s₂ = S2} = ofⁿ S1≠S2
  Reflects-State {s₁ = S2} {s₂ = S0} = ofⁿ (S0≠S2 ∘ _⁻¹)
  Reflects-State {s₁ = S2} {s₂ = S1} = ofⁿ (S1≠S2 ∘ _⁻¹)
  Reflects-State {s₁ = S2} {s₂ = S2} = ofʸ refl

-- Token

data Token : 𝒰 where
  Zero One Two Three : Token

-- Automaton

transition : State → Token → State
transition S0 Zero  = S0
transition S0 One   = S1
transition S0 Two   = S2
transition S0 Three = S0
transition S1 Zero  = S1
transition S1 One   = S2
transition S1 Two   = S0
transition S1 Three = S1
transition S2 Zero  = S2
transition S2 One   = S0
transition S2 Two   = S1
transition S2 Three = S2

processTokens : State → List Token → State
processTokens st []       = st
processTokens st (t ∷ ts) = processTokens (transition st t) ts

run : List Token → State
run = processTokens S0

accept : List Token → Bool
accept ts = run ts ==ˢ S0 

-- Semantics

semst : State → ℕ
semst S0 = 0
semst S1 = 1
semst S2 = 2

semtok : Token → ℕ
semtok Zero  = 0
semtok One   = 1
semtok Two   = 2
semtok Three = 3

sumtok : List Token → ℕ 
sumtok []       = 0
sumtok (t ∷ ts) = semtok t + sumtok ts

semst0 : ∀ {s} → semst s ＝ 0 → s ＝ S0
semst0 {s = S0} e = refl
semst0 {s = S1} e = false! e
semst0 {s = S2} e = false! e

semst<3 : ∀ {s} → semst s < 3
semst<3 {s = S0} = z<s
semst<3 {s = S1} = s<s z<s
semst<3 {s = S2} = s<s (s<s z<s)

-- Main proof

predst : State → ℕ → 𝒰
predst s n = semst s ＝ n % 3

opaque
  unfolding _%_
  predst-transition : ∀ {s t}
                    → predst (transition s t) (semtok t + semst s)
  predst-transition {s = S0} {t = Zero}  = refl
  predst-transition {s = S0} {t = One}   = refl
  predst-transition {s = S0} {t = Two}   = refl
  predst-transition {s = S0} {t = Three} = refl
  predst-transition {s = S1} {t = Zero}  = refl
  predst-transition {s = S1} {t = One}   = refl
  predst-transition {s = S1} {t = Two}   = refl
  predst-transition {s = S1} {t = Three} = refl
  predst-transition {s = S2} {t = Zero}  = refl
  predst-transition {s = S2} {t = One}   = refl
  predst-transition {s = S2} {t = Two}   = refl
  predst-transition {s = S2} {t = Three} = refl

predst-processTokens : ∀ {s ts}
                     → predst (processTokens s ts) (sumtok ts + semst s)
predst-processTokens {s} {ts = []}     = m<n⇒m%n≡m (semst s) 3 (semst<3 {s = s}) ⁻¹
predst-processTokens {s} {ts = t ∷ ts} =
    predst-processTokens {s = transition s t} {ts = ts}
  ∙ ap (λ q → (sumtok ts + q) % 3) (predst-transition {s} {t})
  ∙ %-distribˡ-+ (sumtok ts) ((semtok t + semst s) % 3) 3
  ∙ ap (λ q → (((sumtok ts) % 3) + q) % 3) (m%n%n≡m%n (semtok t + semst s) 3)
  ∙ %-distribˡ-+ (sumtok ts) (semtok t + semst s) 3 ⁻¹
  ∙ ap (_% 3) (+-assoc (sumtok ts) (semtok t) (semst s))
  ∙ ap (λ q → (q + semst s) % 3) (+-comm (sumtok ts) (semtok t))

predst-run : ∀ {ts} → predst (run ts) (sumtok ts)
predst-run {ts} = predst-processTokens {s = S0} {ts = ts} ∙ ap (_% 3) (+-zero-r (sumtok ts))

-- The DFA is a decision procedure for the "is the sum of the tokens divisible by 3?" problem
Reflects-accept-divides : ∀ {ts} → Reflects (3 ∣ sumtok ts) (accept ts)
Reflects-accept-divides {ts} =
  dmap (λ e → %=0→∣ (sumtok ts) 3 $ predst-run {ts} ⁻¹ ∙ ap semst e)
       (contra λ d3 → semst0 {s = processTokens S0 ts} $ predst-run {ts} ∙ ∣→%=0 (sumtok ts) 3 d3)
       Reflects-State

-- projecting out individual directions

accept→divides : ∀ {ts} → ⌞ accept ts ⌟ → 3 ∣ sumtok ts
accept→divides {ts} = so→true! ⦃ Reflects-accept-divides {ts} ⦄

divides→accept : ∀ {ts} → 3 ∣ sumtok ts → ⌞ accept ts ⌟
divides→accept {ts} = true→so! ⦃ Reflects-accept-divides {ts} ⦄