sgl_mark_times

import Definitions.Def_sgl_patch_run
import Definitions.Def_sgl_shift_seg
import Definitions.Def_sgl_xor_walk

/-!
# A tally of fixed width

The polynomial that bounds the delegate's running time is a hypothesis, so
its coefficient and degree are naturals the construction may read off before
the machine is built.  Turning them into tape content needs a machine that
writes a *constant* number of marks: a counter whose state type is `Fin
(c + 1)`, one mark per step.
-/

namespace SipserGacsLautemann

variable {tapes : Nat}

/-- Write `c` marks, walking right. -/
def markTimes (i : Fin tapes) (c : Nat) : TypedMachine tapes (Fin (c + 1))
    where
  start := ⟨0, by omega⟩
  transition := fun s symbols =>
    if h : s.val < c then
      (⟨s.val + 1, by omega⟩,
        fun j =>
          if j = i then (TapeSymbol.bit true, HeadMove.right)
          else (symbols j, HeadMove.stay))
    else (s, fun j => (symbols j, HeadMove.stay))
  result := fun s => if s.val = c then some true else none

theorem markTimes_step (i : Fin tapes) (c m : Nat) (hm : m < c)
    (t : Fin tapes → Tape) :
    (markTimes i c).step ⟨⟨m, by omega⟩, t⟩ =
      ⟨⟨m + 1, by omega⟩, Function.update t i
        (moveDir HeadMove.right (Tape.write (t i) (TapeSymbol.bit true)))⟩ := by
  have hres : (markTimes i c).result ⟨m, by omega⟩ = none := by
    simp only [markTimes]
    rw [if_neg (by omega : ¬(m = c))]
  simp only [TypedMachine.step, hres]
  simp only [markTimes, dif_pos hm]
  congr 1
  funext j
  by_cases hj : j = i
  · subst hj
    simp [moveDir]
  · simp [hj, Tape.write_head_self, Tape.move]

/-- Each step lays one mark down and steps off it. -/
theorem markTimes_run (i : Fin tapes) (c : Nat) :
    ∀ (m : Nat) (hm : m ≤ c) (tape : Fin tapes → Tape) (L : List TapeSymbol),
      tape i = cellsTape L [] →
      ((markTimes i c).step^[m]) ((markTimes i c).startCfg tape) =
        ⟨⟨m, by omega⟩, Function.update tape i
          (cellsTape (List.replicate m (TapeSymbol.bit true) ++ L) [])⟩ := by
  intro m
  induction m with
  | zero =>
      intro _ tape L htape
      show ((markTimes i c).startCfg tape) = _
      rw [show List.replicate 0 (TapeSymbol.bit true) ++ L = L from rfl,
        ← htape, Function.update_eq_self]
      rfl
  | succ m ih =>
      intro hm tape L htape
      rw [Function.iterate_succ_apply', ih (by omega) tape L htape,
        markTimes_step i c m (by omega)]
      congr 1
      funext j
      by_cases hj : j = i
      · subst hj
        rw [Function.update_self, Function.update_self,
          Function.update_self]
        show moveDir HeadMove.right
            (Tape.write (cellsTape
              (List.replicate m (TapeSymbol.bit true) ++ L) []) _) = _
        rw [write_cellsTape, cellsTape_moveRight_headD]
        show cellsTape (TapeSymbol.bit true ::
          (List.replicate m (TapeSymbol.bit true) ++ L)) _ = _
        rw [show List.replicate (m + 1) (TapeSymbol.bit true) ++ L =
          TapeSymbol.bit true ::
            (List.replicate m (TapeSymbol.bit true) ++ L) from rfl]
        rfl
      · rw [Function.update_of_ne hj, Function.update_of_ne hj,
          Function.update_of_ne hj]

/-- **The fixed tally.**  From a frontier the machine leaves `c` marks with
the head just past them, at cost `c`. -/
theorem markTimes_spec (i : Fin tapes) (c : Nat) (tape : Fin tapes → Tape)
    (L : List TapeSymbol) (htape : tape i = cellsTape L []) :
    HaltsExactly (markTimes i c) ((markTimes i c).startCfg tape) c true := by
  constructor
  · rw [markTimes_run i c c (by omega) tape L htape]
    show (markTimes i c).result ⟨c, by omega⟩ = some true
    simp only [markTimes]
    rw [if_pos trivial]
  · intro j hj
    rw [markTimes_run i c j (by omega) tape L htape]
    show (markTimes i c).result ⟨j, by omega⟩ = none
    simp only [markTimes]
    rw [if_neg (by omega : ¬(j = c))]

theorem markTimes_tape (i : Fin tapes) (c : Nat) (tape : Fin tapes → Tape)
    (L : List TapeSymbol) (htape : tape i = cellsTape L []) :
    (((markTimes i c).step^[c]) ((markTimes i c).startCfg tape)).tape =
      Function.update tape i
        (cellsTape (List.replicate c (TapeSymbol.bit true) ++ L) []) := by
  rw [markTimes_run i c c (by omega) tape L htape]

end SipserGacsLautemann