------------------------------------------------------------------------
-- Recognisers form a Kleene algebra
------------------------------------------------------------------------

module TotalRecognisers.LeftRecursion.KleeneAlgebra (Tok : Set) where

open import Algebra
import Algebra.Props.BooleanAlgebra
open import Coinduction
open import Data.Bool hiding (_∧_)
import Data.Bool.Properties as Bool
private
  module BoolCS = CommutativeSemiring Bool.commutativeSemiring-∨-∧
  module BoolBA = Algebra.Props.BooleanAlgebra Bool.booleanAlgebra
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence as Eq
  using (_⇔_; equivalent; module Equivalent)
open import Data.List as List
private
  module ListMonoid {A : Set} = Monoid (List.monoid A)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Product as Prod
open import Relation.Binary.HeterogeneousEquality using (_≅_; refl)
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; refl; _≗_)
open import Relation.Nullary

import TotalRecognisers.LeftRecursion
open TotalRecognisers.LeftRecursion Tok hiding (left-zero)
import TotalRecognisers.LeftRecursion.Lib
open TotalRecognisers.LeftRecursion.Lib Tok
open ⊙ using (_⊙′_)
open KleeneStar₂

------------------------------------------------------------------------
-- The relation _≤_ is a partial order with respect to _≈_

module PartialOrder where

  reflexive : ∀ {n} {p : P n} → p ≤ p
  reflexive = id

  trans : ∀ {n₁ n₂ n₃} {p₁ : P n₁} {p₂ : P n₂} {p₃ : P n₃} →
          p₁ ≤ p₂ → p₂ ≤ p₃ → p₁ ≤ p₃
  trans p₁≤p₂ p₂≤p₃ = p₂≤p₃ ∘ p₁≤p₂

  antisym : ∀ {n₁ n₂} {p₁ : P n₁} {p₂ : P n₂} →
            p₁ ≤ p₂ → p₂ ≤ p₁ → p₁ ≈ p₂
  antisym p₁≤p₂ p₂≤p₁ = equivalent p₁≤p₂ p₂≤p₁

------------------------------------------------------------------------
-- The relation _≈_ is an equality, i.e. a congruential equivalence
-- relation

module Equivalence where

  reflexive : ∀ {n} {p : P n} → p ≈ p
  reflexive = Eq.id

  sym : ∀ {n₁ n₂} {p₁ : P n₁} {p₂ : P n₂} → p₁ ≈ p₂ → p₂ ≈ p₁
  sym p₁≈p₂ = Eq.sym p₁≈p₂

  trans : ∀ {n₁ n₂ n₃} {p₁ : P n₁} {p₂ : P n₂} {p₃ : P n₃} →
          p₁ ≈ p₂ → p₂ ≈ p₃ → p₁ ≈ p₃
  trans p₁≈p₂ p₂≈p₃ = Eq._∘_ p₂≈p₃ p₁≈p₂

♭♯-cong : ∀ {n₁ n₂} b₁ b₂ {p₁ : P n₁} {p₂ : P n₂} →
          p₁ ≈ p₂ → ♭? (♯? {b₁} p₁) ≈ ♭? (♯? {b₂} p₂)
♭♯-cong b₁ b₂ {p₁} {p₂} rewrite ♭?♯? b₁ {p = p₁} | ♭?♯? b₂ {p = p₂} = id

fail-cong : fail ≈ fail
fail-cong = Equivalence.reflexive

empty-cong : empty ≈ empty
empty-cong = Equivalence.reflexive

sat-cong : {f₁ f₂ : Tok → Bool} → f₁ ≗ f₂ → sat f₁ ≈ sat f₂
sat-cong f₁≗f₂ = equivalent (helper f₁≗f₂) (helper (P.sym ∘ f₁≗f₂))
  where
  helper : {f₁ f₂ : Tok → Bool} → f₁ ≗ f₂ → sat f₁ ≤ sat f₂
  helper f₁≗f₂ (sat ok) = sat (P.subst T (f₁≗f₂ _) ok)

∣-cong : ∀ {n₁ n₂ n₃ n₄}
           {p₁ : P n₁} {p₂ : P n₂} {p₃ : P n₃} {p₄ : P n₄} →
         p₁ ≈′ p₃ → p₂ ≈′ p₄ → p₁ ∣ p₂ ≈′ p₃ ∣ p₄
