PrincipalCover.lean

import FrontierDerivative.Basic
import FPRDTransfer.Compile

/-!
# Stationary principal derivative covers

A cover represents every frontier component as a fixed finite union of
principal right ideals `v · B_j`.  The variable prefixes `v` are the stacks of
the already verified letter-synchronous `FPRD.StackMachine`; active flags and
basis indices live in its control.  Exact initialization, one-symbol update,
and readout are explicit fields, so per-prefix existence cannot masquerade as
a stationary construction.
-/

namespace FrontierDerivative

/-- A language of stack words. -/
abbrev StackLang (Γ : Type) := List Γ → Prop

/-- Left prefixing of a stack language. -/
def prefixLang {Γ : Type} (v : List Γ) (B : StackLang Γ) : StackLang Γ :=
  fun z => ∃ b, B b ∧ z = v ++ b

/-- Left derivative by one stack symbol. -/
def leftDerivative {Γ : Type} (X : Γ) (B : StackLang Γ) : StackLang Γ :=
  fun tail => B (X :: tail)

/-- A basis carrying an exact finite-index action for one-symbol derivatives.
Finiteness of `J` is imposed at the mathematical LMR boundary, not by this
operational Lean structure. -/
structure DerivativeBasis (J : Type) (Γ : Type) where
  lang : J → StackLang Γ
  deriv : J → Γ → J
  deriv_exact : ∀ j X tail, lang (deriv j X) tail ↔ lang j (X :: tail)

/-- Derivating an unprefixed basis element stays inside the basis. -/
theorem principalDerivative_nil {J : Type} {Γ : Type}
    (B : DerivativeBasis J Γ) (j : J) (X : Γ) :
    leftDerivative X (prefixLang [] (B.lang j)) = B.lang (B.deriv j X) := by
  funext tail
  simp [leftDerivative, prefixLang, B.deriv_exact]

/-- A matching derivative removes exactly one symbol from the variable prefix. -/
theorem principalDerivative_cons_eq {Γ : Type} (B : StackLang Γ)
    (X : Γ) (v : List Γ) :
    leftDerivative X (prefixLang (X :: v) B) = prefixLang v B := by
  funext tail
  simp [leftDerivative, prefixLang]

/-- A mismatched derivative annihilates a principal summand. -/
theorem principalDerivative_cons_ne {Γ : Type} (B : StackLang Γ)
    {X Y : Γ} (v : List Γ) (hXY : X ≠ Y) :
    leftDerivative X (prefixLang (Y :: v) B) = fun _ => False := by
  funext tail
  simp [leftDerivative, prefixLang, hXY]

/-- A semantic frontier relation indexed by source control state. -/
abbrev FrontierRel (Q : Type) (Γ : Type) := Q → List Γ → Prop

/-- The exact one-symbol derivative of an arbitrary represented frontier. -/
def frontierDerivative {Q : Type} {Input : Type} {Γ : Type}
    (P : Machine Q Input Γ) (R : FrontierRel Q Γ) (a : Input) :
    FrontierRel Q Γ :=
  fun q' z' =>
    ∃ q X tail t,
      R q (X :: tail) ∧
      t ∈ P.transitions ∧
      t.source = q ∧
      t.input = a ∧
      t.top = X ∧
      q' = t.target ∧
      z' = t.replacement ++ tail

theorem frontierDerivative_congr {Q : Type} {Input : Type}
    {Γ : Type} (P : Machine Q Input Γ) {R S : FrontierRel Q Γ}
    (h : ∀ q z, R q z ↔ S q z) (a : Input) (q : Q) (z : List Γ) :
    frontierDerivative P R a q z ↔ frontierDerivative P S a q z := by
  simp only [frontierDerivative, h]

theorem frontier_append_singleton_as_derivative {Q : Type}
    {Input : Type} {Γ : Type}
    [DecidableEq Q] [DecidableEq Input] [DecidableEq Γ]
    (P : Machine Q Input Γ) (u : List Input) (a : Input) (q : Q)
    (z : List Γ) :
    P.Frontier (u ++ [a]) q z ↔
      frontierDerivative P (P.Frontier u) a q z := by
  exact Machine.frontier_append_singleton_iff P u a q z

/-- Fixed cover coordinates.  Slot `i` represents
`stack_i · basis_(meta_i)` when its metadata is active. -/
structure CoverCoordinates (Ctrl : Type) (Q : Type) (J : Type)
    (Γ : Type) (s : Nat) where
  basis : DerivativeBasis J Γ
  owner : Fin s → Q
  slotBasis : Ctrl → Fin s → Option J

namespace CoverCoordinates

variable {Ctrl : Type} {Q : Type} {J : Type} {Γ : Type}
variable {s : Nat}

/-- The frontier relation denoted by one synchronous-stack configuration. -/
def Rep (D : CoverCoordinates Ctrl Q J Γ s) (c : FPRD.Config Ctrl Γ s) :
    FrontierRel Q Γ :=
  fun q z =>
    ∃ i j b,
      D.owner i = q ∧
      D.slotBasis c.ctrl i = some j ∧
      D.basis.lang j b ∧
      z = c.stacks i ++ b

