sgl_records_r

import Definitions.Def_sgl_traj_r

/-!
# The trajectory and its records, with the margin

The same definitions as before, over the margin-carrying carrier.  The proofs
are unchanged; only the hypothesis the delegate is held to has moved from "on
every debris" to "on debris behind a margin", and the carrier now supplies the
margin at each round.
-/

namespace SipserGacsLautemann

open Classical

variable {n states : Nat}

section

variable (L : RoundLayout n) (hL : L.Wf) (gd : Fin n)
  (hgc : gd ≠ L.clk) (hgd : ∀ j, gd ≠ L.dst j) (hgn : gd ≠ L.cnt)
  (hgs : ∀ i, gd ≠ L.src i) (hsc : ∀ i, L.src i ≠ L.clk)
  (hsn : ∀ i, L.src i ≠ L.cnt)
  (M : Machine 4 states)
  (xs Ls Rs : Fin 3 → List TapeSymbol) (Lclk Lg Rg : List TapeSymbol)
  (R B Q : Nat) (hxs : ∀ i, ∀ x ∈ xs i, x ≠ TapeSymbol.blank)
  (hQ : ∀ m j, m ≤ R → (roundContent xs m j).length ≤ Q)
  (hhalts : RoundHaltingMR M xs B R)

/-- One round's data, chosen; the identity past the last round. -/
noncomputable def ostepMR (s : OStateM L gd xs Ls Rs Lclk Lg Rg R B Q) :
    Nat × Nat × Bool × OStateM L gd xs Ls Rs Lclk Lg Rg R B Q :=
  if h : s.idx < R then
    (ostep_existsMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s h).choose
  else (0, 0, false, s)

theorem ostepMR_spec (s : OStateM L gd xs Ls Rs Lclk Lg Rg R B Q)
    (h : s.idx < R) :
    (ostepMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s) = (ostep_existsMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s h).choose := by
  rw [ostepMR, dif_pos h]

/-- The trajectory of carriers. -/
noncomputable def otrajMR (s₀ : OStateM L gd xs Ls Rs Lclk Lg Rg R B Q) :
    Nat → OStateM L gd xs Ls Rs Lclk Lg Rg R B Q
  | 0 => s₀
  | i + 1 => (ostepMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts (otrajMR s₀ i)).2.2.2

theorem otrajMR_idx (s₀ : OStateM L gd xs Ls Rs Lclk Lg Rg R B Q)
    (h0 : s₀.idx = 0) (i : Nat) (hi : i ≤ R) :
    (otrajMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ i).idx = i := by
  induction i with
  | zero => exact h0
  | succ i ih =>
      have hle : i ≤ R := by omega
      have hidx := ih hle
      have hlt : (otrajMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ i).idx < R := by rw [hidx]; omega
      rw [otrajMR, ostepMR_spec L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts _ hlt]
      have := (ostep_existsMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts _ hlt).choose_spec.2.2.2.1
      rw [this, hidx]

/-- The per-round cost. -/
noncomputable def ocostMR (s₀ : OStateM L gd xs Ls Rs Lclk Lg Rg R B Q)
    (i : Nat) : Nat := (ostepMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts (otrajMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ i)).1

/-- The delegate's verdict at round `i`. -/
noncomputable def oansMR (s₀ : OStateM L gd xs Ls Rs Lclk Lg Rg R B Q)
    (i : Nat) : Bool := (ostepMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts (otrajMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ i)).2.2.1

/-- The loop's configuration at round `i`. -/
noncomputable def oconfigMR (s₀ : OStateM L gd xs Ls Rs Lclk Lg Rg R B Q)
    (i : Nat) := (loopBody L gd M).startCfg (otrajMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ i).tp

set_option maxHeartbeats 1000000 in
/-- One chosen round, with the index named. -/
theorem ostepMR_round (t : OStateM L gd xs Ls Rs Lclk Lg Rg R B Q) (i : Nat)
    (hti : t.idx = i) (hi : i < R) :
    HaltsExactly (loopBody L gd M) ((loopBody L gd M).startCfg t.tp)
      (ostepMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts t).1 (decide (i + 1 < R)) ∧
    (ostepMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts t).2.2.2.tp =
      (((loopBody L gd M).step^[(ostepMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts t).1])
        ((loopBody L gd M).startCfg t.tp)).tape ∧
    roundVerdict ((((loopBody L gd M).step^[(ostepMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts t).1])
      ((loopBody L gd M).startCfg t.tp))).state = (ostepMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts t).2.2.1 ∧
    guideLeft ((((loopBody L gd M).step^[(ostepMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts t).1])
      ((loopBody L gd M).startCfg t.tp))).state = decide (i + 1 < R) := by
  subst hti
  rw [ostepMR_spec L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts t hi]
  have hch := (ostep_existsMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts t hi).choose_spec
  exact ⟨hch.2.2.2.2.1, hch.2.2.2.2.2.1, hch.2.2.2.2.2.2.1,
    hch.2.2.2.2.2.2.2⟩

/-- The same, along the trajectory. -/
theorem otrajMR_round (s₀ : OStateM L gd xs Ls Rs Lclk Lg Rg R B Q)
    (h0 : s₀.idx = 0) (i : Nat) (hi : i < R) :
    HaltsExactly (loopBody L gd M) (oconfigMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ i) (ocostMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ i)
      (decide (i + 1 < R)) ∧
    (otrajMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ (i + 1)).tp =
      (((loopBody L gd M).step^[ocostMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ i])
        (oconfigMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ i)).tape ∧
    roundVerdict ((((loopBody L gd M).step^[ocostMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ i])
      (oconfigMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ i))).state = oansMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ i ∧
    guideLeft ((((loopBody L gd M).step^[ocostMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ i])
      (oconfigMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ i))).state = decide (i + 1 < R) :=
  ostepMR_round L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts (otrajMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ i) i
    (otrajMR_idx L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ h0 i (le_of_lt hi)) hi

/-- **A round of the loop.** -/
theorem offsetMR_record (s₀ : OStateM L gd xs Ls Rs Lclk Lg Rg R B Q)
    (h0 : s₀.idx = 0) (i : Nat) (hi : i + 1 < R)
    (hrej : oansMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ i = false) :
    LoopRound (fun _ : Unit => loopBody L gd M) (fun _ _ => ())
      (fun _ b => roundVerdict b || !(guideLeft b))
      (fun _ : Nat => ()) (oconfigMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀) (ocostMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀) i := by
  obtain ⟨hhalt, htp, hrv, hgl⟩ := otrajMR_round L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ h0 i (by omega)
  refine ⟨⟨_, hhalt⟩, ?_, rfl, ?_⟩
  · rw [hrv, hgl, hrej, decide_eq_true hi]
    rfl
  · show (loopBody L gd M).startCfg (otrajMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ (i + 1)).tp = _
    rw [htp]
    rfl

end

end SipserGacsLautemann