∣-cong (refl ∷ rest₁) (refl ∷ rest₂) =
  refl ∷ λ t → ♯ ∣-cong (♭ (rest₁ t)) (♭ (rest₂ t))

·-cong : ∀ {n₁ n₂ n₃ n₄}
           {p₁ : ∞⟨ n₂ ⟩P n₁} {p₂ : ∞⟨ n₁ ⟩P n₂}
           {p₃ : ∞⟨ n₄ ⟩P n₃} {p₄ : ∞⟨ n₃ ⟩P n₄} →
         ♭? p₁ ≈ ♭? p₃ → ♭? p₂ ≈ ♭? p₄ → p₁ · p₂ ≈ p₃ · p₄
·-cong p₁≈p₃ p₂≈p₄ =
  Equivalent.from ≈⇔≤≥ ⟨$⟩
    Prod.zip helper helper
             (Equivalent.to ≈⇔≤≥ ⟨$⟩ p₁≈p₃)
             (Equivalent.to ≈⇔≤≥ ⟨$⟩ p₂≈p₄)
  where
  helper : ∀ {n₁ n₂ n₃ n₄}
             {p₁ : ∞⟨ n₂ ⟩P n₁} {p₂ : ∞⟨ n₁ ⟩P n₂}
             {p₃ : ∞⟨ n₄ ⟩P n₃} {p₄ : ∞⟨ n₃ ⟩P n₄} →
           ♭? p₁ ≤ ♭? p₃ → ♭? p₂ ≤ ♭? p₄ → p₁ · p₂ ≤ p₃ · p₄
  helper ₁≤₃ ₂≤₄ (∈p₁ · ∈p₂) = ₁≤₃ ∈p₁ · ₂≤₄ ∈p₂

⊙-cong : ∀ {n₁ n₂ n₃ n₄}
           {p₁ : P n₁} {p₂ : P n₂} {p₃ : P n₃} {p₄ : P n₄} →
         p₁ ≈ p₃ → p₂ ≈ p₄ → p₁ ⊙ p₂ ≈ p₃ ⊙ p₄
⊙-cong {n₁} {n₂} {n₃} {n₄} ₁≈₃ ₂≈₄ =
  ·-cong (♭♯-cong n₂ n₄ ₁≈₃) (♭♯-cong n₁ n₃ ₂≈₄)

nonempty-cong : ∀ {n₁ n₂} {p₁ : P n₁} {p₂ : P n₂} →
                p₁ ≈′ p₂ → nonempty p₁ ≈′ nonempty p₂
nonempty-cong (_ ∷ rest) = refl ∷ rest

cast-cong : ∀ {n₁ n₂ n₁′ n₂′}
              {p₁ : P n₁} {p₂ : P n₂}
              {eq₁ : n₁ ≡ n₁′} {eq₂ : n₂ ≡ n₂′} →
            p₁ ≈′ p₂ → cast eq₁ p₁ ≈′ cast eq₂ p₂
cast-cong {eq₁ = refl} {refl} (init ∷ rest) = init ∷ rest

⋆-cong : ∀ {n₁ n₂} {p₁ : P n₁} {p₂ : P n₂} →
         p₁ ≈ p₂ → p₁ ⋆ ≈ p₂ ⋆
⋆-cong p₁≈p₂ = Equivalent.from ≈⇔≤≥ ⟨$⟩
                 Prod.map helper helper
                   (Equivalent.to ≈⇔≤≥ ⟨$⟩ p₁≈p₂)
  where
  helper : ∀ {n₁ n₂} {p₁ : P n₁} {p₂ : P n₂} →
           p₁ ≤ p₂ → p₁ ⋆ ≤ p₂ ⋆
  helper p₁≤p₂ (∣-left  empty)                 = ∣-left empty
  helper p₁≤p₂ (∣-right (nonempty ∈p₁ · ∈p₁⋆)) =
    ∣-right {p₁ = empty} (nonempty (p₁≤p₂ ∈p₁) · helper p₁≤p₂ ∈p₁⋆)

^-cong : ∀ {n₁ n₂ i₁ i₂} {p₁ : P n₁} {p₂ : P n₂} →
         p₁ ≈ p₂ → i₁ ≡ i₂ → p₁ ^ i₁ ≈ p₂ ^ i₂
