sgl_prologue13
DefinitionDefinition code
import Definitions.Def_sgl_dig_costs
import Definitions.Def_sgl_clock_poly
/-!
# The prologue, with the polynomial clock
Ten roles: three inputs, the clock, the guide, the counter, the seed, the
ping-pong pair, and an idle partner for the normalising walks. The four
working tapes are none of them — the loop needs those virgin, and the surest
way to hand them over virgin is never to name them here.
The composition is six stages. The clock's stage is the machine from
`clockPoly_exists`, whose role indices are this prologue's under a relabeling;
everything else is a published setup machine.
-/
namespace SipserGacsLautemann
variable {tapes : Nat}
set_option maxHeartbeats 4000000 in
set_option synthInstance.maxHeartbeats 1000000 in
/-- **The prologue.** Roles: `0‥2` inputs, `3` clock, `4` guide, `5` counter,
`6` seed, `7, 8` ping-pong, `9` idle. -/
theorem prologue13_exists (idx : Fin 10 → Fin tapes)
(hinj : Function.Injective idx) (κ d : Nat) :
∃ (S : Type) (_ : Fintype S) (M : TypedMachine tapes S),
∀ (T : Fin tapes → Tape) (x0 x1 x2 : List TapeSymbol),
(∀ c ∈ x0, c ≠ TapeSymbol.blank) →
(∀ c ∈ x1, c ≠ TapeSymbol.blank) →
(∀ c ∈ x2, c ≠ TapeSymbol.blank) →
T (idx 0) = cellsTape [] x0 →
T (idx 1) = cellsTape [] x1 →
T (idx 2) = cellsTape [] x2 →
(∀ k : Fin 10, 3 ≤ k.val → T (idx k) = cellsTape [] []) →
∃ cost : Nat,
cost ≤ 110 * ((κ + 1) *
(x2.length + (x2.length + (x1.length + x0.length)) + 2)
^ (d + 1))
+ 100 * (x2.length + (x2.length + (x1.length + x0.length)) + 2)
+ 300 ∧
HaltsExactly M (M.startCfg T) cost true ∧
(((M.step^[cost]) (M.startCfg T)).tape) (idx 0) =
cellsTape [TapeSymbol.blank] (x0 ++ [TapeSymbol.blank]) ∧
(((M.step^[cost]) (M.startCfg T)).tape) (idx 1) =
cellsTape [TapeSymbol.blank] (x1 ++ [TapeSymbol.blank]) ∧
(((M.step^[cost]) (M.startCfg T)).tape) (idx 2) =
cellsTape [TapeSymbol.blank] (x2 ++ [TapeSymbol.blank]) ∧
(((M.step^[cost]) (M.startCfg T)).tape) (idx 3) =
cellsTape (List.replicate
((x2.length + (x2.length + (x1.length + x0.length)) + 1)
+ (κ + 1) *
(x2.length + (x2.length + (x1.length + x0.length)) + 1)
^ d)
(TapeSymbol.bit true) ++ TapeSymbol.blank :: []) [] ∧
(((M.step^[cost]) (M.startCfg T)).tape) (idx 4) =
cellsTape []
(List.replicate (x2.length + 1) (TapeSymbol.bit true) ++
[TapeSymbol.blank]) ∧
(((M.step^[cost]) (M.startCfg T)).tape) (idx 5) =
cellsTape (List.replicate (x2.length + 2) TapeSymbol.blank) [] ∧
(∀ j, (∀ i : Fin 10, j ≠ idx i) →
(((M.step^[cost]) (M.startCfg T)).tape) j = T j) := by
classical
have hne : ∀ a b : Fin 10, a ≠ b → idx a ≠ idx b :=
fun a b hab h => hab (hinj h)
-- the clock stage's machine, on relabeled roles
set cpIdx : Fin 7 → Fin tapes := fun k =>
idx (match k with
| 0 => 0 | 1 => 1 | 2 => 2 | 3 => 6 | 4 => 7 | 5 => 8 | 6 => 3)
with hcpIdx
have hcpInj : Function.Injective cpIdx := by
intro a b hab
rw [hcpIdx] at hab
have := hinj hab
fin_cases a <;> fin_cases b <;> simp_all
obtain ⟨SC, instC, CP, hCP⟩ := clockPoly_exists cpIdx hcpInj κ d
letI := instC
refine ⟨_, ?_, (inputPrep (idx 0) (idx 9)).andThen fun _ =>
(inputPrep (idx 1) (idx 9)).andThen fun _ =>
(inputPrep (idx 2) (idx 9)).andThen fun _ =>
(prepTape (idx 4)).andThen fun _ =>
CP.andThen fun _ =>
guideSetup (idx 2) (idx 4) (idx 5), ?_⟩
· letI i5 : Fintype (stateOf (guideSetup (idx 2) (idx 4) (idx 5))) :=
inferInstance
letI i4 : Fintype (stateOf (CP.andThen fun _ =>
guideSetup (idx 2) (idx 4) (idx 5))) := inferInstance
letI i3 : Fintype (stateOf ((prepTape (idx 4)).andThen fun _ =>
CP.andThen fun _ => guideSetup (idx 2) (idx 4) (idx 5))) := inferInstance
letI i2 : Fintype (stateOf ((inputPrep (idx 2) (idx 9)).andThen fun _ =>
(prepTape (idx 4)).andThen fun _ =>
CP.andThen fun _ => guideSetup (idx 2) (idx 4) (idx 5))) :=
inferInstance
letI i1 : Fintype (stateOf ((inputPrep (idx 1) (idx 9)).andThen fun _ =>
(inputPrep (idx 2) (idx 9)).andThen fun _ =>
(prepTape (idx 4)).andThen fun _ =>
CP.andThen fun _ => guideSetup (idx 2) (idx 4) (idx 5))) :=
inferInstance
exact inferInstance
intro T x0 x1 x2 hn0 hn1 hn2 hx0 hx1 hx2 hvirgin
-- stage 1..3: the inputs
obtain ⟨c1, hb1, g1, t1⟩ := inputPrep_specB (idx 0) (idx 9)
(hne 0 9 (by decide)) x0 T hn0 hx0
set F1 := Function.update T (idx 0)
(cellsTape [TapeSymbol.blank] (x0 ++ [TapeSymbol.blank])) with hF1
obtain ⟨c2, hb2, g2, t2⟩ := inputPrep_specB (idx 1) (idx 9)
(hne 1 9 (by decide)) x1 F1 hn1
(by rw [hF1, Function.update_of_ne (hne 1 0 (by decide))]; exact hx1)
set F2 := Function.update F1 (idx 1)
(cellsTape [TapeSymbol.blank] (x1 ++ [TapeSymbol.blank])) with hF2
obtain ⟨c3, hb3, g3, t3⟩ := inputPrep_specB (idx 2) (idx 9)
(hne 2 9 (by decide)) x2 F2 hn2
(by rw [hF2, Function.update_of_ne (hne 2 1 (by decide)), hF1,
Function.update_of_ne (hne 2 0 (by decide))]; exact hx2)
set F3 := Function.update F2 (idx 2)
(cellsTape [TapeSymbol.blank] (x2 ++ [TapeSymbol.blank])) with hF3
have hF3v : ∀ j, j ≠ idx 0 → j ≠ idx 1 → j ≠ idx 2 → F3 j = T j := by
intro j h0 h1 h2
rw [hF3, Function.update_of_ne h2, hF2, Function.update_of_ne h1, hF1,
Function.update_of_ne h0]
-- stage 4: the guide's origin marker
obtain ⟨g4, t4⟩ := prepTape_spec (idx 4) F3 []
(by rw [hF3v _ (hne 4 0 (by decide)) (hne 4 1 (by decide))
(hne 4 2 (by decide))]; exact hvirgin 4 (by decide))
set F4 := Function.update F3 (idx 4)
(cellsTape [TapeSymbol.blank] []) with hF4
have hF4v : ∀ j, j ≠ idx 0 → j ≠ idx 1 → j ≠ idx 2 → j ≠ idx 4 →
F4 j = T j := by
intro j h0 h1 h2 h4
rw [hF4, Function.update_of_ne h4]
exact hF3v j h0 h1 h2
have hF4i0 : F4 (idx 0) = cellsTape [TapeSymbol.blank]
(x0 ++ [TapeSymbol.blank]) := by
rw [hF4, Function.update_of_ne (hne 0 4 (by decide)), hF3,
Function.update_of_ne (hne 0 2 (by decide)), hF2,
Function.update_of_ne (hne 0 1 (by decide)), hF1, Function.update_self]
have hF4i1 : F4 (idx 1) = cellsTape [TapeSymbol.blank]
(x1 ++ [TapeSymbol.blank]) := by
rw [hF4, Function.update_of_ne (hne 1 4 (by decide)), hF3,
Function.update_of_ne (hne 1 2 (by decide)), hF2, Function.update_self]
have hF4i2 : F4 (idx 2) = cellsTape [TapeSymbol.blank]
(x2 ++ [TapeSymbol.blank]) := by
rw [hF4, Function.update_of_ne (hne 2 4 (by decide)), hF3,
Function.update_self]
-- stage 5: the polynomial clock
have hcp0 : cpIdx 0 = idx 0 := rfl
have hcp1 : cpIdx 1 = idx 1 := rfl
have hcp2 : cpIdx 2 = idx 2 := rfl
have hcp3 : cpIdx 3 = idx 6 := rfl
have hcp4 : cpIdx 4 = idx 7 := rfl
have hcp5 : cpIdx 5 = idx 8 := rfl
have hcp6 : cpIdx 6 = idx 3 := rfl
obtain ⟨c5, hb5, g5, eclk, e0, e1, e2, hCPo⟩ := hCP F4 x0 x1 x2 [] [] []
[] [] [] hn0 hn1 hn2
(by rw [hcp0, hF4i0])
(by rw [hcp1, hF4i1])
(by rw [hcp2, hF4i2])
(by rw [hcp3, hF4v _ (hne 6 0 (by decide)) (hne 6 1 (by decide))
(hne 6 2 (by decide)) (hne 6 4 (by decide))]
exact hvirgin 6 (by decide))
(by rw [hcp4, hF4v _ (hne 7 0 (by decide)) (hne 7 1 (by decide))
(hne 7 2 (by decide)) (hne 7 4 (by decide))]
exact hvirgin 7 (by decide))
(by rw [hcp5, hF4v _ (hne 8 0 (by decide)) (hne 8 1 (by decide))
(hne 8 2 (by decide)) (hne 8 4 (by decide))]
exact hvirgin 8 (by decide))
(by rw [hcp6, hF4v _ (hne 3 0 (by decide)) (hne 3 1 (by decide))
(hne 3 2 (by decide)) (hne 3 4 (by decide))]
exact hvirgin 3 (by decide))
set F5 := ((CP.step^[c5]) (CP.startCfg F4)).tape with hF5
rw [hcp0] at e0
rw [hcp1] at e1
rw [hcp2] at e2
rw [hcp6] at eclk
have hF5v : ∀ j, j ≠ idx 0 → j ≠ idx 1 → j ≠ idx 2 → j ≠ idx 3 →
j ≠ idx 4 → j ≠ idx 6 → j ≠ idx 7 → j ≠ idx 8 → F5 j = T j := by
intro j h0 h1 h2 h3 h4 h6 h7 h8
rw [hCPo j (by
intro i
fin_cases i <;>
simp only [hcp0, hcp1, hcp2, hcp3, hcp4, hcp5, hcp6] <;>
assumption)]
exact hF4v j h0 h1 h2 h4
-- stage 6: the guide and counter
obtain ⟨c6, hb6, g6, t6⟩ := guideSetup_specB (idx 2) (idx 4) (idx 5)
(hne 2 4 (by decide)) (hne 4 5 (by decide)) (hne 2 5 (by decide))
x2 [] [] F5 hn2 (by rw [e2]; exact hF4i2)
(by rw [hCPo (idx 4) (by
intro i
fin_cases i <;>
simp only [hcp0, hcp1, hcp2, hcp3, hcp4, hcp5, hcp6] <;>
first
| exact hne 4 0 (by decide)
| exact hne 4 1 (by decide)
| exact hne 4 2 (by decide)
| exact hne 4 6 (by decide)
| exact hne 4 7 (by decide)
| exact hne 4 8 (by decide)
| exact hne 4 3 (by decide)), hF4, Function.update_self])
(by rw [hF5v _ (hne 5 0 (by decide)) (hne 5 1 (by decide))
(hne 5 2 (by decide)) (hne 5 3 (by decide)) (hne 5 4 (by decide))
(hne 5 6 (by decide)) (hne 5 7 (by decide)) (hne 5 8 (by decide))]
exact hvirgin 5 (by decide))
-- the chain
have k5 := chainStepC g5 rfl g6
have k4 := chainStepC g4 t4 k5.1
have k3 := chainStepC g3 t3 k4.1
have k2 := chainStepC g2 t2 k3.1
have k1 := chainStepC g1 t1 k2.1
have hIR : ∀ {S₁ S₂ : Type} (bb : Bool) (c : TypedConfiguration tapes S₂),
(TypedConfiguration.inRight (S₁ := S₁) bb c).tape = c.tape :=
fun _ _ => rfl
set F6 := Function.update (Function.update F5 (idx 5)
(cellsTape (List.replicate (x2.length + 2) TapeSymbol.blank) []))
(idx 4) (cellsTape []
(List.replicate (x2.length + 1) (TapeSymbol.bit true) ++
[TapeSymbol.blank])) with hF6
have hfin : ((((inputPrep (idx 0) (idx 9)).andThen fun _ =>
(inputPrep (idx 1) (idx 9)).andThen fun _ =>
(inputPrep (idx 2) (idx 9)).andThen fun _ =>
(prepTape (idx 4)).andThen fun _ =>
CP.andThen fun _ =>
guideSetup (idx 2) (idx 4) (idx 5)).step^[
c1 + 1 + (c2 + 1 + (c3 + 1 + (3 + 1 + (c5 + 1 + c6))))])
(((inputPrep (idx 0) (idx 9)).andThen fun _ =>
(inputPrep (idx 1) (idx 9)).andThen fun _ =>
(inputPrep (idx 2) (idx 9)).andThen fun _ =>
(prepTape (idx 4)).andThen fun _ =>
CP.andThen fun _ =>
guideSetup (idx 2) (idx 4) (idx 5)).startCfg T)).tape =
F6 := by
rw [k1.2, hIR, k2.2, hIR, k3.2, hIR, k4.2, hIR, k5.2, hIR, t6, hF6]
refine ⟨_, ?_, k1.1, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
· -- the cost
have hb5' := hb5
omega
· rw [hfin, hF6, Function.update_of_ne (hne 0 4 (by decide)),
Function.update_of_ne (hne 0 5 (by decide))]
exact e0.trans hF4i0
· rw [hfin, hF6, Function.update_of_ne (hne 1 4 (by decide)),
Function.update_of_ne (hne 1 5 (by decide))]
exact e1.trans hF4i1
· rw [hfin, hF6, Function.update_of_ne (hne 2 4 (by decide)),
Function.update_of_ne (hne 2 5 (by decide))]
exact e2.trans hF4i2
· rw [hfin, hF6, Function.update_of_ne (hne 3 4 (by decide)),
Function.update_of_ne (hne 3 5 (by decide))]
exact eclk
· rw [hfin, hF6, Function.update_self]
· rw [hfin, hF6, Function.update_of_ne (Ne.symm (hne 4 5 (by decide))),
Function.update_self]
· intro j hj
rw [hfin, hF6, Function.update_of_ne (hj 4), Function.update_of_ne (hj 5)]
exact hF5v j (hj 0) (hj 1) (hj 2) (hj 3) (hj 4) (hj 6) (hj 7) (hj 8)
end SipserGacsLautemann