ActionWindowEscapeExamples.lean

import FrontierDerivative.BoundedActionWindow

/-!
# Every fixed action window can fail on a regular projection

One one-state partial visible machine accepts every unary input through its
local action.  For each fixed window depth `k`, the same observed word also
has two successful traces: an initial call followed by `k` local actions, and
`k + 1` local actions.  The traces finish in the same control with different
stacks, while their newest-first depth-`k` action windows agree.

This separates the bounded-action-window coordinate doctrine from language
recognition.  It is not a PEG or scaffold lower bound.
-/

namespace FrontierDerivative.ActionWindowEscapeExamples

open BoundedActionWindow

/-- A unary, one-control visible source. Calls push `7`, locals preserve the
stack, returns fail, and the only control is accepting. -/
def universalProjection : PartialVisible.Machine Unit Unit Nat where
  call := fun _ _ => some ((), 7)
  ret := fun _ _ _ => none
  localStep := fun _ _ => some ()
  init := ()
  accept := fun _ => true

/-- A chronological suffix of `k` local actions. -/
def localActions : Nat → List VisibleAction
  | 0 => []
  | k + 1 => localActions k ++ [.local]

@[simp] theorem localActions_length (k : Nat) : (localActions k).length = k := by
  induction k with
  | zero => rfl
  | succ k ih => simp [localActions, ih]

/-- A unary suffix of `k` observed letters. -/
def unitLetters : Nat → List Unit
  | 0 => []
  | k + 1 => unitLetters k ++ [()]

/-- The shared observed word used by the depth-`k` collision. -/
def collisionWord (k : Nat) : List Unit := [()] ++ unitLetters k

/-- A traced run is also an ordinary successful tagged run when its explicit
action list is forgotten. -/
theorem traced_to_tagged {Input Q Γ : Type}
    {V : PartialVisible.Machine Input Q Γ}
    {w : List Input} {actions : List VisibleAction}
    {c : PartialVisible.Config Q Γ}
    (h : TracedReachable V w actions c) :
    V.TaggedReachable w c := by
  induction h with
  | init => exact PartialVisible.Machine.TaggedReachable.init
  | step a action _ happly ih =>
      exact PartialVisible.Machine.TaggedReachable.step a action ih happly

/-- Appending `k` local rounds preserves the current stack exactly. -/
theorem append_local_trace {w : List Unit} {actions : List VisibleAction}
    {stack : List Nat}
    (h : TracedReachable universalProjection w actions ⟨(), stack⟩) :
    ∀ k,
      TracedReachable universalProjection
        (w ++ unitLetters k) (actions ++ localActions k) ⟨(), stack⟩ := by
  intro k
  induction k with
  | zero => simpa [unitLetters, localActions] using h
  | succ k ih =>
      have hstep := TracedReachable.step () .local ih (by rfl)
      simpa [unitLetters, localActions, List.append_assoc] using hstep

theorem first_call_trace :
    TracedReachable universalProjection [()] [.call] ⟨(), [7]⟩ :=
  TracedReachable.step () .call TracedReachable.init (by rfl)

theorem first_local_trace :
    TracedReachable universalProjection [()] [.local] ⟨(), []⟩ :=
  TracedReachable.step () .local TracedReachable.init (by rfl)

/-- The first collision trace calls once, then remains local for `k` rounds. -/
theorem call_then_locals_trace (k : Nat) :
    TracedReachable universalProjection (collisionWord k)
      ([.call] ++ localActions k) ⟨(), [7]⟩ := by
  exact append_local_trace first_call_trace k

/-- The second collision trace remains local in all `k + 1` rounds. -/
theorem all_locals_trace (k : Nat) :
    TracedReachable universalProjection (collisionWord k)
      ([.local] ++ localActions k) ⟨(), []⟩ := by
  exact append_local_trace first_local_trace k

/-- `windowOf` is the reversed chronological suffix of length at most `k`. -/
theorem windowOf_value (k : Nat) (actions : List VisibleAction) :
    (windowOf k actions).1 = actions.reverse.take k := by
  exact PartialVisible.list_snoc_induction
    (motive := fun xs =>
      (windowOf k xs).1 = xs.reverse.take k)
    (by simp [windowOf, emptyWindow])
    (by
      intro xs action ih
      rw [windowOf_append]
      change (action :: (windowOf k xs).1).take k =
        (xs ++ [action]).reverse.take k
      rw [ih]
      simp only [List.reverse_append, List.reverse_singleton,
        List.singleton_append]
      cases k with
      | zero => rfl
      | succ k =>
          simp only [List.take_succ_cons, List.take_take,
            Nat.min_eq_left (Nat.le_succ k)])
    actions

/-- The differing first action lies exactly beyond the retained depth. -/
theorem collision_windows_equal (k : Nat) :
    windowOf k ([.call] ++ localActions k) =
      windowOf k ([.local] ++ localActions k) := by
  apply Subtype.ext
  rw [windowOf_value, windowOf_value]
  simp only [List.singleton_append, List.reverse_cons]
  have hlength : k ≤ (localActions k).reverse.length := by
    simp
  rw [List.take_append_of_le_length hlength,
    List.take_append_of_le_length hlength]

theorem call_stack_in_windowFrontier (k : Nat) :
    WindowFrontier universalProjection k (collisionWord k)
      (windowOf k ([.call] ++ localActions k)) () [7] :=
  ⟨[.call] ++ localActions k, call_then_locals_trace k, rfl⟩

theorem empty_stack_in_windowFrontier (k : Nat) :
    WindowFrontier universalProjection k (collisionWord k)
      (windowOf k ([.call] ++ localActions k)) () [] :=
  ⟨[.local] ++ localActions k, all_locals_trace k,
    (collision_windows_equal k).symm⟩

/-- No fixed suffix of hidden actions separates the concrete frontier. -/
theorem universal_not_windowSeparated (k : Nat) :
    ¬WindowSeparated universalProjection k := by
  intro hsep
  have hstack : ([7] : List Nat) = [] :=
    hsep (collisionWord k) (windowOf k ([.call] ++ localActions k)) ()
      [7] [] (call_stack_in_windowFrontier k)
      (empty_stack_in_windowFrontier k)
  simp at hstack

/-- Every observed word is accepted through its all-local trace, including
the empty word. -/
theorem universal_accepts (w : List Unit) : universalProjection.Accepts w := by
  have htrace : ∃ actions,
      TracedReachable universalProjection w actions ⟨(), []⟩ := by
    exact PartialVisible.list_snoc_induction
      (motive := fun xs => ∃ actions,
        TracedReachable universalProjection xs actions ⟨(), []⟩)
      ⟨[], TracedReachable.init⟩
      (by
        intro xs letter h
        rcases letter with ⟨⟩
        rcases h with ⟨actions, htrace⟩
        exact ⟨actions ++ [.local],
          TracedReachable.step () .local htrace (by rfl)⟩)
      w
  rcases htrace with ⟨actions, htrace⟩
  exact ⟨(), [], PartialVisible.Machine.tagged_to_frontier
    universalProjection (traced_to_tagged htrace), rfl⟩

#check universal_accepts
#check call_then_locals_trace
#check all_locals_trace
#check collision_windows_equal
#check universal_not_windowSeparated

end FrontierDerivative.ActionWindowEscapeExamples