^-cong {i₁ = i} p₁≈p₂ refl =
  Equivalent.from ≈⇔≤≥ ⟨$⟩
    Prod.map (helper i) (helper i)
             (Equivalent.to ≈⇔≤≥ ⟨$⟩ p₁≈p₂)
  where
  helper : ∀ {n₁ n₂} {p₁ : P n₁} {p₂ : P n₂} i →
           p₁ ≤ p₂ → p₁ ^ i ≤ p₂ ^ i
  helper           zero    p₁≤p₂ empty   = empty
  helper {n₁} {n₂} (suc i) p₁≤p₂ ∈p₁⊙p₁ⁱ
    with ⊙.sound ⟨ n₁ ^ i ⟩-nullable ∈p₁⊙p₁ⁱ
  ... | ∈p₁ ⊙′ ∈p₁ⁱ = ⊙.complete (p₁≤p₂ ∈p₁) (helper i p₁≤p₂ ∈p₁ⁱ)

------------------------------------------------------------------------
-- A variant of _≤_

infix  _≲_

-- If _∣_ is viewed as the join operation of a join-semilattice, then
-- the following definition of order is natural.

_≲_ : ∀ {n₁ n₂} → P n₁ → P n₂ → Set
p₁ ≲ p₂ = p₁ ∣ p₂ ≈ p₂

-- The order above coincides with _≤_.

≤⇔≲ : ∀ {n₁ n₂} (p₁ : P n₁) (p₂ : P n₂) → p₁ ≤ p₂ ⇔ p₁ ≲ p₂
≤⇔≲ {n₁} p₁ p₂ =
  equivalent
    (λ (p₁≤p₂ : p₁ ≤ p₂) {_} →
       equivalent (helper p₁≤p₂) (∣-right {n₁ = n₁}))
    (λ (p₁≲p₂ : p₁ ≲ p₂) s∈p₁ → Equivalent.to p₁≲p₂ ⟨$⟩ ∣-left s∈p₁)
  where
  helper : p₁ ≤ p₂ → p₁ ∣ p₂ ≤ p₂
  helper p₁≤p₂ (∣-left  s∈p₁) = p₁≤p₂ s∈p₁
  helper p₁≤p₂ (∣-right s∈p₂) = s∈p₂

------------------------------------------------------------------------
-- Recognisers form a *-continuous Kleene algebra

-- The definition of *-continuous Kleene algebras used here is the one
-- given by Kozen in "On Kleene Algebras and Closed Semirings", except
-- for the presence of the recogniser indices. Kozen used the order
-- _≲_ in his definition, but as shown above this order is equivalent
-- to _≤_.

-- Additive idempotent commutative monoid. (One of the identity lemmas
-- could be omitted.)

∣-commutative : ∀ {n₁ n₂} (p₁ : P n₁) (p₂ : P n₂) → p₁ ∣ p₂ ≈′ p₂ ∣ p₁
∣-commutative {n₁} {n₂} p₁ p₂ =
  BoolCS.+-comm n₁ n₂ ∷ λ t → ♯ ∣-commutative (D t p₁) (D t p₂)

fail-left-identity : ∀ {n} (p : P n) → fail ∣ p ≈′ p
fail-left-identity p = refl ∷ λ t → ♯ fail-left-identity (D t p)

fail-right-identity : ∀ {n} (p : P n) → p ∣ fail ≈′ p
fail-right-identity {n} p =
  proj₂ BoolCS.+-identity n ∷ λ t → ♯ fail-right-identity (D t p)

∣-associative : ∀ {n₁ n₂ n₃} (p₁ : P n₁) (p₂ : P n₂) (p₃ : P n₃) →
                p₁ ∣ (p₂ ∣ p₃) ≈′ (p₁ ∣ p₂) ∣ p₃
∣-associative {n₁} {n₂} {n₃} p₁ p₂ p₃ =
  P.sym (BoolCS.+-assoc n₁ n₂ n₃) ∷ λ t →
    ♯ ∣-associative (D t p₁) (D t p₂) (D t p₃)

∣-idempotent : ∀ {n} (p : P n) → p ∣ p ≈′ p
∣-idempotent {n} p =
  BoolBA.∨-idempotent n ∷ λ t → ♯ ∣-idempotent (D t p)

-- Multiplicative monoid.

