sgl_marked_loop

import Definitions.Def_sgl_offset_inv

/-!
# Repeating a body once per mark

`guidedWalk` performs one *cell action* per mark of its guide.  Building a
product needs one whole *subroutine* per mark — a run appended for each mark of
the multiplier — and no existing combinator does that.

`markedLoop` does: body, then step the guide, then ask whether the guide still
carries a mark.  It is the offset scheduler's loop with the round replaced by
an arbitrary subroutine and the carry dropped, so `repeatUntilFalse` suffices
where the scheduler needed `loopState`.

The body is described by its effect on the tapes rather than by what it is, so
one proof serves every use.  It must leave the guide alone; that is the only
thing asked of it.
-/

namespace SipserGacsLautemann

variable {tapes : Nat} {S : Type}

/-- Run `body` once for each mark of `g`. -/
def markedLoop (g : Fin tapes) (body : TypedMachine tapes S) :=
  (body.andThen fun _ =>
    (moveUpTo g 1 HeadMove.right).andThen fun _ =>
      TypedMachine.test (notBlankAt g)).repeatUntilFalse

/-- One round's effect: the body, then the guide advances. -/
def markedStep (g : Fin tapes) (f : (Fin tapes → Tape) → (Fin tapes → Tape))
    (T : Fin tapes → Tape) : Fin tapes → Tape :=
  Function.update (f T) g (moveDir HeadMove.right ((f T) g))

/-- The guide's position after `r` rounds. -/
theorem markedStep_guide (g : Fin tapes)
    (f : (Fin tapes → Tape) → (Fin tapes → Tape))
    (hfg : ∀ T, (f T) g = T g) (m : Nat) (Lg Rg : List TapeSymbol) :
    ∀ (r : Nat) (T : Fin tapes → Tape), r ≤ m →
      T g = cellsTape (List.replicate r (TapeSymbol.bit true) ++ Lg)
        (List.replicate (m - r) (TapeSymbol.bit true) ++
          TapeSymbol.blank :: Rg) →
      (markedStep g f T) g =
        cellsTape (List.replicate (r + 1) (TapeSymbol.bit true) ++ Lg)
          (List.replicate (m - (r + 1)) (TapeSymbol.bit true) ++
            TapeSymbol.blank :: Rg) ∨ r = m := by
  intro r T hr hT
  by_cases hrm : r < m
  · left
    rw [markedStep, Function.update_self, hfg, hT]
    exact guide_reenters m r hrm Lg Rg
  · right
    omega

