sgl_tally2

import Definitions.Def_sgl_offset_inv

/-!
# The tally, re-homed

`tallyOnto` and `writeMark` live in the clock-setup module, which sits at the
top of the prologue chain — far deeper than anything the multiplier needs.
The platform compiles a submission's entire import closure from source, so an
import that is merely convenient costs minutes of someone else's compile time.
These are the same machines under new names, homed at the depth they require.
-/

namespace SipserGacsLautemann

variable {tapes : Nat}

/-- Write a mark and advance. -/
def putMark (i : Fin tapes) :=
  TypedMachine.act (fun symbols j =>
    if j = i then (TapeSymbol.bit true, HeadMove.right)
    else (symbols j, HeadMove.stay))

theorem putMark_spec (i : Fin tapes) (L R : List TapeSymbol)
    (T : Fin tapes → Tape) (hT : T i = cellsTape L R) :
    HaltsExactly (putMark i) ((putMark i).startCfg T) 1 true ∧
    (((putMark i).step^[1]) ((putMark i).startCfg T)).tape =
      Function.update T i (cellsTape (TapeSymbol.bit true :: L) R.tail) := by
  classical
  refine ⟨TypedMachine.act_spec
    (fun symbols : Fin tapes → TapeSymbol => fun j =>
      if j = i then (TapeSymbol.bit true, HeadMove.right)
      else (symbols j, HeadMove.stay)) T, ?_⟩
  rw [Function.iterate_one]
  funext j
  by_cases hj : j = i
  · rw [hj]
    have hcell : Tape.move (Tape.write (T i) (TapeSymbol.bit true))
        HeadMove.right = cellsTape (TapeSymbol.bit true :: L) R.tail := by
      rw [hT, write_cellsTape]
      exact cellsTape_moveRight L (TapeSymbol.bit true) R.tail
    simp [putMark, TypedMachine.step, TypedMachine.act,
      TypedMachine.startCfg, hcell]
  · simp [putMark, TypedMachine.step, TypedMachine.act,
      TypedMachine.startCfg, hj, Tape.write_head_self, Tape.move]

/-- Tally one input onto a target, rewinding only the input. -/
def copyTally (s w : Fin tapes) :=
  (guidedWalk s w HeadMove.right (some (TapeSymbol.bit true))).andThen fun _ =>
    rewindRun s

set_option maxHeartbeats 4000000 in
/-- **One tally.**  The target gains one mark per cell of the input and its head
sits past them; the input is restored. -/
theorem copyTally_spec (s w : Fin tapes) (hsw : s ≠ w)
    (x Ls Rs Lw Rw : List TapeSymbol) (T : Fin tapes → Tape)
    (hnb : ∀ c ∈ x, c ≠ TapeSymbol.blank)
    (hs : T s = cellsTape (TapeSymbol.blank :: Ls)
      (x ++ TapeSymbol.blank :: Rs))
    (hw : T w = cellsTape Lw Rw) :
    ∃ cost : Nat,
      HaltsExactly (copyTally s w) ((copyTally s w).startCfg T) cost true ∧
      (((copyTally s w).step^[cost]) ((copyTally s w).startCfg T)).tape =
        Function.update T w
          (cellsTape (List.replicate x.length (TapeSymbol.bit true) ++ Lw)
            (Rw.drop x.length)) := by
  classical
  obtain ⟨hia, hib⟩ := guidedStep_write_iterate s w hsw x T
    (TapeSymbol.blank :: Ls) (TapeSymbol.blank :: Rs) Lw Rw (by rw [hs]) hw
  obtain ⟨hW, hWt⟩ := guidedWalk_spec s w hsw HeadMove.right
    (some (TapeSymbol.bit true)) x.length T
    (guidedStep_write_marks s w hsw x T (TapeSymbol.blank :: Ls)
      (TapeSymbol.blank :: Rs) Lw Rw hnb (by rw [hs]) hw)
    (by rw [hia]; rfl)
  set T1 := ((guidedStep s w HeadMove.right
    (some (TapeSymbol.bit true)))^[x.length]) T with hT1
  have hT1s : T1 s = cellsTape (x.reverse ++ TapeSymbol.blank :: Ls)
      (TapeSymbol.blank :: Rs) := hia
  obtain ⟨hR, hRt⟩ := rewindRun_spec s x Ls Rs TapeSymbol.blank T1 hnb
    (by rw [hT1s])
  have hch := chainStepC hW hWt hR
  refine ⟨_, hch.1, ?_⟩
  have hfin : ((copyTally s w).step^[_])
      ((copyTally s w).startCfg T) = _ := hch.2
  rw [hfin]
  show (((rewindRun s).step^[_]) ((rewindRun s).startCfg T1)).tape = _
  rw [hRt]
  funext j
  by_cases hj : j = s
  · subst hj
    rw [Function.update_self, Function.update_of_ne hsw, hs]
  · rw [Function.update_of_ne hj]
    by_cases hj2 : j = w
    · subst hj2
      rw [Function.update_self]
      exact hib
    · rw [Function.update_of_ne hj2, hT1,
        guidedStep_other s w HeadMove.right (some (TapeSymbol.bit true))
          x.length T j hj hj2]

