sgl_power_rec

import Definitions.Def_sgl_power_step

/-!
# One degree up

The power machine for degree `d + 1` is the machine for degree `d`, then a
rewind onto the run it built, then one multiplication by the seed, then one
step right to bury the consumed multiplier under a blank.

That last step is what keeps the recursion honest.  A consumed multiplier has
its marks at the top of its left context, and a fresh run laid directly on top
of them would merge with them — two runs of the same symbol are one run, and
the next rewind would walk back over both.  One rightward step materialises a
blank above the marks, and the merge cannot happen.

The specification each degree satisfies is stated once, and the parity of the
degree says which of the two working tapes holds the run.
-/

namespace SipserGacsLautemann

variable {tapes : Nat}

/-- The tape holding the run at degree `d`. -/
def pTape (a b : Fin tapes) (d : Nat) : Fin tapes :=
  if d % 2 = 0 then a else b

/-- The other one. -/
def pOther (a b : Fin tapes) (d : Nat) : Fin tapes :=
  if d % 2 = 0 then b else a

theorem pTape_succ (a b : Fin tapes) (d : Nat) :
    pTape a b (d + 1) = pOther a b d := by
  rcases Nat.mod_two_eq_zero_or_one d with h | h <;>
    simp [pTape, pOther, Nat.succ_mod_two_eq_zero_iff,
      Nat.succ_mod_two_eq_one_iff, h]

theorem pOther_succ (a b : Fin tapes) (d : Nat) :
    pOther a b (d + 1) = pTape a b d := by
  rcases Nat.mod_two_eq_zero_or_one d with h | h <;>
    simp [pTape, pOther, Nat.succ_mod_two_eq_zero_iff,
      Nat.succ_mod_two_eq_one_iff, h]

theorem pTape_cases (a b : Fin tapes) (d : Nat) :
    pTape a b d = a ∨ pTape a b d = b := by
  rw [pTape]; split <;> simp

theorem pOther_cases (a b : Fin tapes) (d : Nat) :
    pOther a b d = a ∨ pOther a b d = b := by
  rw [pOther]; split <;> simp

theorem pTape_ne_pOther (a b : Fin tapes) (hab : a ≠ b) (d : Nat) :
    pTape a b d ≠ pOther a b d := by
  rw [pTape, pOther]; split
  · exact hab
  · exact Ne.symm hab

/-- **What the machine for degree `d` does.**  From a seed of `N + 1` marks
and two virgin working tapes: a run of `(N+1)^d` on the parity tape with a
blank below it and the head past it, the other tape blank-topped and
right-empty, the seed restored, everything else untouched. -/
def PowerSpec (s a b : Fin tapes) (N d : Nat) {S : Type}
    (M : TypedMachine tapes S) (cost : Nat) : Prop :=
  ∃ v : Bool, ∀ (T : Fin tapes → Tape) (Ls Rs : List TapeSymbol),
    T s = cellsTape (TapeSymbol.blank :: Ls)
      (List.replicate (N + 1) (TapeSymbol.bit true) ++
        TapeSymbol.blank :: Rs) →
    T a = cellsTape [] [] → T b = cellsTape [] [] →
    HaltsExactly M (M.startCfg T) cost v ∧
    (∃ La, (((M.step^[cost]) (M.startCfg T)).tape) (pTape a b d) =
      cellsTape (List.replicate ((N + 1) ^ d) (TapeSymbol.bit true) ++
        TapeSymbol.blank :: La) []) ∧
    (∃ Lb, (((M.step^[cost]) (M.startCfg T)).tape) (pOther a b d) =
      cellsTape (TapeSymbol.blank :: Lb) []) ∧
    (((M.step^[cost]) (M.startCfg T)).tape) s = T s ∧
    (∀ j, j ≠ s → j ≠ a → j ≠ b →
      (((M.step^[cost]) (M.startCfg T)).tape) j = T j)

