Basic.lean

import Std

/-!
# Frontier derivatives for a normalized real-time pushdown machine

This file isolates the small theorem used by the FPRD forgotten-action note.
A transition consumes exactly one input symbol, inspects the leftmost (top)
stack symbol, and replaces it by a finite word.  The transition table is a
finite list, so `step`, `advance`, and `run` are executable.

The file does not formalize visibly pushdown automata, their determinization,
PEGs, scaffolding automata, or any theorem connecting those classes.
-/

namespace FrontierDerivative

universe uQ uInput uΓ

/-- A finite-control state paired with a stack whose top is the left end. -/
structure Config (Q : Type uQ) (Γ : Type uΓ) where
  state : Q
  stack : List Γ
  deriving DecidableEq, Repr

/-- One input-consuming, top-rewriting transition. -/
structure Transition (Q : Type uQ) (Input : Type uInput) (Γ : Type uΓ) where
  source : Q
  input : Input
  top : Γ
  target : Q
  replacement : List Γ
  deriving DecidableEq, Repr

/-- A normalized nondeterministic pushdown machine with final-state readout. -/
structure Machine (Q : Type uQ) (Input : Type uInput) (Γ : Type uΓ) where
  transitions : List (Transition Q Input Γ)
  initial : Config Q Γ
  final : Q → Bool

namespace Transition

variable {Q : Type uQ} {Input : Type uInput} {Γ : Type uΓ}

/-- Execute a transition when its source, input, and top symbol match. -/
def apply? [DecidableEq Q] [DecidableEq Input] [DecidableEq Γ]
    (t : Transition Q Input Γ) (a : Input) (c : Config Q Γ) : Option (Config Q Γ) :=
  match c.stack with
  | [] => none
  | X :: tail =>
      if t.source = c.state ∧ t.input = a ∧ t.top = X then
        some ⟨t.target, t.replacement ++ tail⟩
      else
        none

