import FrontierDerivative.PrincipalCover

/-!
# Finite principal-cover derivative normalization

This module extends the stationary-cover substrate with list-valued derivative
tables. A basis derivative may expand into a finite principal cover. One-symbol
derivatives are therefore exposed locally once such a table is supplied.

The flattening calibration uses the one-element epsilon basis. It proves that
every finite list of stack words has an exact derivative-local cover. This
removes derivative access depth only by allowing one term per listed stack; it
does not bound cover width.
-/

namespace FrontierDerivative
namespace PrincipalCover

variable {Basis Γ : Type}

/-- One term denoting a concrete stem followed by a basis language. -/
structure Term (Basis Γ : Type) where
  stem : List Γ
  base : Basis

/-- A finite list of principal terms. -/
abbrev Cover (Basis Γ : Type) := List (Term Basis Γ)

/-- Semantics of one principal term. -/
def Term.denote (basis : Basis → StackLang Γ) (term : Term Basis Γ) :
    StackLang Γ :=
  prefixLang term.stem (basis term.base)

/-- Semantics of a finite principal cover. -/
def denote (basis : Basis → StackLang Γ) (cover : Cover Basis Γ) :
    StackLang Γ :=
  fun stack => ∃ term, term ∈ cover ∧ term.denote basis stack

/-- Pointwise union of two stack languages. -/
def unionLang (A B : StackLang Γ) : StackLang Γ :=
  fun stack => A stack ∨ B stack

theorem denote_cons (basis : Basis → StackLang Γ) (term : Term Basis Γ)
    (cover : Cover Basis Γ) :
    denote basis (term :: cover) =
      unionLang (term.denote basis) (denote basis cover) := by
  funext stack
  apply propext
  simp [denote, unionLang]

/-- Structural append for covers. -/
def append : Cover Basis Γ → Cover Basis Γ → Cover Basis Γ
  | [], right => right
  | term :: left, right => term :: append left right

theorem denote_append (basis : Basis → StackLang Γ)
    (left right : Cover Basis Γ) :
    denote basis (append left right) =
      unionLang (denote basis left) (denote basis right) := by
  induction left with
  | nil =>
      funext stack
      apply propext
      simp [append, denote, unionLang]
  | cons term left ih =>
      rw [append, denote_cons, ih, denote_cons]
      funext stack
      apply propext
      simp only [unionLang]
      exact or_assoc.symm

/-- A finite list-valued table witnessing one-symbol derivative closure of a
basis. The basis carrier itself is not required to be finite here. -/
structure DerivBasis (Basis Γ : Type) where
  lang : Basis → StackLang Γ
  derive : Γ → Basis → Cover Basis Γ
  sound : ∀ X b, leftDerivative X (lang b) = denote lang (derive X b)

/-- Differentiate one principal term. -/
def deriveTerm [DecidableEq Γ] (D : DerivBasis Basis Γ) (X : Γ)
    (term : Term Basis Γ) : Cover Basis Γ :=
  match term.stem with
  | [] => D.derive X term.base
  | Y :: rest =>
      if X = Y then [{ stem := rest, base := term.base }] else []

/-- Differentiate a cover term by term. -/
def deriveCover [DecidableEq Γ] (D : DerivBasis Basis Γ) (X : Γ) :
    Cover Basis Γ → Cover Basis Γ
  | [] => []
  | term :: cover =>
      append (deriveTerm D X term) (deriveCover D X cover)

/-- One principal term is differentiated exactly. -/
theorem deriveTerm_sound [DecidableEq Γ] (D : DerivBasis Basis Γ)
    (X : Γ) (term : Term Basis Γ) :
    denote D.lang (deriveTerm D X term) =
      leftDerivative X (term.denote D.lang) := by
  cases term with
  | mk stem base =>
      cases stem with
      | nil =>
          rw [deriveTerm, ← D.sound X base]
          funext stack
          apply propext
          simp [Term.denote, leftDerivative, prefixLang]
      | cons Y rest =>
          by_cases h : X = Y
          · subst Y
            funext stack
            apply propext
            simp [deriveTerm, denote, Term.denote, leftDerivative, prefixLang]
          · funext stack
            apply propext
            simp [deriveTerm, h, denote, Term.denote, leftDerivative,
              prefixLang]

/-- Every one-symbol derivative of a finite cover has an exact finite cover.
This normalization does not bound cover width. -/
theorem deriveCover_sound [DecidableEq Γ] (D : DerivBasis Basis Γ)
    (X : Γ) (cover : Cover Basis Γ) :
    denote D.lang (deriveCover D X cover) =
      leftDerivative X (denote D.lang cover) := by
  induction cover with
  | nil =>
      funext stack
      apply propext
      simp [deriveCover, denote, leftDerivative]
  | cons term cover ih =>
      rw [deriveCover, denote_append, deriveTerm_sound, ih, denote_cons]
      rfl

/-- The one-element basis whose language is the singleton empty stack. -/
inductive EpsilonBasis where
  | epsilon
deriving DecidableEq, Repr

/-- The singleton language containing only the empty stack. -/
def epsilonLang : EpsilonBasis → StackLang Γ :=
  fun _ stack => stack = []

/-- Every derivative of the epsilon basis language has the empty cover. -/
def epsilonDerivBasis [DecidableEq Γ] : DerivBasis EpsilonBasis Γ where
  lang := epsilonLang
  derive := fun _ _ => []
  sound := by
    intro X b
    funext stack
    apply propext
    constructor
    · intro h
      change X :: stack = [] at h
      cases h
    · intro h
      rcases h with ⟨term, hmem, _⟩
      cases hmem

/-- One epsilon-basis term for every listed stack. -/
def exactCover : List (List Γ) → Cover EpsilonBasis Γ
  | [] => []
  | stack :: stacks =>
      { stem := stack, base := .epsilon } :: exactCover stacks

theorem epsilonTerm_iff_eq (word stack : List Γ) :
    Term.denote (epsilonLang (Γ := Γ))
        { stem := word, base := .epsilon } stack ↔
      stack = word := by
  constructor
  · intro h
    rcases h with ⟨rest, hrest, hstack⟩
    change rest = [] at hrest
    subst rest
    simpa using hstack
  · intro h
    subst stack
    exact ⟨[], rfl, by simp⟩

/-- Every finite listed frontier is represented exactly by its epsilon-basis
cover, before any optional deduplication. -/
theorem exactCover_iff_mem (stacks : List (List Γ)) (stack : List Γ) :
    denote (epsilonLang (Γ := Γ)) (exactCover stacks) stack ↔
      stack ∈ stacks := by
  induction stacks with
  | nil => simp [denote, exactCover]
  | cons first rest ih =>
      rw [exactCover, denote_cons]
      simp only [unionLang, List.mem_cons]
      rw [epsilonTerm_iff_eq, ih]

end PrincipalCover
end FrontierDerivative