Automata and finite types in agda

Decidable.agda

module Decidable where

open import Agda.Builtin.Equality public

data ⊥ : Set where

¬_ : (A : Set) → Set
¬ A = A → ⊥

⊥-elim : {A : Set} → ⊥ → A
⊥-elim ()

_≢_ : {A : Set} → A → A → Set
x ≢ y = ¬(x ≡ y)

infix 0 ¬_
infix 1 _≢_

data Dec (A : Set) : Set where
  yes :   A → Dec A
  no  : ¬ A → Dec A

Pred : Set → Set₁
Pred A = A → Set

Decidable : {A : Set} → Pred A → Set
Decidable P = ∀ x → Dec (P x)

Decidable≡ : Set → Set
Decidable≡ A = (x y : A) → Dec (x ≡ y)

Dfa.agda

module Dfa where

open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.Sigma renaming (Σ to ∃)

open import Decidable
open import List

open import Finite

-- We actually allow an infinite alphabet

record Dfa (n : ℕ) (Σ : Set) : Set where
  constructor dfa
  field
    δ  : Fin n → Σ → Fin n
    q₀ : Fin n
    fs : List (Fin n)

  δ* : Fin n → List Σ → Fin n
  δ* q [] = q
  δ* q (x ∷ xs) = δ* (δ q x) xs

  accepts : List Σ → Set
  accepts xs = δ* q₀ xs ∈ fs

  accepts? : (xs : List Σ) → Dec (accepts xs)
  accepts? xs = decide∈ _F≟_ (δ* q₀ xs) fs

open Dfa using (accepts; accepts?)


private
  ∣_∣ : {A : Set} → List A → ℕ
  ∣ [] ∣ = zero
  ∣ x ∷ xs ∣ = suc ∣ xs ∣

  _^_ : {A : Set} → List A → ℕ → List A
  xs ^ zero = []
  xs ^ suc n = xs ++ (xs ^ n)

  data _≤_ : ℕ → ℕ → Set where
    z≤n : ∀{n}           → zero  ≤ n
    s≤s : ∀{m n} → m ≤ n → suc m ≤ suc n

record Pump {n : ℕ} {Σ : Set} (m : Dfa n Σ) (w : List Σ) (p : ℕ) : Set where
  constructor pump
  field
    x y z       : List Σ
    xyz≡w       : x ++ y ++ z ≡ w
    y-not-empty : y ≢ []
    ∣xy∣<p      : ∣ x ++ y ∣ ≤ p
    membership  : ∀ k → accepts m (x ++ (y ^ k) ++ z)

record Loop {n Σ} (m : Dfa n Σ) : Set where
  constructor loop
  field
    q     : Fin n
    σs    : List Σ
    loops : (Dfa.δ* m q σs) ≡ q

pidgeon : ∀{n Σ} → (m : Dfa n Σ) → (xs : List Σ) → n ≤ ∣ xs ∣ → accepts m xs → Loop m
pidgeon {zero} (dfa δ q₀ .(_ ∷ _)) xs x [ x₂ ] = {!   !}
pidgeon {zero} (dfa δ q₀ .(x₁ ∷ _)) xs x (x₁ ∷ acc) = {!   !}
pidgeon {suc n} m xs x acc = {!   !}

--pumping : ∀{n Σ} → (m : Dfa n Σ) → ∃ ℕ (λ p → ∀ w → p ≤ ∣ w ∣ → Pump m w p)
--fst (pumping {n} m) = n
--Pump.x (snd (pumping m) w n≤∣w∣) = {!   !}
--Pump.y (snd (pumping m) w n≤∣w∣) = {!   !}
--Pump.z (snd (pumping m) w n≤∣w∣) = {!   !}
--Pump.xyz≡w (snd (pumping m) w n≤∣w∣) = {!   !}
--Pump.y-not-empty (snd (pumping m) w n≤∣w∣) = {!   !}
--Pump.∣xy∣<p (snd (pumping m) w n≤∣w∣) = {!   !}
--Pump.membership (snd (pumping m) w n≤∣w∣) = {!   !}
--
--

Finite.agda

module Finite where

open import Agda.Builtin.Equality
open import Agda.Builtin.Nat renaming (Nat to ℕ) hiding (_+_ ; _<_)
open import Agda.Builtin.Sigma

open import Decidable

postulate ≡sym : {A : Set} {x y : A} → x ≡ y → y ≡ x
postulate ≡trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z

data Inspect {A : Set} (x : A) : Set where
  _with≡_ : ∀ y → x ≡ y → Inspect x

