sgl_power_all

import Definitions.Def_sgl_power_rec

/-!
# A machine for every degree

The recursion, closed: for each degree there is a machine — with a finite
state space, which the eventual bridge to `Machine` will need — satisfying the
power specification within `50 · (N+2)^(d+1)` steps.

The induction is at the meta level.  The degree is known when the machine is
built, so the machine for `d + 1` is the machine for `d` with three more
stages; no tape ever counts to `d`.  The state type grows with each degree,
which is why the statement quantifies over it existentially.
-/

namespace SipserGacsLautemann

variable {tapes : Nat}

set_option maxHeartbeats 1000000 in
/-- The base machine: origin markers on both working tapes and a single mark —
`(N+1)^0` of them — on the first. -/
theorem powerSpec_zero (s a b : Fin tapes) (hsa : s ≠ a) (hsb : s ≠ b)
    (hab : a ≠ b) (N : Nat) :
    PowerSpec s a b N 0
      ((prepTape a).andThen fun _ =>
        (putMark a).andThen fun _ => prepTape b)
      (3 + 1 + (1 + 1 + 3)) := by
  classical
  refine ⟨true, ?_⟩
  intro T Ls Rs hs ha hb
  obtain ⟨g1, s1⟩ := prepTape_spec a T [] ha
  set T1 := Function.update T a (cellsTape [TapeSymbol.blank] []) with hT1
  have hT1a : T1 a = cellsTape [TapeSymbol.blank] [] := by
    rw [hT1, Function.update_self]
  obtain ⟨g2, s2⟩ := putMark_spec a [TapeSymbol.blank] [] T1 hT1a
  set T2 := Function.update T1 a
    (cellsTape (TapeSymbol.bit true :: [TapeSymbol.blank])
      ([] : List TapeSymbol).tail) with hT2
  have hT2b : T2 b = cellsTape [] [] := by
    rw [hT2, Function.update_of_ne (Ne.symm hab), hT1,
      Function.update_of_ne (Ne.symm hab)]
    exact hb
  obtain ⟨g3, s3⟩ := prepTape_spec b T2 [] hT2b
  have k2 := chainStepC g2 s2 g3
  have k1 := chainStepC g1 s1 k2.1
  have hIR : ∀ {S₁ S₂ : Type} (bb : Bool) (c : TypedConfiguration tapes S₂),
      (TypedConfiguration.inRight (S₁ := S₁) bb c).tape = c.tape :=
    fun _ _ => rfl
  have hpt : pTape a b 0 = a := rfl
  have hpo : pOther a b 0 = b := rfl
  refine ⟨k1.1, ?_, ?_, ?_, ?_⟩
  · refine ⟨[], ?_⟩
    rw [hpt, k1.2, hIR, k2.2, hIR, s3, Function.update_of_ne hab, hT2,
      Function.update_self, pow_zero]
    rfl
  · refine ⟨[], ?_⟩
    rw [hpo, k1.2, hIR, k2.2, hIR, s3, Function.update_self]
  · rw [k1.2, hIR, k2.2, hIR, s3, Function.update_of_ne hsb, hT2,
      Function.update_of_ne hsa, hT1, Function.update_of_ne hsa]
  · intro j hjs hja hjb
    rw [k1.2, hIR, k2.2, hIR, s3, Function.update_of_ne hjb, hT2,
      Function.update_of_ne hja, hT1, Function.update_of_ne hja]

set_option maxHeartbeats 1000000 in
/-- **A machine for every degree.** -/
theorem power_exists (s a b : Fin tapes) (hsa : s ≠ a) (hsb : s ≠ b)
    (hab : a ≠ b) (N : Nat) :
    ∀ d : Nat, ∃ (S : Type) (_ : Fintype S) (M : TypedMachine tapes S)
      (cost : Nat),
      cost ≤ 50 * (N + 2) ^ (d + 1) ∧ PowerSpec s a b N d M cost := by
  intro d
  induction d with
  | zero =>
      refine ⟨_, inferInstance, _, _, ?_, powerSpec_zero s a b hsa hsb hab N⟩
      rw [pow_one]
      omega
  | succ d ih =>
      obtain ⟨S, inst, M, cost, hb, hP⟩ := ih
      refine ⟨_, ?_, _, _, ?_, powerSpec_step s a b hsa hsb hab N d M cost hP⟩
      · letI := inst
        infer_instance
      · -- the arithmetic
        set ℓ := (N + 1) ^ d with hℓ
        have hℓ1 : 1 ≤ ℓ := Nat.one_le_pow d (N + 1) (by omega)
        have hK : (ℓ - 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)
            - ((N + 1) * 5 + 4 + 1 + ((N + 1) * 4 + 3 + 1 + 1)
              + 1 + (1 + 1 + 1) + 1) := Nat.sub_one_mul _ _
        have hKle : ℓ * ((N + 1) * 5 + 4 + 1 + ((N + 1) * 4 + 3 + 1 + 1)
            + 1 + (1 + 1 + 1) + 1) ≤ ℓ * (36 * (N + 2)) :=
          Nat.mul_le_mul_left ℓ (by omega)
        have hK2 : (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) :=
          Nat.le_mul_of_pos_left _ (by omega)
        have h4ℓ : 4 * ℓ ≤ 4 * (ℓ * (N + 2)) := by
          have : ℓ ≤ ℓ * (N + 2) := Nat.le_mul_of_pos_right ℓ (by omega)
          omega
        have hℓP : ℓ * (N + 2) ≤ (N + 2) ^ d * (N + 2) :=
          Nat.mul_le_mul_right (N + 2)
            (by rw [hℓ]; exact Nat.pow_le_pow_left (by omega) d)
        have hpow1 : (N + 2) ^ d * (N + 2) = (N + 2) ^ (d + 1) := by
          rw [pow_succ]
        have hpow2 : (N + 2) ^ (d + 1) * (N + 2) = (N + 2) ^ (d + 1 + 1) :=
          (pow_succ (N + 2) (d + 1)).symm
        have hmono : (N + 2) ^ (d + 1) * 2 ≤ (N + 2) ^ (d + 1) * (N + 2) :=
          Nat.mul_le_mul_left _ (by omega)
        have hge1 : 1 ≤ (N + 2) ^ (d + 1) := Nat.one_le_pow _ _ (by omega)
        have hmul36 : ℓ * (36 * (N + 2)) = 36 * (ℓ * (N + 2)) := by ring
        omega

end SipserGacsLautemann