sgl_ss_tapes

import Definitions.Def_sgl_xor_walk
import Definitions.Def_sgl_tape_locality
import Definitions.Def_sgl_embed_clock

/-!
# Tape bridges for the single-shift machine

Four small facts the single-shift assembly needs.

* A tape advanced `k` cells right still presents `R.drop k`, whatever
  piles up on its left.
* `xorCells` cannot see an explicit terminating blank: the zipper pads
  with blanks anyway.
* A prepared input tape — origin marker and explicit terminator — agrees
  with the raw `cellsTape [] x` at every radius, so a delegate started on
  one behaves as on the other.
* A tape family whose clock tape is pristine *is* its own `clockTapes`
  presentation, letting `embedClock_spec` apply in place.
-/

namespace SipserGacsLautemann

/-- Whatever accumulates on the left, `k` right-moves expose `R.drop k`. -/
theorem moveRight_iterate_exists (k : Nat) :
    ∀ (L R : List TapeSymbol),
      ∃ L' : List TapeSymbol,
        ((Tape.move · HeadMove.right)^[k]) (cellsTape L R) =
          cellsTape L' (R.drop k) := by
  induction k with
  | zero => intro L R; exact ⟨L, by simp⟩
  | succ k ih =>
      intro L R
      rw [Function.iterate_succ_apply]
      obtain ⟨L', hL'⟩ := ih (R.headD TapeSymbol.blank :: L) R.tail
      refine ⟨L', ?_⟩
      have hmv : Tape.move (cellsTape L R) HeadMove.right =
          cellsTape (R.headD TapeSymbol.blank :: L) R.tail :=
        cellsTape_moveRight_headD L R
      rw [hmv, hL']
      congr 1
      rw [← List.drop_one, List.drop_drop, Nat.add_comm]

/-- The zipper pads with blanks, so an explicit terminator is invisible. -/
theorem xorCells_append_blank :
    ∀ (cs Rs : List TapeSymbol),
      xorCells cs (Rs ++ [TapeSymbol.blank]) = xorCells cs Rs := by
  intro cs
  induction cs with
  | nil => intro Rs; rfl
  | cons c cs ih =>
      intro Rs
      cases Rs with
      | nil =>
          show TapeSymbol.bit _ :: xorCells cs ([TapeSymbol.blank].tail) =
            TapeSymbol.bit _ :: xorCells cs ([].tail)
          rfl
      | cons r Rs =>
          show TapeSymbol.bit _ :: xorCells cs (Rs ++ [TapeSymbol.blank]) =
            TapeSymbol.bit _ :: xorCells cs Rs
          rw [ih Rs]
          rfl

/-- Every cell `xorCells` writes is a bit. -/
theorem xorCells_nonblank :
    ∀ (cs Rs : List TapeSymbol), ∀ c ∈ xorCells cs Rs,
      c ≠ TapeSymbol.blank := by
  intro cs
  induction cs with
  | nil => intro Rs c hc; simp [xorCells] at hc
  | cons a cs ih =>
      intro Rs c hc
      rw [xorCells] at hc
      rcases List.mem_cons.mp hc with h | h
      · rw [h]; simp
      · exact ih Rs.tail c h

/-- `getD` cannot see a single appended blank when the default is blank. -/
theorem ssGetD_append_blank :
    ∀ (l : List TapeSymbol) (i : Nat),
      (l ++ [TapeSymbol.blank]).getD i TapeSymbol.blank =
        l.getD i TapeSymbol.blank := by
  intro l
  induction l with
  | nil =>
      intro i
      cases i with
      | zero => rfl
      | succ i => simp [List.getD]
  | cons a l ih =>
      intro i
      cases i with
      | zero => rfl
      | succ i =>
          show (l ++ [TapeSymbol.blank]).getD i TapeSymbol.blank =
            l.getD i TapeSymbol.blank
          exact ih i

/-- **A prepared tape is observationally the raw tape.**  Origin marker and
explicit terminator sit exactly where the zipper would have padded blanks. -/
theorem tapeAgree_prepared (t : Nat) (x : List TapeSymbol) :
    TapeAgree t
      (cellsTape [TapeSymbol.blank] (x ++ [TapeSymbol.blank]))
      (cellsTape [] x) := by
  refine ⟨?_, ?_, ?_⟩
  · show (x ++ [TapeSymbol.blank]).headD TapeSymbol.blank =
      x.headD TapeSymbol.blank
    cases x with
    | nil => rfl
    | cons a x => rfl
  · intro i _
    show ([TapeSymbol.blank] : List TapeSymbol).getD i TapeSymbol.blank =
      ([] : List TapeSymbol).getD i TapeSymbol.blank
    cases i with
    | zero => rfl
    | succ i => simp [List.getD]
  · intro i _
    show (x ++ [TapeSymbol.blank]).tail.getD i TapeSymbol.blank =
      x.tail.getD i TapeSymbol.blank
    cases x with
    | nil => simp [List.getD]
    | cons a x =>
        show (x ++ [TapeSymbol.blank]).getD i TapeSymbol.blank =
          x.getD i TapeSymbol.blank
        exact ssGetD_append_blank x i

/-- A tape agrees with itself at every radius. -/
theorem tapeAgree_refl (t : Nat) (a : Tape) : TapeAgree t a a :=
  ⟨rfl, fun _ _ => rfl, fun _ _ => rfl⟩

/-- **A pristine-clock family is its own `clockTapes` presentation.** -/
theorem clockTapes_self {k n : Nat} (ι : Fin k → Fin n) (clk : Fin n)
    (cur : Fin n → Tape) (hclk : cur clk = cellsTape [] []) :
    clockTapes ι clk cur (fun j => cur (ι j)) 0 = cur := by
  funext i
  show (if i = clk then cellsTape (List.replicate 0 (TapeSymbol.bit true)) []
    else if h : ∃ j, ι j = i then (fun j => cur (ι j)) h.choose
    else cur i) = cur i
  by_cases hi : i = clk
  · rw [if_pos hi, List.replicate_zero, hi, hclk]
  · rw [if_neg hi]
    by_cases hex : ∃ j, ι j = i
    · rw [dif_pos hex]
      show cur (ι hex.choose) = cur i
      rw [hex.choose_spec]
    · rw [dif_neg hex]

end SipserGacsLautemann