inspect : {A : Set} → (x : A) → Inspect x
inspect x = x with≡ refl

infixr 4 _×_
_×_ : Set → Set → Set
A × B = Σ A λ _ → B

Injective : {A B : Set} → (A → B) → Set
Injective {A} {B} f = {x y : A} → f x ≡ f y → x ≡ y

record Isom (A B : Set) : Set where
  constructor isom
  field
    morph : A → B
    inj   : Injective morph
    sur   : ∀ y → Σ A (λ x → morph x ≡ y)
open Isom

data Fin : ℕ → Set where
  fzero : ∀{n} → Fin (suc n)
  fsuc  : ∀{n} → Fin n → Fin (suc n)

record IsFinite (A : Set) : Set where
  field
    ∣_∣ : ℕ
    index : Isom A (Fin ∣_∣)
open IsFinite

record Collision {A B : Set} (f : A → B) : Set where
  field
    x y : A
    distinct : x ≢ y
    collide  : f x ≡ f y

¬Inj→Col : {n m : ℕ} → (f : (Fin n) → (Fin m)) → ¬(Injective f) → Collision f
¬Inj→Col f ¬inj = {!   !}

Any : ∀{n m} → (P : Fin m → Set) → (f : Fin n → Fin m) → Set
Any {n} P f = Σ (Fin n) (λ x → P (f x))

any : ∀{n m} {P : Fin m → Set} → (p : Decidable P) → (f : Fin n → Fin m) → Dec (Any P f)
any {zero} p f = no φ
                 where
                   φ : _
                   φ (() , _)
any {suc n} p f with p (f fzero)
...             | yes Px = yes (fzero , Px)
...             | no ¬Px with any {n} p λ x → f (fsuc x)
...                      | yes (x , Psx) = yes (fsuc x , Psx)
...                      | no ¬any       = no φ
                                           where
                                             φ : _
                                             φ (fzero  , Px) = ¬Px Px
                                             φ (fsuc x , Px) = ¬any (x , Px)

-- Finite types have a decidable equality

infix 3 _F≟_
_F≟_ : ∀{n} → Decidable≡ (Fin n)
fzero F≟ fzero = yes refl
fzero F≟ fsuc y = no (λ ())
fsuc x F≟ fzero = no (λ ())
fsuc x F≟ fsuc y  with x F≟ y
fsuc x F≟ fsuc y | yes refl = yes refl
fsuc x F≟ fsuc y | no neq = no φ where φ : _
                                       φ refl = neq refl

finiteEq : ∀{A} → IsFinite A → Decidable≡ A
finiteEq {A} finA x y with (morph (index finA) x) F≟ (morph (index finA) y)
finiteEq {A} finA x y | yes eq = yes (inj (index finA) eq)
finiteEq {A} finA x y | no neq = no φ where φ : _
                                            φ refl = neq refl

-- Example : Bool is finite

private
  data Bool : Set where
    false : Bool
    true  : Bool

  Bool≈Fin2 : Isom Bool (Fin 2)
  morph Bool≈Fin2 false = fzero
  morph Bool≈Fin2 true = fsuc fzero
  inj Bool≈Fin2 {false} {false} refl = refl
  inj Bool≈Fin2 {false} {true} ()
  inj Bool≈Fin2 {true} {false} ()
  inj Bool≈Fin2 {true} {true} refl = refl
  sur Bool≈Fin2 fzero = false , refl
  sur Bool≈Fin2 (fsuc fzero) = true , refl
  sur Bool≈Fin2 (fsuc (fsuc ()))

  boolFinite : IsFinite Bool
  ∣ boolFinite ∣ = 2
  index boolFinite = Bool≈Fin2

  boolEq : Decidable≡ Bool
  boolEq = finiteEq boolFinite

data _≼_ : ∀{n m} → Fin n → Fin m → Set where
  0≼x : ∀{n m} {x : Fin m} → fzero {n} ≼ x
  s≼s : ∀{n m} {x : Fin n} {y : Fin m} → x ≼ y → fsuc x ≼ fsuc y

≼torefl : ∀{n} {x y : Fin n} → x ≼ y → y ≼ x → x ≡ y
≼torefl 0≼x 0≼x = refl
≼torefl (s≼s x≼y) (s≼s y≼x) with ≼torefl x≼y y≼x
≼torefl (s≼s x≼y) (s≼s y≼x) | refl = refl

_≼≼_ : ∀{n m} → Fin n → Fin m → Set
x ≼≼ y = fsuc x ≼ y