end CoverCoordinates

/--
A stationary principal cover for `P` executed by `C`.

`step_exact` is the canonicalizer obligation: one fixed synchronous transition
must compute the exact semantic derivative, not merely a bounded cover that is
chosen afresh at each prefix or horizon.
-/
structure PrincipalCover {Q : Type} {Input : Type} {Γ : Type}
    [DecidableEq Q] [DecidableEq Input] [DecidableEq Γ]
    {Ctrl : Type} {s : Nat} (P : Machine Q Input Γ)
    (C : FPRD.StackMachine Input Ctrl Γ s) (J : Type) where
  coordinates : CoverCoordinates Ctrl Q J Γ s
  valid : FPRD.Config Ctrl Γ s → Prop
  init_valid : valid C.initConfig
  step_valid : ∀ c a, valid c → valid (C.stepConfig c a)
  init_exact : ∀ q z,
    coordinates.Rep C.initConfig q z ↔ P.Frontier [] q z
  step_exact : ∀ c a, valid c → ∀ q z,
    coordinates.Rep (C.stepConfig c a) q z ↔
      frontierDerivative P (coordinates.Rep c) a q z
  readout_exact : ∀ c, valid c → (
    C.accept c.ctrl = true ↔
      ∃ q z, coordinates.Rep c q z ∧ P.final q = true)

namespace PrincipalCover

variable {Q : Type} {Input : Type} {Γ : Type}
variable {J : Type} {Ctrl : Type} {s : Nat}
variable [DecidableEq Q] [DecidableEq Input] [DecidableEq Γ]
variable {P : Machine Q Input Γ} {C : FPRD.StackMachine Input Ctrl Γ s}

/-- Reverse-list induction, kept local so the run proof follows prefix growth. -/
theorem list_snoc_induction {α : Type} {motive : List α → Prop}
    (hnil : motive [])
    (hsnoc : ∀ xs x, motive xs → motive (xs ++ [x])) :
    ∀ xs, motive xs := by
  intro xs
  have hreverse : ∀ ys : List α, motive ys.reverse := by
    intro ys
    induction ys with
    | nil => simpa using hnil
    | cons x ys ih =>
        simpa only [List.reverse_cons] using hsnoc ys.reverse x ih
  simpa using hreverse xs.reverse

/-- The stationary cover denotes the exact semantic frontier after every word. -/
theorem cover_run_valid (K : PrincipalCover P C J) (w : List Input) :
    K.valid (C.run w) := by
  have hall : ∀ w : List Input, K.valid (C.run w) := by
    apply list_snoc_induction
    · exact K.init_valid
    · intro w a ih
      rw [FPRD.StackMachine.run_append]
      exact K.step_valid (C.run w) a ih
  exact hall w

/-- The stationary cover denotes the exact semantic frontier after every word. -/
theorem cover_run_exact (K : PrincipalCover P C J) (w : List Input)
    (q : Q) (z : List Γ) :
    K.coordinates.Rep (C.run w) q z ↔ P.Frontier w q z := by
  have hall : ∀ w : List Input, ∀ q z,
      K.coordinates.Rep (C.run w) q z ↔ P.Frontier w q z := by
    apply list_snoc_induction
    · intro q z
      exact K.init_exact q z
    · intro w a ih q z
      rw [FPRD.StackMachine.run_append]
      rw [K.step_exact (C.run w) a (K.cover_run_valid w)]
      rw [frontier_append_singleton_as_derivative]
      exact frontierDerivative_congr P (fun q z => ih q z) a q z
  exact hall w q z

/-- The cover executor accepts exactly the normalized frontier machine. -/
theorem cover_decides_iff (K : PrincipalCover P C J) (w : List Input) :
    C.decides w = true ↔ P.Accepts w := by
  rw [FPRD.StackMachine.decides]
  have hread := K.readout_exact (C.run w) (K.cover_run_valid w)
  rw [hread]
  rw [Machine.accepts_iff_final_frontier]
  constructor
  · rintro ⟨q, z, hrep, hfinal⟩
    exact ⟨q, z, (K.cover_run_exact w q z).1 hrep, hfinal⟩
  · rintro ⟨q, z, hfrontier, hfinal⟩
    exact ⟨q, z, (K.cover_run_exact w q z).2 hfrontier, hfinal⟩

/--
The already verified persistent-stack compiler turns the cover executor into a
scaffolding automaton with the same language.  LMR's external Theorem 16 then
places the reversal of this language in PEL when all carriers are finite.
-/
theorem compiled_cover_decides_iff (K : PrincipalCover P C J)
    (w : List Input) :
    (FPRD.compile C).decides w = true ↔ P.Accepts w := by
  rw [FPRD.compile_decides]
  exact K.cover_decides_iff w

end PrincipalCover

end FrontierDerivative