{-# OPTIONS --without-K --safe #-}

open import Relation.Binary hiding (Decidable; Irrelevant; Recomputable)

module Cfe.Language.Properties
  {c ℓ} (over : Setoid c ℓ)
  where

open Setoid over using ()
  renaming
    ( Carrier to C
    ; _≈_ to _∼_
    ; refl to ∼-refl
    ; sym to ∼-sym
    ; trans to ∼-trans
    )

open import Algebra
open import Cfe.Language.Base over
open import Cfe.List.Compare over
open import Data.Empty using (⊥-elim)
import Data.Fin as Fin
open import Data.List as L
open import Data.List.Properties
open import Data.List.Relation.Binary.Equality.Setoid over
import Data.List.Relation.Unary.Any as Any
open import Data.Nat using (ℕ; zero; suc; _≤_; z≤n; s≤s)
open import Data.Product as P
open import Data.Sum as S
open import Function hiding (_⟶_)
open import Level renaming (suc to ℓsuc)
import Relation.Binary.Construct.On as On
open import Relation.Binary.PropositionalEquality hiding (setoid; [_])
open import Relation.Nullary hiding (Irrelevant)
open import Relation.Nullary.Decidable
open import Relation.Nullary.Product using (_×-dec_)
open import Relation.Nullary.Sum using (_⊎-dec_)

private
  variable
    a b d ℓ₁ ℓ₂ : Level
    A X : Language b
    B Y : Language d
    U Z : Language ℓ₁
    V : Language ℓ₂
    F : Language a → Language a
    G : Language b → Language b

  w++[]≋w : ∀ w → w ++ [] ≋ w
  w++[]≋w [] = []
  w++[]≋w (x ∷ w) = ∼-refl ∷ w++[]≋w w

------------------------------------------------------------------------
-- Properties of First
------------------------------------------------------------------------

First-resp-∼ : ∀ (A : Language a) {c c′} → c ∼ c′ → First A c → First A c′
First-resp-∼ A c∼c′ (w , cw∈A) = w , ∈-resp-≋ (c∼c′ ∷ ≋-refl) cw∈A
  where open Language A

------------------------------------------------------------------------
-- Properties of _⊆_
------------------------------------------------------------------------
-- Relational properties of _⊆_

⊆-refl : Reflexive (_⊆_ {a})
⊆-refl = sub id

⊆-reflexive : (_≈_ {a} {b}) ⇒ _⊆_
⊆-reflexive = proj₁

⊇-reflexive : (_≈_ {a} {b}) ⇒ flip _⊆_
⊇-reflexive = proj₂

⊆-trans : Trans (_⊆_ {a}) (_⊆_ {b} {d}) _⊆_
⊆-trans (sub A⊆B) (sub B⊆C) = sub (B⊆C ∘ A⊆B)

⊆-antisym : Antisym (_⊆_ {a} {b}) _⊆_ _≈_
⊆-antisym = _,_

⊆-min : Min (_⊆_ {a} {b}) ∅
⊆-min _ = sub λ ()

⊆-respʳ-≈ : Y ≈ Z → X ⊆ Y → X ⊆ Z
⊆-respʳ-≈ Y≈Z X⊆Y = ⊆-trans X⊆Y (⊆-reflexive Y≈Z)

⊆-respˡ-≈ : Y ≈ Z → Y ⊆ X → Z ⊆ X
⊆-respˡ-≈ Y≈Z Y⊆X = ⊆-trans (⊇-reflexive Y≈Z) Y⊆X

------------------------------------------------------------------------
-- Membership properties of _⊆_

∈-resp-⊆ : ∀ {w} → (w ∈_) ⟶ (w ∈_) Respects (_⊆_ {a} {b})
∈-resp-⊆ (sub A⊆B) = A⊆B

∉-resp-⊇ : ∀ {w} → (w ∉_) ⟶ (w ∉_) Respects flip (_⊆_ {b} {a})
∉-resp-⊇ (sub A⊇B) w∉A = w∉A ∘ A⊇B

Null-resp-⊆ : Null {a} ⟶ Null {b} Respects _⊆_
Null-resp-⊆ = ∈-resp-⊆

First-resp-⊆ : ∀ {c} → flip (First {a}) c ⟶ flip (First {b}) c Respects _⊆_
First-resp-⊆ (sub A⊆B) = P.map₂ A⊆B

Flast-resp-⊆ : ∀ {c} → flip (Flast {a}) c ⟶ flip (Flast {b}) c Respects _⊆_
Flast-resp-⊆ (sub A⊆B) = P.map₂ (P.map₂ (P.map A⊆B (P.map₂ A⊆B)))

------------------------------------------------------------------------
-- Properties of _≈_
------------------------------------------------------------------------
-- Relational properties of _≈_

≈-refl : Reflexive (_≈_ {a})
≈-refl = ⊆-refl , ⊆-refl

≈-reflexive : _≡_ ⇒ (_≈_ {a})
≈-reflexive refl = ≈-refl

≈-sym : Sym (_≈_ {a} {b}) _≈_
≈-sym = P.swap

≈-trans : Trans (_≈_ {a}) (_≈_ {b} {d}) _≈_
≈-trans = P.zip ⊆-trans (flip ⊆-trans)

------------------------------------------------------------------------
-- Structures

≈-isPartialEquivalence : IsPartialEquivalence (_≈_ {a})
≈-isPartialEquivalence = record
  { sym   = ≈-sym
  ; trans = ≈-trans
  }

≈-isEquivalence : IsEquivalence (_≈_ {a})
≈-isEquivalence = record
  { refl  = ≈-refl
  ; sym   = ≈-sym
  ; trans = ≈-trans
  }

⊆-isPreorder : IsPreorder (_≈_ {a}) _⊆_
⊆-isPreorder = record
  { isEquivalence = ≈-isEquivalence
  ; reflexive     = ⊆-reflexive
  ; trans         = ⊆-trans
  }

⊆-isPartialOrder : IsPartialOrder (_≈_ {a}) _⊆_
⊆-isPartialOrder = record
  { isPreorder = ⊆-isPreorder
  ; antisym    = ⊆-antisym
  }

------------------------------------------------------------------------
-- Bundles

partialSetoid : ∀ {a} → PartialSetoid _ _
partialSetoid {a} = record { isPartialEquivalence = ≈-isPartialEquivalence {a} }

setoid : ∀ {a} → Setoid _ _
setoid {a} = record { isEquivalence = ≈-isEquivalence {a} }

⊆-preorder : ∀ {a} → Preorder _ _ _
⊆-preorder {a} = record { isPreorder = ⊆-isPreorder {a} }

⊆-poset : ∀ {a} → Poset _ _ _
⊆-poset {a} = record { isPartialOrder = ⊆-isPartialOrder {a} }

-- Shamelessly adapted from Relation.Binary.Reasoning.Base.Double
module ⊆-Reasoning where
  infix 4 _IsRelatedTo_

  data _IsRelatedTo_ (A : Language a) (B : Language b) : Set (c ⊔ ℓ ⊔ ℓsuc (a ⊔ b)) where
    nonstrict : (A⊆B : A ⊆ B) → A IsRelatedTo B
    equals    : (A≈B : A ≈ B) → A IsRelatedTo B

  ------------------------------------------------------------------------
  -- A record that is used to ensure that the final relation proved by the
  -- chain of reasoning can be converted into the required relation.

  data IsEquality {A : Language a} {B : Language b} : A IsRelatedTo B → Set (c ⊔ ℓ ⊔ ℓsuc (a ⊔ b)) where
    isEquality : ∀ A≈B → IsEquality (equals A≈B)

  IsEquality? : ∀ (A⊆B : A IsRelatedTo B) → Dec (IsEquality A⊆B)
  IsEquality? (nonstrict _) = no λ()
  IsEquality? (equals A≈B)  = yes (isEquality A≈B)

  extractEquality : ∀ {A⊆B : A IsRelatedTo B} → IsEquality A⊆B → A ≈ B
  extractEquality (isEquality A≈B) = A≈B

  ------------------------------------------------------------------------
  -- Reasoning combinators

  -- See `Relation.Binary.Reasoning.Base.Partial` for the design decisions
  -- behind these combinators.

  infix  1 begin_ begin-equality_
  infixr 2 step-⊆ step-≈ step-≈˘ step-≡ step-≡˘ _≡⟨⟩_
  infix  3 _∎

  -- Beginnings of various types of proofs

  begin_ : (r : A IsRelatedTo B) → A ⊆ B
  begin (nonstrict A⊆B) = A⊆B
  begin (equals    A≈B) = ⊆-reflexive A≈B

  begin-equality_ : ∀ (r : A IsRelatedTo B) → {s : True (IsEquality? r)} → A ≈ B
  begin-equality_ r {s} = extractEquality (toWitness s)

  -- Step with the main relation

  step-⊆ : ∀ (X : Language a) → Y IsRelatedTo Z → X ⊆ Y → X IsRelatedTo Z
  step-⊆ X (nonstrict Y⊆Z) X⊆Y = nonstrict (⊆-trans X⊆Y Y⊆Z)
  step-⊆ X (equals    Y≈Z) X⊆Y = nonstrict (⊆-respʳ-≈ Y≈Z X⊆Y)

  -- Step with the setoid equality

  step-≈ : ∀ (X : Language a) → Y IsRelatedTo Z → X ≈ Y → X IsRelatedTo Z
  step-≈ X (nonstrict Y⊆Z) X≈Y = nonstrict (⊆-respˡ-≈ (≈-sym X≈Y) Y⊆Z)
  step-≈ X (equals    Y≈Z) X≈Y = equals    (≈-trans X≈Y Y≈Z)

  -- Flipped step with the setoid equality

  step-≈˘ : ∀ (X : Language a) → Y IsRelatedTo Z → Y ≈ X → X IsRelatedTo Z
  step-≈˘ X Y⊆Z Y≈X = step-≈ X Y⊆Z (≈-sym Y≈X)

  -- Step with non-trivial propositional equality

  step-≡ : ∀ (X : Language a) → Y IsRelatedTo Z → X ≡ Y → X IsRelatedTo Z
  step-≡ X (nonstrict Y⊆Z) X≡Y = nonstrict (case X≡Y of λ { refl → Y⊆Z })
  step-≡ X (equals    Y≈Z) X≡Y = equals    (case X≡Y of λ { refl → Y≈Z })

  -- Flipped step with non-trivial propositional equality

  step-≡˘ : ∀ (X : Language a) → Y IsRelatedTo Z → Y ≡ X → X IsRelatedTo Z
  step-≡˘ X Y⊆Z Y≡X = step-≡ X Y⊆Z (sym Y≡X)

  -- Step with trivial propositional equality

  _≡⟨⟩_ : ∀ (X : Language a) → X IsRelatedTo Y → X IsRelatedTo Y
  X ≡⟨⟩ X⊆Y = X⊆Y

  -- Termination step

  _∎ : ∀ (X : Language a) → X IsRelatedTo X
  X ∎ = equals ≈-refl

  -- Syntax declarations

  syntax step-⊆  X Y⊆Z X⊆Y = X ⊆⟨  X⊆Y ⟩ Y⊆Z
  syntax step-≈  X Y⊆Z X≈Y = X ≈⟨  X≈Y ⟩ Y⊆Z
  syntax step-≈˘ X Y⊆Z Y≈X = X ≈˘⟨ Y≈X ⟩ Y⊆Z
  syntax step-≡  X Y⊆Z X≡Y = X ≡⟨  X≡Y ⟩ Y⊆Z
  syntax step-≡˘ X Y⊆Z Y≡X = X ≡˘⟨ Y≡X ⟩ Y⊆Z

------------------------------------------------------------------------
-- Membership properties of _≈_

∈-resp-≈ : ∀ {w} → (w ∈_) ⟶ (w ∈_) Respects (_≈_ {a} {b})
∈-resp-≈ = ∈-resp-⊆ ∘ ⊆-reflexive

∉-resp-≈ : ∀ {w} → (w ∉_) ⟶ (w ∉_) Respects flip (_≈_ {b} {a})
∉-resp-≈ = ∉-resp-⊇ ∘ ⊆-reflexive

Null-resp-≈ : Null {a} ⟶ Null {b} Respects _≈_
Null-resp-≈ = Null-resp-⊆ ∘ ⊆-reflexive

First-resp-≈ : ∀ {c} → flip (First {a}) c ⟶ flip (First {b}) c Respects _≈_
First-resp-≈ = First-resp-⊆ ∘ ⊆-reflexive

Flast-resp-≈ : ∀ {c} → flip (Flast {a}) c ⟶ flip (Flast {b}) c Respects _≈_
Flast-resp-≈ = Flast-resp-⊆ ∘ ⊆-reflexive

------------------------------------------------------------------------
-- Proof properties of _≈_

Decidable-resp-≈ : Decidable {a} ⟶ Decidable {b} Respects _≈_
Decidable-resp-≈ (sub A⊆B , sub A⊇B) A? l = map′ A⊆B A⊇B (A? l)

Recomputable-resp-≈ : Recomputable {a} ⟶ Recomputable {b} Respects _≈_
Recomputable-resp-≈ (sub A⊆B , sub A⊇B) recomp l∈B = A⊆B (recomp (A⊇B l∈B))

------------------------------------------------------------------------
-- Properties of ∅
------------------------------------------------------------------------
-- Membership properties of ∅

w∉∅ : ∀ w → w ∉ ∅ {a}
w∉∅ _ ()

ε∉∅ : ¬ Null {a} ∅
ε∉∅ ()

∄[First[∅]] : ∀ c → ¬ First {a} ∅ c
∄[First[∅]] _ ()

∄[Flast[∅]] : ∀ c → ¬ Flast {a} ∅ c
∄[Flast[∅]] _ ()

ε∉A+∄[First[A]]⇒A≈∅ : ¬ Null A → (∀ c → ¬ First A c) → A ≈ ∅ {a}
ε∉A+∄[First[A]]⇒A≈∅ {A = A} ε∉A cw∉A =
  ⊆-antisym
    (sub λ {w} w∈A → case ∃[ w ] w ∈ A ∋ w , w∈A of λ
      { ([]    ,  ε∈A) → lift (ε∉A ε∈A)
      ; (c ∷ w , cw∈A) → lift (cw∉A c (w , cw∈A))
      })
    (⊆-min A)

------------------------------------------------------------------------
-- Proof properties of ∅

∅? : Decidable (∅ {a})
∅? w = no λ ()

∅-irrelevant : Irrelevant (∅ {a})
∅-irrelevant ()

∅-recomputable : Recomputable (∅ {a})
∅-recomputable ()

------------------------------------------------------------------------
-- Properties of ｛ε｝
------------------------------------------------------------------------
-- Membership properties of ∅

ε∈｛ε｝ : Null (｛ε｝{a})
ε∈｛ε｝ = lift refl

∄[First[｛ε｝]] : ∀ c → ¬ First (｛ε｝ {a}) c
∄[First[｛ε｝]] _ ()

∄[Flast[｛ε｝]] : ∀ c → ¬ Flast (｛ε｝ {a}) c
∄[Flast[｛ε｝]] _ ()

∄[First[A]]⇒A⊆｛ε｝ : (∀ c → ¬ First A c) → A ⊆ ｛ε｝ {a}
∄[First[A]]⇒A⊆｛ε｝ {A = A} cw∉A =
  sub λ {w} w∈A → case ∃[ w ] w ∈ A ∋ w , w∈A return (λ (w , _) → w ∈ ｛ε｝) of λ
    { ([]    ,  w∈A) → lift refl
    ; (c ∷ w , cw∈A) → ⊥-elim (cw∉A c (w , cw∈A))
    }

------------------------------------------------------------------------
-- Proof properties of ｛ε｝

｛ε｝? : Decidable (｛ε｝ {a})
｛ε｝? []      = yes (lift refl)
｛ε｝? (_ ∷ _) = no λ ()

｛ε｝-irrelevant : Irrelevant (｛ε｝ {a})
｛ε｝-irrelevant (lift refl) (lift refl) = refl

｛ε｝-recomputable : Recomputable (｛ε｝ {a})
｛ε｝-recomputable {w = []} _ = lift refl

------------------------------------------------------------------------
-- Properties of ｛_｝
------------------------------------------------------------------------
-- Membership properties of ｛_｝

ε∉｛c｝ : ∀ c → ¬ Null ｛ c ｝
ε∉｛c｝ _ ()

c′∈First[｛c｝]⇒c∼c′ : ∀ {c c′} → First ｛ c ｝ c′ → c ∼ c′
c′∈First[｛c｝]⇒c∼c′ (_ , c∼c′ ∷ []) = c∼c′

c∼c′⇒c′∈｛c｝ : ∀ {c c′} → c ∼ c′ → [ c′ ] ∈ ｛ c ｝
c∼c′⇒c′∈｛c｝ c∼c′ = c∼c′ ∷ []

∄[Flast[｛c｝]] : ∀ {c} c′ → ¬ Flast ｛ c ｝ c′
∄[Flast[｛c｝]] _ (_ , _ , _ ∷ [] , _ , _ ∷ ())

xyw∉｛c｝ : ∀ c x y w → x ∷ y ∷ w ∉ ｛ c ｝
xyw∉｛c｝ c x y w (_ ∷ ())

------------------------------------------------------------------------
-- Algebraic properties of ｛_｝

｛｝-cong : ∀ {c c′} → c ∼ c′ → ｛ c ｝ ≈ ｛ c′ ｝
｛｝-cong c∼c′ =
  ⊆-antisym
    (sub λ { (c∼x ∷ []) → c∼c′⇒c′∈｛c｝ (∼-trans (∼-sym c∼c′) c∼x) })
    (sub λ { (c′∼x ∷ []) → c∼c′⇒c′∈｛c｝ (∼-trans c∼c′ c′∼x) })

｛｝-inj : ∀ {c c′} → ｛ c ｝ ≈ ｛ c′ ｝ → c ∼ c′
｛｝-inj {c} c≈c′ with ∈-resp-≈ c≈c′ (∼-refl ∷ [])
...                  | (c′∼c ∷ []) = ∼-sym c′∼c

------------------------------------------------------------------------
-- Properties of _∙_
------------------------------------------------------------------------
-- Membership properties of _∙_

-- Null

ε∈A⇒B⊆A∙B : ∀ (A : Language b) (B : Language d) → Null A → B ⊆ A ∙ B
ε∈A⇒B⊆A∙B _ _ ε∈A = sub λ w∈B → -, -, ε∈A , w∈B , ≋-refl

ε∈B⇒A⊆A∙B : ∀ (A : Language b) (B : Language d) → Null B → A ⊆ A ∙ B
ε∈B⇒A⊆A∙B _ _ ε∈B = sub λ {w} w∈A → -, -, w∈A , ε∈B , w++[]≋w w

ε∈A+ε∈B⇒ε∈A∙B : Null A → Null B → Null (A ∙ B)
ε∈A+ε∈B⇒ε∈A∙B ε∈A ε∈B = -, -, ε∈A , ε∈B , ≋-refl

ε∈A∙B⇒ε∈A : ∀ (A : Language b) (B : Language d) → Null (A ∙ B) → Null A
ε∈A∙B⇒ε∈A _ _ ([] , [] , ε∈A , ε∈B , []) = ε∈A

ε∈A∙B⇒ε∈B : ∀ (A : Language b) (B : Language d) → Null (A ∙ B) → Null B
ε∈A∙B⇒ε∈B _ _ ([] , [] , ε∈A , ε∈B , []) = ε∈B

-- First

c∈First[A]+w′∈B⇒c∈First[A∙B] : ∀ {c} → First A c → ∃[ w ] w ∈ B → First (A ∙ B) c
c∈First[A]+w′∈B⇒c∈First[A∙B] (_ , cw∈A) (_ , w′∈B) = -, -, -, cw∈A , w′∈B , ≋-refl

ε∈A+c∈First[B]⇒c∈First[A∙B] : ∀ {c} → Null A → First B c → First (A ∙ B) c
ε∈A+c∈First[B]⇒c∈First[A∙B] ε∈A (_ , cw∈B) = -, -, -, ε∈A , cw∈B , ≋-refl

c∈First[A∙B]⇒c∈First[A]⊎ε∈A+c∈First[B] :
  ∀ (A : Language a) (B : Language b) {c} → First (A ∙ B) c → First A c ⊎ Null A × First B c
c∈First[A∙B]⇒c∈First[A]⊎ε∈A+c∈First[B] _ B (_ , []     , xw₂ , ε∈A   , xw₂∈B , x∼c ∷ _) =
  inj₂ (ε∈A , First-resp-∼ B x∼c (-, xw₂∈B))
c∈First[A∙B]⇒c∈First[A]⊎ε∈A+c∈First[B] A _ (_ , x ∷ w₁ , _   , xw₁∈A , _     , x∼c ∷ _) =
  inj₁ (First-resp-∼ A x∼c (-, xw₁∈A))

-- Flast

c∈Flast[B]+w∈A⇒c∈Flast[A∙B] : ∀ {c} → Flast B c → ∃[ w ] w ∈ A → Flast (A ∙ B) c
c∈Flast[B]+w∈A⇒c∈Flast[A∙B]         (_ , _ ,  w∈B , _ ,  wcw′∈B) (       [] ,     ε∈A) =
  -, -, (-, -, ε∈A , w∈B , ≋-refl) , -, -, -, ε∈A , wcw′∈B , ≋-refl
c∈Flast[B]+w∈A⇒c∈Flast[A∙B] {c = c} (x , w , xw∈B , w′ , xwcw′∈B) (c′ ∷ w′′ , c′w′′∈A) =
  -, -, c′w′′xw∈A∙B , -, c′w′′xwcw′∈A∙B
  where
  c′w′′xw∈A∙B    = -, -, c′w′′∈A , xw∈B , ≋-refl
  c′w′′xwcw′∈A∙B = -, -, c′w′′∈A , xwcw′∈B , ∼-refl ∷ ≋-reflexive (sym (++-assoc w′′ (x ∷ w) (c ∷ w′)))

ε∈B+x∈First[A]+c∈First[B]⇒c∈Flast[A∙B] :
  ∀ {c} → Null B → ∃[ x ] First A x → First B c → Flast (A ∙ B) c
ε∈B+x∈First[A]+c∈First[B]⇒c∈Flast[A∙B] ε∈B (x , w , xw∈A) (_ , cw′∈B) = -, -, xw∈A∙B , -, xwcw′∈A∙B
  where
  xw∈A∙B    = -, -, xw∈A , ε∈B , w++[]≋w (x ∷ w)
  xwcw′∈A∙B = -, -, xw∈A , cw′∈B , ≋-refl

ε∈B+c∈Flast[A]⇒c∈Flast[A∙B] : ∀ {c} → Null B → Flast A c → Flast (A ∙ B) c
ε∈B+c∈Flast[A]⇒c∈Flast[A∙B] {c = c} ε∈B (x , w , xw∈A , w′ , xwcw′∈A) = -, -, xw∈A∙B , -, xwcw′∈A∙B
  where
  xw∈A∙B    = -, -, xw∈A , ε∈B , w++[]≋w (x ∷ w)
  xwcw′∈A∙B = -, -, xwcw′∈A , ε∈B , w++[]≋w (x ∷ w ++ c ∷ w′)

------------------------------------------------------------------------
-- Algebraic properties of _∙_

∙-mono : X ⊆ Y → U ⊆ V → X ∙ U ⊆ Y ∙ V
∙-mono (sub X⊆Y) (sub U⊆V) = sub λ (_ , _ , w₁∈X , w₂∈U , eq) → -, -, X⊆Y w₁∈X , U⊆V w₂∈U , eq

∙-cong : X ≈ Y → U ≈ V → X ∙ U ≈ Y ∙ V
∙-cong X≈Y U≈V = ⊆-antisym
  (∙-mono (⊆-reflexive X≈Y) (⊆-reflexive U≈V))
  (∙-mono (⊇-reflexive X≈Y) (⊇-reflexive U≈V))

∙-assoc : ∀ (A : Language a) (B : Language b) (C : Language d) → (A ∙ B) ∙ C ≈ A ∙ (B ∙ C)
∙-assoc A B C =
  (sub λ {w} (w₁w₂ , w₃ , (w₁ , w₂ , w₁∈A , w₂∈B , eq₁) , w₃∈C , eq₂) →
    -, -, w₁∈A , (-, -, w₂∈B , w₃∈C , ≋-refl) ,
      (begin
        w₁ ++ w₂ ++ w₃   ≡˘⟨ ++-assoc w₁ w₂ w₃ ⟩
        (w₁ ++ w₂) ++ w₃ ≈⟨ ++⁺ eq₁ ≋-refl ⟩
        w₁w₂ ++ w₃       ≈⟨ eq₂ ⟩
        w ∎)) ,
  (sub λ {w} (w₁ , w₂w₃ , w₁∈A , (w₂ , w₃ , w₂∈B , w₃∈C , eq₁) , eq₂) →
    -, -, (-, -, w₁∈A , w₂∈B , ≋-refl) , w₃∈C ,
      (begin
        (w₁ ++ w₂) ++ w₃ ≡⟨ ++-assoc w₁ w₂ w₃ ⟩
        w₁ ++ w₂ ++ w₃   ≈⟨ ++⁺ ≋-refl eq₁ ⟩
        w₁ ++ w₂w₃       ≈⟨ eq₂ ⟩
        w ∎))
  where
  open import Relation.Binary.Reasoning.Setoid ≋-setoid

∙-identityˡ : ∀ (A : Language a) → ｛ε｝ {b} ∙ A ≈ A
∙-identityˡ A =
  ⊆-antisym
    (sub λ { (_ , _ , lift refl , w′∈A , eq) → A.∈-resp-≋ eq w′∈A })
    (ε∈A⇒B⊆A∙B ｛ε｝ A ε∈｛ε｝)
  where
  module A = Language A

∙-identityʳ : ∀ (A : Language a) → A ∙ ｛ε｝ {b} ≈ A
∙-identityʳ X =
  ⊆-antisym
    (sub λ {w} → λ
      { (w′ , _ , w′∈X , lift refl , eq) →
        X.∈-resp-≋
          (begin
            w′       ≈˘⟨ w++[]≋w w′ ⟩
            w′ ++ [] ≈⟨ eq ⟩
            w        ∎)
          w′∈X
      })
    (ε∈B⇒A⊆A∙B X ｛ε｝ ε∈｛ε｝)
  where
  open import Relation.Binary.Reasoning.Setoid ≋-setoid
  module X = Language X

∙-identity : (∀ (A : Language a) → ｛ε｝ {b} ∙ A ≈ A) × (∀ (A : Language a) → A ∙ ｛ε｝ {b} ≈ A)
∙-identity = ∙-identityˡ , ∙-identityʳ

∙-zeroˡ : ∀ (A : Language a) → ∅ {b} ∙ A ≈ ∅ {d}
∙-zeroˡ A = ⊆-antisym (sub λ ()) (⊆-min (∅ ∙ A))

∙-zeroʳ : ∀ (A : Language a) → A ∙ ∅ {b} ≈ ∅ {d}
∙-zeroʳ A = ⊆-antisym (sub λ ()) (⊆-min (A ∙ ∅))

∙-zero : (∀ (A : Language a) → ∅ {b} ∙ A ≈ ∅ {d}) × (∀ (A : Language a) → A ∙ ∅ {b} ≈ ∅ {d})
∙-zero = ∙-zeroˡ , ∙-zeroʳ

------------------------------------------------------------------------
-- Structures

∙-isMagma : ∀ {a} → IsMagma _≈_ (_∙_ {c ⊔ ℓ ⊔ a})
∙-isMagma = record
  { isEquivalence = ≈-isEquivalence
  ; ∙-cong        = ∙-cong
  }

∙-isSemigroup : ∀ {a} → IsSemigroup _≈_ (_∙_ {c ⊔ ℓ ⊔ a})
∙-isSemigroup {a} = record
  { isMagma = ∙-isMagma {a}
  ; assoc   = ∙-assoc
  }

∙-isMonoid : ∀ {a} → IsMonoid _≈_ _∙_ (｛ε｝ {ℓ ⊔ a})
∙-isMonoid {a} = record
  { isSemigroup = ∙-isSemigroup {a}
  ; identity    = ∙-identity
  }

------------------------------------------------------------------------
-- Bundles

∙-magma : ∀ {a} → Magma _ _
∙-magma {a} = record { isMagma = ∙-isMagma {a} }

∙-semigroup : ∀ {a} → Semigroup _ _
∙-semigroup {a} = record { isSemigroup = ∙-isSemigroup {a} }

∙-monoid : ∀ {a} → Monoid _ _
∙-monoid {a} = record { isMonoid = ∙-isMonoid {a} }

------------------------------------------------------------------------
-- Other properties of _∙_

∙-uniqueₗ :
  ∀ (A : Language a) (B : Language b) →
  (∀ {c} → ¬ (Flast A c × First B c)) →
  ¬ Null A →
  ∀ {w} (p q : w ∈ A ∙ B) → (_≋_ on proj₁) p q
∙-uniqueₗ A B ∄[l₁∩f₂] ε∉A (   [] , _ , ε∈A , _             )                  _                       = ⊥-elim (ε∉A ε∈A)
∙-uniqueₗ A B ∄[l₁∩f₂] ε∉A (_ ∷ _  , _                      ) ([] , _ , ε∈A , _                      ) = ⊥-elim (ε∉A ε∈A)
∙-uniqueₗ A B ∄[l₁∩f₂] ε∉A (x ∷ w₁ , w₂ , xw₁∈A , w₂∈B , eq₁) (x′ ∷ w₁′ , w₂′ , x′w₁′∈A , w₂′∈B , eq₂)
  with compare (x ∷ w₁) w₂ (x′ ∷ w₁′) w₂′ (≋-trans eq₁ (≋-sym eq₂))
... | cmp with <?> cmp
... | tri< l _ _ = ⊥-elim (∄[l₁∩f₂] (c∈Flast[A] , c∈First[B]))
  where
  module A   = Language A
  module B   = Language B
  lsplit     = left-split cmp l
  xw∈A       = x′w₁′∈A
  xwcw′∈A    = A.∈-resp-≋ ((proj₁ ∘ proj₂ ∘ proj₂) lsplit) xw₁∈A
  cw′∈B      = B.∈-resp-≋ (≋-sym ((proj₂ ∘ proj₂ ∘ proj₂) lsplit)) w₂′∈B
  c∈Flast[A] = -, -, xw∈A , -, xwcw′∈A
  c∈First[B] = -, cw′∈B
... | tri≈ _ e _ = proj₁ (eq-split cmp e)
... | tri> _ _ r = ⊥-elim (∄[l₁∩f₂] (c∈Flast[A] , c∈First[B]))
  where
  module A   = Language A
  module B   = Language B
  rsplit     = right-split cmp r
  xw∈A       = xw₁∈A
  xwcw′∈A    = A.∈-resp-≋ (≋-sym ((proj₁ ∘ proj₂ ∘ proj₂) rsplit)) x′w₁′∈A
  cw′∈B      = B.∈-resp-≋ ((proj₂ ∘ proj₂ ∘ proj₂) rsplit) w₂∈B
  c∈Flast[A] = -, -, xw∈A , -, xwcw′∈A
  c∈First[B] = -, cw′∈B

∙-uniqueᵣ :
  ∀ (A : Language a) (B : Language b) →
  (∀ {c} → ¬ (Flast A c × First B c)) →
  ¬ Null A →
  ∀ {w} (p q : w ∈ A ∙ B) → (_≋_ on proj₁ ∘ proj₂) p q
∙-uniqueᵣ A B ∄[l₁∩f₂] ε∉A (   []  ,  _ ,   ε∈A , _         )                                        _ = ⊥-elim (ε∉A ε∈A)
∙-uniqueᵣ A B ∄[l₁∩f₂] ε∉A (_ ∷  _ , _                      ) (      [] ,   _ ,     ε∈A , _          ) = ⊥-elim (ε∉A ε∈A)
∙-uniqueᵣ A B ∄[l₁∩f₂] ε∉A (x ∷ w₁ , w₂ , xw₁∈A , w₂∈B , eq₁) (x′ ∷ w₁′ , w₂′ , x′w₁′∈A , w₂′∈B , eq₂)
  with compare (x ∷ w₁) w₂ (x′ ∷ w₁′) w₂′ (≋-trans eq₁ (≋-sym eq₂))
... | cmp with <?> cmp
... | tri< l _ _ = ⊥-elim (∄[l₁∩f₂] (c∈Flast[A] , c∈First[B]))
  where
  module A   = Language A
  module B   = Language B
  lsplit     = left-split cmp l
  xw∈A       = x′w₁′∈A
  xwcw′∈A    = A.∈-resp-≋ ((proj₁ ∘ proj₂ ∘ proj₂) lsplit) xw₁∈A
  cw′∈B      = B.∈-resp-≋ (≋-sym ((proj₂ ∘ proj₂ ∘ proj₂) lsplit)) w₂′∈B
  c∈Flast[A] = -, -, xw∈A , -, xwcw′∈A
  c∈First[B] = -, cw′∈B
... | tri≈ _ e _ = proj₂ (eq-split cmp e)
... | tri> _ _ r = ⊥-elim (∄[l₁∩f₂] (c∈Flast[A] , c∈First[B]))
  where
  module A   = Language A
  module B   = Language B
  rsplit     = right-split cmp r
  xw∈A       = xw₁∈A
  xwcw′∈A    = A.∈-resp-≋ (≋-sym ((proj₁ ∘ proj₂ ∘ proj₂) rsplit)) x′w₁′∈A
  cw′∈B      = B.∈-resp-≋ ((proj₂ ∘ proj₂ ∘ proj₂) rsplit) w₂∈B
  c∈Flast[A] = -, -, xw∈A , -, xwcw′∈A
  c∈First[B] = -, cw′∈B

------------------------------------------------------------------------
-- Proof properties of _∙_

_∙?_ : Decidable A → Decidable B → Decidable (A ∙ B)
_∙?_ {A = A} {B = B} A? B? [] =
  map′
    (λ (ε∈A , ε∈B) → -, -, ε∈A , ε∈B , [])
    (λ {([] , [] , ε∈A , ε∈B , []) → ε∈A , ε∈B})
    (A? [] ×-dec B? [])
_∙?_ {A = A} {B = B} A? B? (x ∷ w) =
  map′
    (λ
      { (inj₁ (ε∈A , xw∈B))                → -, -, ε∈A , xw∈B , ≋-refl
      ; (inj₂ (_ , _ , xw₁∈A , w₂∈B , eq)) → -, -, xw₁∈A , w₂∈B , ∼-refl ∷ eq
      })
    (λ
      { (    [] , _ ,    ε∈A , w′∈B ,        eq) → inj₁ (ε∈A , B.∈-resp-≋ eq w′∈B)
      ; (x′ ∷ _ , _ , x′w₁∈A , w₂∈B , x′∼x ∷ eq) →
        inj₂ (-, -, A.∈-resp-≋ (x′∼x ∷ ≋-refl) x′w₁∈A , w₂∈B , eq)
      })
    (A? [] ×-dec B? (x ∷ w) ⊎-dec (_∙?_ {A = A′} {B = B} (A? ∘ (x ∷_)) B?) w)
  where
  module A = Language A
  module B = Language B
  A′ : Language _
  A′ = record
    { 𝕃 = λ w → x ∷ w ∈ A
    ; ∈-resp-≋ = λ w≋w′ → A.∈-resp-≋ (∼-refl ∷ w≋w′)
    }

------------------------------------------------------------------------
-- Properties of _∪_
------------------------------------------------------------------------
-- Membership properties of _∪_

-- Null

ε∈A⇒ε∈A∪B : ∀ (A : Language b) (B : Language d) → Null A → Null (A ∪ B)
ε∈A⇒ε∈A∪B _ _ = inj₁

ε∈B⇒ε∈A∪B : ∀ (A : Language b) (B : Language d) → Null B → Null (A ∪ B)
ε∈B⇒ε∈A∪B _ _ = inj₂

ε∈A∪B⇒ε∈A⊎ε∈B : ∀ (A : Language b) (B : Language d) → Null (A ∪ B) → Null A ⊎ Null B
ε∈A∪B⇒ε∈A⊎ε∈B _ _ = id

-- First

c∈First[A]⇒c∈First[A∪B] : ∀ {c} → First A c → First (A ∪ B) c
c∈First[A]⇒c∈First[A∪B] = P.map₂ inj₁

c∈First[B]⇒c∈First[A∪B] : ∀ {c} → First B c → First (A ∪ B) c
c∈First[B]⇒c∈First[A∪B] = P.map₂ inj₂

c∈First[A∪B]⇒c∈First[A]∪c∈First[B] : ∀ {c} → First (A ∪ B) c → First A c ⊎ First B c
c∈First[A∪B]⇒c∈First[A]∪c∈First[B] (_ , cw∈A∪B) = S.map -,_ -,_ cw∈A∪B

-- Flast

c∈Flast[A]⇒c∈Flast[A∪B] : ∀ {c} → Flast A c → Flast (A ∪ B) c
c∈Flast[A]⇒c∈Flast[A∪B] = P.map₂ (P.map₂ (P.map inj₁ (P.map₂ inj₁)))

c∈Flast[B]⇒c∈Flast[A∪B] : ∀ {c} → Flast B c → Flast (A ∪ B) c
c∈Flast[B]⇒c∈Flast[A∪B] = P.map₂ (P.map₂ (P.map inj₂ (P.map₂ inj₂)))

-- TODO: rename this
∄[c∈First[A]∩First[B]]+c∈Flast[A∪B]⇒c∈Flast[A]⊎c∈Flast[B] :
  ∀ {c} → (∀ {x} → ¬ (First A x × First B x)) → Flast (A ∪ B) c → Flast A c ⊎ Flast B c
∄[c∈First[A]∩First[B]]+c∈Flast[A∪B]⇒c∈Flast[A]⊎c∈Flast[B] ∄[f₁∩f₂] (_ , _ , inj₁ xw∈A , _ , inj₁ xwcw′∈A) = inj₁ (-, -, xw∈A , -, xwcw′∈A)
∄[c∈First[A]∩First[B]]+c∈Flast[A∪B]⇒c∈Flast[A]⊎c∈Flast[B] ∄[f₁∩f₂] (_ , _ , inj₁ xw∈A , _ , inj₂ xwcw′∈B) = ⊥-elim (∄[f₁∩f₂] ((-, xw∈A) , (-, xwcw′∈B)))
∄[c∈First[A]∩First[B]]+c∈Flast[A∪B]⇒c∈Flast[A]⊎c∈Flast[B] ∄[f₁∩f₂] (_ , _ , inj₂ xw∈B , _ , inj₁ xwcw′∈A) = ⊥-elim (∄[f₁∩f₂] ((-, xwcw′∈A) , (-, xw∈B)))
∄[c∈First[A]∩First[B]]+c∈Flast[A∪B]⇒c∈Flast[A]⊎c∈Flast[B] ∄[f₁∩f₂] (_ , _ , inj₂ xw∈B , _ , inj₂ xwcw′∈B) = inj₂ (-, -, xw∈B , -, xwcw′∈B)

------------------------------------------------------------------------
-- Algebraic properties of _∪_

∪-mono : X ⊆ Y → U ⊆ V → X ∪ U ⊆ Y ∪ V
∪-mono (sub X⊆Y) (sub U⊆V) = sub (S.map X⊆Y U⊆V)

∪-cong : X ≈ Y → U ≈ V → X ∪ U ≈ Y ∪ V
∪-cong X≈Y U≈V = ⊆-antisym
  (∪-mono (⊆-reflexive X≈Y) (⊆-reflexive U≈V))
  (∪-mono (⊇-reflexive X≈Y) (⊇-reflexive U≈V))

∪-assoc : ∀ (A : Language a) (B : Language b) (C : Language d) → (A ∪ B) ∪ C ≈ A ∪ (B ∪ C)
∪-assoc _ _ _ = ⊆-antisym (sub S.assocʳ) (sub S.assocˡ)

∪-comm : ∀ (A : Language a) (B : Language b) → A ∪ B ≈ B ∪ A
∪-comm _ _ = ⊆-antisym (sub S.swap) (sub S.swap)

∪-identityˡ : ∀ (A : Language a) → ∅ {b} ∪ A ≈ A
∪-identityˡ _ = ⊆-antisym (sub λ { (inj₁ ()) ; (inj₂ w∈A) → w∈A }) (sub inj₂)

∪-identityʳ : ∀ (A : Language a) → A ∪ ∅ {b} ≈ A
∪-identityʳ _ = ⊆-antisym (sub λ { (inj₁ w∈A) → w∈A ; (inj₂ ()) }) (sub inj₁)

∪-identity : (∀ (A : Language a) → ∅ {b} ∪ A ≈ A) × (∀ (A : Language a) → A ∪ ∅ {b} ≈ A)
∪-identity = ∪-identityˡ , ∪-identityʳ

∙-distribˡ-∪ : ∀ (A : Language a) (B : Language b) (C : Language d) → A ∙ (B ∪ C) ≈ A ∙ B ∪ A ∙ C
∙-distribˡ-∪ _ _ _ =
  ⊆-antisym
    (sub λ
      { (_ , _ , w₁∈A , inj₁ w₂∈B , eq) → inj₁ (-, -, w₁∈A , w₂∈B , eq)
      ; (_ , _ , w₁∈A , inj₂ w₂∈C , eq) → inj₂ (-, -, w₁∈A , w₂∈C , eq)
      })
    (sub λ
      { (inj₁ (_ , _ , w₁∈A , w₂∈B , eq)) → -, -, w₁∈A , inj₁ w₂∈B , eq
      ; (inj₂ (_ , _ , w₁∈A , w₂∈C , eq)) → -, -, w₁∈A , inj₂ w₂∈C , eq
      })

∙-distribʳ-∪ : ∀ (A : Language a) (B : Language b) (C : Language d) → (B ∪ C) ∙ A ≈ B ∙ A ∪ C ∙ A
∙-distribʳ-∪ _ _ _ =
  ⊆-antisym
    (sub λ
      { (_ , _ , inj₁ w₁∈B , w₂∈A , eq) → inj₁ (-, -, w₁∈B , w₂∈A , eq)
      ; (_ , _ , inj₂ w₁∈C , w₂∈A , eq) → inj₂ (-, -, w₁∈C , w₂∈A , eq)
      })
    (sub λ
      { (inj₁ (_ , _ , w₁∈B , w₂∈A , eq)) → -, -, inj₁ w₁∈B , w₂∈A , eq
      ; (inj₂ (_ , _ , w₁∈C , w₂∈A , eq)) → -, -, inj₂ w₁∈C , w₂∈A , eq
      })

∙-distrib-∪ :
  (∀ (A : Language a) (B : Language b) (C : Language d) → A ∙ (B ∪ C) ≈ A ∙ B ∪ A ∙ C) ×
  (∀ (A : Language a) (B : Language b) (C : Language d) → (B ∪ C) ∙ A ≈ B ∙ A ∪ C ∙ A)
∙-distrib-∪ = ∙-distribˡ-∪ , ∙-distribʳ-∪

∪-idem : ∀ (A : Language a) → A ∪ A ≈ A
∪-idem A = ⊆-antisym (sub reduce) (sub inj₁)

------------------------------------------------------------------------
-- Structures

∪-isMagma : IsMagma _≈_ (_∪_ {a})
∪-isMagma = record
  { isEquivalence = ≈-isEquivalence
  ; ∙-cong        = ∪-cong
  }

∪-isCommutativeMagma : IsCommutativeMagma _≈_ (_∪_ {a})
∪-isCommutativeMagma = record
  { isMagma = ∪-isMagma
  ; comm    = ∪-comm
  }

∪-isSemigroup : IsSemigroup _≈_ (_∪_ {a})
∪-isSemigroup = record
  { isMagma = ∪-isMagma
  ; assoc   = ∪-assoc
  }

∪-isBand : IsBand _≈_ (_∪_ {a})
∪-isBand = record
  { isSemigroup = ∪-isSemigroup
  ; idem        = ∪-idem
  }

∪-isCommutativeSemigroup : IsCommutativeSemigroup _≈_ (_∪_ {a})
∪-isCommutativeSemigroup = record
  { isSemigroup = ∪-isSemigroup
  ; comm        = ∪-comm
  }

∪-isSemilattice : IsSemilattice _≈_ (_∪_ {a})
∪-isSemilattice = record
  { isBand = ∪-isBand
  ; comm   = ∪-comm
  }

∪-isMonoid : IsMonoid _≈_ _∪_ (∅ {a})
∪-isMonoid = record
  { isSemigroup = ∪-isSemigroup
  ; identity    = ∪-identity
  }

∪-isCommutativeMonoid : IsCommutativeMonoid _≈_ _∪_ (∅ {a})
∪-isCommutativeMonoid = record
  { isMonoid = ∪-isMonoid
  ; comm     = ∪-comm
  }

∪-isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid _≈_ _∪_ (∅ {a})
∪-isIdempotentCommutativeMonoid = record
  { isCommutativeMonoid = ∪-isCommutativeMonoid
  ; idem                = ∪-idem
  }

∪-∙-isNearSemiring : IsNearSemiring _≈_ _∪_ _∙_ (∅ {c ⊔ ℓ ⊔ a})
∪-∙-isNearSemiring {a} = record
  { +-isMonoid    = ∪-isMonoid
  ; *-isSemigroup = ∙-isSemigroup {a}
  ; distribʳ      = ∙-distribʳ-∪
  ; zeroˡ         = ∙-zeroˡ
  }

∪-∙-isSemiringWithoutOne : IsSemiringWithoutOne _≈_ _∪_ _∙_ (∅ {c ⊔ ℓ ⊔ a})
∪-∙-isSemiringWithoutOne {a} = record
  { +-isCommutativeMonoid = ∪-isCommutativeMonoid
  ; *-isSemigroup         = ∙-isSemigroup {a}
  ; distrib               = ∙-distrib-∪
  ; zero                  = ∙-zero
  }

∪-∙-isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero _≈_ _∪_ _∙_ ∅ (｛ε｝ {ℓ ⊔ a})
∪-∙-isSemiringWithoutAnnihilatingZero {a} = record
  { +-isCommutativeMonoid = ∪-isCommutativeMonoid
  ; *-isMonoid            = ∙-isMonoid {a}
  ; distrib               = ∙-distrib-∪
  }

∪-∙-isSemiring : IsSemiring _≈_ _∪_ _∙_ ∅ (｛ε｝ {ℓ ⊔ a})
∪-∙-isSemiring {a} = record
  { isSemiringWithoutAnnihilatingZero = ∪-∙-isSemiringWithoutAnnihilatingZero {a}
  ; zero                              = ∙-zero
  }

------------------------------------------------------------------------
-- Bundles

∪-magma : ∀ {a} → Magma _ _
∪-magma {a} = record { isMagma = ∪-isMagma {a} }

∪-commutativeMagma : ∀ {a} → CommutativeMagma _ _
∪-commutativeMagma {a} = record { isCommutativeMagma = ∪-isCommutativeMagma {a} }

∪-semigroup : ∀ {a} → Semigroup _ _
∪-semigroup {a} = record { isSemigroup = ∪-isSemigroup {a} }

∪-band : ∀ {a} → Band _ _
∪-band {a} = record { isBand = ∪-isBand {a} }

∪-commutativeSemigroup : ∀ {a} → CommutativeSemigroup _ _
∪-commutativeSemigroup {a} = record { isCommutativeSemigroup = ∪-isCommutativeSemigroup {a} }

∪-semilattice : ∀ {a} → Semilattice _ _
∪-semilattice {a} = record { isSemilattice = ∪-isSemilattice {a} }

∪-monoid : ∀ {a} → Monoid _ _
∪-monoid {a} = record { isMonoid = ∪-isMonoid {a} }

∪-commutativeMonoid : ∀ {a} → CommutativeMonoid _ _
∪-commutativeMonoid {a} = record { isCommutativeMonoid = ∪-isCommutativeMonoid {a} }

∪-idempotentCommutativeMonoid : ∀ {a} → IdempotentCommutativeMonoid _ _
∪-idempotentCommutativeMonoid {a} = record
  { isIdempotentCommutativeMonoid = ∪-isIdempotentCommutativeMonoid {a} }

∪-∙-nearSemiring : ∀ {a} → NearSemiring _ _
∪-∙-nearSemiring {a} = record { isNearSemiring = ∪-∙-isNearSemiring {a} }

∪-∙-semiringWithoutOne : ∀ {a} → SemiringWithoutOne _ _
∪-∙-semiringWithoutOne {a} = record { isSemiringWithoutOne = ∪-∙-isSemiringWithoutOne {a} }

∪-∙-semiringWithoutAnnihilatingZero : ∀ {a} → SemiringWithoutAnnihilatingZero _ _
∪-∙-semiringWithoutAnnihilatingZero {a} = record { isSemiringWithoutAnnihilatingZero = ∪-∙-isSemiringWithoutAnnihilatingZero {a} }

∪-∙-semiring : ∀ {a} → Semiring _ _
∪-∙-semiring {a} = record { isSemiring = ∪-∙-isSemiring {a} }

------------------------------------------------------------------------
-- Other properties of _∪_

∪-selective :
  ¬ (Null A × Null B) →
  (∀ {c} → ¬ (First A c × First B c)) →
  ∀ {w} → w ∈ A ∪ B → (w ∈ A × w ∉ B) ⊎ (w ∉ A × w ∈ B)
∪-selective ε∉A∩B ∄[f₁∩f₂] {[]}    (inj₁ ε∈A) = inj₁ (ε∈A , ε∉A∩B ∘ (ε∈A ,_))
∪-selective ε∉A∩B ∄[f₁∩f₂] {c ∷ w} (inj₁ cw∈A) = inj₁ (cw∈A , ∄[f₁∩f₂] ∘ ((w , cw∈A) ,_) ∘ (w ,_))
∪-selective ε∉A∩B ∄[f₁∩f₂] {[]}    (inj₂ ε∈B) = inj₂ (ε∉A∩B ∘ (_, ε∈B) , ε∈B)
∪-selective ε∉A∩B ∄[f₁∩f₂] {c ∷ w} (inj₂ cw∈B) = inj₂ (∄[f₁∩f₂] ∘ (_, (w , cw∈B)) ∘ (w ,_) , cw∈B)

------------------------------------------------------------------------
-- Proof properties of _∪_

_∪?_ : Decidable A → Decidable B → Decidable (A ∪ B)
(A? ∪? B?) w = A? w ⊎-dec B? w

------------------------------------------------------------------------
-- Properties of Iter
------------------------------------------------------------------------
-- Membership properties of Iter

FⁿFA≡Fⁿ⁺¹A : ∀ n → Iter {a} F (F A) n ≡ Iter F A (suc n)
FⁿFA≡Fⁿ⁺¹A         zero    = refl
FⁿFA≡Fⁿ⁺¹A {F = F} (suc n) = cong F (FⁿFA≡Fⁿ⁺¹A n)

Iter-monoˡ : (∀ {A B} → A ⊆ B → F A ⊆ G B) → ∀ n → A ⊆ B → Iter F A n ⊆ Iter G B n
Iter-monoˡ mono zero    A⊆B = A⊆B
Iter-monoˡ mono (suc n) A⊆B = mono (Iter-monoˡ mono n A⊆B)

Iter-congˡ : (∀ {A B} → A ≈ B → F A ≈ G B) → ∀ n → A ≈ B → Iter F A n ≈ Iter G B n
Iter-congˡ cong zero    A≈B = A≈B
Iter-congˡ cong (suc n) A≈B = cong (Iter-congˡ cong n A≈B)

Iter-step : (∀ {A B} → A ⊆ B → F A ⊆ F B) → A ⊆ F A → ∀ n → Iter F A n ⊆ Iter F A (suc n)
Iter-step mono A⊆FA zero    = A⊆FA
Iter-step mono A⊆FA (suc n) = mono (Iter-step mono A⊆FA n)

Iter-monoʳ : (∀ {A B} → A ⊆ B → F A ⊆ F B) → A ⊆ F A → ∀ {m n} → m ≤ n → Iter F A m ⊆ Iter F A n
Iter-monoʳ                 mono A⊆FA {n = zero}  z≤n       = ⊆-refl
Iter-monoʳ {F = F} {A = A} mono A⊆FA {n = suc n} z≤n       = begin
  A              ⊆⟨ A⊆FA ⟩
  F A            ⊆⟨ mono (Iter-monoʳ mono A⊆FA {n = n} z≤n) ⟩
  F (Iter F A n) ∎
  where open ⊆-Reasoning
Iter-monoʳ                 mono A⊆FA             (s≤s m≤n) = mono (Iter-monoʳ mono A⊆FA m≤n)

------------------------------------------------------------------------
-- Properties of Sup
------------------------------------------------------------------------
-- Membership properties of Sup

FⁿA⊆SupFA : ∀ n → Iter F A n ⊆ Sup F A
FⁿA⊆SupFA n = sub (n ,_)

FⁿFA⊆SupFA : ∀ n → Iter F (F A) n ⊆ Sup F A
FⁿFA⊆SupFA {F = F} {A = A} n = begin
  Iter F (F A) n   ≡⟨ FⁿFA≡Fⁿ⁺¹A n ⟩
  Iter F A (suc n) ⊆⟨ FⁿA⊆SupFA (suc n) ⟩
  Sup F A          ∎
  where open ⊆-Reasoning

∀[FⁿA⊆B]⇒SupFA⊆B : (∀ n → Iter F A n ⊆ B) → Sup F A ⊆ B
∀[FⁿA⊆B]⇒SupFA⊆B FⁿA⊆B = sub λ (n , w∈FⁿA) → ∈-resp-⊆ (FⁿA⊆B n) w∈FⁿA

∃[B⊆FⁿA]⇒B⊆SupFA : ∀ n → B ⊆ Iter F A n → B ⊆ Sup F A
∃[B⊆FⁿA]⇒B⊆SupFA n B⊆FⁿA = sub λ w∈B → n , ∈-resp-⊆ B⊆FⁿA w∈B

∀[FⁿA≈GⁿB]⇒SupFA≈SupGB : (∀ n → Iter F A n ≈ Iter G B n) → Sup F A ≈ Sup G B
∀[FⁿA≈GⁿB]⇒SupFA≈SupGB FⁿA≈GⁿB =
  ⊆-antisym
    (sub λ (n , w∈FⁿA) → n , ∈-resp-≈ (FⁿA≈GⁿB n) w∈FⁿA)
    (sub λ (n , w∈GⁿB) → n , ∈-resp-≈ (≈-sym (FⁿA≈GⁿB n)) w∈GⁿB)
------------------------------------------------------------------------
-- Properties of ⋃_
------------------------------------------------------------------------
-- Membership properties of ⋃_

Fⁿ⊆⋃F : ∀ n → Iter F ∅ n ⊆ ⋃ F
Fⁿ⊆⋃F = FⁿA⊆SupFA

∀[Fⁿ⊆B]⇒⋃F⊆B : (∀ n → Iter F ∅ n ⊆ B) → ⋃ F ⊆ B
∀[Fⁿ⊆B]⇒⋃F⊆B = ∀[FⁿA⊆B]⇒SupFA⊆B

∃[B⊆Fⁿ]⇒B⊆⋃F : ∀ n → B ⊆ Iter F ∅ n → B ⊆ ⋃ F
∃[B⊆Fⁿ]⇒B⊆⋃F = ∃[B⊆FⁿA]⇒B⊆SupFA

∀[Fⁿ≈Gⁿ]⇒⋃F≈⋃G : (∀ n → Iter F ∅ n ≈ Iter G ∅ n) → ⋃ F ≈ ⋃ G
∀[Fⁿ≈Gⁿ]⇒⋃F≈⋃G = ∀[FⁿA≈GⁿB]⇒SupFA≈SupGB

------------------------------------------------------------------------
-- Functional properties of ⋃_

⋃-mono : (∀ {A B} → A ⊆ B → F A ⊆ G B) → ⋃ F ⊆ ⋃ G
⋃-mono {F = F} {G = G} mono-ext = ∀[Fⁿ⊆B]⇒⋃F⊆B λ n → (begin
  Iter F ∅ n ⊆⟨ Iter-monoˡ mono-ext n (⊆-min ∅) ⟩
  Iter G ∅ n ⊆⟨ Fⁿ⊆⋃F n ⟩
  ⋃ G        ∎)
  where open ⊆-Reasoning

⋃-cong : (∀ {A B} → A ≈ B → F A ≈ G B) → ⋃ F ≈ ⋃ G
⋃-cong ext = ∀[Fⁿ≈Gⁿ]⇒⋃F≈⋃G λ n → Iter-congˡ ext n (⊆-antisym (⊆-min ∅) (⊆-min ∅))

⋃-inverseʳ : ∀ (A : Language a) → ⋃ (const A) ≈ A
⋃-inverseʳ _ = ⊆-antisym (sub λ {(suc _ , w∈A) → w∈A}) (Fⁿ⊆⋃F 1)

⋃-unroll : (∀ {A B} → A ⊆ B → F A ⊆ F B) → ⋃ F ⊆ F (⋃ F)
⋃-unroll {F = F} mono-ext = ∀[Fⁿ⊆B]⇒⋃F⊆B λ
  { zero    → ⊆-min (F (⋃ F))
  ; (suc n) → mono-ext (Fⁿ⊆⋃F n)
  }

------------------------------------------------------------------------
-- Other properties of Null
------------------------------------------------------------------------

∣w∣≡0+w∈A⇒ε∈A : ∀ {w} → length w ≡ 0 → w ∈ A → Null A
∣w∣≡0+w∈A⇒ε∈A {w = []} _ ε∈A = ε∈A