OPLSS 2024

Brozozowski.agda

open import Data.Bool.Base
open import Relation.Binary.PropositionalEquality.Core
open import Relation.Nullary

module _ (A : Set) (dec : (a b : A) → Dec (a ≡ b)) where
  record DFA (S : Set) : Set where
    field F : S → Bool
    field t : A -> S -> S

  data RE : Set where
    zero one : RE
    sing : A → RE
    juxt disj : RE → RE → RE
    star : RE → RE

  boolToRE : Bool → RE
  boolToRE false = zero
  boolToRE true = one

  instance
    open DFA
    impl : DFA RE
    F impl zero = false
    F impl one = true
    F impl (sing x) = false
    F impl (juxt s s') = F impl s ∧ F impl s'
    F impl (disj s s') = F impl s ∨ F impl s'
    F impl (star x) = false
    t impl a zero = zero
    t impl a one = zero
    t impl a (sing x) = boolToRE (isYes (dec a x))
    t impl a (juxt e f) = disj (juxt (t impl a e) f) (juxt (boolToRE (F impl e)) (t impl a f))
    t impl a (disj s s') = disj (t impl a s) (t impl a s')
    t impl a (star x) = juxt (t impl a x) (star x)