LastActionRefinement.lean

import FrontierDerivative.FiniteReindexing

/-!
# Canonical last-action visible refinements

The refined control remembers whether the current configuration is initial or
which hidden visible action produced it. If each action-specific contribution
to an original target control carries at most one stack, this fixed refinement
is control-functional and reaches the existing compiler chain.
-/

namespace FrontierDerivative.LastActionRefinement

open FiniteRefinement
open FiniteReindexing

universe uΓ

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

/-- The exact contribution of one fixed hidden action to the next observed
frontier. Failed commands contribute nothing. -/
def ActionFrontier (V : PartialVisible.Machine Input Q Γ) (w : List Input)
    (a : Input) (action : VisibleAction) (q : Q) (z : List Γ) : Prop :=
  ∃ q0 z0,
    V.Frontier w q0 z0 ∧
      V.apply a action ⟨q0, z0⟩ = some ⟨q, z⟩

/-- For a fixed prefix, next letter, final hidden action, and target control,
there is at most one resulting concrete stack. -/
def LastActionSeparated (V : PartialVisible.Machine Input Q Γ) : Prop :=
  ∀ w a action q z₁ z₂,
    ActionFrontier V w a action q z₁ →
    ActionFrontier V w a action q z₂ →
    z₁ = z₂

/-- Canonical control splitting by the hidden action that produced the current
configuration. `none` is reserved for the initial boundary. -/
def rememberAction (V : PartialVisible.Machine Input Q Γ) :
    PartialVisible.Machine Input (Q × Option VisibleAction) Γ where
  call := fun state a =>
    (V.call state.1 a).map fun next => ((next.1, some .call), next.2)
  ret := fun state a top =>
    (V.ret state.1 a top).map fun q => (q, some .ret)
  localStep := fun state a =>
    (V.localStep state.1 a).map fun q => (q, some .local)
  init := (V.init, none)
  accept := fun state => V.accept state.1

