```------------------------------------------------------------------------
-- This module proves that the context-sensitive language aⁿbⁿcⁿ can
-- be recognised
------------------------------------------------------------------------

-- This is obvious given the proof in
-- TotalRecognisers.LeftRecursion.ExpressiveStrength but the code
-- below provides a non-trivial example of the use of the parser
-- combinators.

module TotalRecognisers.LeftRecursion.NotOnlyContextFree where

open import Algebra
open import Coinduction
open import Data.Bool using (Bool; true; false; _∨_)
open import Function
open import Data.List as List using (List; []; _∷_; _++_; [_])
import Data.List.Properties
private
module ListMonoid {A : Set} =
Monoid (Data.List.Properties.++-monoid A)
open import Data.Nat as Nat using (ℕ; zero; suc; _+_)
import Data.Nat.Properties as NatProp
open NatProp.SemiringSolver
private
module NatCS = CommutativeSemiring NatProp.commutativeSemiring
open import Data.Product
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open ≡-Reasoning

import TotalRecognisers.LeftRecursion
import TotalRecognisers.LeftRecursion.Lib as Lib

------------------------------------------------------------------------
-- The alphabet

data Tok : Set where
a b c : Tok

_≟_ : Decidable (_≡_ {A = Tok})
a ≟ a = yes refl
a ≟ b = no λ()
a ≟ c = no λ()
b ≟ a = no λ()
b ≟ b = yes refl
b ≟ c = no λ()
c ≟ a = no λ()
c ≟ b = no λ()
c ≟ c = yes refl

open TotalRecognisers.LeftRecursion Tok
open Lib Tok
private
open module TokTok = Lib.Tok Tok _≟_ using (tok)

------------------------------------------------------------------------
-- An auxiliary definition and a boring lemma

infixr 8 _^^_

_^^_ : Tok → ℕ → List Tok
_^^_ = flip List.replicate

private

shallow-comm : ∀ i n → i + suc n ≡ suc (i + n)
shallow-comm i n =
solve 2 (λ i n → i :+ (con 1 :+ n) := con 1 :+ i :+ n) refl i n

------------------------------------------------------------------------
-- Some lemmas relating _^^_, _^_ and tok

tok-^-complete : ∀ t i → t ^^ i ∈ tok t ^ i
tok-^-complete t zero    = empty
tok-^-complete t (suc i) =
add-♭♯ ⟨ false ^ i ⟩-nullable TokTok.complete · tok-^-complete t i

tok-^-sound : ∀ t i {s} → s ∈ tok t ^ i → s ≡ t ^^ i
tok-^-sound t zero    empty     = refl
tok-^-sound t (suc i) (t∈ · s∈)
with TokTok.sound (drop-♭♯ ⟨ false ^ i ⟩-nullable t∈)
... | refl = cong (_∷_ t) (tok-^-sound t i s∈)

------------------------------------------------------------------------
-- aⁿbⁿcⁿ

-- The context-sensitive language { aⁿbⁿcⁿ | n ∈ ℕ } can be recognised
-- using the parser combinators defined in this development.

private

-- The two functions below are not actually mutually recursive, but
-- are placed in a mutual block to ensure that the constraints
-- generated by the second function can be used to instantiate the
-- underscore in the body of the first.

mutual

aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-index : ℕ → Bool
aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-index _ = _

aⁿbⁱ⁺ⁿcⁱ⁺ⁿ : (i : ℕ) → P (aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-index i)
aⁿbⁱ⁺ⁿcⁱ⁺ⁿ i = cast lem (♯? (tok a) · ♯ aⁿbⁱ⁺ⁿcⁱ⁺ⁿ (suc i))
∣ tok b ^ i ⊙ tok c ^ i
where lem = left-zero (aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-index (suc i))

aⁿbⁿcⁿ : P true
aⁿbⁿcⁿ = aⁿbⁱ⁺ⁿcⁱ⁺ⁿ 0

-- Let us prove that aⁿbⁿcⁿ is correctly defined.

aⁿbⁿcⁿ-string : ℕ → List Tok
aⁿbⁿcⁿ-string n = a ^^ n ++ b ^^ n ++ c ^^ n

private

aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-string : ℕ → ℕ → List Tok
aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-string n i = a ^^ n ++ b ^^ (i + n) ++ c ^^ (i + n)

aⁿbⁿcⁿ-complete : ∀ n → aⁿbⁿcⁿ-string n ∈ aⁿbⁿcⁿ
aⁿbⁿcⁿ-complete n = aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-complete n 0
where
aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-complete : ∀ n i → aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-string n i ∈ aⁿbⁱ⁺ⁿcⁱ⁺ⁿ i
aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-complete zero i with i + 0 | proj₂ NatCS.+-identity i
... | .i | refl = ∣-right {n₁ = false} (helper b · helper c)
where
helper = λ (t : Tok) →
add-♭♯ ⟨ false ^ i ⟩-nullable (tok-^-complete t i)
aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-complete (suc n) i with i + suc n | shallow-comm i n
... | .(suc i + n) | refl =
∣-left \$ cast {eq = lem} (
add-♭♯ (aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-index (suc i)) TokTok.complete ·
aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-complete n (suc i))
where lem = left-zero (aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-index (suc i))

aⁿbⁿcⁿ-sound : ∀ {s} → s ∈ aⁿbⁿcⁿ → ∃ λ n → s ≡ aⁿbⁿcⁿ-string n
aⁿbⁿcⁿ-sound = aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-sound 0
where
aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-sound : ∀ {s} i → s ∈ aⁿbⁱ⁺ⁿcⁱ⁺ⁿ i →
∃ λ n → s ≡ aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-string n i
aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-sound i (∣-left (cast (t∈ · s∈)))
with TokTok.sound (drop-♭♯ (aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-index (suc i)) t∈)
... | refl with aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-sound (suc i) s∈
... | (n , refl) = suc n , (begin
a ^^ suc n ++ b ^^ (suc i + n) ++ c ^^ (suc i + n)
≡⟨ cong (λ i → a ^^ suc n ++ b ^^ i ++ c ^^ i)
(sym (shallow-comm i n)) ⟩
a ^^ suc n ++ b ^^ (i + suc n) ++ c ^^ (i + suc n)
∎)
aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-sound i (∣-right (_·_ {s₁} {s₂} s₁∈ s₂∈)) = 0 , (begin
s₁ ++ s₂
≡⟨ cong₂ _++_ (tok-^-sound b i
(drop-♭♯ ⟨ false ^ i ⟩-nullable s₁∈))
(tok-^-sound c i
(drop-♭♯ ⟨ false ^ i ⟩-nullable s₂∈)) ⟩
b ^^ i ++ c ^^ i
≡⟨ cong (λ i → b ^^ i ++ c ^^ i)
(sym (proj₂ NatCS.+-identity i)) ⟩
b ^^ (i + 0) ++ c ^^ (i + 0)
∎)
```