set_option maxHeartbeats 1000000 in
/-- **One round of the marked loop.** -/
theorem markedLoop_round (g : Fin tapes) (body : TypedMachine tapes S)
    (f : (Fin tapes → Tape) → (Fin tapes → Tape)) (cb : Nat)
    (hbody : ∀ T, HaltsExactly body (body.startCfg T) cb true ∧
      ((body.step^[cb]) (body.startCfg T)).tape = f T)
    (hfg : ∀ T, (f T) g = T g)
    (m r : Nat) (hr : r < m) (T : Fin tapes → Tape)
    (Lg Rg : List TapeSymbol)
    (hT : T g = cellsTape (List.replicate r (TapeSymbol.bit true) ++ Lg)
      (List.replicate (m - r) (TapeSymbol.bit true) ++
        TapeSymbol.blank :: Rg)) :
    HaltsExactly (body.andThen fun _ =>
        (moveUpTo g 1 HeadMove.right).andThen fun _ =>
          TypedMachine.test (notBlankAt g))
      ((body.andThen fun _ =>
        (moveUpTo g 1 HeadMove.right).andThen fun _ =>
          TypedMachine.test (notBlankAt g)).startCfg T)
      (cb + 1 + (1 + 1 + 1)) (decide (r + 1 < m)) ∧
    (((body.andThen fun _ =>
        (moveUpTo g 1 HeadMove.right).andThen fun _ =>
          TypedMachine.test (notBlankAt g)).step^[cb + 1 + (1 + 1 + 1)])
      ((body.andThen fun _ =>
        (moveUpTo g 1 HeadMove.right).andThen fun _ =>
          TypedMachine.test (notBlankAt g)).startCfg T)).tape =
      markedStep g f T := by
  classical
  obtain ⟨g1, s1⟩ := hbody T
  have g2 := moveUpTo_spec g 1 HeadMove.right (by omega) (f T)
  have s2 : (((moveUpTo g 1 HeadMove.right).step^[1])
      ((moveUpTo g 1 HeadMove.right).startCfg (f T))).tape =
      markedStep g f T := by
    rw [moveUpTo_tape g 1 HeadMove.right (by omega) (f T), markedStep,
      Function.iterate_one]
  have hgd : (markedStep g f T) g =
      cellsTape (List.replicate (r + 1) (TapeSymbol.bit true) ++ Lg)
        (List.replicate (m - (r + 1)) (TapeSymbol.bit true) ++
          TapeSymbol.blank :: Rg) := by
    rw [markedStep, Function.update_self, hfg, hT]
    exact guide_reenters m r hr Lg Rg
  have hread : notBlankAt g (fun i => ((markedStep g f T) i).head) =
      decide (r + 1 < m) := by
    have hhead := guide_head m (r + 1) Lg Rg
    rw [← hgd] at hhead
    by_cases hrm : r + 1 < m
    · rw [if_pos hrm] at hhead
      rw [notBlankAt_true g _ (by rw [hhead]; simp), decide_eq_true hrm]
    · rw [if_neg hrm] at hhead
      rw [notBlankAt_false g _ hhead, decide_eq_false hrm]
  have g3 := TypedMachine.test_spec (notBlankAt g) (markedStep g f T)
  rw [hread] at g3
  have k2 := chainStepC g2 s2 g3
  have k1 := chainStepC g1 s1 k2.1
  refine ⟨k1.1, ?_⟩
  have hIR : ∀ {S₁ S₂ : Type} (b : Bool) (c : TypedConfiguration tapes S₂),
      (TypedConfiguration.inRight (S₁ := S₁) b c).tape = c.tape :=
    fun _ _ => rfl
  rw [k1.2, hIR, k2.2, hIR, TypedMachine.test_tape]

/-- The guide's position after `r` rounds. -/
theorem markedStep_iterate_guide (g : Fin tapes)
    (f : (Fin tapes → Tape) → (Fin tapes → Tape))
    (hfg : ∀ T, (f T) g = T g) (m : Nat) (Lg Rg : List TapeSymbol)
    (T : Fin tapes → Tape)
    (hT : T g = cellsTape Lg
      (List.replicate m (TapeSymbol.bit true) ++ TapeSymbol.blank :: Rg)) :
    ∀ r : Nat, r ≤ m →
      (((markedStep g f)^[r]) T) g =
        cellsTape (List.replicate r (TapeSymbol.bit true) ++ Lg)
          (List.replicate (m - r) (TapeSymbol.bit true) ++
            TapeSymbol.blank :: Rg) := by
  intro r
  induction r with
  | zero => intro _; simpa using hT
  | succ r ih =>
      intro hr
      have hprev := ih (by omega)
      rw [Function.iterate_succ_apply', markedStep, Function.update_self, hfg,
        hprev]
      exact guide_reenters m r (by omega) Lg Rg

