sgl_left_loop

import Definitions.Def_sgl_simul_walk

/-!
# One subroutine per mark, walking left

The marks were counted by walking right; the work happens walking back.  Each
round steps the guide left and asks what it landed on: a mark runs the body, 
the blank below the run exits without running it — so the body runs exactly
once per mark, and the off-by-one that a test-after-body loop would commit at
the origin never arises.
-/

namespace SipserGacsLautemann

variable {tapes : Nat} {S : Type}

/-- A leftward move, uniformly: the cell below the head — blank if the left
context has run out — takes the head's place, and the head cell joins the
right context. -/
theorem cellsTape_moveLeft_headD (L R : List TapeSymbol) :
    moveDir HeadMove.left (cellsTape L R) =
      cellsTape L.tail (L.headD TapeSymbol.blank ::
        (R.headD TapeSymbol.blank :: R.tail)) := by
  cases L with
  | nil => cases R <;> rfl
  | cons a rest => cases R <;> rfl

/-- Halt at once with a fixed verdict, at any state type — the do-nothing
branch a typed dispatch needs when its other branch is a real machine. -/
def TypedMachine.idle (s₀ : S) (v : Bool) : TypedMachine tapes S where
  start := s₀
  transition := fun s symbols => (s, fun i => (symbols i, HeadMove.stay))
  result := fun _ => some v

theorem TypedMachine.idle_spec (s₀ : S) (v : Bool) (T : Fin tapes → Tape) :
    HaltsExactly (TypedMachine.idle (tapes := tapes) s₀ v)
      ((TypedMachine.idle (tapes := tapes) s₀ v).startCfg T) 0 v := by
  constructor
  · rfl
  · intro j hj
    omega

/-- One round: step left, then run the body if a mark is there. -/
def leftBody (g : Fin tapes) (inner : TypedMachine tapes S) :=
  (moveUpTo g 1 HeadMove.left).andThen fun _ =>
    (TypedMachine.test (notBlankAt g)).andThen fun v =>
      if v then inner.andThen fun _ => TypedMachine.halt (tapes := tapes) true
      else
        (TypedMachine.idle (tapes := tapes) inner.start false).andThen fun _ =>
          TypedMachine.halt (tapes := tapes) false

/-- The loop. -/
noncomputable def leftLoop (g : Fin tapes) (inner : TypedMachine tapes S) :=
  (leftBody g inner).repeatUntilFalse

