sgl_marked_loop_inv

import Definitions.Def_sgl_marked_loop

/-!
# The marked loop, over an invariant

`markedLoop_spec` asks its body to behave on *every* tape configuration.  Real
bodies do not: `tallyOnto` needs its source in the standard shape, and says
nothing otherwise.  What is true is that the body behaves whenever a suitable
invariant holds, and that it re-establishes the invariant — which is exactly
the case for a tally, since it restores its source exactly.

So the body's contract is relativised to an invariant the round preserves.
Nothing else changes.
-/

namespace SipserGacsLautemann

variable {tapes : Nat} {S : Type}

section

variable (g : Fin tapes) (body : TypedMachine tapes S)
  (Inv : (Fin tapes → Tape) → Prop)
  (f : (Fin tapes → Tape) → (Fin tapes → Tape)) (cb : Nat)

/-- The invariant survives every round. -/
theorem markedStep_inv (hpres : ∀ T, Inv T → Inv (markedStep g f T))
    (T : Fin tapes → Tape) (hT : Inv T) :
    ∀ r : Nat, Inv (((markedStep g f)^[r]) T) := by
  intro r
  induction r with
  | zero => exact hT
  | succ r ih =>
      rw [Function.iterate_succ_apply']
      exact hpres _ ih

/-- The guide's position after `r` rounds, under the invariant. -/
theorem markedStep_guide_inv (hpres : ∀ T, Inv T → Inv (markedStep g f T))
    (hfg : ∀ T, Inv T → (f T) g = T g) (m : Nat) (Lg Rg : List TapeSymbol)
    (T : Fin tapes → Tape) (hT : Inv T)
    (hg : 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 hg
  | succ r ih =>
      intro hr
      have hprev := ih (by omega)
      have hinv := markedStep_inv g Inv f hpres T hT r
      rw [Function.iterate_succ_apply', markedStep, Function.update_self,
        hfg _ hinv, hprev]
      exact guide_reenters m r (by omega) Lg Rg

set_option maxHeartbeats 1000000 in
/-- **One round, under the invariant.** -/
theorem markedLoop_round_inv
    (hbody : ∀ T, Inv T → HaltsExactly body (body.startCfg T) cb true ∧
      ((body.step^[cb]) (body.startCfg T)).tape = f T)
    (hfg : ∀ T, Inv T → (f T) g = T g)
    (m r : Nat) (hr : r < m) (T : Fin tapes → Tape)
    (hT : Inv T) (Lg Rg : List TapeSymbol)
    (hg : 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 hT
  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 T hT, hg]
    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]

set_option maxHeartbeats 1000000 in
/-- **The marked loop, under an invariant.** -/
theorem markedLoop_spec_inv
    (hbody : ∀ T, Inv T → HaltsExactly body (body.startCfg T) cb true ∧
      ((body.step^[cb]) (body.startCfg T)).tape = f T)
    (hpres : ∀ T, Inv T → Inv (markedStep g f T))
    (hfg : ∀ T, Inv T → (f T) g = T g)
    (m : Nat) (hm : 1 ≤ m) (T : Fin tapes → Tape) (hT : Inv T)
    (Lg Rg : List TapeSymbol)
    (hg : 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 hgr := markedStep_guide_inv g Inv f hpres hfg m Lg Rg T hT hg r
      (by omega)
    have hinv := markedStep_inv g Inv f hpres T hT r
    obtain ⟨h1, h2⟩ := markedLoop_round_inv g body Inv f cb hbody hfg m r hr
      (((markedStep g f)^[r]) T) hinv Lg Rg hgr
    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

end SipserGacsLautemann