set_option maxHeartbeats 4000000 in
/-- The tally, with its cost named. -/
theorem copyTally_exact (s w : Fin tapes) (hsw : s ≠ w)
    (x Ls Rs Lw Rw : List TapeSymbol) (T : Fin tapes → Tape)
    (hnb : ∀ c ∈ x, c ≠ TapeSymbol.blank)
    (hs : T s = cellsTape (TapeSymbol.blank :: Ls)
      (x ++ TapeSymbol.blank :: Rs))
    (hw : T w = cellsTape Lw Rw) :
    HaltsExactly (copyTally s w) ((copyTally s w).startCfg T)
        (x.length * 5 + 4 + 1 + (x.length * 4 + 3 + 1 + 1)) true ∧
      (((copyTally s w).step^[x.length * 5 + 4 + 1 +
        (x.length * 4 + 3 + 1 + 1)]) ((copyTally s w).startCfg T)).tape =
        Function.update T w
          (cellsTape (List.replicate x.length (TapeSymbol.bit true) ++ Lw)
            (Rw.drop x.length)) := by
  classical
  obtain ⟨hia, hib⟩ := guidedStep_write_iterate s w hsw x T
    (TapeSymbol.blank :: Ls) (TapeSymbol.blank :: Rs) Lw Rw (by rw [hs]) hw
  obtain ⟨hW, hWt⟩ := guidedWalk_spec s w hsw HeadMove.right
    (some (TapeSymbol.bit true)) x.length T
    (guidedStep_write_marks s w hsw x T (TapeSymbol.blank :: Ls)
      (TapeSymbol.blank :: Rs) Lw Rw hnb (by rw [hs]) hw)
    (by rw [hia]; rfl)
  set T1 := ((guidedStep s w HeadMove.right
    (some (TapeSymbol.bit true)))^[x.length]) T with hT1
  have hT1s : T1 s = cellsTape (x.reverse ++ TapeSymbol.blank :: Ls)
      (TapeSymbol.blank :: Rs) := hia
  obtain ⟨hR, hRt⟩ := rewindRun_spec s x Ls Rs TapeSymbol.blank T1 hnb
    (by rw [hT1s])
  have hch := chainStepC hW hWt hR
  refine ⟨hch.1, ?_⟩
  have hfin : ((copyTally s w).step^[_])
      ((copyTally s w).startCfg T) = _ := hch.2
  rw [hfin]
  show (((rewindRun s).step^[_]) ((rewindRun s).startCfg T1)).tape = _
  rw [hRt]
  funext j
  by_cases hj : j = s
  · subst hj
    rw [Function.update_self, Function.update_of_ne hsw, hs]
  · rw [Function.update_of_ne hj]
    by_cases hj2 : j = w
    · subst hj2
      rw [Function.update_self]
      exact hib
    · rw [Function.update_of_ne hj2, hT1,
        guidedStep_other s w HeadMove.right (some (TapeSymbol.bit true))
          x.length T j hj hj2]


end SipserGacsLautemann