data Compare {n m} (x : Fin n) (y : Fin m) : Set where
  less : x ≼≼ y → Compare x y
  equi : x ≼ y → y ≼ x → Compare x y
  more : y ≼≼ x → Compare x y

compare : ∀{n m} → (x : Fin n) → (y : Fin m) → Compare x y
compare fzero fzero = equi 0≼x 0≼x
compare fzero (fsuc y) = less (s≼s 0≼x)
compare (fsuc x) fzero = more (s≼s 0≼x)
compare (fsuc x) (fsuc y) with compare x y
compare (fsuc x) (fsuc y) | less x≼≼y = less (s≼s x≼≼y)
compare (fsuc x) (fsuc y) | equi x≼y y≼x = equi (s≼s x≼y) (s≼s y≼x)
compare (fsuc x) (fsuc y) | more y≼≼x = more (s≼s y≼≼x)

-- Naturals

prec : ∀ n m → suc n ≡ suc m → n ≡ m
prec n .n refl = refl

suc≢ : ∀ n → (suc n) ≢ n
suc≢ n ()

data _≤_ : ℕ → ℕ → Set where
  0≤n    : ∀{n} → zero ≤ n
  sn≤sm : ∀{n m} → n ≤ m → (suc n) ≤ (suc m)

≤refl : ∀ n → n ≤ n
≤refl zero = 0≤n
≤refl (suc n) = sn≤sm (≤refl n)

≤trans : ∀ x y z → x ≤ y → y ≤ z → x ≤ z
≤trans .0 y z 0≤n y≤z = 0≤n
≤trans (suc x) (suc y) (suc z) (sn≤sm x≤y) (sn≤sm y≤z) = sn≤sm (≤trans x y z x≤y y≤z)

_<_ : ℕ → ℕ → Set
n < m = suc n ≤ m

_≤?_ : (n m : ℕ) → Dec (n ≤ m)
zero ≤? zero = yes 0≤n
zero ≤? suc m = yes 0≤n
suc n ≤? zero = no (λ ())
suc n ≤? suc m with n ≤? m
...            | yes n≤m = yes (sn≤sm n≤m)
...            | no ¬n≤m = no φ
                           where φ : _
                                 φ (sn≤sm n≤m) = ¬n≤m n≤m

order : ∀ n m → ¬(n ≤ m) → m ≤ n
order zero m ¬n≤m = ⊥-elim (¬n≤m 0≤n)
order (suc n) zero ¬n≤m = 0≤n
order (suc n) (suc m) ¬n≤m = sn≤sm (order n m (λ z → ¬n≤m (sn≤sm z)))

injpres : ∀{n m} → (f : Fin (suc n) → Fin (suc m)) → Injective f → Σ (Fin n → Fin m) Injective
fst (injpres f inj) x with inspect (f fzero) | inspect (f (fsuc x))
fst (injpres f inj) x | fzero with≡ f0≡ | fzero with≡ fsx≡ with inj (≡trans f0≡ (≡sym fsx≡))
fst (injpres f inj) x | fzero with≡ f0≡ | fzero with≡ fsx≡ | ()
fst (injpres f inj) x | fzero with≡ f0≡ | fsuc fsx with≡ fsx≡ = fsx
fst (injpres f inj) x | fsuc fzero with≡ f0≡ | fzero with≡ fsx≡ = fzero
fst (injpres f inj) x | fsuc (fsuc y) with≡ f0≡ | fzero with≡ fsx≡ = fzero
fst (injpres f inj) x | f0@(fsuc y) with≡ f0≡ | fsx@(fsuc z) with≡ fsx≡ with compare fsx f0
fst (injpres f inj) x | fsuc y with≡ f0≡ | fsuc z with≡ fsx≡ | less x₁ = {!   !}
fst (injpres f inj) x | fsuc y with≡ f0≡ | fsuc z with≡ fsx≡ | equi x₁ x₂ with inj {fzero} {fsuc x} (≼torefl {!   !} {!   !})
... | c = {! c !}
fst (injpres f inj) x | fsuc y with≡ f0≡ | fsuc z with≡ fsx≡ | more x₁ = {!   !}
snd (injpres f inj) = {!   !}



pospidgeon : ∀{n m} → (f : Fin n → Fin m) → Injective f → n ≤ m
pospidgeon {zero} {m} f finj = 0≤n
pospidgeon {suc n} {zero} f finj with f fzero
pospidgeon {suc n} {zero} f finj | ()
pospidgeon {suc n} {suc m} f finj with injpres f finj
pospidgeon {suc n} {suc m} f finj | df , dfinj = sn≤sm (pospidgeon df dfinj)


