sgl_tail

import Definitions.Def_sgl_seed

/-!
# The clock's tail

The same accumulation as the seed — one mark, four tallies — laid on top of
whatever the clock already holds, with no rewind at the end: the loop wants
the clock's head past its marks, which is where a tally leaves it.

The tail is what pays for the size conditions the polynomial part alone
cannot: the margin needs `Q + B + 2 ≤ 2A` and the polynomial part only
guarantees `2B`, which fails against `Q` at low degrees.  One extra copy of
the inputs closes it at every degree.
-/

namespace SipserGacsLautemann

variable {tapes : Nat}

/-- Mark, then four tallies onto the clock. -/
def tailSetup (s0 s1 s2 clk : Fin tapes) :=
  (putMark clk).andThen fun _ =>
    (copyTally s0 clk).andThen fun _ =>
      (copyTally s1 clk).andThen fun _ =>
        (copyTally s2 clk).andThen fun _ =>
          copyTally s2 clk

set_option maxHeartbeats 4000000 in
/-- **The tail: `N + 1` more marks, head past them.** -/
theorem tailSetup_spec (s0 s1 s2 clk : Fin tapes)
    (h0 : s0 ≠ clk) (h1 : s1 ≠ clk) (h2 : s2 ≠ clk)
    (x0 x1 x2 L0 L1 L2 R0 R1 R2 Lc : List TapeSymbol) (T : Fin tapes → Tape)
    (hn0 : ∀ c ∈ x0, c ≠ TapeSymbol.blank)
    (hn1 : ∀ c ∈ x1, c ≠ TapeSymbol.blank)
    (hn2 : ∀ c ∈ x2, c ≠ TapeSymbol.blank)
    (hs0 : T s0 = cellsTape (TapeSymbol.blank :: L0)
      (x0 ++ TapeSymbol.blank :: R0))
    (hs1 : T s1 = cellsTape (TapeSymbol.blank :: L1)
      (x1 ++ TapeSymbol.blank :: R1))
    (hs2 : T s2 = cellsTape (TapeSymbol.blank :: L2)
      (x2 ++ TapeSymbol.blank :: R2))
    (hclk : T clk = cellsTape Lc []) :
    ∃ cost : Nat,
      cost ≤ 9 * (x2.length + (x2.length + (x1.length + (x0.length + 1)))) + 36 ∧
      HaltsExactly (tailSetup s0 s1 s2 clk)
        ((tailSetup s0 s1 s2 clk).startCfg T) cost true ∧
      (((tailSetup s0 s1 s2 clk).step^[cost])
        ((tailSetup s0 s1 s2 clk).startCfg T)).tape =
        Function.update T clk
          (cellsTape (List.replicate
            (x2.length + (x2.length + (x1.length + (x0.length + 1))))
            (TapeSymbol.bit true) ++ Lc) []) := by
  classical
  obtain ⟨gB, sB⟩ := putMark_spec clk Lc [] T hclk
  set TB := Function.update T clk
    (cellsTape (TapeSymbol.bit true :: Lc)
      ([] : List TapeSymbol).tail) with hTB
  have hTBd : TB clk = cellsTape
      (List.replicate 1 (TapeSymbol.bit true) ++ Lc) [] := by
    rw [hTB, Function.update_self]
    rfl
  have hTBo : ∀ (s : Fin tapes), s ≠ clk → TB s = T s := by
    intro s hs
    rw [hTB, Function.update_of_ne hs]
  obtain ⟨g1, t1⟩ := copyTally_exact s0 clk h0 x0 L0 R0
    (List.replicate 1 (TapeSymbol.bit true) ++ Lc) [] TB hn0
    (by rw [hTBo s0 h0]; exact hs0) hTBd
  set T1 := Function.update TB clk
    (cellsTape (List.replicate x0.length (TapeSymbol.bit true) ++
      (List.replicate 1 (TapeSymbol.bit true) ++ Lc))
      (([] : List TapeSymbol).drop x0.length)) with hT1
  have hT1d : T1 clk = cellsTape
      (List.replicate (x0.length + 1) (TapeSymbol.bit true) ++ Lc) [] := by
    rw [hT1, Function.update_self, ← List.append_assoc, ← List.replicate_add]
    simp
  have hT1o : ∀ (s : Fin tapes), s ≠ clk → T1 s = T s := by
    intro s hs
    rw [hT1, Function.update_of_ne hs]
    exact hTBo s hs
  obtain ⟨g2, t2⟩ := copyTally_exact s1 clk h1 x1 L1 R1
    (List.replicate (x0.length + 1) (TapeSymbol.bit true) ++ Lc) [] T1 hn1
    (by rw [hT1o s1 h1]; exact hs1) hT1d
  set T2 := Function.update T1 clk
    (cellsTape (List.replicate x1.length (TapeSymbol.bit true) ++
      (List.replicate (x0.length + 1) (TapeSymbol.bit true) ++ Lc))
      (([] : List TapeSymbol).drop x1.length)) with hT2
  have hT2d : T2 clk = cellsTape
      (List.replicate (x1.length + (x0.length + 1)) (TapeSymbol.bit true)
        ++ Lc) [] := by
    rw [hT2, Function.update_self, ← List.append_assoc, ← List.replicate_add]
    simp
  have hT2o : ∀ (s : Fin tapes), s ≠ clk → T2 s = T s := by
    intro s hs
    rw [hT2, Function.update_of_ne hs]
    exact hT1o s hs
  obtain ⟨g3, t3⟩ := copyTally_exact s2 clk h2 x2 L2 R2
    (List.replicate (x1.length + (x0.length + 1)) (TapeSymbol.bit true)
      ++ Lc) [] T2 hn2
    (by rw [hT2o s2 h2]; exact hs2) hT2d
  set T3 := Function.update T2 clk
    (cellsTape (List.replicate x2.length (TapeSymbol.bit true) ++
      (List.replicate (x1.length + (x0.length + 1)) (TapeSymbol.bit true)
        ++ Lc))
      (([] : List TapeSymbol).drop x2.length)) with hT3
  have hT3d : T3 clk = cellsTape
      (List.replicate (x2.length + (x1.length + (x0.length + 1)))
        (TapeSymbol.bit true) ++ Lc) [] := by
    rw [hT3, Function.update_self, ← List.append_assoc, ← List.replicate_add]
    simp
  have hT3o : ∀ (s : Fin tapes), s ≠ clk → T3 s = T s := by
    intro s hs
    rw [hT3, Function.update_of_ne hs]
    exact hT2o s hs
  obtain ⟨g4, t4⟩ := copyTally_exact s2 clk h2 x2 L2 R2
    (List.replicate (x2.length + (x1.length + (x0.length + 1)))
      (TapeSymbol.bit true) ++ Lc) [] T3 hn2
    (by rw [hT3o s2 h2]; exact hs2) hT3d
  have k4 := chainStepC g3 t3 g4
  have k3 := chainStepC g2 t2 k4.1
  have k2 := chainStepC g1 t1 k3.1
  have k1 := chainStepC gB sB k2.1
  refine ⟨_, by simp; omega, k1.1, ?_⟩
  have hIR : ∀ {S₁ S₂ : Type} (bb : Bool) (c : TypedConfiguration tapes S₂),
      (TypedConfiguration.inRight (S₁ := S₁) bb c).tape = c.tape :=
    fun _ _ => rfl
  have hfin : ((tailSetup s0 s1 s2 clk).step^[_])
      ((tailSetup s0 s1 s2 clk).startCfg T) = _ := k1.2
  rw [hfin, hIR, k2.2, hIR, k3.2, hIR, k4.2, hIR, t4]
  funext j
  by_cases hj : j = clk
  · subst hj
    rw [Function.update_self, Function.update_self, ← List.append_assoc,
      ← List.replicate_add]
    simp
  · rw [Function.update_of_ne hj, Function.update_of_ne hj, hT3,
      Function.update_of_ne hj]
    exact hT2o j hj

end SipserGacsLautemann