sgl_simul_walk

import Definitions.Def_sgl_xor_walk

/-!
# The simultaneous walk

Two heads advance together until either reads blank.  The number of steps is
the minimum of the two runs' lengths — which is how a machine takes a minimum
without arithmetic: consume both and stop at the first to run out.
-/

namespace SipserGacsLautemann

variable {tapes : Nat}

/-- Both heads carry marks. -/
def bothMarked (a b : Fin tapes) : (Fin tapes → TapeSymbol) → Bool :=
  fun symbols =>
    match symbols a, symbols b with
    | TapeSymbol.bit _, TapeSymbol.bit _ => true
    | _, _ => false

theorem bothMarked_true (a b : Fin tapes) (t : Fin tapes → Tape)
    (ha : (t a).head ≠ TapeSymbol.blank) (hb : (t b).head ≠ TapeSymbol.blank) :
    bothMarked a b (fun j => (t j).head) = true := by
  show (match (t a).head, (t b).head with
    | TapeSymbol.bit _, TapeSymbol.bit _ => true
    | _, _ => false) = true
  cases hca : (t a).head with
  | blank => exact absurd hca ha
  | bit x =>
      cases hcb : (t b).head with
      | blank => exact absurd hcb hb
      | bit y => rfl

theorem bothMarked_false_left (a b : Fin tapes) (t : Fin tapes → Tape)
    (ha : (t a).head = TapeSymbol.blank) :
    bothMarked a b (fun j => (t j).head) = false := by
  show (match (t a).head, (t b).head with
    | TapeSymbol.bit _, TapeSymbol.bit _ => true
    | _, _ => false) = false
  rw [ha]

theorem bothMarked_false_right (a b : Fin tapes) (t : Fin tapes → Tape)
    (hb : (t b).head = TapeSymbol.blank) :
    bothMarked a b (fun j => (t j).head) = false := by
  show (match (t a).head, (t b).head with
    | TapeSymbol.bit _, TapeSymbol.bit _ => true
    | _, _ => false) = false
  rw [hb]
  cases (t a).head <;> rfl

/-- One step: both advance. -/
def simulStep (a b : Fin tapes) (T : Fin tapes → Tape) : Fin tapes → Tape :=
  fun i =>
    if i = a then moveDir HeadMove.right (T a)
    else if i = b then moveDir HeadMove.right (T b)
    else T i

/-- The action. -/
def simulAction (a b : Fin tapes) : (Fin tapes → TapeSymbol) →
    Fin tapes → TapeSymbol × HeadMove :=
  fun symbols i =>
    if i = a then (symbols i, HeadMove.right)
    else if i = b then (symbols i, HeadMove.right)
    else (symbols i, HeadMove.stay)

theorem simulStep_eq (a b : Fin tapes) (T : Fin tapes → Tape) :
    applyAction T (simulAction a b) = simulStep a b T := by
  funext i
  show applyAction T (simulAction a b) i =
    (if i = a then moveDir HeadMove.right (T a)
      else if i = b then moveDir HeadMove.right (T b)
      else T i)
  by_cases hi : i = a
  · subst hi
    simp [applyAction, simulAction, Tape.write_head_self, moveDir]
  · rw [if_neg hi]
    by_cases hi2 : i = b
    · subst hi2
      simp [applyAction, simulAction, hi, Tape.write_head_self, moveDir]
    · simp [applyAction, simulAction, hi, hi2, Tape.write_head_self,
        Tape.move]

/-- One round of the walk. -/
def simulBody (a b : Fin tapes) :=
  (TypedMachine.test (bothMarked a b)).andThen fun v =>
    if v then
      (TypedMachine.act (simulAction a b)).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. -/
noncomputable def simulWalk (a b : Fin tapes) := (simulBody a b).repeatUntilFalse

