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

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

open import Algebra
import Algebra.Lattice.Properties.BooleanAlgebra
open import Codata.Musical.Notation
open import Data.Bool hiding (_∧_; _≤_)
import Data.Bool.Properties as Bool
private
  module BoolCS = CommutativeSemiring Bool.∨-∧-commutativeSemiring
  module BoolBA = Algebra.Lattice.Properties.BooleanAlgebra
                    Bool.∨-∧-booleanAlgebra
open import Function.Base
open import Function.Bundles renaming (module Equivalence to Eq)
import Function.Properties.Equivalence as Eq
open import Data.List
open import Data.List.Properties
private
  module ListMonoid {A : Set} = Monoid (++-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.Binary.Structures
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₁ = mk⇔ 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 = IsEquivalence.refl Eq.isEquivalence

  sym :  {n₁ n₂} {p₁ : P n₁} {p₂ : P n₂}  p₁  p₂  p₂  p₁
  sym p₁≈p₂ = IsEquivalence.sym Eq.isEquivalence 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₃ = IsEquivalence.trans Eq.isEquivalence 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₂ = mk⇔ (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₄ =
  Eq.from ≈⇔≤≥ $
  Prod.zip helper helper (Eq.to ≈⇔≤≥ p₁≈p₃) (Eq.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₂ = Eq.from ≈⇔≤≥ $ Prod.map helper helper (Eq.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 =
  Eq.from ≈⇔≤≥ $ Prod.map (helper i) (helper i) (Eq.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 4 _≲_

-- 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₂ =
  mk⇔
     (p₁≤p₂ : p₁  p₂) {_} 
       mk⇔ (helper p₁≤p₂) (∣-right {n₁ = n₁}))
     (p₁≲p₂ : p₁  p₂) s∈p₁  Eq.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 = n} p = BoolBA.∨-idem n  λ t   ∣-idempotent (D t p)

-- Multiplicative monoid.

empty-left-identity :  {n} (p : P n)  empty  p  p
empty-left-identity {n} p = mk⇔ 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 =
  mk⇔
    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₃ = mk⇔ 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₃ = mk⇔ 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₃ = mk⇔ 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 = mk⇔ 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 = mk⇔ 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  Eq.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₃