/-- The remembered action performs exactly the original action and stack
transformation in the same input round. -/
theorem remember_apply (V : PartialVisible.Machine Input Q Γ)
    (a : Input) (action : VisibleAction) (q q' : Q)
    (memory : Option VisibleAction) (z z' : List Γ) :
    (rememberAction V).apply a action ⟨(q, memory), z⟩ =
        some ⟨(q', some action), z'⟩ ↔
      V.apply a action ⟨q, z⟩ = some ⟨q', z'⟩ := by
  cases action <;>
    simp [rememberAction, PartialVisible.Machine.apply]

/-- Forgetting the remembered action is a lawful T105 refinement. -/
def rememberRefinement (V : PartialVisible.Machine Input Q Γ) :
    Refinement V (rememberAction V) where
  erase := Prod.fst
  init_eq := rfl
  accept_eq := by intro; rfl
  apply_sound := by
    intro a action state z state' z' h
    rcases state with ⟨q, memory⟩
    rcases state' with ⟨q', memory'⟩
    cases action
    · simp [rememberAction, PartialVisible.Machine.apply] at h ⊢
      rcases h with ⟨target, symbol, hcall, ⟨htarget, _⟩, hstack⟩
      exact ⟨target, symbol, hcall, htarget, hstack⟩
    · simp [rememberAction, PartialVisible.Machine.apply] at h ⊢
      rcases h with ⟨target, hret, ⟨htarget, _⟩, hstack⟩
      exact ⟨target, hret, htarget, hstack⟩
    · simp [rememberAction, PartialVisible.Machine.apply] at h ⊢
      rcases h with ⟨target, hlocal, ⟨htarget, _⟩, hstack⟩
      exact ⟨target, hlocal, htarget, hstack⟩
  apply_complete := by
    intro a action state z q' z' h
    rcases state with ⟨q, memory⟩
    refine ⟨(q', some action), ?_, rfl⟩
    exact (remember_apply V a action q q' memory z z').2 h

/-- A successor with remembered `action` is exactly that action's original
successor, not merely some hidden action successor. -/
theorem remember_successor_iff (V : PartialVisible.Machine Input Q Γ)
    (a : Input) (action : VisibleAction) (q0 q : Q)
    (memory : Option VisibleAction) (z0 z : List Γ) :
    (⟨(q, some action), z⟩ :
        PartialVisible.Config (Q × Option VisibleAction) Γ) ∈
        (rememberAction V).successors a ⟨(q0, memory), z0⟩ ↔
      V.apply a action ⟨q0, z0⟩ = some ⟨q, z⟩ := by
  rw [PartialVisible.Machine.mem_successors_iff]
  constructor
  · rintro ⟨actual, h⟩
    cases actual <;> cases action <;>
      simp [rememberAction, PartialVisible.Machine.apply] at h ⊢
    all_goals exact h
  · intro h
    exact ⟨action, (remember_apply V a action q0 q memory z0 z).2 h⟩

/-- At epsilon only the original initial control, `none`, and the empty stack
are reachable. -/
theorem frontier_nil_iff (V : PartialVisible.Machine Input Q Γ)
    (q : Q) (memory : Option VisibleAction) (z : List Γ) :
    (rememberAction V).Frontier [] (q, memory) z ↔
      q = V.init ∧ memory = none ∧ z = [] := by
  unfold PartialVisible.Machine.Frontier PartialVisible.Machine.run
  simp only [List.foldl_nil, List.mem_singleton]
  unfold PartialVisible.Machine.initConfig
  dsimp [rememberAction]
  change (⟨(q, memory), z⟩ :
    PartialVisible.Config (Q × Option VisibleAction) Γ) =
      ⟨(V.init, none), []⟩ ↔ q = V.init ∧ memory = none ∧ z = []
  constructor
  · intro h
    cases h
    exact ⟨rfl, rfl, rfl⟩
  · rintro ⟨rfl, rfl, rfl⟩
    rfl

/-- On a nonempty prefix, the remembered-action frontier is exactly the
original action-specific frontier. -/
theorem frontier_some_iff (V : PartialVisible.Machine Input Q Γ)
    (w : List Input) (a : Input) (action : VisibleAction)
    (q : Q) (z : List Γ) :
    (rememberAction V).Frontier (w ++ [a]) (q, some action) z ↔
      ActionFrontier V w a action q z := by
  rw [PartialVisible.Machine.frontier_append]
  constructor
  · rintro ⟨state0, z0, hprev, hnext⟩
    rcases state0 with ⟨q0, memory⟩
    have horiginal : V.Frontier w q0 z0 :=
      ((rememberRefinement V).frontier_iff_refined w q0 z0).2
        ⟨(q0, memory), hprev, rfl⟩
    exact ⟨q0, z0, horiginal,
      (remember_successor_iff V a action q0 q memory z0 z).1 hnext⟩
  · rintro ⟨q0, z0, horiginal, hnext⟩
    rcases ((rememberRefinement V).frontier_iff_refined w q0 z0).1 horiginal with
      ⟨state0, hprev, herase⟩
    rcases state0 with ⟨q1, memory⟩
    change q1 = q0 at herase
    subst q1
    exact ⟨(q0, memory), z0, hprev,
      (remember_successor_iff V a action q0 q memory z0 z).2 hnext⟩

/-- The initial marker never survives a consumed input symbol. -/
theorem frontier_none_nonempty (V : PartialVisible.Machine Input Q Γ)
    (w : List Input) (a : Input) (q : Q) (z : List Γ) :
    ¬(rememberAction V).Frontier (w ++ [a]) (q, none) z := by
  rw [PartialVisible.Machine.frontier_append]
  rintro ⟨state0, z0, _hprev, hnext⟩
  rw [PartialVisible.Machine.mem_successors_iff] at hnext
  rcases hnext with ⟨action, happly⟩
  rcases state0 with ⟨q0, memory⟩
  cases action <;>
    simp [rememberAction, PartialVisible.Machine.apply] at happly

/-- Last-action separation makes the canonical action-memory frontier
control-functional. -/
theorem remember_controlFunctional
    (V : PartialVisible.Machine Input Q Γ)
    (hsep : LastActionSeparated V) :
    ControlFunctionalOn (rememberAction V) := by
  apply PartialVisible.list_snoc_induction
    (motive := fun word => ∀ state z₁ z₂,
      (rememberAction V).Frontier word state z₁ →
      (rememberAction V).Frontier word state z₂ → z₁ = z₂)
  · intro state z₁ z₂ h₁ h₂
    rcases state with ⟨q, memory⟩
    rcases (frontier_nil_iff V q memory z₁).1 h₁ with ⟨_, _, rfl⟩
    rcases (frontier_nil_iff V q memory z₂).1 h₂ with ⟨_, _, rfl⟩
    rfl
  · intro w a _ih state z₁ z₂ h₁ h₂
    rcases state with ⟨q, memory⟩
    cases memory with
    | none => exact False.elim (frontier_none_nonempty V w a q z₁ h₁)
    | some action =>
        exact hsep w a action q z₁ z₂
          ((frontier_some_iff V w a action q z₁).1 h₁)
          ((frontier_some_iff V w a action q z₂).1 h₂)

/-- A supplied finite enumeration turns the canonical last-action refinement
into a scaffold for the original forgotten-action projection. -/
theorem compiled_decides_lastAction {s : Nat}
    (V : PartialVisible.Machine Input Q Γ)
    (hsep : LastActionSeparated V)
    (e : ControlEquiv (Q × Option VisibleAction) (Fin s))
    (w : List Input) :
    (RootSharingMachine.compile
      (ControlFunctional.executor (rename (rememberAction V) e))).decides w =
        true ↔ V.Accepts w := by
  exact compiled_decides_original_via_equiv (rememberRefinement V) e
    (remember_controlFunctional V hsep) w

#check ActionFrontier
#check rememberRefinement
#check frontier_some_iff
#check frontier_none_nonempty
#check remember_controlFunctional
#check compiled_decides_lastAction

end FrontierDerivative.LastActionRefinement