sgl_seed

import Definitions.Def_sgl_coeff

/-!
# The seed

A run of `N + 1` marks, where `N` bounds the delegate's total input length at
every offset: the three inputs and the third one again, since the unary offset
never exceeds it.  One padding mark under four tallies, then a rewind into
source shape — the shape the power machine reads its multiplicand from.

The extra mark is not padding for safety's sake: the power machine's inner
loop runs once per mark of its multiplier, and a loop of the test-after-act
shape must run at least once.  `N + 1 ≥ 1` always does; `N` alone would fail
on empty inputs.
-/

namespace SipserGacsLautemann

variable {tapes : Nat}

/-- Mark, four tallies, rewind. -/
def seedSetup (s0 s1 s2 sd : Fin tapes) :=
  (prepTape sd).andThen fun _ =>
    (putMark sd).andThen fun _ =>
      (copyTally s0 sd).andThen fun _ =>
        (copyTally s1 sd).andThen fun _ =>
          (copyTally s2 sd).andThen fun _ =>
            (copyTally s2 sd).andThen fun _ =>
              rewindRun sd

set_option maxHeartbeats 4000000 in
/-- **The seed, in source shape.** -/
theorem seedSetup_spec (s0 s1 s2 sd : Fin tapes)
    (h0 : s0 ≠ sd) (h1 : s1 ≠ sd) (h2 : s2 ≠ sd)
    (x0 x1 x2 L0 L1 L2 R0 R1 R2 : 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))
    (hsd : T sd = cellsTape [] []) :
    ∃ cost : Nat,
      cost ≤ 13 * (x2.length + (x2.length + (x1.length + (x0.length + 1)))) + 47 ∧
      HaltsExactly (seedSetup s0 s1 s2 sd)
        ((seedSetup s0 s1 s2 sd).startCfg T) cost true ∧
      (((seedSetup s0 s1 s2 sd).step^[cost])
        ((seedSetup s0 s1 s2 sd).startCfg T)).tape =
        Function.update T sd
          (cellsTape [TapeSymbol.blank]
            (List.replicate
              (x2.length + (x2.length + (x1.length + (x0.length + 1))))
              (TapeSymbol.bit true) ++ TapeSymbol.blank :: [])) := by
  classical
  obtain ⟨gA, sA⟩ := prepTape_spec sd T [] hsd
  set T0 := Function.update T sd (cellsTape [TapeSymbol.blank] []) with hT0
  have hT0d : T0 sd = cellsTape [TapeSymbol.blank] [] := by
    rw [hT0, Function.update_self]
  obtain ⟨gB, sB⟩ := putMark_spec sd [TapeSymbol.blank] [] T0 hT0d
  set TB := Function.update T0 sd
    (cellsTape (TapeSymbol.bit true :: [TapeSymbol.blank])
      ([] : List TapeSymbol).tail) with hTB
  have hTBd : TB sd = cellsTape
      (List.replicate 1 (TapeSymbol.bit true) ++ [TapeSymbol.blank]) [] := by
    rw [hTB, Function.update_self]
    rfl
  have hTBo : ∀ (s : Fin tapes), s ≠ sd → TB s = T s := by
    intro s hs
    rw [hTB, Function.update_of_ne hs, hT0, Function.update_of_ne hs]
  obtain ⟨g1, t1⟩ := copyTally_exact s0 sd h0 x0 L0 R0
    (List.replicate 1 (TapeSymbol.bit true) ++ [TapeSymbol.blank]) [] TB hn0
    (by rw [hTBo s0 h0]; exact hs0) hTBd
  set T1 := Function.update TB sd
    (cellsTape (List.replicate x0.length (TapeSymbol.bit true) ++
      (List.replicate 1 (TapeSymbol.bit true) ++ [TapeSymbol.blank]))
      (([] : List TapeSymbol).drop x0.length)) with hT1
  have hT1d : T1 sd = cellsTape
      (List.replicate (x0.length + 1) (TapeSymbol.bit true) ++
        [TapeSymbol.blank]) [] := by
    rw [hT1, Function.update_self, ← List.append_assoc, ← List.replicate_add]
    simp
  have hT1o : ∀ (s : Fin tapes), s ≠ sd → 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 sd h1 x1 L1 R1
    (List.replicate (x0.length + 1) (TapeSymbol.bit true) ++
      [TapeSymbol.blank]) [] T1 hn1
    (by rw [hT1o s1 h1]; exact hs1) hT1d
  set T2 := Function.update T1 sd
    (cellsTape (List.replicate x1.length (TapeSymbol.bit true) ++
      (List.replicate (x0.length + 1) (TapeSymbol.bit true) ++
        [TapeSymbol.blank]))
      (([] : List TapeSymbol).drop x1.length)) with hT2
  have hT2d : T2 sd = cellsTape
      (List.replicate (x1.length + (x0.length + 1)) (TapeSymbol.bit true) ++
        [TapeSymbol.blank]) [] := by
    rw [hT2, Function.update_self, ← List.append_assoc, ← List.replicate_add]
    simp
  have hT2o : ∀ (s : Fin tapes), s ≠ sd → 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 sd h2 x2 L2 R2
    (List.replicate (x1.length + (x0.length + 1)) (TapeSymbol.bit true) ++
      [TapeSymbol.blank]) [] T2 hn2
    (by rw [hT2o s2 h2]; exact hs2) hT2d
  set T3 := Function.update T2 sd
    (cellsTape (List.replicate x2.length (TapeSymbol.bit true) ++
      (List.replicate (x1.length + (x0.length + 1)) (TapeSymbol.bit true) ++
        [TapeSymbol.blank]))
      (([] : List TapeSymbol).drop x2.length)) with hT3
  have hT3d : T3 sd = cellsTape
      (List.replicate (x2.length + (x1.length + (x0.length + 1)))
        (TapeSymbol.bit true) ++ [TapeSymbol.blank]) [] := by
    rw [hT3, Function.update_self, ← List.append_assoc, ← List.replicate_add]
    simp
  have hT3o : ∀ (s : Fin tapes), s ≠ sd → 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 sd h2 x2 L2 R2
    (List.replicate (x2.length + (x1.length + (x0.length + 1)))
      (TapeSymbol.bit true) ++ [TapeSymbol.blank]) [] T3 hn2
    (by rw [hT3o s2 h2]; exact hs2) hT3d
  set T4 := Function.update T3 sd
    (cellsTape (List.replicate x2.length (TapeSymbol.bit true) ++
      (List.replicate (x2.length + (x1.length + (x0.length + 1)))
        (TapeSymbol.bit true) ++ [TapeSymbol.blank]))
      (([] : List TapeSymbol).drop x2.length)) with hT4
  set NN := x2.length + (x2.length + (x1.length + (x0.length + 1))) with hNN
  have hT4d : T4 sd = cellsTape
      (List.replicate NN (TapeSymbol.bit true) ++ [TapeSymbol.blank]) [] := by
    rw [hT4, Function.update_self, ← List.append_assoc, ← List.replicate_add,
      hNN]
    simp
  have hnbN : ∀ c ∈ List.replicate NN (TapeSymbol.bit true),
      c ≠ TapeSymbol.blank := by
    intro c hc
    rw [List.eq_of_mem_replicate hc]
    simp
  obtain ⟨gR, sR⟩ := rewindRun_spec sd
    (List.replicate NN (TapeSymbol.bit true)) [] [] TapeSymbol.blank T4 hnbN
    (by rw [hT4d, List.reverse_replicate]; rfl)
  have k5 := chainStepC g4 t4 gR
  have k4 := chainStepC g3 t3 k5.1
  have k3 := chainStepC g2 t2 k4.1
  have k2 := chainStepC g1 t1 k3.1
  have k1 := chainStepC gB sB k2.1
  have k0 := chainStepC gA sA k1.1
  refine ⟨_, by simp; omega, k0.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 : ((seedSetup s0 s1 s2 sd).step^[_])
      ((seedSetup s0 s1 s2 sd).startCfg T) = _ := k0.2
  rw [hfin, hIR, k1.2, hIR, k2.2, hIR, k3.2, hIR, k4.2, hIR, k5.2, hIR, sR]
  funext j
  by_cases hj : j = sd
  · subst hj
    rw [Function.update_self, Function.update_self]
  · rw [Function.update_of_ne hj, Function.update_of_ne hj, hT4,
      Function.update_of_ne hj]
    exact hT3o j hj

end SipserGacsLautemann