Last active
September 6, 2024 09:50
-
-
Save clayrat/211d567432c486bfbc334453d492238b to your computer and use it in GitHub Desktop.
Div3DFA
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 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} ⦄ |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment