sgl_verdict_write

import Definitions.Def_sgl_split_walk

/-!
# Depositing a verdict

One stride of the round-robin: the verdict lands on the first of three tapes
whose head is blank, and when the third is written all three advance.  The
symbol is a constant here — the verdict the delegate just reported — so no
source tape is read.
-/

namespace SipserGacsLautemann

variable {tapes : Nat}

/-- The stride's effect. -/
def putStep (v : Bool) (o1 o2 o3 : Fin tapes) (T : Fin tapes → Tape) :
    Fin tapes → Tape :=
  fun i =>
    if (T o1).head = TapeSymbol.blank then
      if i = o1 then Tape.write (T o1) (TapeSymbol.bit v) else T i
    else if (T o2).head = TapeSymbol.blank then
      if i = o2 then Tape.write (T o2) (TapeSymbol.bit v) else T i
    else
      if i = o3 then
        moveDir HeadMove.right (Tape.write (T o3) (TapeSymbol.bit v))
      else if i = o1 then moveDir HeadMove.right (T o1)
      else if i = o2 then moveDir HeadMove.right (T o2)
      else T i

/-- The stride's action. -/
def putAction (v : Bool) (o1 o2 o3 : Fin tapes) :
    (Fin tapes → TapeSymbol) → Fin tapes → TapeSymbol × HeadMove :=
  fun symbols i =>
    if symbols o1 = TapeSymbol.blank then
      if i = o1 then (TapeSymbol.bit v, HeadMove.stay)
      else (symbols i, HeadMove.stay)
    else if symbols o2 = TapeSymbol.blank then
      if i = o2 then (TapeSymbol.bit v, HeadMove.stay)
      else (symbols i, HeadMove.stay)
    else
      if i = o3 then (TapeSymbol.bit v, HeadMove.right)
      else if i = o1 then (symbols i, HeadMove.right)
      else if i = o2 then (symbols i, HeadMove.right)
      else (symbols i, HeadMove.stay)

/-- Deposit the verdict. -/
def putVerdict (v : Bool) (o1 o2 o3 : Fin tapes) :=
  TypedMachine.act (putAction v o1 o2 o3)

theorem putStep_eq (v : Bool) (o1 o2 o3 : Fin tapes)
    (h12 : o1 ≠ o2) (h13 : o1 ≠ o3) (h23 : o2 ≠ o3)
    (T : Fin tapes → Tape) :
    applyAction T (putAction v o1 o2 o3) = putStep v o1 o2 o3 T := by
  funext i
  simp only [putStep]
  by_cases hpa : (T o1).head = TapeSymbol.blank
  · rw [if_pos hpa]
    by_cases hio : i = o1
    · subst hio
      simp [applyAction, putAction, hpa, moveDir, Tape.move]
    · rw [if_neg hio]
      simp [applyAction, putAction, hpa, hio, Tape.write_head_self,
        Tape.move]
  · rw [if_neg hpa]
    by_cases hpb : (T o2).head = TapeSymbol.blank
    · rw [if_pos hpb]
      by_cases hio : i = o2
      · subst hio
        simp [applyAction, putAction, hpa, hpb, moveDir, Tape.move]
      · rw [if_neg hio]
        simp [applyAction, putAction, hpa, hpb, hio, Tape.write_head_self,
          Tape.move]
    · rw [if_neg hpb]
      by_cases hio : i = o3
      · subst hio
        simp [applyAction, putAction, hpa, hpb, moveDir]
      · rw [if_neg hio]
        by_cases hja : i = o1
        · subst hja
          simp [applyAction, putAction, hpa, hpb, hio,
            Tape.write_head_self, moveDir]
        · rw [if_neg hja]
          by_cases hjb : i = o2
          · subst hjb
            simp [applyAction, putAction, hpa, hpb, hio, hja,
              Tape.write_head_self, moveDir]
          · rw [if_neg hjb]
            simp [applyAction, putAction, hpa, hpb, hio, hja, hjb,
              Tape.write_head_self, Tape.move]