set_option maxHeartbeats 1000000 in
/-- A round landing on a mark: the body runs. -/
theorem leftBody_mark (g : Fin tapes) (inner : TypedMachine tapes S)
    (T F : Fin tapes → Tape) (cb : Nat)
    (hmark : ((Function.update T g (moveDir HeadMove.left (T g)) g)).head ≠
      TapeSymbol.blank)
    (hinner : HaltsExactly inner
      (inner.startCfg (Function.update T g (moveDir HeadMove.left (T g))))
      cb true)
    (hinnert : ((inner.step^[cb])
      (inner.startCfg
        (Function.update T g (moveDir HeadMove.left (T g))))).tape = F) :
    HaltsExactly (leftBody g inner) ((leftBody g inner).startCfg T)
      (1 + 1 + (1 + 1 + (cb + 1 + 0))) true ∧
    (((leftBody g inner).step^[1 + 1 + (1 + 1 + (cb + 1 + 0))])
      ((leftBody g inner).startCfg T)).tape = F := by
  classical
  set T1 := Function.update T g (moveDir HeadMove.left (T g)) with hT1
  have g0 := moveUpTo_spec g 1 HeadMove.left (by omega) T
  have s0 : (((moveUpTo g 1 HeadMove.left).step^[1])
      ((moveUpTo g 1 HeadMove.left).startCfg T)).tape = T1 := by
    rw [moveUpTo_tape g 1 HeadMove.left (by omega) T, hT1,
      Function.iterate_one]
  have htest := TypedMachine.test_spec (notBlankAt g) T1
  rw [notBlankAt_true g T1 hmark] at htest
  have htestt : (((TypedMachine.test (notBlankAt g)).step^[1])
      ((TypedMachine.test (notBlankAt g)).startCfg T1)).tape = T1 := by
    rw [Function.iterate_one]
    funext j
    simp [TypedMachine.step, TypedMachine.test, TypedMachine.startCfg,
      Tape.write_head_self, Tape.move]
  have hhalt := TypedMachine.halt_spec (tapes := tapes) true
    ((TypedMachine.halt (tapes := tapes) true).startCfg F)
  have hin := chainStepC hinner hinnert hhalt
  have hdisp := chainStepD
    (M₂ := fun v =>
      if v then inner.andThen fun _ => TypedMachine.halt (tapes := tapes) true
      else
        (TypedMachine.idle (tapes := tapes) inner.start false).andThen fun _ =>
          TypedMachine.halt (tapes := tapes) false)
    htest htestt (by simpa using hin.1)
  have hmain := chainStepC g0 s0 hdisp.1
  refine ⟨hmain.1, ?_⟩
  have hfin : ((leftBody g inner).step^[1 + 1 + (1 + 1 + (cb + 1 + 0))])
      ((leftBody g inner).startCfg T) = _ := hmain.2
  rw [hfin]
  have hIR : ∀ {S₁ S₂ : Type} (bb : Bool) (c : TypedConfiguration tapes S₂),
      (TypedConfiguration.inRight (S₁ := S₁) bb c).tape = c.tape :=
    fun _ _ => rfl
  rw [hIR]
  have hd := hdisp.2
  have hd' : (((TypedMachine.test (notBlankAt g)).andThen fun v =>
      if v then inner.andThen fun _ => TypedMachine.halt (tapes := tapes) true
      else
        (TypedMachine.idle (tapes := tapes) inner.start false).andThen fun _ =>
          TypedMachine.halt (tapes := tapes) false).step^[1 + 1 + (cb + 1 + 0)])
      (((TypedMachine.test (notBlankAt g)).andThen fun v =>
      if v then inner.andThen fun _ => TypedMachine.halt (tapes := tapes) true
      else
        (TypedMachine.idle (tapes := tapes) inner.start false).andThen fun _ =>
          TypedMachine.halt (tapes := tapes) false).startCfg T1) = _ := hd
  rw [hd', hIR]
  show (((if true then
      inner.andThen fun _ => TypedMachine.halt (tapes := tapes) true
    else
      (TypedMachine.idle (tapes := tapes) inner.start false).andThen fun _ =>
        TypedMachine.halt (tapes := tapes) false).step^[cb + 1 + 0])
    ((if true then
      inner.andThen fun _ => TypedMachine.halt (tapes := tapes) true
    else
      (TypedMachine.idle (tapes := tapes) inner.start false).andThen fun _ =>
        TypedMachine.halt (tapes := tapes) false).startCfg T1)).tape = _
  simp only [if_true]
  rw [hin.2, hIR]
  show ((( TypedMachine.halt (tapes := tapes) true).step^[0])
    ((TypedMachine.halt (tapes := tapes) true).startCfg F)).tape = F
  rfl

set_option maxHeartbeats 1000000 in
/-- A round landing on the blank below the run: the exit. -/
theorem leftBody_blank (g : Fin tapes) (inner : TypedMachine tapes S)
    (T : Fin tapes → Tape)
    (hblank : ((Function.update T g (moveDir HeadMove.left (T g)) g)).head =
      TapeSymbol.blank) :
    HaltsExactly (leftBody g inner) ((leftBody g inner).startCfg T)
      (1 + 1 + (1 + 1 + (0 + 1 + 0))) false ∧
    (((leftBody g inner).step^[1 + 1 + (1 + 1 + (0 + 1 + 0))])
      ((leftBody g inner).startCfg T)).tape =
      Function.update T g (moveDir HeadMove.left (T g)) := by
  classical
  set T1 := Function.update T g (moveDir HeadMove.left (T g)) with hT1
  have g0 := moveUpTo_spec g 1 HeadMove.left (by omega) T
  have s0 : (((moveUpTo g 1 HeadMove.left).step^[1])
      ((moveUpTo g 1 HeadMove.left).startCfg T)).tape = T1 := by
    rw [moveUpTo_tape g 1 HeadMove.left (by omega) T, hT1,
      Function.iterate_one]
  have htest := TypedMachine.test_spec (notBlankAt g) T1
  rw [notBlankAt_false g T1 hblank] at htest
  have htestt : (((TypedMachine.test (notBlankAt g)).step^[1])
      ((TypedMachine.test (notBlankAt g)).startCfg T1)).tape = T1 := by
    rw [Function.iterate_one]
    funext j
    simp [TypedMachine.step, TypedMachine.test, TypedMachine.startCfg,
      Tape.write_head_self, Tape.move]
  have hidle := TypedMachine.idle_spec (tapes := tapes) inner.start false T1
  have hidlet : (((TypedMachine.idle (tapes := tapes) inner.start
      false).step^[0])
      ((TypedMachine.idle (tapes := tapes) inner.start
        false).startCfg T1)).tape = T1 := rfl
  have hhalt := TypedMachine.halt_spec (tapes := tapes) false
    ((TypedMachine.halt (tapes := tapes) false).startCfg T1)
  have hin := chainStepC hidle hidlet hhalt
  have hdisp := chainStepD
    (M₂ := fun v =>
      if v then inner.andThen fun _ => TypedMachine.halt (tapes := tapes) true
      else
        (TypedMachine.idle (tapes := tapes) inner.start false).andThen fun _ =>
          TypedMachine.halt (tapes := tapes) false)
    htest htestt (by simpa using hin.1)
  have hmain := chainStepC g0 s0 hdisp.1
  refine ⟨hmain.1, ?_⟩
  have hfin : ((leftBody g inner).step^[1 + 1 + (1 + 1 + (0 + 1 + 0))])
      ((leftBody g inner).startCfg T) = _ := hmain.2
  rw [hfin]
  have hIR : ∀ {S₁ S₂ : Type} (bb : Bool) (c : TypedConfiguration tapes S₂),
      (TypedConfiguration.inRight (S₁ := S₁) bb c).tape = c.tape :=
    fun _ _ => rfl
  rw [hIR]
  have hd' : (((TypedMachine.test (notBlankAt g)).andThen fun v =>
      if v then inner.andThen fun _ => TypedMachine.halt (tapes := tapes) true
      else
        (TypedMachine.idle (tapes := tapes) inner.start false).andThen fun _ =>
          TypedMachine.halt (tapes := tapes) false).step^[1 + 1 + (0 + 1 + 0)])
      (((TypedMachine.test (notBlankAt g)).andThen fun v =>
      if v then inner.andThen fun _ => TypedMachine.halt (tapes := tapes) true
      else
        (TypedMachine.idle (tapes := tapes) inner.start false).andThen fun _ =>
          TypedMachine.halt (tapes := tapes) false).startCfg T1) =
      _ := hdisp.2
  rw [hd', hIR]
  show (((if false then
      inner.andThen fun _ => TypedMachine.halt (tapes := tapes) true
    else
      (TypedMachine.idle (tapes := tapes) inner.start false).andThen fun _ =>
        TypedMachine.halt (tapes := tapes) false).step^[0 + 1 + 0])
    ((if false then
      inner.andThen fun _ => TypedMachine.halt (tapes := tapes) true
    else
      (TypedMachine.idle (tapes := tapes) inner.start false).andThen fun _ =>
        TypedMachine.halt (tapes := tapes) false).startCfg T1)).tape = _
  simp only [Bool.false_eq_true, if_false]
  rw [hin.2, hIR]
  rfl

set_option maxHeartbeats 1000000 in
/-- **The left loop, under an invariant.**  The body's effect `f` maps a
round's start to its end — the leftward step is absorbed into it — and runs
once per mark below the guide's head.  The exit consumes the blank below the
run and nothing else. -/
theorem leftLoop_spec_inv (g : Fin tapes) (inner : TypedMachine tapes S)
    (Inv : (Fin tapes → Tape) → Prop)
    (f : (Fin tapes → Tape) → (Fin tapes → Tape)) (cb : Nat)
    (hbody : ∀ T, Inv T →
      HaltsExactly inner
        (inner.startCfg (Function.update T g (moveDir HeadMove.left (T g))))
        cb true ∧
      ((inner.step^[cb])
        (inner.startCfg
          (Function.update T g (moveDir HeadMove.left (T g))))).tape = f T)
    (hpres : ∀ T, Inv T → Inv (f T))
    (hfg : ∀ T, Inv T → (f T) g =
      (Function.update T g (moveDir HeadMove.left (T g))) g)
    (m : Nat) (L0 R0 : List TapeSymbol) (T₀ : Fin tapes → Tape)
    (hInv0 : Inv T₀)
    (hg0 : T₀ g = cellsTape
      (List.replicate m (TapeSymbol.bit true) ++ TapeSymbol.blank :: L0) R0) :
    HaltsExactly (leftLoop g inner) ((leftLoop g inner).startCfg T₀)
      (m * (1 + 1 + (1 + 1 + (cb + 1 + 0)) + 1) +
        (1 + 1 + (1 + 1 + (0 + 1 + 0)))) false ∧
    (((leftLoop g inner).step^[
        m * (1 + 1 + (1 + 1 + (cb + 1 + 0)) + 1) +
          (1 + 1 + (1 + 1 + (0 + 1 + 0)))])
      ((leftLoop g inner).startCfg T₀)).tape =
      Function.update ((f^[m]) T₀) g
        (moveDir HeadMove.left (((f^[m]) T₀) g)) := by
  classical
  -- the trajectory's shape
  have haux : ∀ r, r ≤ m → Inv ((f^[r]) T₀) ∧
      ∃ R' : List TapeSymbol, ((f^[r]) T₀) g = cellsTape
        (List.replicate (m - r) (TapeSymbol.bit true) ++
          TapeSymbol.blank :: L0) R' := by
    intro r
    induction r with
    | zero => intro _; exact ⟨hInv0, R0, by simpa using hg0⟩
    | succ r ih =>
        intro hr
        obtain ⟨hI, R', hR'⟩ := ih (by omega)
        have hI' : Inv ((f^[r + 1]) T₀) := by
          rw [Function.iterate_succ_apply']
          exact hpres _ hI
        refine ⟨hI', ?_⟩
        rw [Function.iterate_succ_apply', hfg _ hI, Function.update_self,
          hR', cellsTape_moveLeft_headD]
        have hcons : List.replicate (m - r) (TapeSymbol.bit true) ++
            TapeSymbol.blank :: L0 =
            TapeSymbol.bit true :: (List.replicate (m - (r + 1))
              (TapeSymbol.bit true) ++ TapeSymbol.blank :: L0) := by
          have : m - r = (m - (r + 1)) + 1 := by omega
          rw [this, List.replicate_succ]
          rfl
        rw [hcons]
        exact ⟨_, rfl⟩
  set CB := 1 + 1 + (1 + 1 + (cb + 1 + 0)) with hCB
  set body := leftBody g inner with hbody'
  set cfg : Nat → TypedConfiguration tapes _ :=
    fun r => body.startCfg ((f^[r]) T₀) with hcfg
  have hround : ∀ r, r < m →
      HaltsExactly body (cfg r) CB true ∧
        cfg (r + 1) = ⟨body.start, ((body.step^[CB]) (cfg r)).tape⟩ := by
    intro r hr
    obtain ⟨hI, R', hR'⟩ := haux r (by omega)
    have hmark : ((Function.update ((f^[r]) T₀) g
        (moveDir HeadMove.left (((f^[r]) T₀) g)) g)).head ≠
        TapeSymbol.blank := by
      rw [Function.update_self, hR', cellsTape_moveLeft_headD]
      have hcons : List.replicate (m - r) (TapeSymbol.bit true) ++
          TapeSymbol.blank :: L0 =
          TapeSymbol.bit true :: (List.replicate (m - (r + 1))
            (TapeSymbol.bit true) ++ TapeSymbol.blank :: L0) := by
        have : m - r = (m - (r + 1)) + 1 := by omega
        rw [this, List.replicate_succ]
        rfl
      rw [hcons]
      simp [cellsTape]
    obtain ⟨hbH, hbT⟩ := hbody ((f^[r]) T₀) hI
    obtain ⟨hh, ht⟩ := leftBody_mark g inner ((f^[r]) T₀) (f ((f^[r]) T₀))
      cb hmark hbH hbT
    refine ⟨by rw [hcfg]; exact hh, ?_⟩
    show body.startCfg ((f^[r + 1]) T₀) = _
    rw [Function.iterate_succ_apply', hcfg]
    have ht' : ((body.step^[CB]) (body.startCfg ((f^[r]) T₀))).tape =
        f ((f^[r]) T₀) := ht
    rw [ht']
    rfl
  have hblank : ((Function.update ((f^[m]) T₀) g
      (moveDir HeadMove.left (((f^[m]) T₀) g)) g)).head =
      TapeSymbol.blank := by
    obtain ⟨hI, R', hR'⟩ := haux m (le_refl m)
    rw [Function.update_self, hR', cellsTape_moveLeft_headD]
    simp [cellsTape]
  obtain ⟨hhx, htx⟩ := leftBody_blank g inner ((f^[m]) T₀) hblank
  have hexitr : HaltsExactly body (cfg m) (1 + 1 + (1 + 1 + (0 + 1 + 0)))
      false := by
    rw [hcfg]
    exact hhx
  have hspec := TypedMachine.repeatUntilFalse_spec body cfg (fun _ => CB) m
    (1 + 1 + (1 + 1 + (0 + 1 + 0))) hround hexitr
  rw [loopCost_const] at hspec
  have hrun := TypedMachine.repeatUntilFalse_rounds body cfg (fun _ => CB) m
    hround
  rw [loopCost_const] at hrun
  have hpart1 : HaltsExactly (leftLoop g inner)
      ((leftLoop g inner).startCfg T₀)
      (m * (CB + 1) + (1 + 1 + (1 + 1 + (0 + 1 + 0)))) false := by
    show HaltsExactly body.repeatUntilFalse
      (body.repeatUntilFalse.startCfg T₀) _ false
    have hc0 : body.repeatUntilFalse.startCfg T₀ = cfg 0 := rfl
    rw [hc0]
    exact hspec
  refine ⟨hpart1, ?_⟩
  have hstart : (leftLoop g inner).startCfg T₀ = cfg 0 := rfl
  rw [hstart, show m * (CB + 1) + (1 + 1 + (1 + 1 + (0 + 1 + 0))) =
    (1 + 1 + (1 + 1 + (0 + 1 + 0))) + m * (CB + 1) by omega,
    Function.iterate_add_apply]
  show ((leftLoop g inner).step^[1 + 1 + (1 + 1 + (0 + 1 + 0))]
    (((leftLoop g inner).step^[m * (CB + 1)]) (cfg 0))).tape = _
  rw [show (leftLoop g inner) = body.repeatUntilFalse from rfl, hrun]
  have htp : ((body.repeatUntilFalse.step^[1 + 1 + (1 + 1 + (0 + 1 + 0))])
      (cfg m)).tape =
      ((body.step^[1 + 1 + (1 + 1 + (0 + 1 + 0))]) (cfg m)).tape := by
    rw [body.repeatUntilFalse_iterate_fresh (cfg m) _ hexitr.fresh]
  rw [htp, hcfg]
  exact htx

end SipserGacsLautemann