FiniteReindexing.lean

import FrontierDerivative.FiniteRefinement

/-!
# Exact finite-control reindexing

An equivalence of control types changes only their names. It preserves every
same-round visible action and concrete stack, composes with T105 refinements,
and lets an arbitrary named finite refinement use the `Fin` slots required by
the T104 allocator.
-/

namespace FrontierDerivative.FiniteReindexing

open FiniteRefinement

universe uΓ

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

/-- A core-only equivalence of control carriers. The project deliberately does
not import Mathlib merely to rename finite states. -/
structure ControlEquiv (R : Type) (R' : Type) where
  toFun : R → R'
  invFun : R' → R
  left_inv : ∀ r, invFun (toFun r) = r
  right_inv : ∀ r', toFun (invFun r') = r'

namespace ControlEquiv

theorem toFun_injective (e : ControlEquiv R R') : Function.Injective e.toFun := by
  intro x y h
  rw [← e.left_inv x, ← e.left_inv y, h]

theorem invFun_injective (e : ControlEquiv R R') : Function.Injective e.invFun := by
  intro x y h
  rw [← e.right_inv x, ← e.right_inv y, h]

def symm (e : ControlEquiv R R') : ControlEquiv R' R where
  toFun := e.invFun
  invFun := e.toFun
  left_inv := e.right_inv
  right_inv := e.left_inv

end ControlEquiv

/-- Transport a partial visible machine along a control equivalence. -/
def rename (W : PartialVisible.Machine Input R Γ) (e : ControlEquiv R R') :
    PartialVisible.Machine Input R' Γ where
  call := fun r a =>
    (W.call (e.invFun r) a).map fun next => (e.toFun next.1, next.2)
  ret := fun r a top => (W.ret (e.invFun r) a top).map e.toFun
  localStep := fun r a => (W.localStep (e.invFun r) a).map e.toFun
  init := e.toFun W.init
  accept := fun r => W.accept (e.invFun r)

/-- Reindexing commutes exactly with one hidden visible action and the concrete
stack transformation. -/
theorem rename_apply (W : PartialVisible.Machine Input R Γ)
    (e : ControlEquiv R R')
    (a : Input) (action : VisibleAction) (r r' : R) (z z' : List Γ) :
    (rename W e).apply a action ⟨e.toFun r, z⟩ =
        some ⟨e.toFun r', z'⟩ ↔
      W.apply a action ⟨r, z⟩ = some ⟨r', z'⟩ := by
  have heq (x y : R) : e.toFun x = e.toFun y ↔ x = y := by
    constructor
    · intro h
      exact ControlEquiv.toFun_injective e h
    · exact congrArg e.toFun
  cases action <;>
    simp [rename, PartialVisible.Machine.apply, e.left_inv, heq]

/-- Exact control renaming is a same-input, same-action, same-stack T105
refinement whose erasure is the inverse equivalence. -/
def renameRefinement (W : PartialVisible.Machine Input R Γ)
    (e : ControlEquiv R R') :
    Refinement W (rename W e) where
  erase := e.invFun
  init_eq := e.left_inv W.init
  accept_eq := by intro; rfl
  apply_sound := by
    intro a action r z r' z' h
    have h' :
        (rename W e).apply a action ⟨e.toFun (e.invFun r), z⟩ =
          some ⟨e.toFun (e.invFun r'), z'⟩ := by
      simpa [e.right_inv] using h
    exact (rename_apply W e a action (e.invFun r) (e.invFun r') z z').1 h'
  apply_complete := by
    intro a action r z q' z' h
    refine ⟨e.toFun q', ?_, e.left_inv q'⟩
    have h' := (rename_apply W e a action (e.invFun r) q' z z').2 h
    simpa [e.right_inv] using h'

/-! ## Refinement composition -/

/-- Same-action, same-stack visible refinements compose. -/
def refinementTrans
    {V : PartialVisible.Machine Input Q Γ}
    {W : PartialVisible.Machine Input R Γ}
    {X : PartialVisible.Machine Input S Γ}
    (H : Refinement V W) (K : Refinement W X) : Refinement V X where
  erase := fun x => H.erase (K.erase x)
  init_eq := by rw [K.init_eq, H.init_eq]
  accept_eq := by
    intro x
    rw [K.accept_eq, H.accept_eq]
  apply_sound := by
    intro a action x z x' z' h
    exact H.apply_sound a action (K.erase x) z (K.erase x') z'
      (K.apply_sound a action x z x' z' h)
  apply_complete := by
    intro a action x z q' z' h
    rcases H.apply_complete a action (K.erase x) z q' z' h with
      ⟨r', hr, heraseH⟩
    rcases K.apply_complete a action x z r' z' hr with
      ⟨x', hx, heraseK⟩
    exact ⟨x', hx, by rw [heraseK, heraseH]⟩

/-! ## Arbitrary finite controls through canonical `Fin` slots -/

/-- Control functionality stated for an arbitrary control carrier. -/
def ControlFunctionalOn (W : PartialVisible.Machine Input R Γ) : Prop :=
  ∀ w r z₁ z₂, W.Frontier w r z₁ → W.Frontier w r z₂ → z₁ = z₂

/-- Exact frontier transport at the uniquely corresponding renamed control. -/
theorem frontier_rename (W : PartialVisible.Machine Input R Γ)
    (e : ControlEquiv R R')
    (w : List Input) (r : R) (z : List Γ) :
    (rename W e).Frontier w (e.toFun r) z ↔ W.Frontier w r z := by
  let H : Refinement W (rename W e) := renameRefinement W e
  constructor
  · intro h
    exact (H.frontier_iff_refined w r z).2
      ⟨e.toFun r, h, e.left_inv r⟩
  · intro h
    rcases (H.frontier_iff_refined w r z).1 h with
      ⟨r', hr', herase⟩
    have herase' : e.invFun r' = r := by simpa [H] using herase
    have heq : r' = e.toFun r := by
      apply e.invFun_injective
      rw [herase', e.left_inv]
    simpa [heq] using hr'

/-- Control functionality is invariant under exact control renaming. -/
theorem controlFunctional_iff
    (W : PartialVisible.Machine Input R Γ) (e : ControlEquiv R R') :
    ControlFunctionalOn (rename W e) ↔ ControlFunctionalOn W := by
  constructor
  · intro hfun w r z₁ z₂ h₁ h₂
    exact hfun w (e.toFun r) z₁ z₂
      ((frontier_rename W e w r z₁).2 h₁)
      ((frontier_rename W e w r z₂).2 h₂)
  · intro hfun w r' z₁ z₂ h₁ h₂
    exact hfun w (e.invFun r') z₁ z₂
      ((frontier_rename W e w (e.invFun r') z₁).1
        (by simpa [e.right_inv] using h₁))
      ((frontier_rename W e w (e.invFun r') z₂).1
        (by simpa [e.right_inv] using h₂))

/-- A named control-functional machine compiles after a supplied equivalence
to the fixed `Fin` slot family. -/
theorem compiled_decides_via_equiv {s : Nat}
    (W : PartialVisible.Machine Input R Γ) (e : ControlEquiv R (Fin s))
    (hfun : ControlFunctionalOn W) (w : List Input) :
    (RootSharingMachine.compile
      (ControlFunctional.executor (rename W e))).decides w = true ↔
      W.Accepts w := by
  exact (renameRefinement W e).compiled_decides_original
    ((controlFunctional_iff W e).2 hfun) w

/-- An arbitrary named finite refinement compiles the original projected
language after composing with a supplied equivalence to `Fin` controls. -/
theorem compiled_decides_original_via_equiv {s : Nat}
    {V : PartialVisible.Machine Input Q Γ}
    {W : PartialVisible.Machine Input R Γ}
    (H : Refinement V W) (e : ControlEquiv R (Fin s))
    (hfun : ControlFunctionalOn W) (w : List Input) :
    (RootSharingMachine.compile
      (ControlFunctional.executor (rename W e))).decides w = true ↔
      V.Accepts w := by
  exact (refinementTrans H (renameRefinement W e)).compiled_decides_original
    ((controlFunctional_iff W e).2 hfun) w

#check renameRefinement
#check refinementTrans
#check controlFunctional_iff
#check compiled_decides_via_equiv
#check compiled_decides_original_via_equiv

end FrontierDerivative.FiniteReindexing