FiniteRefinement.lean

import FrontierDerivative.ControlFunctional

/-!
# Finite-control visible refinements

A local state splitting preserves each input/action/stack step and may separate
several stacks that shared one original control. If the refined frontier is
control-functional, FPRD-T104 supplies the canonical allocator for the original
projected language as well.
-/

namespace FrontierDerivative.FiniteRefinement

universe uΓ

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

/-- A same-action, same-stack local refinement of a partial visible machine. -/
structure Refinement (V : PartialVisible.Machine Input Q Γ)
    (W : PartialVisible.Machine Input R Γ) where
  erase : R → Q
  init_eq : erase W.init = V.init
  accept_eq : ∀ r, W.accept r = V.accept (erase r)
  apply_sound : ∀ a action r z r' z',
    W.apply a action ⟨r, z⟩ = some ⟨r', z'⟩ →
    V.apply a action ⟨erase r, z⟩ = some ⟨erase r', z'⟩
  apply_complete : ∀ a action r z q' z',
    V.apply a action ⟨erase r, z⟩ = some ⟨q', z'⟩ →
    ∃ r', W.apply a action ⟨r, z⟩ = some ⟨r', z'⟩ ∧ erase r' = q'

namespace Refinement

variable {V : PartialVisible.Machine Input Q Γ}
variable {W : PartialVisible.Machine Input R Γ}

theorem successor_sound (H : Refinement V W) (a : Input) (r r' : R)
    (z z' : List Γ)
    (h : (⟨r', z'⟩ : PartialVisible.Config R Γ) ∈ W.successors a ⟨r, z⟩) :
    (⟨H.erase r', z'⟩ : PartialVisible.Config Q Γ) ∈
      V.successors a ⟨H.erase r, z⟩ := by
  rw [PartialVisible.Machine.mem_successors_iff] at h ⊢
  rcases h with ⟨action, happly⟩
  exact ⟨action, H.apply_sound a action r z r' z' happly⟩

theorem successor_complete (H : Refinement V W) (a : Input) (r : R)
    (z : List Γ) (q' : Q) (z' : List Γ)
    (h : (⟨q', z'⟩ : PartialVisible.Config Q Γ) ∈
      V.successors a ⟨H.erase r, z⟩) :
    ∃ r',
      (⟨r', z'⟩ : PartialVisible.Config R Γ) ∈ W.successors a ⟨r, z⟩ ∧
      H.erase r' = q' := by
  rw [PartialVisible.Machine.mem_successors_iff] at h
  rcases h with ⟨action, happly⟩
  rcases H.apply_complete a action r z q' z' happly with
    ⟨r', hrefined, herase⟩
  exact ⟨r', (PartialVisible.Machine.mem_successors_iff W a _ _).2
    ⟨action, hrefined⟩, herase⟩

/-- Exact all-prefix projection of the refined frontier. -/
theorem frontier_iff_refined (H : Refinement V W) :
    ∀ (w : List Input) (q : Q) (z : List Γ),
      V.Frontier w q z ↔
        ∃ r, W.Frontier w r z ∧ H.erase r = q := by
  apply PartialVisible.list_snoc_induction
    (motive := fun w => ∀ q z,
      V.Frontier w q z ↔ ∃ r, W.Frontier w r z ∧ H.erase r = q)
  · intro q z
    constructor
    · intro h
      simp [PartialVisible.Machine.Frontier, PartialVisible.Machine.run,
        PartialVisible.Machine.initConfig] at h
      rcases h with ⟨rfl, rfl⟩
      exact ⟨W.init, by
        simp [PartialVisible.Machine.Frontier, PartialVisible.Machine.run,
          PartialVisible.Machine.initConfig], H.init_eq⟩
    · rintro ⟨r, hfrontier, herase⟩
      simp [PartialVisible.Machine.Frontier, PartialVisible.Machine.run,
        PartialVisible.Machine.initConfig] at hfrontier
      rcases hfrontier with ⟨rfl, rfl⟩
      simp [PartialVisible.Machine.Frontier, PartialVisible.Machine.run,
        PartialVisible.Machine.initConfig]
      exact (H.init_eq.symm.trans herase).symm
  · intro w a ih q z
    constructor
    · intro hfrontier
      rcases (PartialVisible.Machine.frontier_append V w a q z).1 hfrontier with
        ⟨q0, z0, hprev, hnext⟩
      rcases (ih q0 z0).1 hprev with ⟨r0, hrefined, herase0⟩
      subst q0
      rcases H.successor_complete a r0 z0 q z hnext with
        ⟨r, hnextRefined, herase⟩
      exact ⟨r, (PartialVisible.Machine.frontier_append W w a r z).2
        ⟨r0, z0, hrefined, hnextRefined⟩, herase⟩
    · rintro ⟨r, hrefined, herase⟩
      rcases (PartialVisible.Machine.frontier_append W w a r z).1 hrefined with
        ⟨r0, z0, hprev, hnext⟩
      have horiginalPrev : V.Frontier w (H.erase r0) z0 :=
        (ih (H.erase r0) z0).2 ⟨r0, hprev, rfl⟩
      have horiginalNext := H.successor_sound a r0 r z0 z hnext
      subst q
      exact (PartialVisible.Machine.frontier_append V w a (H.erase r) z).2
        ⟨H.erase r0, z0, horiginalPrev, horiginalNext⟩

/-- Refinement preserves projected acceptance, including the empty word. -/
theorem accepts_iff_refined (H : Refinement V W) (w : List Input) :
    V.Accepts w ↔ W.Accepts w := by
  constructor
  · rintro ⟨q, z, hfrontier, hfinal⟩
    rcases (H.frontier_iff_refined w q z).1 hfrontier with
      ⟨r, hrefined, herase⟩
    refine ⟨r, z, hrefined, ?_⟩
    rw [H.accept_eq, herase]
    exact hfinal
  · rintro ⟨r, z, hrefined, hfinal⟩
    refine ⟨H.erase r, z,
      (H.frontier_iff_refined w (H.erase r) z).2 ⟨r, hrefined, rfl⟩, ?_⟩
    rw [← H.accept_eq]
    exact hfinal

/-- A control-functional finite refinement compiles through the existing
T104/T102/T101 chain and decides the original projected language. -/
theorem compiled_decides_original {s : Nat}
    {W : PartialVisible.Machine Input (Fin s) Γ}
    (H : Refinement V W) (hfun : ControlFunctional.ControlFunctional W)
    (w : List Input) :
    (RootSharingMachine.compile (ControlFunctional.executor W)).decides w = true ↔
      V.Accepts w := by
  rw [ControlFunctional.compiled_decides W hfun]
  exact (H.accepts_iff_refined w).symm

#check frontier_iff_refined
#check accepts_iff_refined
#check compiled_decides_original

end Refinement

end FrontierDerivative.FiniteRefinement