set_option maxHeartbeats 4000000 in
/-- **One degree up.** -/
theorem powerSpec_step (s a b : Fin tapes) (hsa : s ≠ a) (hsb : s ≠ b)
    (hab : a ≠ b) (N d : Nat) {S : Type} (M : TypedMachine tapes S)
    (cost : Nat) (hP : PowerSpec s a b N d M cost) :
    PowerSpec s a b N (d + 1)
      (M.andThen fun _ => (rewindRun (pTape a b d)).andThen fun _ =>
        (multiply (pTape a b d) s (pOther a b d)).andThen fun _ =>
          moveUpTo (pTape a b d) 1 HeadMove.right)
      (cost + 1 + ((N + 1) ^ d * 4 + 3 + 1 + 1 + 1 +
        ((((N + 1) ^ d) - 1) * ((N + 1) * 5 + 4 + 1 +
            ((N + 1) * 4 + 3 + 1 + 1) + 1 + (1 + 1 + 1) + 1)
          + ((N + 1) * 5 + 4 + 1 + ((N + 1) * 4 + 3 + 1 + 1)
            + 1 + (1 + 1 + 1)) + 1 + 1))) := by
  classical
  obtain ⟨v, hp⟩ := hP
  refine ⟨true, ?_⟩
  intro T Ls Rs hs ha hb
  obtain ⟨hM, ⟨La, hFa⟩, ⟨Lb, hFb⟩, hFs, hFo⟩ := hp T Ls Rs hs ha hb
  set ℓ := (N + 1) ^ d with hℓ
  have hℓ1 : 1 ≤ ℓ := Nat.one_le_pow d (N + 1) (by omega)
  set mt := pTape a b d with hmt
  set ot := pOther a b d with hot
  have hsm : s ≠ mt := by
    rcases pTape_cases a b d with h | h <;> rw [hmt, h]
    · exact hsa
    · exact hsb
  have hsd : s ≠ ot := by
    rcases pOther_cases a b d with h | h <;> rw [hot, h]
    · exact hsa
    · exact hsb
  have hdm : ot ≠ mt := (pTape_ne_pOther a b hab d).symm
  set F1 := ((M.step^[cost]) (M.startCfg T)).tape with hF1
  -- the rewind
  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 mt (List.replicate ℓ (TapeSymbol.bit true))
    La [] TapeSymbol.blank F1 hnb
    (by rw [hFa, List.reverse_replicate]; rfl)
  have hlenℓ : (List.replicate ℓ (TapeSymbol.bit true)).length = ℓ :=
    List.length_replicate
  rw [hlenℓ] at gR sR
  set F2 := Function.update F1 mt
    (cellsTape (TapeSymbol.blank :: La)
      (List.replicate ℓ (TapeSymbol.bit true) ++ TapeSymbol.blank :: []))
    with hF2
  have hF2s : F2 s = cellsTape (TapeSymbol.blank :: Ls)
      (List.replicate (N + 1) (TapeSymbol.bit true) ++
        TapeSymbol.blank :: Rs) := by
    rw [hF2, Function.update_of_ne hsm, hFs]
    exact hs
  have hF2m : F2 mt = cellsTape (TapeSymbol.blank :: La)
      (List.replicate ℓ (TapeSymbol.bit true) ++ TapeSymbol.blank :: []) := by
    rw [hF2, Function.update_self]
  have hF2o : F2 ot = cellsTape (TapeSymbol.blank :: Lb) [] := by
    rw [hF2, Function.update_of_ne hdm]
    exact hFb
  -- the multiplication
  have hnbS : ∀ c ∈ List.replicate (N + 1) (TapeSymbol.bit true),
      c ≠ TapeSymbol.blank := by
    intro c hc
    rw [List.eq_of_mem_replicate hc]
    simp
  have hlen : (List.replicate (N + 1) (TapeSymbol.bit true)).length = N + 1 :=
    List.length_replicate
  obtain ⟨gX, sX⟩ := multiply_run mt s ot hsd hdm hsm
    (List.replicate (N + 1) (TapeSymbol.bit true)) Ls Rs
    (TapeSymbol.blank :: La) [] ℓ hℓ1 F2 hnbS hF2s hF2m
  rw [hlen] at gX sX
  set F3 := ((markedStep mt (tallyEffect s ot (N + 1)))^[ℓ]) F2 with hF3
  -- the burying step
  have hF3m : F3 mt = cellsTape
      (List.replicate ℓ (TapeSymbol.bit true) ++ (TapeSymbol.blank :: La))
      (TapeSymbol.blank :: []) := by
    rw [hF3]
    have := multiply_mult mt s ot hsd hdm hsm
      (List.replicate (N + 1) (TapeSymbol.bit true)) Ls Rs
      (TapeSymbol.blank :: La) [] ℓ F2 hF2s hF2m
    rw [hlen] at this
    exact this
  have gV := moveUpTo_spec mt 1 HeadMove.right (by omega) F3
  have sV : (((moveUpTo mt 1 HeadMove.right).step^[1])
      ((moveUpTo mt 1 HeadMove.right).startCfg F3)).tape =
      Function.update F3 mt (moveDir HeadMove.right (F3 mt)) := by
    rw [moveUpTo_tape mt 1 HeadMove.right (by omega) F3, Function.iterate_one]
  set F4 := Function.update F3 mt (moveDir HeadMove.right (F3 mt)) with hF4
  -- the chain
  have k3 := chainStepC gX sX gV
  have k2 := chainStepC gR sR k3.1
  have k1 := chainStepC hM rfl k2.1
  have hIR : ∀ {S₁ S₂ : Type} (bb : Bool) (c : TypedConfiguration tapes S₂),
      (TypedConfiguration.inRight (S₁ := S₁) bb c).tape = c.tape :=
    fun _ _ => rfl
  refine ⟨k1.1, ?_, ?_, ?_, ?_⟩
  · -- the new run
    refine ⟨Lb, ?_⟩
    have hpow : (N + 1) ^ (d + 1) = ℓ * (N + 1) := by rw [hℓ, pow_succ]
    rw [pTape_succ, ← hot, k1.2, hIR, k2.2, hIR, k3.2, hIR, sV, hF4,
      Function.update_of_ne hdm, hF3, hpow]
    exact tallyEffect_iterate mt s ot hdm (N + 1) (TapeSymbol.blank :: Lb)
      ℓ F2 hF2o
  · -- the buried multiplier
    refine ⟨List.replicate ℓ (TapeSymbol.bit true) ++ TapeSymbol.blank :: La,
      ?_⟩
    rw [pOther_succ, ← hmt, k1.2, hIR, k2.2, hIR, k3.2, hIR, sV, hF4,
      Function.update_self, hF3m]
    rfl
  · -- the seed
    rw [k1.2, hIR, k2.2, hIR, k3.2, hIR, sV, hF4, Function.update_of_ne hsm,
      hF3, multiply_other mt s ot (N + 1) ℓ F2 s hsm hsd, hF2s, hs]
  · -- everything else
    intro j hjs hja hjb
    have hjm : j ≠ mt := by
      rcases pTape_cases a b d with h | h <;> rw [hmt, h]
      · exact hja
      · exact hjb
    have hjo : j ≠ ot := by
      rcases pOther_cases a b d with h | h <;> rw [hot, h]
      · exact hja
      · exact hjb
    rw [k1.2, hIR, k2.2, hIR, k3.2, hIR, sV, hF4, Function.update_of_ne hjm,
      hF3, multiply_other mt s ot (N + 1) ℓ F2 j hjm hjo, hF2,
      Function.update_of_ne hjm]
    exact hFo j hjs hja hjb

end SipserGacsLautemann