```------------------------------------------------------------------------
-- Simple recognisers
------------------------------------------------------------------------

open import Relation.Binary
open import Relation.Binary.PropositionalEquality hiding ([_])

-- The recognisers are parametrised on the alphabet.

module TotalRecognisers.Simple
(Tok : Set)
(_≟_ : Decidable (_≡_ {A = Tok}))
-- The tokens must come with decidable equality.
where

open import Algebra
open import Coinduction
open import Data.Bool hiding (_≟_)
import Data.Bool.Properties as Bool
private
module BoolCS = CommutativeSemiring Bool.commutativeSemiring-∧-∨
open import Function
open import Data.List
open import Data.Product
open import Relation.Nullary

------------------------------------------------------------------------
-- Recogniser combinators

infixl 10 _·_
infixl  5 _∣_

mutual

-- The index is true if the corresponding language contains the
-- empty string (is nullable).

data P : Bool → Set where
fail  : P false
empty : P true
tok   : Tok → P false
_∣_   : ∀ {n₁ n₂} → P n₁ →            P n₂ → P (n₁ ∨ n₂)
_·_   : ∀ {n₁ n₂} → P n₁ → ∞⟨ not n₁ ⟩P n₂ → P (n₁ ∧ n₂)

-- Coinductive if the index is true.

∞⟨_⟩P : Bool → Bool → Set
∞⟨ true  ⟩P n = ∞ (P n)
∞⟨ false ⟩P n =    P n

------------------------------------------------------------------------
-- Conditional coinduction helpers

delayed? : ∀ {b n} → ∞⟨ b ⟩P n → Bool
delayed? {b = b} _ = b

♭? : ∀ {b n} → ∞⟨ b ⟩P n → P n
♭? {true}  x = ♭ x
♭? {false} x =   x

♯? : ∀ {b n} → P n → ∞⟨ b ⟩P n
♯? {true}  x = ♯ x
♯? {false} x =   x

-- A lemma.

♭?♯? : ∀ b {n} {p : P n} → ♭? {b} (♯? p) ≡ p
♭?♯? true  = refl
♭?♯? false = refl

------------------------------------------------------------------------
-- Semantics

-- The semantics is defined inductively: s ∈ p iff the string s is
-- contained in the language defined by p.

infix 4 _∈_

data _∈_ : ∀ {n} → List Tok → P n → Set where
empty   : [] ∈ empty
tok     : ∀ {t} → [ t ] ∈ tok t
∣-left  : ∀ {s n₁ n₂} {p₁ : P n₁} {p₂ : P n₂} →
s ∈ p₁ → s ∈ p₁ ∣ p₂
∣-right : ∀ {s n₁ n₂} {p₁ : P n₁} {p₂ : P n₂} →
s ∈ p₂ → s ∈ p₁ ∣ p₂
_·_     : ∀ {s₁ s₂ n₁ n₂} {p₁ : P n₁} {p₂ : ∞⟨ not n₁ ⟩P n₂} →
s₁ ∈ p₁ → s₂ ∈ ♭? p₂ → s₁ ++ s₂ ∈ p₁ · p₂

-- A lemma.

cast : ∀ {n} {p p′ : P n} {s} → p ≡ p′ → s ∈ p → s ∈ p′
cast refl s∈ = s∈

------------------------------------------------------------------------
-- Nullability

-- The nullability index is correct.

⇒ : ∀ {n} {p : P n} → [] ∈ p → n ≡ true
⇒ pr = ⇒′ pr refl
where
⇒′ : ∀ {n s} {p : P n} → s ∈ p → s ≡ [] → n ≡ true
⇒′ empty                   refl = refl
⇒′ tok                     ()
⇒′ (∣-left            pr₁) refl with ⇒ pr₁
⇒′ (∣-left            pr₁) refl | refl = refl
⇒′ (∣-right           pr₂) refl with ⇒ pr₂
⇒′ (∣-right {n₁ = n₁} pr₂) refl | refl = proj₂ BoolCS.zero n₁
⇒′ (_·_ {[]}    pr₁ pr₂)   refl = cong₂ _∧_ (⇒ pr₁) (⇒ pr₂)
⇒′ (_·_ {_ ∷ _} pr₁ pr₂)   ()

⇐ : ∀ {n} (p : P n) → n ≡ true → [] ∈ p
⇐ fail                         ()
⇐ empty                        refl = empty
⇐ (tok t)                      ()
⇐ (_∣_ {true}           p₁ p₂) refl = ∣-left            (⇐ p₁ refl)
⇐ (_∣_ {false} {true}   p₁ p₂) refl = ∣-right {p₁ = p₁} (⇐ p₂ refl)
⇐ (_∣_ {false} {false}  p₁ p₂) ()
⇐ (_·_ {true}  p₁ p₂)          refl = ⇐ p₁ refl · ⇐ p₂ refl
⇐ (_·_ {false} p₁ p₂)          ()

-- We can decide if the empty string belongs to a given language.

nullable? : ∀ {n} (p : P n) → Dec ([] ∈ p)
nullable? {true}  p = yes (⇐ p refl)
nullable? {false} p = no helper
where
helper : ¬ [] ∈ p
helper []∈p with ⇒ []∈p
... | ()

------------------------------------------------------------------------
-- Derivative

-- D-nullable and D are placed in a mutual block to ensure that the
-- underscores in the definition of D-nullable can be solved by
-- constraints introduced in the body of D. The functions are not
-- actually mutually recursive.

mutual

-- The index of the derivative. The right-hand sides (excluding
-- t′ ≟ t and delayed? p₂) are inferable, but included here so that
-- they can easily be inspected.

D-nullable : ∀ {n} → Tok → P n → Bool
D-nullable t fail      = false
D-nullable t empty     = false
D-nullable t (tok t′)  with t′ ≟ t
D-nullable t (tok t′)  | yes t′≡t = true
D-nullable t (tok t′)  | no  t′≢t = false
D-nullable t (p₁ ∣ p₂) = D-nullable t p₁ ∨ D-nullable t p₂
D-nullable t (p₁ · p₂) with delayed? p₂
D-nullable t (p₁ · p₂) | true  = D-nullable t p₁ ∧ _
D-nullable t (p₁ · p₂) | false = D-nullable t p₁ ∧ _ ∨ D-nullable t p₂

-- D t p is the "derivative" of p with respect to t. It is specified
-- by the equivalence s ∈ D t p ⇔ t ∷ s ∈ p (proved below).

D : ∀ {n} (t : Tok) (p : P n) → P (D-nullable t p)
D t fail      = fail
D t empty     = fail
D t (tok t′)  with t′ ≟ t
D t (tok t′)  | yes t′≡t = empty
D t (tok t′)  | no  t′≢t = fail
D t (p₁ ∣ p₂) = D t p₁ ∣ D t p₂
D t (p₁ · p₂) with delayed? p₂
D t (p₁ · p₂) | true  = D t p₁ · ♯? (♭ p₂)
D t (p₁ · p₂) | false = D t p₁ · ♯?    p₂ ∣ D t p₂

-- D is correct.

D-sound : ∀ {s n} {t} {p : P n} → s ∈ D t p → t ∷ s ∈ p
D-sound s∈ = D-sound′ _ _ s∈
where
D-sound′ : ∀ {s n} t (p : P n) → s ∈ D t p → t ∷ s ∈ p
D-sound′ t fail                ()
D-sound′ t empty               ()
D-sound′ t (tok t′)            _                   with t′ ≟ t
D-sound′ t (tok .t)            empty               | yes refl = tok
D-sound′ t (tok t′)            ()                  | no  t′≢t
D-sound′ t (p₁ ∣ p₂)           (∣-left  ∈₁)        = ∣-left            (D-sound′ t p₁ ∈₁)
D-sound′ t (p₁ ∣ p₂)           (∣-right ∈₂)        = ∣-right {p₁ = p₁} (D-sound′ t p₂ ∈₂)
D-sound′ t (_·_ {true}  p₁ p₂) (∣-left  (∈₁ · ∈₂)) = D-sound′ t p₁ ∈₁ · cast (♭?♯? (not (D-nullable t p₁))) ∈₂
D-sound′ t (_·_ {true}  p₁ p₂) (∣-right ∈₂)        = ⇐ p₁ refl · D-sound′ t p₂ ∈₂
D-sound′ t (_·_ {false} p₁ p₂) (∈₁ · ∈₂)           = D-sound′ t p₁ ∈₁ · cast (♭?♯? (not (D-nullable t p₁))) ∈₂

D-complete : ∀ {s n} {t} {p : P n} → t ∷ s ∈ p → s ∈ D t p
D-complete {t = t} t∷s∈ = D-complete′ _ t∷s∈ refl
where
D-complete′ : ∀ {s s′ n} (p : P n) → s′ ∈ p → s′ ≡ t ∷ s → s ∈ D t p
D-complete′         fail     ()  refl
D-complete′         empty    ()  refl
D-complete′         (tok t′) _   refl with t′ ≟ t
D-complete′         (tok .t) tok refl | yes refl = empty
D-complete′ {[]}    (tok .t) tok refl | no  t′≢t with t′≢t refl
D-complete′ {[]}    (tok .t) tok refl | no  t′≢t | ()
D-complete′ {_ ∷ _} (tok t′) ()  refl | no  t′≢t
D-complete′ (p₁ ∣ p₂)           (∣-left  ∈₁)         refl = ∣-left                    (D-complete ∈₁)
D-complete′ (p₁ ∣ p₂)           (∣-right ∈₂)         refl = ∣-right {p₁ = D t p₁}     (D-complete ∈₂)
D-complete′ (_·_ {true}  p₁ p₂) (_·_ {[]}     ∈₁ ∈₂) refl = ∣-right {p₁ = D t p₁ · _} (D-complete ∈₂)
D-complete′ (_·_ {true}  p₁ p₂) (_·_ {._ ∷ _} ∈₁ ∈₂) refl = ∣-left (D-complete ∈₁ · cast (sym (♭?♯? (not (D-nullable t p₁)))) ∈₂)
D-complete′ (_·_ {false} p₁ p₂) (_·_ {[]}     ∈₁ ∈₂) refl with ⇒ ∈₁
D-complete′ (_·_ {false} p₁ p₂) (_·_ {[]}     ∈₁ ∈₂) refl | ()
D-complete′ (_·_ {false} p₁ p₂) (_·_ {._ ∷ _} ∈₁ ∈₂) refl = D-complete ∈₁ · cast (sym (♭?♯? (not (D-nullable t p₁)))) ∈₂

------------------------------------------------------------------------
-- _∈_ is decidable

-- _∈?_ runs a recogniser. Note that the result is yes or no plus a
-- /proof/ verifying that the answer is correct.

infix 4 _∈?_

_∈?_ : ∀ {n} (s : List Tok) (p : P n) → Dec (s ∈ p)
[]    ∈? p = nullable? p
t ∷ s ∈? p with s ∈? D t p
t ∷ s ∈? p | yes s∈Dtp = yes (D-sound s∈Dtp)
t ∷ s ∈? p | no  s∉Dtp = no  (s∉Dtp ∘ D-complete)
```