set_option maxHeartbeats 1000000 in
/-- A round with both heads marked. -/
theorem simulBody_mark (a b : Fin tapes) (T : Fin tapes → Tape)
    (hma : (T a).head ≠ TapeSymbol.blank)
    (hmb : (T b).head ≠ TapeSymbol.blank) :
    HaltsExactly (simulBody a b) ((simulBody a b).startCfg T) (1 + 1 + (1 + 1 + 0))
      true ∧
    (((simulBody a b).step^[1 + 1 + (1 + 1 + 0)])
      ((simulBody a b).startCfg T)).tape = simulStep a b T := by
  have htest := TypedMachine.test_spec (bothMarked a b) T
  rw [bothMarked_true a b T hma hmb] at htest
  have htestt : (((TypedMachine.test (bothMarked a b)).step^[1])
      ((TypedMachine.test (bothMarked a b)).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 (simulAction a b) T
  have hactt : (((TypedMachine.act (simulAction a b)).step^[1])
      ((TypedMachine.act (simulAction a b)).startCfg T)).tape =
      simulStep a b T := by
    rw [Function.iterate_one, ← simulStep_eq a b]
    funext j
    simp [TypedMachine.step, TypedMachine.act, TypedMachine.startCfg,
      applyAction]
  have hhalt := TypedMachine.halt_spec (tapes := tapes) true
    ((TypedMachine.halt (tapes := tapes) true).startCfg (simulStep a b T))
  have hinner := chainStepC hact hactt hhalt
  have hmain := chainStepD
    (M₂ := fun v =>
      if v then
        (TypedMachine.act (simulAction a b)).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' : ((simulBody a b).step^[1 + 1 + (1 + 1 + 0)])
      ((simulBody a b).startCfg T) = _ := hfin
  rw [hfin']
  have hi := hinner.2
  show (TypedConfiguration.inRight true
    (((if true then
        (TypedMachine.act (simulAction a b)).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 (simulAction a b)).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 with either head blank: the exit. -/
theorem simulBody_blank (a b : Fin tapes) (T : Fin tapes → Tape)
    (hstop : bothMarked a b (fun j => (T j).head) = false) :
    HaltsExactly (simulBody a b) ((simulBody a b).startCfg T) (1 + 1 + (1 + 1 + 0))
      false ∧
    (((simulBody a b).step^[1 + 1 + (1 + 1 + 0)])
      ((simulBody a b).startCfg T)).tape = T := by
  have htest := TypedMachine.test_spec (bothMarked a b) T
  rw [hstop] at htest
  have htestt : (((TypedMachine.test (bothMarked a b)).step^[1])
      ((TypedMachine.test (bothMarked a b)).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 v =>
      if v then
        (TypedMachine.act (simulAction a b)).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' : ((simulBody a b).step^[1 + 1 + (1 + 1 + 0)])
      ((simulBody a b).startCfg T) = _ := hfin
  rw [hfin']
  simp only [Bool.false_eq_true, if_false]
  rw [hinner.2]
  rfl

/-! ## The iterate and the spec -/

/-- One step, uniformly. -/
theorem simulStep_tapes (a b : Fin tapes) (hab : a ≠ b)
    (T : Fin tapes → Tape) (La Ra Lb Rb : List TapeSymbol)
    (ha : T a = cellsTape La Ra) (hb : T b = cellsTape Lb Rb) :
    (simulStep a b T) a = cellsTape (Ra.headD TapeSymbol.blank :: La)
      Ra.tail ∧
    (simulStep a b T) b = cellsTape (Rb.headD TapeSymbol.blank :: Lb)
      Rb.tail := by
  constructor
  · show (if a = a then _ else _) = _
    rw [if_pos rfl, ha, cellsTape_moveRight_headD]
  · show (if b = a then _ else if b = b then _ else _) = _
    rw [if_neg (fun h => hab h.symm), if_pos rfl, hb,
      cellsTape_moveRight_headD]

/-- After `r` rounds both heads have advanced `r` cells. -/
theorem simulStep_iterate (a b : Fin tapes) (hab : a ≠ b) :
    ∀ (r : Nat) (T : Fin tapes → Tape) (La Ra Lb Rb : List TapeSymbol),
      T a = cellsTape La Ra → T b = cellsTape Lb Rb →
      (∃ La', (((simulStep a b)^[r]) T) a = cellsTape La' (Ra.drop r)) ∧
      (∃ Lb', (((simulStep a b)^[r]) T) b = cellsTape Lb' (Rb.drop r)) := by
  intro r
  induction r with
  | zero => intro T La Ra Lb Rb ha hb; exact ⟨⟨La, by simpa using ha⟩,
      ⟨Lb, by simpa using hb⟩⟩
  | succ r ih =>
      intro T La Ra Lb Rb ha hb
      rw [Function.iterate_succ_apply]
      obtain ⟨ha', hb'⟩ := simulStep_tapes a b hab T La Ra Lb Rb ha hb
      obtain ⟨⟨La', hA⟩, ⟨Lb', hB⟩⟩ := ih (simulStep a b T) _ Ra.tail _
        Rb.tail ha' hb'
      refine ⟨⟨La', ?_⟩, ⟨Lb', ?_⟩⟩
      · rw [hA]
        congr 1
        cases Ra with
        | nil => simp
        | cons x xs => rfl
      · rw [hB]
        congr 1
        cases Rb with
        | nil => simp
        | cons x xs => rfl

/-- Untouched tapes. -/
theorem simulStep_other (a b : Fin tapes) :
    ∀ (m : Nat) (T : Fin tapes → Tape) (j : Fin tapes), j ≠ a → j ≠ b →
      (((simulStep a b)^[m]) T) j = T j := by
  intro m
  induction m with
  | zero => intro T j _ _; rfl
  | succ m ih =>
      intro T j hja hjb
      rw [Function.iterate_succ_apply]
      have hstep : (simulStep a b T) j = T j := by
        show (if j = a then _ else if j = b then _ else T j) = T j
        rw [if_neg hja, if_neg hjb]
      rw [ih (simulStep a b T) j hja hjb, hstep]

/-- A run's cell within its length is not blank. -/
theorem run_getD_nonblank (cs R : List TapeSymbol)
    (hnb : ∀ c ∈ cs, c ≠ TapeSymbol.blank) (k : Nat) (hk : k < cs.length) :
    (((cs ++ TapeSymbol.blank :: R).drop k).headD TapeSymbol.blank) ≠
      TapeSymbol.blank := by
  have hdrop : (cs ++ TapeSymbol.blank :: R).drop k =
      cs.drop k ++ TapeSymbol.blank :: R := List.drop_append_of_le_length
        (le_of_lt hk)
  rw [hdrop]
  cases hcs : cs.drop k with
  | nil =>
      exfalso
      have hlen := congrArg List.length hcs
      rw [List.length_drop] at hlen
      simp at hlen
      omega
  | cons c rest =>
      have hc : c ∈ cs := by
        have : c ∈ cs.drop k := by rw [hcs]; simp
        exact List.mem_of_mem_drop this
      exact hnb c hc

/-- The run's end reads blank. -/
theorem run_end_blank (cs R : List TapeSymbol) :
    (((cs ++ TapeSymbol.blank :: R).drop cs.length).headD TapeSymbol.blank) =
      TapeSymbol.blank := by
  rw [List.drop_append_of_le_length (le_refl _)]
  simp

set_option maxHeartbeats 1000000 in
/-- **The simultaneous walk stops at the shorter run.** -/
theorem simulWalk_spec (a b : Fin tapes) (hab : a ≠ b)
    (as bs La Ra Lb Rb : List TapeSymbol) (T : Fin tapes → Tape)
    (hna : ∀ c ∈ as, c ≠ TapeSymbol.blank)
    (hnb : ∀ c ∈ bs, c ≠ TapeSymbol.blank)
    (ha : T a = cellsTape La (as ++ TapeSymbol.blank :: Ra))
    (hb : T b = cellsTape Lb (bs ++ TapeSymbol.blank :: Rb)) :
    HaltsExactly (simulWalk a b) ((simulWalk a b).startCfg T)
      ((min as.length bs.length) * 5 + 4) false ∧
    (((simulWalk a b).step^[(min as.length bs.length) * 5 + 4])
      ((simulWalk a b).startCfg T)).tape =
      ((simulStep a b)^[min as.length bs.length]) T := by
  classical
  set m := min as.length bs.length with hm
  set body := simulBody a b with hbody
  set cfg : Nat → TypedConfiguration tapes _ :=
    fun r => body.startCfg (((simulStep a b)^[r]) T) with hcfg
  have hheads : ∀ r, (∃ La', (((simulStep a b)^[r]) T) a =
      cellsTape La' ((as ++ TapeSymbol.blank :: Ra).drop r)) ∧
      (∃ Lb', (((simulStep a b)^[r]) T) b =
      cellsTape Lb' ((bs ++ TapeSymbol.blank :: Rb).drop r)) :=
    fun r => simulStep_iterate a b hab r T La _ Lb _ ha hb
  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 ⟨⟨La', hA⟩, ⟨Lb', hB⟩⟩ := hheads r
    have hma : ((((simulStep a b)^[r]) T) a).head ≠ TapeSymbol.blank := by
      rw [hA]
      exact run_getD_nonblank as Ra hna r (by omega)
    have hmb : ((((simulStep a b)^[r]) T) b).head ≠ TapeSymbol.blank := by
      rw [hB]
      exact run_getD_nonblank bs Rb hnb r (by omega)
    obtain ⟨hh, ht⟩ := simulBody_mark a b (((simulStep a b)^[r]) T) hma hmb
    have hh4 : HaltsExactly body (cfg r) 4 true := by
      rw [hcfg, hbody]
      simpa using hh
    refine ⟨hh4, ?_⟩
    show body.startCfg (((simulStep a b)^[r + 1]) T) = _
    rw [Function.iterate_succ_apply', ← ht]
    rfl
  have hstop : bothMarked a b
      (fun j => ((((simulStep a b)^[m]) T) j).head) = false := by
    obtain ⟨⟨La', hA⟩, ⟨Lb', hB⟩⟩ := hheads m
    rcases Nat.le_total as.length bs.length with hle | hle
    · have hma : ((((simulStep a b)^[m]) T) a).head = TapeSymbol.blank := by
        rw [hA, hm, Nat.min_eq_left hle]
        exact run_end_blank as Ra
      exact bothMarked_false_left a b _ hma
    · have hmb : ((((simulStep a b)^[m]) T) b).head = TapeSymbol.blank := by
        rw [hB, hm, Nat.min_eq_right hle]
        exact run_end_blank bs Rb
      exact bothMarked_false_right a b _ hmb
  obtain ⟨hhx, htx⟩ := simulBody_blank a b (((simulStep a b)^[m]) T) hstop
  have hexitr : HaltsExactly body (cfg m) 4 false := by
    rw [hcfg, hbody]
    simpa using hhx
  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
  have hpart1 : HaltsExactly (simulWalk a b) ((simulWalk a b).startCfg T)
      (m * 5 + 4) false := by
    show HaltsExactly body.repeatUntilFalse (body.repeatUntilFalse.startCfg T)
      (m * 5 + 4) false
    have hc0 : body.repeatUntilFalse.startCfg T = cfg 0 := rfl
    rw [hc0]
    exact hspec
  refine ⟨hpart1, ?_⟩
  have hstart : (simulWalk a b).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 ((simulWalk a b).step^[4]
    (((simulWalk a b).step^[m * (4 + 1)]) (cfg 0))).tape = _
  rw [show (simulWalk a b) = 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]
  simpa using htx

end SipserGacsLautemann