set_option maxHeartbeats 1000000 in
/-- **The marked loop.**  The body runs once per mark of the guide, and the
guide ends past them. -/
theorem markedLoop_spec (g : Fin tapes) (body : TypedMachine tapes S)
    (f : (Fin tapes → Tape) → (Fin tapes → Tape)) (cb : Nat)
    (hbody : ∀ T, HaltsExactly body (body.startCfg T) cb true ∧
      ((body.step^[cb]) (body.startCfg T)).tape = f T)
    (hfg : ∀ T, (f T) g = T g)
    (m : Nat) (hm : 1 ≤ m) (T : Fin tapes → Tape) (Lg Rg : List TapeSymbol)
    (hT : T g = cellsTape Lg
      (List.replicate m (TapeSymbol.bit true) ++ TapeSymbol.blank :: Rg)) :
    HaltsExactly (markedLoop g body) ((markedLoop g body).startCfg T)
      ((m - 1) * (cb + 1 + (1 + 1 + 1) + 1) + (cb + 1 + (1 + 1 + 1))) false ∧
    (((markedLoop g body).step^[
        (m - 1) * (cb + 1 + (1 + 1 + 1) + 1) + (cb + 1 + (1 + 1 + 1))])
      ((markedLoop g body).startCfg T)).tape = ((markedStep g f)^[m]) T := by
  classical
  set body' := body.andThen fun _ =>
    (moveUpTo g 1 HeadMove.right).andThen fun _ =>
      TypedMachine.test (notBlankAt g) with hbody'
  set cfg : Nat → TypedConfiguration tapes _ :=
    fun r => body'.startCfg (((markedStep g f)^[r]) T) with hcfg
  have hkey : ∀ r, r < m →
      HaltsExactly body' (cfg r) (cb + 1 + (1 + 1 + 1)) (decide (r + 1 < m)) ∧
      ((body'.step^[cb + 1 + (1 + 1 + 1)]) (cfg r)).tape =
        ((markedStep g f)^[r + 1]) T := by
    intro r hr
    have hg := markedStep_iterate_guide g f hfg m Lg Rg T hT r (by omega)
    obtain ⟨h1, h2⟩ := markedLoop_round g body f cb hbody hfg m r hr
      (((markedStep g f)^[r]) T) Lg Rg hg
    refine ⟨h1, ?_⟩
    rw [h2, Function.iterate_succ_apply']
  have hround : ∀ i, i < m - 1 →
      HaltsExactly body' (cfg i) (cb + 1 + (1 + 1 + 1)) true ∧
      cfg (i + 1) =
        ⟨body'.start, ((body'.step^[cb + 1 + (1 + 1 + 1)]) (cfg i)).tape⟩ := by
    intro i hi
    obtain ⟨h1, h2⟩ := hkey i (by omega)
    rw [decide_eq_true (by omega : i + 1 < m)] at h1
    refine ⟨h1, ?_⟩
    show body'.startCfg (((markedStep g f)^[i + 1]) T) = _
    rw [← h2]
    rfl
  have hexitr : HaltsExactly body' (cfg (m - 1)) (cb + 1 + (1 + 1 + 1)) false := by
    obtain ⟨h1, _⟩ := hkey (m - 1) (by omega)
    rw [decide_eq_false (by omega : ¬ (m - 1) + 1 < m)] at h1
    exact h1
  have hspec := TypedMachine.repeatUntilFalse_spec body' cfg
    (fun _ => cb + 1 + (1 + 1 + 1)) (m - 1) (cb + 1 + (1 + 1 + 1))
    hround hexitr
  rw [loopCost_const] at hspec
  have hrun := TypedMachine.repeatUntilFalse_rounds body' cfg
    (fun _ => cb + 1 + (1 + 1 + 1)) (m - 1) hround
  rw [loopCost_const] at hrun
  have hstart : (markedLoop g body).startCfg T = cfg 0 := rfl
  refine ⟨by rw [hstart]; exact hspec, ?_⟩
  rw [hstart, Nat.add_comm, Function.iterate_add_apply]
  show ((body'.repeatUntilFalse.step^[cb + 1 + (1 + 1 + 1)])
    ((body'.repeatUntilFalse.step^[(m - 1) * (cb + 1 + (1 + 1 + 1) + 1)])
      (cfg 0))).tape = _
  rw [hrun, body'.repeatUntilFalse_iterate_fresh (cfg (m - 1))
    (cb + 1 + (1 + 1 + 1)) hexitr.fresh]
  obtain ⟨_, h2⟩ := hkey (m - 1) (by omega)
  rw [h2]
  congr 1
  omega

end SipserGacsLautemann