sgl_xor_walk

import Definitions.Def_sgl_offset_inv

/-!
# The XOR walk

Walk two tapes in step, replacing the guide's cell by the exclusive-or of the
two heads.  Cells past the source's written region read as blank, and blank
must count as `false` — the decode this machine implements pads with `false`
beyond the encoded shifts, and the exclusive-or of anything with `false` is
itself.
-/

namespace SipserGacsLautemann

variable {tapes : Nat}

/-- A cell's Boolean, blanks reading false. -/
def cellBool : TapeSymbol → Bool
  | TapeSymbol.blank => false
  | TapeSymbol.bit b => b

/-- One step: write `g != s` onto the guide, advance both heads. -/
def xorStep (g s : Fin tapes) (T : Fin tapes → Tape) : Fin tapes → Tape :=
  fun i =>
    if i = g then
      moveDir HeadMove.right
        (Tape.write (T g)
          (TapeSymbol.bit (cellBool (T g).head != cellBool (T s).head)))
    else if i = s then moveDir HeadMove.right (T s)
    else T i

/-- The walk's action, applied when the guide still carries a mark. -/
def xorAction (g s : Fin tapes) : (Fin tapes → TapeSymbol) →
    Fin tapes → TapeSymbol × HeadMove :=
  fun symbols i =>
    if i = g then
      (TapeSymbol.bit (cellBool (symbols g) != cellBool (symbols s)),
        HeadMove.right)
    else if i = s then (symbols i, HeadMove.right)
    else (symbols i, HeadMove.stay)

/-- One round of the walk. -/
def xorBody (g s : Fin tapes) :=
  (TypedMachine.test (notBlankAt g)).andThen fun b =>
    if b then
      (TypedMachine.act (xorAction g s)).andThen fun _ =>
        TypedMachine.halt (tapes := tapes) true
    else
      (TypedMachine.act (fun symbols i => (symbols i, HeadMove.stay))).andThen
        fun _ => TypedMachine.halt (tapes := tapes) false

/-- The walk: one xor step per guide mark, stopping at the guide's blank. -/
noncomputable def xorWalk (g s : Fin tapes) := (xorBody g s).repeatUntilFalse

theorem xorStep_eq (g s : Fin tapes) (hgs : g ≠ s) (T : Fin tapes → Tape) :
    applyAction T (xorAction g s) = xorStep g s T := by
  funext i
  show applyAction T (xorAction g s) i =
    (if i = g then
      moveDir HeadMove.right
        (Tape.write (T g)
          (TapeSymbol.bit (cellBool (T g).head != cellBool (T s).head)))
    else if i = s then moveDir HeadMove.right (T s)
    else T i)
  by_cases hi : i = g
  · subst hi
    simp [applyAction, xorAction, moveDir]
  · rw [if_neg hi]
    by_cases hi2 : i = s
    · subst hi2
      simp [applyAction, xorAction, hi, Tape.write_head_self, moveDir]
    · simp [applyAction, xorAction, hi, hi2, Tape.write_head_self, Tape.move]