pidgeon : ∀{n} → (f : Fin (suc n) → Fin n) → Collision f
pidgeon = ?

List.agda

module List where

open import Agda.Builtin.List public
open import Decidable

infixr 5 _++_

_++_ : {A : Set} → List A → List A → List A
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)


infixr 5 _∷_
data All {A : Set} (P : Pred A) : List A → Set where
  []  : All P []
  _∷_ : ∀{x xs} → P x → All P xs → All P (x ∷ xs)

private
  -- Some lemmae for All
  headAll : ∀{A x xs} {P : Pred A} → All P (x ∷ xs) → P x
  headAll (Px ∷ _) = Px

  tailAll : ∀{A x xs} {P : Pred A} → All P (x ∷ xs) → All P xs
  tailAll (_ ∷ ∀xsP) = ∀xsP

-- All is decidable for decidable predicates
all : {A : Set} {P : Pred A} → (P? : Decidable P) → (xs : List A) → Dec (All P xs)
all P? [] = yes []
all P? (x ∷ xs) with P? x
...             | no ¬Px = no λ φ → ¬Px (headAll φ)
...             | yes Px with all P? xs
...                      | yes ∀xsP = yes (Px ∷ ∀xsP)
...                      | no ¬∀xsP = no λ φ → ¬∀xsP (tailAll φ)


data Any {A : Set} (P : Pred A) : List A → Set where
  [_] : ∀{xs} → ∀{x} → P x      → Any P (x ∷ xs)
  _∷_ : ∀{xs} → ∀ x  → Any P xs → Any P (x ∷ xs)

private
  -- Some lemmae for Any
  hereAny : ∀{A x xs} {P : Pred A} → Any P (x ∷ xs) → ¬(Any P xs) → P x
  hereAny [ Px ]     ¬∃xsP = Px
  hereAny (_ ∷ ∃xsP) ¬∃xsP = ⊥-elim (¬∃xsP ∃xsP)

  laterAny : ∀{A x xs} {P : Pred A} → Any P (x ∷ xs) → ¬(P x) → (Any P xs)
  laterAny [ Px ]     ¬Px = ⊥-elim (¬Px Px)
  laterAny (_ ∷ ∃xsP) ¬Px = ∃xsP

-- Any is decidable for decidable predicates
any : {A : Set} {P : Pred A} → (P? : Decidable P) → (xs : List A) → Dec (Any P xs)
any P? [] = no (λ ())
any P? (x ∷ xs) with P? x
...             | yes Px = yes [ Px ]
...             | no ¬Px with any P? xs
...                      | yes ∃xsP = yes (x ∷ ∃xsP)
...                      | no ¬∃xsP = no λ φ → ¬Px (hereAny φ ¬∃xsP)


-- Any can be used to define membership
infix 0 _∈_ _∉_

_∈_ : {A : Set} → (x : A) → List A → Set
x ∈ xs = Any (x ≡_) xs

_∉_ : {A : Set} → (x : A) → List A → Set
x ∉ xs = ¬(x ∈ xs)

-- Memberhsip is decidable if equality is decidable.
decide∈ : {A : Set} → Decidable≡ A → (x : A) → (xs : List A) → Dec (x ∈ xs)
decide∈ _≟_ x xs = any (x ≟_) xs

Nfa.agda

module Nfa where

open import Agda.Builtin.Nat renaming (Nat to ℕ)

open import Decidable
open import List

open import Finite

private
  -- Technical preliminaries

  flatten : {A : Set} → List (List A) → List A
  flatten [] = []
  flatten (xss ∷ yss) = xss ++ flatten yss

  map : {A B : Set} → (A → B) → List A → List B
  map f [] = []
  map f (x ∷ xs) = f x ∷ map f xs


data Nsymbol (Σ : Set) : Set where
  σ : Σ → Nsymbol Σ
  ε : Nsymbol Σ

record Nfa (n : ℕ) (Σ : Set) : Set where
  constructor nfa
  field
    δ  : Fin n → Nsymbol Σ → List (Fin n)
    q₀ : Fin n
    fs : List (Fin n)

  δ* : Fin n → List (Nsymbol Σ) → List (Fin n)
  δ* q [] = q ∷ []
  δ* q (x ∷ xs) = flatten (map (λ p → δ* p xs) (δ q x))

  accepts : List Σ → Set
  accepts xs = Any (_∈ fs) (δ* q₀ (map σ xs))

  accepts? : (xs : List Σ) → Dec (accepts xs)
  accepts? xs = any (λ p → decide∈ _F≟_ p fs) (δ* q₀ (map σ xs))