sgl_coeff

import Definitions.Def_sgl_tally2

/-!
# The coefficient

`κ` copies of a run, laid end to end on the clock.  One rewind puts the head
on the run's first mark; after that each tally restores its source exactly, so
the copies need no rewinding between them — the machine for `κ + 1` copies is
the machine for `κ` with one more tally.

The count is `κ ≥ 1` by construction, which also absorbs the degenerate
coefficient: a polynomial bound with coefficient `c` is also bounded with
coefficient `c + 1`, and a positive count is what the tally loop needs.
-/

namespace SipserGacsLautemann

variable {tapes : Nat}

/-- What the copier for count `κ` does: the run rewound to source shape, the
clock grown by `κ` copies, everything else untouched. -/
def CoeffSpec (s' clk : Fin tapes) (κ : Nat) {S : Type}
    (M : TypedMachine tapes S) : Prop :=
  ∃ v : Bool, ∀ (T : Fin tapes → Tape) (ℓ : Nat) (Lr Lc : List TapeSymbol),
    T s' = cellsTape (List.replicate ℓ (TapeSymbol.bit true) ++
      TapeSymbol.blank :: Lr) [] →
    T clk = cellsTape Lc [] →
    ∃ cost : Nat,
      cost ≤ 4 * ℓ + 5 + κ * (9 * ℓ + 11) ∧
      HaltsExactly M (M.startCfg T) cost v ∧
      (((M.step^[cost]) (M.startCfg T)).tape) s' =
        cellsTape (TapeSymbol.blank :: Lr)
          (List.replicate ℓ (TapeSymbol.bit true) ++ TapeSymbol.blank :: []) ∧
      (((M.step^[cost]) (M.startCfg T)).tape) clk =
        cellsTape (List.replicate (κ * ℓ) (TapeSymbol.bit true) ++ Lc) [] ∧
      (∀ j, j ≠ s' → j ≠ clk →
        (((M.step^[cost]) (M.startCfg T)).tape) j = T j)