set_option maxHeartbeats 1000000 in
/-- A round on a marked guide cell. -/
theorem xorBody_mark (g s : Fin tapes) (hgs : g ≠ s) (T : Fin tapes → Tape)
    (hmark : (T g).head ≠ TapeSymbol.blank) :
    HaltsExactly (xorBody g s) ((xorBody g s).startCfg T) (1 + 1 + (1 + 1 + 0))
      true ∧
    (((xorBody g s).step^[1 + 1 + (1 + 1 + 0)])
      ((xorBody g s).startCfg T)).tape = xorStep g s T := by
  have htest := TypedMachine.test_spec (notBlankAt g) T
  rw [notBlankAt_true g T hmark] at htest
  have htestt : (((TypedMachine.test (notBlankAt g)).step^[1])
      ((TypedMachine.test (notBlankAt g)).startCfg T)).tape = T := by
    rw [Function.iterate_one]
    funext j
    simp [TypedMachine.step, TypedMachine.test, TypedMachine.startCfg,
      Tape.write_head_self, Tape.move]
  have hact := TypedMachine.act_spec (xorAction g s) T
  have hactt : (((TypedMachine.act (xorAction g s)).step^[1])
      ((TypedMachine.act (xorAction g s)).startCfg T)).tape =
      xorStep g s T := by
    rw [Function.iterate_one, ← xorStep_eq g s hgs]
    funext j
    simp [TypedMachine.step, TypedMachine.act, TypedMachine.startCfg,
      applyAction]
  have hhalt := TypedMachine.halt_spec (tapes := tapes) true
    ((TypedMachine.halt (tapes := tapes) true).startCfg (xorStep g s T))
  have hinner := chainStepC hact hactt hhalt
  have hmain := chainStepD
    (M₂ := fun b =>
      if b then
        (TypedMachine.act (xorAction g s)).andThen fun _ =>
          TypedMachine.halt (tapes := tapes) true
      else
        (TypedMachine.act (fun symbols i => (symbols i, HeadMove.stay))).andThen
          fun _ => TypedMachine.halt (tapes := tapes) false)
    htest htestt (by simpa using hinner.1)
  refine ⟨hmain.1, ?_⟩
  have hfin := hmain.2
  have hfin' : ((xorBody g s).step^[1 + 1 + (1 + 1 + 0)])
      ((xorBody g s).startCfg T) = _ := hfin
  rw [hfin']
  have hi := hinner.2
  show (TypedConfiguration.inRight true
    (((if true then
        (TypedMachine.act (xorAction g s)).andThen fun _ =>
          TypedMachine.halt (tapes := tapes) true
      else
        (TypedMachine.act (fun symbols i =>
          (symbols i, HeadMove.stay))).andThen
          fun _ => TypedMachine.halt (tapes := tapes) false).step^[1 + 1 + 0])
      ((if true then
        (TypedMachine.act (xorAction g s)).andThen fun _ =>
          TypedMachine.halt (tapes := tapes) true
      else
        (TypedMachine.act (fun symbols i =>
          (symbols i, HeadMove.stay))).andThen
          fun _ => TypedMachine.halt (tapes := tapes) false).startCfg
        T))).tape = _
  simp only [if_true]
  rw [hi]
  rfl

set_option maxHeartbeats 1000000 in
/-- A round on a blank guide cell: the exit. -/
theorem xorBody_blank (g s : Fin tapes) (T : Fin tapes → Tape)
    (hblank : (T g).head = TapeSymbol.blank) :
    HaltsExactly (xorBody g s) ((xorBody g s).startCfg T) (1 + 1 + (1 + 1 + 0))
      false ∧
    (((xorBody g s).step^[1 + 1 + (1 + 1 + 0)])
      ((xorBody g s).startCfg T)).tape = T := by
  have htest := TypedMachine.test_spec (notBlankAt g) T
  rw [notBlankAt_false g T hblank] at htest
  have htestt : (((TypedMachine.test (notBlankAt g)).step^[1])
      ((TypedMachine.test (notBlankAt g)).startCfg T)).tape = T := by
    rw [Function.iterate_one]
    funext j
    simp [TypedMachine.step, TypedMachine.test, TypedMachine.startCfg,
      Tape.write_head_self, Tape.move]
  have hact := TypedMachine.act_spec
    (fun symbols : Fin tapes → TapeSymbol => fun i =>
      (symbols i, HeadMove.stay)) T
  have hactt : (((TypedMachine.act
      (fun symbols : Fin tapes → TapeSymbol => fun i =>
        (symbols i, HeadMove.stay))).step^[1])
      ((TypedMachine.act
        (fun symbols : Fin tapes → TapeSymbol => fun i =>
          (symbols i, HeadMove.stay))).startCfg T)).tape = T := by
    rw [Function.iterate_one]
    funext j
    simp [TypedMachine.step, TypedMachine.act, TypedMachine.startCfg,
      applyAction, Tape.write_head_self, Tape.move]
  have hhalt := TypedMachine.halt_spec (tapes := tapes) false
    ((TypedMachine.halt (tapes := tapes) false).startCfg T)
  have hinner := chainStepC hact hactt hhalt
  have hmain := chainStepD
    (M₂ := fun b =>
      if b then
        (TypedMachine.act (xorAction g s)).andThen fun _ =>
          TypedMachine.halt (tapes := tapes) true
      else
        (TypedMachine.act (fun symbols i => (symbols i, HeadMove.stay))).andThen
          fun _ => TypedMachine.halt (tapes := tapes) false)
    htest htestt (by simpa using hinner.1)
  refine ⟨hmain.1, ?_⟩
  have hfin := hmain.2
  have hfin' : ((xorBody g s).step^[1 + 1 + (1 + 1 + 0)])
      ((xorBody g s).startCfg T) = _ := hfin
  rw [hfin']
  simp only [Bool.false_eq_true, if_false]
  rw [hinner.2]
  rfl

set_option maxHeartbeats 1000000 in
/-- **The xor walk.**  If the guide carries `m` marks from its head, the walk
performs exactly `m` xor steps and halts with the guide on the
blank past them. -/
theorem xorWalk_spec (g s : Fin tapes) (hgs : g ≠ s) (m : Nat)
    (T : Fin tapes → Tape)
    (hmarks : ∀ r, r < m →
      ((((xorStep g s)^[r]) T) g).head ≠ TapeSymbol.blank)
    (hexit : ((((xorStep g s)^[m]) T) g).head = TapeSymbol.blank) :
    HaltsExactly (xorWalk g s)
      ((xorWalk g s).startCfg T) (m * 5 + 4) false ∧
    (((xorWalk g s).step^[m * 5 + 4])
      ((xorWalk g s).startCfg T)).tape =
      ((xorStep g s)^[m]) T := by
  classical
  set body := xorBody g s with hbody
  set cfg : Nat → TypedConfiguration tapes _ :=
    fun r => body.startCfg (((xorStep g s)^[r]) T) with hcfg
  have hround : ∀ r, r < m →
      HaltsExactly body (cfg r) 4 true ∧
        cfg (r + 1) = ⟨body.start, ((body.step^[4]) (cfg r)).tape⟩ := by
    intro r hr
    obtain ⟨hh, ht⟩ := xorBody_mark g s hgs
      (((xorStep g s)^[r]) T) (hmarks r hr)
    have hh4 : HaltsExactly body (cfg r) 4 true := by
      rw [hcfg, hbody]; simpa using hh
    have ht4 : ((body.step^[4]) (cfg r)).tape =
        ((xorStep g s)^[r + 1]) T := by
      rw [hcfg, hbody]
      rw [show (4 : Nat) = 1 + 1 + (1 + 1 + 0) from rfl]
      rw [ht, Function.iterate_succ_apply']
    refine ⟨hh4, ?_⟩
    show body.startCfg (((xorStep g s)^[r + 1]) T) = _
    rw [← ht4]
    rfl
  have hexitr : HaltsExactly body (cfg m) 4 false := by
    have := (xorBody_blank g s (((xorStep g s)^[m]) T)
      hexit).1
    rw [hcfg, hbody]; simpa using this
  have hspec := TypedMachine.repeatUntilFalse_spec body cfg (fun _ => 4) m 4
    hround hexitr
  have hcost : loopCost (fun _ => 4) m + 4 = m * 5 + 4 := by
    rw [loopCost_const]
  rw [hcost] at hspec
  have hrun := TypedMachine.repeatUntilFalse_rounds body cfg (fun _ => 4) m
    hround
  rw [loopCost_const] at hrun
  refine ⟨by rw [hcfg] at hspec; exact hspec, ?_⟩
  have hstart : (xorWalk g s).startCfg T = cfg 0 := by
    rw [hcfg]; rfl
  rw [hstart, show m * 5 + 4 = 4 + m * (4 + 1) by omega,
    Function.iterate_add_apply]
  show ((xorWalk g s).step^[4]
    (((xorWalk g s).step^[m * (4 + 1)]) (cfg 0))).tape = _
  rw [show (xorWalk g s) = body.repeatUntilFalse from rfl, hrun]
  have htp : ((body.repeatUntilFalse.step^[4]) (cfg m)).tape =
      ((body.step^[4]) (cfg m)).tape := by
    rw [body.repeatUntilFalse_iterate_fresh (cfg m) 4 hexitr.fresh]
  rw [htp, hcfg, hbody]
  exact (xorBody_blank g s (((xorStep g s)^[m]) T)
    hexit).2

/-! ## The caller-facing form -/

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

/-- The written run: one cell per guide cell, source blanks reading false. -/
def xorCells : List TapeSymbol → List TapeSymbol → List TapeSymbol
  | [], _ => []
  | c :: cs, ss =>
      TapeSymbol.bit (cellBool c != cellBool (ss.headD TapeSymbol.blank)) ::
        xorCells cs ss.tail

@[simp] theorem xorCells_nil (ss : List TapeSymbol) : xorCells [] ss = [] :=
  rfl

theorem xorCells_length : ∀ (cs ss : List TapeSymbol),
    (xorCells cs ss).length = cs.length := by
  intro cs
  induction cs with
  | nil => intro ss; rfl
  | cons c cs ih => intro ss; simp [xorCells, ih]

/-- One round, in `cellsTape` form. -/
theorem xorStep_tapes (g s : Fin tapes) (hgs : g ≠ s) (T : Fin tapes → Tape)
    (c : TapeSymbol) (Lg Rg Ls Rs : List TapeSymbol)
    (hg : T g = cellsTape Lg (c :: Rg)) (hs : T s = cellsTape Ls Rs) :
    (xorStep g s T) g = cellsTape
      (TapeSymbol.bit (cellBool c !=
        cellBool (Rs.headD TapeSymbol.blank)) :: Lg) Rg ∧
    (xorStep g s T) s = cellsTape (Rs.headD TapeSymbol.blank :: Ls)
      Rs.tail := by
  constructor
  · show (if g = g then _ else _) = _
    rw [if_pos rfl, hg, hs]
    show moveDir HeadMove.right (Tape.write (cellsTape Lg (c :: Rg))
      (TapeSymbol.bit (cellBool (cellsTape Lg (c :: Rg)).head !=
        cellBool (cellsTape Ls Rs).head))) = _
    rw [show (cellsTape Lg (c :: Rg)).head = c from rfl,
      show (cellsTape Ls Rs).head = Rs.headD TapeSymbol.blank from rfl,
      write_cellsTape]
    exact cellsTape_moveRight Lg _ Rg
  · show (if s = g then _ else if s = s then _ else _) = _
    rw [if_neg (fun h => hgs h.symm), if_pos rfl, hs,
      cellsTape_moveRight_headD]

/-- **The xor, accumulated.** -/
theorem xorStep_iterate (g s : Fin tapes) (hgs : g ≠ s) :
    ∀ (cs : List TapeSymbol) (T : Fin tapes → Tape)
      (Lg Rg Ls Rs : List TapeSymbol),
      T g = cellsTape Lg (cs ++ Rg) → T s = cellsTape Ls Rs →
      (((xorStep g s)^[cs.length]) T) g =
        cellsTape ((xorCells cs Rs).reverse ++ Lg) Rg ∧
      ∃ Ls' : List TapeSymbol,
        (((xorStep g s)^[cs.length]) T) s =
          cellsTape Ls' (Rs.drop cs.length) := by
  intro cs
  induction cs with
  | nil => intro T Lg Rg Ls Rs hg hs; exact ⟨by simpa using hg, Ls, by
      simpa using hs⟩
  | cons c cs ih =>
      intro T Lg Rg Ls Rs hg hs
      rw [List.length_cons, Function.iterate_succ_apply]
      obtain ⟨hg', hs'⟩ := xorStep_tapes g s hgs T c Lg (cs ++ Rg) Ls Rs
        (by rw [hg]; rfl) hs
      obtain ⟨ha, Ls', hb⟩ := ih (xorStep g s T)
        (TapeSymbol.bit (cellBool c !=
          cellBool (Rs.headD TapeSymbol.blank)) :: Lg) Rg
        (Rs.headD TapeSymbol.blank :: Ls) Rs.tail hg' hs'
      refine ⟨?_, Ls', ?_⟩
      · rw [ha]
        show cellsTape _ Rg = cellsTape _ Rg
        congr 1
        show (xorCells cs Rs.tail).reverse ++ _ :: Lg = _
        rw [show xorCells (c :: cs) Rs = TapeSymbol.bit (cellBool c !=
          cellBool (Rs.headD TapeSymbol.blank)) :: xorCells cs Rs.tail
          from rfl]
        simp
      · rw [hb]
        congr 1
        cases Rs with
        | nil => simp
        | cons a rest => rfl

/-- The marks hypothesis: the guide reads non-blank until the run ends. -/
theorem xorStep_marks (g s : Fin tapes) (hgs : g ≠ s) :
    ∀ (cs : List TapeSymbol) (T : Fin tapes → Tape)
      (Lg Rg Ls Rs : List TapeSymbol),
      (∀ c ∈ cs, c ≠ TapeSymbol.blank) →
      T g = cellsTape Lg (cs ++ Rg) → T s = cellsTape Ls Rs →
      ∀ r, r < cs.length →
        ((((xorStep g s)^[r]) T) g).head ≠ TapeSymbol.blank := by
  intro cs
  induction cs with
  | nil => intro _ _ _ _ _ _ _ _ r hr; simp at hr
  | cons c cs ih =>
      intro T Lg Rg Ls Rs hnb hg hs r hr
      cases r with
      | zero =>
          rw [Function.iterate_zero_apply, hg]
          exact hnb c (by simp)
      | succ r =>
          obtain ⟨hg', hs'⟩ := xorStep_tapes g s hgs T c Lg (cs ++ Rg) Ls Rs
            (by rw [hg]; rfl) hs
          rw [Function.iterate_succ_apply]
          exact ih (xorStep g s T) _ Rg _ Rs.tail
            (fun x hx => hnb x (by simp [hx])) hg' hs' r (by simpa using hr)

/-- Other tapes are untouched. -/
theorem xorStep_other (g s : Fin tapes) :
    ∀ (m : Nat) (T : Fin tapes → Tape) (j : Fin tapes), j ≠ g → j ≠ s →
      (((xorStep g s)^[m]) T) j = T j := by
  intro m
  induction m with
  | zero => intro T j _ _; rfl
  | succ m ih =>
      intro T j hjg hjs
      rw [Function.iterate_succ_apply]
      have hstep : (xorStep g s T) j = T j := by
        show (if j = g then _ else if j = s then _ else T j) = T j
        rw [if_neg hjg, if_neg hjs]
      rw [ih (xorStep g s T) j hjg hjs, hstep]

end SipserGacsLautemann