empty-left-identity : ∀ {n} (p : P n) → empty ⊙ p ≈ p
empty-left-identity {n} p =
  equivalent helper (λ s∈p → ⊙.complete empty s∈p)
  where
  helper : empty ⊙ p ≤ p
  helper ∈empty⊙p with ⊙.sound n ∈empty⊙p
  ... | empty ⊙′ s∈p = s∈p

empty-right-identity : ∀ {n} (p : P n) → p ⊙ empty ≈ p
empty-right-identity {n} p =
  equivalent
    helper
    (λ s∈p → cast∈ (proj₂ ListMonoid.identity _) refl
                   (⊙.complete s∈p empty))
  where
  helper : ∀ {s} → s ∈ p ⊙ empty → s ∈ p
  helper ∈p⊙empty with ⊙.sound true ∈p⊙empty
  helper ∈p⊙empty | ∈p ⊙′ empty =
    cast∈ (P.sym (proj₂ ListMonoid.identity _)) refl ∈p

·-associative : ∀ {n₁ n₂ n₃} (p₁ : P n₁) (p₂ : P n₂) (p₃ : P n₃) →
                p₁ ⊙ (p₂ ⊙ p₃) ≈ (p₁ ⊙ p₂) ⊙ p₃
·-associative {n₁} {n₂} {n₃} p₁ p₂ p₃ = equivalent helper₁ helper₂
  where
  helper₁ : p₁ ⊙ (p₂ ⊙ p₃) ≤ (p₁ ⊙ p₂) ⊙ p₃
  helper₁ ∈⊙⊙ with ⊙.sound (n₂ ∧ n₃) ∈⊙⊙
  ... | _⊙′_ {s₁ = s₁} ∈p₁ ∈⊙ with ⊙.sound n₃ ∈⊙
  ...   | ∈p₂ ⊙′ ∈p₃ =
    cast∈ (ListMonoid.assoc s₁ _ _) refl $
      ⊙.complete (⊙.complete ∈p₁ ∈p₂) ∈p₃

  helper₂ : (p₁ ⊙ p₂) ⊙ p₃ ≤ p₁ ⊙ (p₂ ⊙ p₃)
  helper₂ ∈⊙⊙ with ⊙.sound n₃ ∈⊙⊙
  ... | ∈⊙ ⊙′ ∈p₃ with ⊙.sound n₂ ∈⊙
  ...   | _⊙′_ {s₁ = s₁} ∈p₁ ∈p₂ =
    cast∈ (P.sym $ ListMonoid.assoc s₁ _ _) refl $
      ⊙.complete ∈p₁ (⊙.complete ∈p₂ ∈p₃)

-- Distributivity.

left-distributive :
  ∀ {n₁ n₂ n₃} (p₁ : P n₁) (p₂ : P n₂) (p₃ : P n₃) →
  p₁ ⊙ (p₂ ∣ p₃) ≈ p₁ ⊙ p₂ ∣ p₁ ⊙ p₃
left-distributive {n₁} {n₂} {n₃} p₁ p₂ p₃ = equivalent helper₁ helper₂
  where
  helper₁ : p₁ ⊙ (p₂ ∣ p₃) ≤ p₁ ⊙ p₂ ∣ p₁ ⊙ p₃
  helper₁ ∈⊙∣ with ⊙.sound (n₂ ∨ n₃) ∈⊙∣
  ... | ∈p₁ ⊙′ ∣-left  ∈p₂ = ∣-left $ ⊙.complete ∈p₁ ∈p₂
  ... | ∈p₁ ⊙′ ∣-right ∈p₃ = ∣-right {n₁ = n₁ ∧ n₂} $ ⊙.complete ∈p₁ ∈p₃

  helper₂ : p₁ ⊙ p₂ ∣ p₁ ⊙ p₃ ≤ p₁ ⊙ (p₂ ∣ p₃)
  helper₂ (∣-left ∈⊙) with ⊙.sound n₂ ∈⊙
  ... | ∈p₁ ⊙′ ∈p₂ = ⊙.complete ∈p₁ (∣-left ∈p₂)
  helper₂ (∣-right ∈⊙) with ⊙.sound n₃ ∈⊙
  ... | ∈p₁ ⊙′ ∈p₃ = ⊙.complete ∈p₁ (∣-right {n₁ = n₂} ∈p₃)

right-distributive :
  ∀ {n₁ n₂ n₃} (p₁ : P n₁) (p₂ : P n₂) (p₃ : P n₃) →
  (p₁ ∣ p₂) ⊙ p₃ ≈ p₁ ⊙ p₃ ∣ p₂ ⊙ p₃