/-- The executable transition agrees with the normalized top-rewrite rule. -/
theorem apply?_eq_some_iff [DecidableEq Q] [DecidableEq Input] [DecidableEq Γ]
    (t : Transition Q Input Γ) (a : Input) (c c' : Config Q Γ) :
    t.apply? a c = some c' ↔
      ∃ tail,
        c.state = t.source ∧
        c.stack = t.top :: tail ∧
        a = t.input ∧
        c' = ⟨t.target, t.replacement ++ tail⟩ := by
  cases hstack : c.stack with
  | nil => simp [apply?, hstack]
  | cons X tail =>
      simp [apply?, hstack]
      constructor
      · rintro ⟨⟨hsource, hinput, htop⟩, hout⟩
        exact ⟨hsource.symm, tail, ⟨htop.symm, rfl⟩, hinput.symm, hout.symm⟩
      · rintro ⟨hsource, tail', ⟨htop, htail⟩, hinput, hout⟩
        subst tail'
        exact ⟨⟨hsource.symm, hinput.symm, htop.symm⟩, hout.symm⟩

end Transition

namespace Machine

variable {Q : Type uQ} {Input : Type uInput} {Γ : Type uΓ}
variable [DecidableEq Q] [DecidableEq Input] [DecidableEq Γ]

/-- All successors of one configuration on one arriving symbol. -/
def step (M : Machine Q Input Γ) (a : Input) (c : Config Q Γ) : List (Config Q Γ) :=
  M.transitions.filterMap fun t => t.apply? a c

/-- Apply one arriving symbol to every live configuration. -/
def advance (M : Machine Q Input Γ) (cs : List (Config Q Γ)) (a : Input) :
    List (Config Q Γ) :=
  cs.flatMap (M.step a)

/-- Execute a word from an arbitrary finite frontier. -/
def runFrom (M : Machine Q Input Γ) (cs : List (Config Q Γ)) (w : List Input) :
    List (Config Q Γ) :=
  w.foldl M.advance cs

/-- Execute a word from the singleton initial frontier. -/
def run (M : Machine Q Input Γ) (w : List Input) : List (Config Q Γ) :=
  M.runFrom [M.initial] w

/-- The semantic frontier component at control state `q` after prefix `u`. -/
def Frontier (M : Machine Q Input Γ) (u : List Input) (q : Q) (z : List Γ) : Prop :=
  (⟨q, z⟩ : Config Q Γ) ∈ M.run u

/-- Final-state acceptance from the finite frontier. -/
def Accepts (M : Machine Q Input Γ) (u : List Input) : Prop :=
  ∃ c ∈ M.run u, M.final c.state = true

theorem mem_step_iff (M : Machine Q Input Γ) (a : Input) (c c' : Config Q Γ) :
    c' ∈ M.step a c ↔
      ∃ t ∈ M.transitions, t.apply? a c = some c' := by
  simp [step]

theorem mem_advance_iff (M : Machine Q Input Γ) (cs : List (Config Q Γ))
    (a : Input) (c' : Config Q Γ) :
    c' ∈ M.advance cs a ↔
      ∃ c ∈ cs, ∃ t ∈ M.transitions, t.apply? a c = some c' := by
  simp [advance, mem_step_iff]

theorem runFrom_append (M : Machine Q Input Γ) (cs : List (Config Q Γ))
    (u v : List Input) :
    M.runFrom cs (u ++ v) = M.runFrom (M.runFrom cs u) v := by
  simp [runFrom, List.foldl_append]

theorem run_append_singleton (M : Machine Q Input Γ) (u : List Input) (a : Input) :
    M.run (u ++ [a]) = M.advance (M.run u) a := by
  simp [run, runFrom, List.foldl_append]

/--
The exact frontier derivative recurrence.  A stack word is in the frontier
after `u ++ [a]` exactly when a stack in the frontier after `u` has top `X`
and one listed transition replaces `X` by `γ`.  In language notation this is
`S_{ua}(q') = ⋃ γ (X⁻¹ S_u(q))`.
-/
theorem frontier_append_singleton_iff (M : Machine Q Input Γ) (u : List Input)
    (a : Input) (q' : Q) (z' : List Γ) :
    M.Frontier (u ++ [a]) q' z' ↔
      ∃ q X tail t,
        M.Frontier u q (X :: tail) ∧
        t ∈ M.transitions ∧
        t.source = q ∧
        t.input = a ∧
        t.top = X ∧
        q' = t.target ∧
        z' = t.replacement ++ tail := by
  rw [Frontier, run_append_singleton, mem_advance_iff]
  constructor
  · rintro ⟨⟨q, z⟩, hc, t, ht, happly⟩
    rw [Transition.apply?_eq_some_iff] at happly
    obtain ⟨tail, hstate, hstack, hinput, hout⟩ := happly
    change q = t.source at hstate
    change z = t.top :: tail at hstack
    subst z
    refine ⟨q, t.top, tail, t, hc, ht, ?_, ?_, rfl, ?_, ?_⟩
    · exact hstate.symm
    · exact hinput.symm
    · exact congrArg Config.state hout
    · exact congrArg Config.stack hout
  · rintro ⟨q, X, tail, t, hfrontier, ht, hsource, hinput, htop,
      htarget, hstack⟩
    refine ⟨⟨q, X :: tail⟩, hfrontier, t, ht, ?_⟩
    rw [Transition.apply?_eq_some_iff]
    refine ⟨tail, hsource.symm, ?_, hinput.symm, ?_⟩
    · simp [htop]
    · cases htarget
      cases hstack
      rfl

/-- Acceptance is exactly nonemptiness of some final frontier component. -/
theorem accepts_iff_final_frontier (M : Machine Q Input Γ) (u : List Input) :
    M.Accepts u ↔
      ∃ q z, M.Frontier u q z ∧ M.final q = true := by
  constructor
  · rintro ⟨c, hc, hfinal⟩
    exact ⟨c.state, c.stack, hc, hfinal⟩
  · rintro ⟨q, z, hfrontier, hfinal⟩
    exact ⟨⟨q, z⟩, hfrontier, hfinal⟩

/-- Empty-input behavior is the initial configuration, including its report. -/
theorem accepts_nil_iff (M : Machine Q Input Γ) :
    M.Accepts [] ↔ M.final M.initial.state = true := by
  simp [Accepts, run, runFrom]

end Machine

end FrontierDerivative