{-# OPTIONS --allow-unsolved-metas #-}
open import Library
module _ (A : Set) where
infix 1 _≅_
infix 2 _∋_
infixl 4 _∪_
infixl 6 _·_
infixr 15 _*
record Lang : Set where
coinductive
field ν : Bool
δ : (a : A) → Lang
open Lang
_∋_ : Lang → (List A → Bool)
l ∋ [] = ν l
l ∋ a ∷ as = δ l a ∋ as
lang : (List A → Bool) → Lang
ν (lang mem) = mem []
δ (lang mem) a = lang λ as → mem (a ∷ as)
∅ : Lang
ν ∅ = false
δ ∅ a = ∅
ε : Lang
ν ε = true
δ ε a = ∅
_∪_ : (k l : Lang) → Lang
ν (k ∪ l) = ν k ∨ ν l
δ (k ∪ l) a = δ k a ∪ δ l a
{-# TERMINATING #-}
_·_ : (k l : Lang) → Lang
ν (k · l) = ν k ∧ ν l
δ (k · l) a = if ν k then (δ k a · l) ∪ δ l a else (δ k a · l)
{-# TERMINATING #-}
_* : Lang → Lang
ν (l *) = true
δ (l *) a = δ l a · (l *)
record _≅_ (l k : Lang) : Set where
coinductive
field
≅ν : ν l ≡ ν k
≅δ : (a : A) → δ l a ≅ δ k a
open _≅_ public
≅refl : ∀{l} → l ≅ l
≅ν ≅refl = refl
≅δ ≅refl a = ≅refl
≅sym : ∀{k l} (p : l ≅ k) → k ≅ l
≅ν (≅sym p) = sym (≅ν p)
≅δ (≅sym p) a = ≅sym (≅δ p a)
≅trans : ∀{k l m} (p : k ≅ l) (q : l ≅ m) → k ≅ m
≅ν (≅trans p q) = trans (≅ν p) (≅ν q)
≅δ (≅trans p q) a = ≅trans (≅δ p a) (≅δ q a)
≅isEquivalence : IsEquivalence _≅_
IsEquivalence.refl ≅isEquivalence = ≅refl
IsEquivalence.sym ≅isEquivalence = ≅sym
IsEquivalence.trans ≅isEquivalence = ≅trans
Bis : Setoid lzero lzero
Setoid.Carrier Bis = Lang
Setoid._≈_ Bis = _≅_
Setoid.isEquivalence Bis = ≅isEquivalence
union-cong : ∀{k k' l l' : Lang} (p : k ≅ k') (q : l ≅ l') → (k ∪ l) ≅ (k' ∪ l')
≅ν (union-cong p q) rewrite ≅ν p | ≅ν q = refl
≅δ (union-cong p q) a = union-cong (≅δ p a) (≅δ q a)
{-# TERMINATING #-}
dist : (k {l m} : Lang) → k · (l ∪ m) ≅ (k · l) ∪ (k · m)
≅ν (dist k) = ∧-∨-distribˡ (ν k) _ _
≅δ (dist k) a with ν k
≅δ (dist k {l} {m}) a | true = begin
δ k a · (l ∪ m) ∪ (δ l a ∪ δ m a)
≈⟨ union-cong (dist (δ k a)) {!!} ⟩
(δ k a · l ∪ δ k a · m) ∪ (δ l a ∪ δ m a)
≈⟨ {!!} ⟩
(δ k a · l ∪ δ l a) ∪ (δ k a · m ∪ δ m a)
∎
where open EqR Bis
≅δ (dist k) a | false = dist (δ k a)