theorem putVerdict_spec (v : Bool) (o1 o2 o3 : Fin tapes)
    (h12 : o1 ≠ o2) (h13 : o1 ≠ o3) (h23 : o2 ≠ o3)
    (T : Fin tapes → Tape) :
    HaltsExactly (putVerdict v o1 o2 o3)
      ((putVerdict v o1 o2 o3).startCfg T) 1 true ∧
    (((putVerdict v o1 o2 o3).step^[1])
      ((putVerdict v o1 o2 o3).startCfg T)).tape =
      putStep v o1 o2 o3 T := by
  refine ⟨TypedMachine.act_spec _ T, ?_⟩
  rw [Function.iterate_one, ← putStep_eq v o1 o2 o3 h12 h13 h23]
  funext j
  show applyAction T (putAction v o1 o2 o3) j = _
  rfl

/-- Phase 0: the first tape is free. -/
theorem putStep_phase0 (v : Bool) (o1 o2 o3 : Fin tapes)
    (h12 : o1 ≠ o2) (h13 : o1 ≠ o3) (h23 : o2 ≠ o3)
    (T : Fin tapes → Tape) (hpa : (T o1).head = TapeSymbol.blank) :
    (putStep v o1 o2 o3 T) o1 = Tape.write (T o1) (TapeSymbol.bit v) ∧
    (∀ j, j ≠ o1 → (putStep v o1 o2 o3 T) j = T j) := by
  refine ⟨?_, ?_⟩
  · simp only [putStep]
    rw [if_pos hpa, if_pos trivial]
  · intro j hj
    simp only [putStep]
    rw [if_pos hpa, if_neg hj]

/-- Phase 1: the first is taken, the second is free. -/
theorem putStep_phase1 (v : Bool) (o1 o2 o3 : Fin tapes)
    (h12 : o1 ≠ o2) (h13 : o1 ≠ o3) (h23 : o2 ≠ o3)
    (T : Fin tapes → Tape) (hpa : (T o1).head ≠ TapeSymbol.blank)
    (hpb : (T o2).head = TapeSymbol.blank) :
    (putStep v o1 o2 o3 T) o2 = Tape.write (T o2) (TapeSymbol.bit v) ∧
    (∀ j, j ≠ o2 → (putStep v o1 o2 o3 T) j = T j) := by
  refine ⟨?_, ?_⟩
  · simp only [putStep]
    rw [if_neg hpa, if_pos hpb, if_pos trivial]
  · intro j hj
    simp only [putStep]
    rw [if_neg hpa, if_pos hpb, if_neg hj]

/-- Phase 2: both are taken — write the third and advance all three. -/
theorem putStep_phase2 (v : Bool) (o1 o2 o3 : Fin tapes)
    (h12 : o1 ≠ o2) (h13 : o1 ≠ o3) (h23 : o2 ≠ o3)
    (T : Fin tapes → Tape) (hpa : (T o1).head ≠ TapeSymbol.blank)
    (hpb : (T o2).head ≠ TapeSymbol.blank) :
    (putStep v o1 o2 o3 T) o1 = moveDir HeadMove.right (T o1) ∧
    (putStep v o1 o2 o3 T) o2 = moveDir HeadMove.right (T o2) ∧
    (putStep v o1 o2 o3 T) o3 =
      moveDir HeadMove.right
        (Tape.write (T o3) (TapeSymbol.bit v)) ∧
    (∀ j, j ≠ o1 → j ≠ o2 → j ≠ o3 →
      (putStep v o1 o2 o3 T) j = T j) := by
  refine ⟨?_, ?_, ?_, ?_⟩ <;> simp only [putStep]
  · rw [if_neg hpa, if_neg hpb, if_neg h13, if_pos trivial]
  · rw [if_neg hpa, if_neg hpb, if_neg h23, if_neg (Ne.symm h12),
      if_pos trivial]
  · rw [if_neg hpa, if_neg hpb, if_pos trivial]
  · intro j hj1 hj2 hj3
    rw [if_neg hpa, if_neg hpb, if_neg hj3, if_neg hj1, if_neg hj2]