set_option maxHeartbeats 1000000 in
/-- One copy: rewind, then tally. -/
theorem coeffSpec_one (s' clk : Fin tapes) (hsc : s' ≠ clk) :
    CoeffSpec s' clk 1
      ((rewindRun s').andThen fun _ => copyTally s' clk) := by
  classical
  refine ⟨true, ?_⟩
  intro T ℓ Lr Lc hrun hclk
  have hnb : ∀ c ∈ List.replicate ℓ (TapeSymbol.bit true),
      c ≠ TapeSymbol.blank := by
    intro c hc
    rw [List.eq_of_mem_replicate hc]
    simp
  obtain ⟨gR, sR⟩ := rewindRun_spec s'
    (List.replicate ℓ (TapeSymbol.bit true)) Lr [] TapeSymbol.blank T hnb
    (by rw [hrun, List.reverse_replicate]; rfl)
  have hlenℓ : (List.replicate ℓ (TapeSymbol.bit true)).length = ℓ :=
    List.length_replicate
  rw [hlenℓ] at gR sR
  set T1 := Function.update T s'
    (cellsTape (TapeSymbol.blank :: Lr)
      (List.replicate ℓ (TapeSymbol.bit true) ++ TapeSymbol.blank :: []))
    with hT1
  have hT1s : T1 s' = cellsTape (TapeSymbol.blank :: Lr)
      (List.replicate ℓ (TapeSymbol.bit true) ++ TapeSymbol.blank :: []) := by
    rw [hT1, Function.update_self]
  have hT1c : T1 clk = cellsTape Lc [] := by
    rw [hT1, Function.update_of_ne (Ne.symm hsc)]
    exact hclk
  obtain ⟨gC, sC⟩ := copyTally_exact s' clk hsc
    (List.replicate ℓ (TapeSymbol.bit true)) Lr [] Lc [] T1 hnb hT1s hT1c
  rw [hlenℓ] at gC sC
  have hch := chainStepC gR sR gC
  have hIR : ∀ {S₁ S₂ : Type} (bb : Bool) (c : TypedConfiguration tapes S₂),
      (TypedConfiguration.inRight (S₁ := S₁) bb c).tape = c.tape :=
    fun _ _ => rfl
  have htp : ((((rewindRun s').andThen fun _ => copyTally s' clk).step^[
      ℓ * 4 + 3 + 1 + 1 + 1 + (ℓ * 5 + 4 + 1 + (ℓ * 4 + 3 + 1 + 1))])
      (((rewindRun s').andThen fun _ => copyTally s' clk).startCfg T)).tape =
      Function.update T1 clk
        (cellsTape (List.replicate ℓ (TapeSymbol.bit true) ++ Lc)
          (([] : List TapeSymbol).drop ℓ)) := by
    rw [hch.2, hIR]
    exact sC
  refine ⟨_, by omega, hch.1, ?_, ?_, ?_⟩
  · rw [htp, Function.update_of_ne hsc]
    exact hT1s
  · rw [htp, Function.update_self]
    have h1 : (1 : Nat) * ℓ = ℓ := Nat.one_mul ℓ
    rw [h1]
    cases hℓ : ℓ with
    | zero => rfl
    | succ k => simp
  · intro j hjs hjc
    rw [htp, Function.update_of_ne hjc, hT1, Function.update_of_ne hjs]

set_option maxHeartbeats 1000000 in
/-- One more copy. -/
theorem coeffSpec_succ (s' clk : Fin tapes) (hsc : s' ≠ clk) (κ : Nat)
    {S : Type} (M : TypedMachine tapes S) (hM : CoeffSpec s' clk κ M) :
    CoeffSpec s' clk (κ + 1) (M.andThen fun _ => copyTally s' clk) := by
  classical
  obtain ⟨v, hp⟩ := hM
  refine ⟨true, ?_⟩
  intro T ℓ Lr Lc hrun hclk
  obtain ⟨cost, hcb, hM1, hs1, hc1, ho1⟩ := hp T ℓ Lr Lc hrun hclk
  set F1 := ((M.step^[cost]) (M.startCfg T)).tape with hF1
  have hnb : ∀ c ∈ List.replicate ℓ (TapeSymbol.bit true),
      c ≠ TapeSymbol.blank := by
    intro c hc
    rw [List.eq_of_mem_replicate hc]
    simp
  obtain ⟨gC, sC⟩ := copyTally_exact s' clk hsc
    (List.replicate ℓ (TapeSymbol.bit true)) Lr []
    (List.replicate (κ * ℓ) (TapeSymbol.bit true) ++ Lc) [] F1 hnb hs1 hc1
  have hlenℓ : (List.replicate ℓ (TapeSymbol.bit true)).length = ℓ :=
    List.length_replicate
  rw [hlenℓ] at gC sC
  have hch := chainStepC hM1 rfl gC
  have hIR : ∀ {S₁ S₂ : Type} (bb : Bool) (c : TypedConfiguration tapes S₂),
      (TypedConfiguration.inRight (S₁ := S₁) bb c).tape = c.tape :=
    fun _ _ => rfl
  have htp : (((M.andThen fun _ => copyTally s' clk).step^[
      cost + 1 + (ℓ * 5 + 4 + 1 + (ℓ * 4 + 3 + 1 + 1))])
      ((M.andThen fun _ => copyTally s' clk).startCfg T)).tape =
      Function.update F1 clk
        (cellsTape (List.replicate ℓ (TapeSymbol.bit true) ++
          (List.replicate (κ * ℓ) (TapeSymbol.bit true) ++ Lc))
          (([] : List TapeSymbol).drop ℓ)) := by
    rw [hch.2, hIR]
    exact sC
  have hmul : (κ + 1) * (9 * ℓ + 11) = κ * (9 * ℓ + 11) + (9 * ℓ + 11) :=
    Nat.succ_mul κ (9 * ℓ + 11)
  refine ⟨_, by omega, hch.1, ?_, ?_, ?_⟩
  · rw [htp, Function.update_of_ne hsc]
    exact hs1
  · rw [htp, Function.update_self, ← List.append_assoc, ← List.replicate_add]
    have hadd : ℓ + κ * ℓ = (κ + 1) * ℓ := by ring
    rw [hadd]
    cases hℓ : ℓ with
    | zero => simp
    | succ k => simp
  · intro j hjs hjc
    rw [htp, Function.update_of_ne hjc]
    exact ho1 j hjs hjc

set_option maxHeartbeats 1000000 in
/-- **A copier for every count.** -/
theorem coeff_exists (s' clk : Fin tapes) (hsc : s' ≠ clk) :
    ∀ κ : Nat, ∃ (S : Type) (_ : Fintype S) (M : TypedMachine tapes S),
      CoeffSpec s' clk (κ + 1) M := by
  intro κ
  induction κ with
  | zero =>
      exact ⟨_, inferInstance, _, coeffSpec_one s' clk hsc⟩
  | succ κ ih =>
      obtain ⟨S, inst, M, hM⟩ := ih
      refine ⟨_, ?_, _, coeffSpec_succ s' clk hsc (κ + 1) M hM⟩
      letI := inst
      infer_instance

end SipserGacsLautemann