right-distributive {n₁} {n₂} {n₃} p₁ p₂ p₃ = equivalent helper₁ helper₂
  where
  helper₁ : (p₁ ∣ p₂) ⊙ p₃ ≤ p₁ ⊙ p₃ ∣ p₂ ⊙ p₃
  helper₁ ∈∣⊙ with ⊙.sound n₃ ∈∣⊙
  ... | ∣-left  ∈p₁ ⊙′ ∈p₃ = ∣-left $ ⊙.complete ∈p₁ ∈p₃
  ... | ∣-right ∈p₂ ⊙′ ∈p₃ = ∣-right {n₁ = n₁ ∧ n₃} $ ⊙.complete ∈p₂ ∈p₃

  helper₂ : p₁ ⊙ p₃ ∣ p₂ ⊙ p₃ ≤ (p₁ ∣ p₂) ⊙ p₃
  helper₂ (∣-left ∈⊙) with ⊙.sound n₃ ∈⊙
  ... | ∈p₁ ⊙′ ∈p₃ = ⊙.complete (∣-left ∈p₁) ∈p₃
  helper₂ (∣-right ∈⊙) with ⊙.sound n₃ ∈⊙
  ... | ∈p₂ ⊙′ ∈p₃ = ⊙.complete (∣-right {n₁ = n₁} ∈p₂) ∈p₃

-- Zero.

left-zero : ∀ {n} (p : P n) → fail ⊙ p ≈ fail
left-zero {n} p = equivalent helper (λ ())
  where
  helper : fail ⊙ p ≤ fail
  helper ∈fail⊙ with ⊙.sound n ∈fail⊙
  ... | () ⊙′ _

right-zero : ∀ {n} (p : P n) → p ⊙ fail ≈ fail
right-zero {n} p = equivalent helper (λ ())
  where
  helper : p ⊙ fail ≤ fail
  helper ∈⊙fail with ⊙.sound false ∈⊙fail
  ... | _ ⊙′ ()

-- *-continuity.

*-continuity-upper-bound :
  ∀ {n₁ n₂ n₃} (p₁ : P n₁) (p₂ : P n₂) (p₃ : P n₃) →
  ∀ i → p₁ ⊙ p₂ ^ i ⊙ p₃ ≤ p₁ ⊙ p₂ ⋆ ⊙ p₃
*-continuity-upper-bound {n₁} {n₂} {n₃} _ _ _ i ∈⊙ⁱ⊙
  with ⊙.sound n₃ ∈⊙ⁱ⊙
... | ∈⊙ⁱ ⊙′ ∈p₃ with ⊙.sound ⟨ n₂ ^ i ⟩-nullable ∈⊙ⁱ
...   | ∈p₁ ⊙′ ∈p₂ⁱ = ⊙.complete (⊙.complete ∈p₁ (^≤⋆ i ∈p₂ⁱ)) ∈p₃

*-continuity-least-upper-bound :
  ∀ {n₁ n₂ n₃ n} (p₁ : P n₁) (p₂ : P n₂) (p₃ : P n₃) (p : P n) →
  (∀ i → p₁ ⊙ p₂ ^ i ⊙ p₃ ≤ p) → p₁ ⊙ p₂ ⋆ ⊙ p₃ ≤ p
*-continuity-least-upper-bound {n₁} {n₂} {n₃} {n} p₁ p₂ p₃ p ub =
  helper ∘ _⟨$⟩_ (Equivalent.from $ ·-associative p₁ (p₂ ⋆) p₃)
  where
  helper : p₁ ⊙ (p₂ ⋆ ⊙ p₃) ≤ p
  helper ∈⊙⋆⊙ with ⊙.sound (true ∧ n₃) ∈⊙⋆⊙
  ... | _⊙′_ {s₁ = s₁} ∈p₁ ∈⋆⊙ with ⊙.sound n₃ ∈⋆⊙
  ...   | ∈p₂⋆ ⊙′ ∈p₃ with ⋆≤^ ∈p₂⋆
  ...     | (i , ∈p₂ⁱ) =
    cast∈ (ListMonoid.assoc s₁ _ _) refl $
      ub i $ ⊙.complete (⊙.complete ∈p₁ ∈p₂ⁱ) ∈p₃