/-- Only the three collecting tapes are touched. -/
theorem putStep_other (v : Bool) (o1 o2 o3 : Fin tapes)
    (h12 : o1 ≠ o2) (h13 : o1 ≠ o3) (h23 : o2 ≠ o3)
    (T : Fin tapes → Tape) (j : Fin tapes)
    (hj1 : j ≠ o1) (hj2 : j ≠ o2) (hj3 : j ≠ o3) :
    putStep v o1 o2 o3 T j = T j := by
  by_cases hpa : (T o1).head = TapeSymbol.blank
  · exact (putStep_phase0 v o1 o2 o3 h12 h13 h23 T hpa).2 j hj1
  · by_cases hpb : (T o2).head = TapeSymbol.blank
    · exact (putStep_phase1 v o1 o2 o3 h12 h13 h23 T hpa hpb).2 j hj2
    · exact (putStep_phase2 v o1 o2 o3 h12 h13 h23 T hpa hpb).2.2.2 j hj1
        hj2 hj3

/-! ## Three deposits fill a slot on each tape -/

set_option maxHeartbeats 2000000 in
/-- **A group of three deposits.**  From aligned frontiers, three verdicts
land one on each tape and the heads realign. -/
theorem putGroup (u v w : Bool) (o1 o2 o3 : Fin tapes)
    (h12 : o1 ≠ o2) (h13 : o1 ≠ o3) (h23 : o2 ≠ o3)
    (T : Fin tapes → Tape) (L1 L2 L3 : List TapeSymbol)
    (h1 : T o1 = cellsTape L1 []) (h2 : T o2 = cellsTape L2 [])
    (h3 : T o3 = cellsTape L3 []) :
    (putStep w o1 o2 o3 (putStep v o1 o2 o3 (putStep u o1 o2 o3 T))) o1 =
      cellsTape (TapeSymbol.bit u :: L1) [] ∧
    (putStep w o1 o2 o3 (putStep v o1 o2 o3 (putStep u o1 o2 o3 T))) o2 =
      cellsTape (TapeSymbol.bit v :: L2) [] ∧
    (putStep w o1 o2 o3 (putStep v o1 o2 o3 (putStep u o1 o2 o3 T))) o3 =
      cellsTape (TapeSymbol.bit w :: L3) [] ∧
    (∀ j, j ≠ o1 → j ≠ o2 → j ≠ o3 →
      (putStep w o1 o2 o3 (putStep v o1 o2 o3 (putStep u o1 o2 o3 T))) j =
        T j) := by
  -- first deposit
  have hp0 : (T o1).head = TapeSymbol.blank := by rw [h1]; rfl
  obtain ⟨s1a, s1o⟩ := putStep_phase0 u o1 o2 o3 h12 h13 h23 T hp0
  have s1a' : (putStep u o1 o2 o3 T) o1 = cellsTape L1
      [TapeSymbol.bit u] := by
    rw [s1a, h1, write_cellsTape]
    rfl
  have s1b : (putStep u o1 o2 o3 T) o2 = cellsTape L2 [] := by
    rw [s1o o2 (Ne.symm h12), h2]
  have s1c : (putStep u o1 o2 o3 T) o3 = cellsTape L3 [] := by
    rw [s1o o3 (Ne.symm h13), h3]
  -- second deposit
  have hp1a : ((putStep u o1 o2 o3 T) o1).head ≠ TapeSymbol.blank := by
    rw [s1a']
    simp [cellsTape]
  have hp1b : ((putStep u o1 o2 o3 T) o2).head = TapeSymbol.blank := by
    rw [s1b]; rfl
  obtain ⟨s2b, s2o⟩ := putStep_phase1 v o1 o2 o3 h12 h13 h23
    (putStep u o1 o2 o3 T) hp1a hp1b
  have s2b' : (putStep v o1 o2 o3 (putStep u o1 o2 o3 T)) o2 =
      cellsTape L2 [TapeSymbol.bit v] := by
    rw [s2b, s1b, write_cellsTape]
    rfl
  have s2a : (putStep v o1 o2 o3 (putStep u o1 o2 o3 T)) o1 =
      cellsTape L1 [TapeSymbol.bit u] := by
    rw [s2o o1 h12, s1a']
  have s2c : (putStep v o1 o2 o3 (putStep u o1 o2 o3 T)) o3 =
      cellsTape L3 [] := by
    rw [s2o o3 (Ne.symm h23), s1c]
  -- third deposit
  have hp2a : ((putStep v o1 o2 o3 (putStep u o1 o2 o3 T)) o1).head ≠
      TapeSymbol.blank := by
    rw [s2a]
    simp [cellsTape]
  have hp2b : ((putStep v o1 o2 o3 (putStep u o1 o2 o3 T)) o2).head ≠
      TapeSymbol.blank := by
    rw [s2b']
    simp [cellsTape]
  obtain ⟨s3a, s3b, s3c, s3o⟩ := putStep_phase2 w o1 o2 o3 h12 h13 h23
    (putStep v o1 o2 o3 (putStep u o1 o2 o3 T)) hp2a hp2b
  refine ⟨?_, ?_, ?_, ?_⟩
  · rw [s3a, s2a, cellsTape_moveRight_headD]
    rfl
  · rw [s3b, s2b', cellsTape_moveRight_headD]
    rfl
  · rw [s3c, s2c, write_cellsTape, cellsTape_moveRight_headD]
    rfl
  · intro j hj1 hj2 hj3
    rw [s3o j hj1 hj2 hj3, s2o j hj2, s1o j hj1]


/-! ## The deposit, as an action on the triple alone -/

/-- The deposit's effect on the three collecting tapes. -/
def putTriple (v : Bool) (t : Tape × Tape × Tape) : Tape × Tape × Tape :=
  if t.1.head = TapeSymbol.blank then
    (Tape.write t.1 (TapeSymbol.bit v), t.2.1, t.2.2)
  else if t.2.1.head = TapeSymbol.blank then
    (t.1, Tape.write t.2.1 (TapeSymbol.bit v), t.2.2)
  else
    (moveDir HeadMove.right t.1, moveDir HeadMove.right t.2.1,
      moveDir HeadMove.right (Tape.write t.2.2 (TapeSymbol.bit v)))

/-- **The deposit reads and writes only the triple.** -/
theorem putStep_triple (v : Bool) (o1 o2 o3 : Fin tapes)
    (h12 : o1 ≠ o2) (h13 : o1 ≠ o3) (h23 : o2 ≠ o3)
    (T : Fin tapes → Tape) :
    ((putStep v o1 o2 o3 T) o1, (putStep v o1 o2 o3 T) o2,
        (putStep v o1 o2 o3 T) o3) =
      putTriple v (T o1, T o2, T o3) := by
  unfold putTriple
  by_cases hpa : (T o1).head = TapeSymbol.blank
  · rw [if_pos hpa]
    obtain ⟨s1, so⟩ := putStep_phase0 v o1 o2 o3 h12 h13 h23 T hpa
    rw [s1, so o2 (Ne.symm h12), so o3 (Ne.symm h13)]
  · rw [if_neg hpa]
    by_cases hpb : (T o2).head = TapeSymbol.blank
    · rw [if_pos hpb]
      obtain ⟨s2, so⟩ := putStep_phase1 v o1 o2 o3 h12 h13 h23 T hpa hpb
      rw [s2, so o1 h12, so o3 (Ne.symm h23)]
    · rw [if_neg hpb]
      obtain ⟨s1, s2, s3, _⟩ := putStep_phase2 v o1 o2 o3 h12 h13 h23 T hpa
        hpb
      rw [s1, s2, s3]

/-- Deposits, in order. -/
def putTripleAll : List Bool → Tape × Tape × Tape → Tape × Tape × Tape
  | [], t => t
  | v :: vs, t => putTripleAll vs (putTriple v t)

end SipserGacsLautemann