sgl_casc_level
DefinitionDefinition code
import Definitions.Def_sgl_fold3_walk
import Definitions.Def_sgl_copy_back
/-!
# One cascade level
Advance the three output heads one cell — turning each frontier blank into
the rewind anchor — run the three-to-three fold, then rewind the outputs to
the start of their new runs. The level's outputs present exactly the shape
its inputs presented: a run of vote cells, blank-terminated, head on the
first cell. The inputs end at their frontiers, ready to serve as the next
level's outputs.
-/
namespace SipserGacsLautemann
variable {tapes : Nat}
/-- One cascade level, from inputs `i⋆` onto outputs `o⋆`. -/
noncomputable def cascLevel (f : Bool → Bool → Bool → Bool)
(i1 i2 i3 o1 o2 o3 : Fin tapes) :=
(moveUpTo o1 1 HeadMove.right).andThen fun _ =>
(moveUpTo o2 1 HeadMove.right).andThen fun _ =>
(moveUpTo o3 1 HeadMove.right).andThen fun _ =>
(fold3Walk f i1 i2 i3 o1 o2 o3).andThen fun _ =>
(rewindRun o1).andThen fun _ =>
(rewindRun o2).andThen fun _ =>
rewindRun o3
set_option maxHeartbeats 4000000 in
/-- **One level, on triple-length runs.** -/
theorem cascLevel_spec (f : Bool → Bool → Bool → Bool)
(i1 i2 i3 o1 o2 o3 : Fin tapes)
(hab : i1 ≠ i2) (hac : i1 ≠ i3) (hbc : i2 ≠ i3)
(h2ab : o1 ≠ o2) (h2ac : o1 ≠ o3) (h2bc : o2 ≠ o3)
(ha2a : o1 ≠ i1) (ha2b : o1 ≠ i2) (ha2c : o1 ≠ i3)
(hb2a : o2 ≠ i1) (hb2b : o2 ≠ i2) (hb2c : o2 ≠ i3)
(hc2a : o3 ≠ i1) (hc2b : o3 ≠ i2) (hc2c : o3 ≠ i3)
(t : Nat) (as bs cs : List TapeSymbol)
(hla : as.length = 3 * t) (hlb : bs.length = 3 * t)
(hlc : cs.length = 3 * t)
(hnba : ∀ x ∈ as, x ≠ TapeSymbol.blank)
(T : Fin tapes → Tape)
(Li1 Li2 Li3 Lo1 Lo2 Lo3 : List TapeSymbol)
(hi1 : T i1 = cellsTape Li1 (as ++ TapeSymbol.blank :: []))
(hi2 : T i2 = cellsTape Li2 (bs ++ TapeSymbol.blank :: []))
(hi3 : T i3 = cellsTape Li3 (cs ++ TapeSymbol.blank :: []))
(ho1 : T o1 = cellsTape Lo1 []) (ho2 : T o2 = cellsTape Lo2 [])
(ho3 : T o3 = cellsTape Lo3 []) :
∃ cost : Nat,
cost ≤ 27 * t + 30 ∧
HaltsExactly (cascLevel f i1 i2 i3 o1 o2 o3)
((cascLevel f i1 i2 i3 o1 o2 o3).startCfg T) cost true ∧
(((cascLevel f i1 i2 i3 o1 o2 o3).step^[cost])
((cascLevel f i1 i2 i3 o1 o2 o3).startCfg T)).tape i1 =
cellsTape (as.reverse ++ Li1) (TapeSymbol.blank :: []) ∧
(((cascLevel f i1 i2 i3 o1 o2 o3).step^[cost])
((cascLevel f i1 i2 i3 o1 o2 o3).startCfg T)).tape i2 =
cellsTape (bs.reverse ++ Li2) (TapeSymbol.blank :: []) ∧
(((cascLevel f i1 i2 i3 o1 o2 o3).step^[cost])
((cascLevel f i1 i2 i3 o1 o2 o3).startCfg T)).tape i3 =
cellsTape (cs.reverse ++ Li3) (TapeSymbol.blank :: []) ∧
(((cascLevel f i1 i2 i3 o1 o2 o3).step^[cost])
((cascLevel f i1 i2 i3 o1 o2 o3).startCfg T)).tape o1 =
cellsTape (TapeSymbol.blank :: Lo1)
(third0 (foldCells f as bs cs) ++ TapeSymbol.blank :: []) ∧
(((cascLevel f i1 i2 i3 o1 o2 o3).step^[cost])
((cascLevel f i1 i2 i3 o1 o2 o3).startCfg T)).tape o2 =
cellsTape (TapeSymbol.blank :: Lo2)
(third1 (foldCells f as bs cs) ++ TapeSymbol.blank :: []) ∧
(((cascLevel f i1 i2 i3 o1 o2 o3).step^[cost])
((cascLevel f i1 i2 i3 o1 o2 o3).startCfg T)).tape o3 =
cellsTape (TapeSymbol.blank :: Lo3)
(third2 (foldCells f as bs cs) ++ TapeSymbol.blank :: []) ∧
(∀ j, j ≠ i1 → j ≠ i2 → j ≠ i3 → j ≠ o1 → j ≠ o2 → j ≠ o3 →
(((cascLevel f i1 i2 i3 o1 o2 o3).step^[cost])
((cascLevel f i1 i2 i3 o1 o2 o3).startCfg T)).tape j = T j) := by
classical
-- stage 1-3: advance the outputs, creating the anchors
have g1 := moveUpTo_spec o1 1 HeadMove.right (by omega) T
have t1 := moveUpTo_tape o1 1 HeadMove.right (by omega) T
generalize hU1 : Function.update T o1
((moveDir HeadMove.right)^[1] (T o1)) = U1 at t1
have ho1' : U1 o1 = cellsTape (TapeSymbol.blank :: Lo1) [] := by
rw [← hU1, Function.update_self, Function.iterate_one, ho1,
cellsTape_moveRight_headD]
rfl
have g2 := moveUpTo_spec o2 1 HeadMove.right (by omega) U1
have t2 := moveUpTo_tape o2 1 HeadMove.right (by omega) U1
generalize hU2 : Function.update U1 o2
((moveDir HeadMove.right)^[1] (U1 o2)) = U2 at t2
have ho2' : U2 o2 = cellsTape (TapeSymbol.blank :: Lo2) [] := by
rw [← hU2, Function.update_self, Function.iterate_one, ← hU1,
Function.update_of_ne h2ab.symm, ho2, cellsTape_moveRight_headD]
rfl
have g3 := moveUpTo_spec o3 1 HeadMove.right (by omega) U2
have t3 := moveUpTo_tape o3 1 HeadMove.right (by omega) U2
generalize hU3 : Function.update U2 o3
((moveDir HeadMove.right)^[1] (U2 o3)) = U3 at t3
have ho3' : U3 o3 = cellsTape (TapeSymbol.blank :: Lo3) [] := by
rw [← hU3, Function.update_self, Function.iterate_one, ← hU2,
Function.update_of_ne h2bc.symm, ← hU1,
Function.update_of_ne h2ac.symm, ho3, cellsTape_moveRight_headD]
rfl
-- shapes at the fold's start
have hU3i1 : U3 i1 = cellsTape Li1 (as ++ TapeSymbol.blank :: []) := by
rw [← hU3, Function.update_of_ne hc2a.symm, ← hU2,
Function.update_of_ne hb2a.symm, ← hU1,
Function.update_of_ne ha2a.symm, hi1]
have hU3i2 : U3 i2 = cellsTape Li2 (bs ++ TapeSymbol.blank :: []) := by
rw [← hU3, Function.update_of_ne hc2b.symm, ← hU2,
Function.update_of_ne hb2b.symm, ← hU1,
Function.update_of_ne ha2b.symm, hi2]
have hU3i3 : U3 i3 = cellsTape Li3 (cs ++ TapeSymbol.blank :: []) := by
rw [← hU3, Function.update_of_ne hc2c.symm, ← hU2,
Function.update_of_ne hb2c.symm, ← hU1,
Function.update_of_ne ha2c.symm, hi3]
have hU3o1 : U3 o1 = cellsTape (TapeSymbol.blank :: Lo1) [] := by
rw [← hU3, Function.update_of_ne h2ac, ← hU2,
Function.update_of_ne h2ab]
exact ho1'
have hU3o2 : U3 o2 = cellsTape (TapeSymbol.blank :: Lo2) [] := by
rw [← hU3, Function.update_of_ne h2bc]
exact ho2'
have hU3o3 : U3 o3 = cellsTape (TapeSymbol.blank :: Lo3) [] :=
ho3'
-- stage 4: the fold
obtain ⟨hmk, hex⟩ := fold3_marks f i1 i2 i3 o1 o2 o3 hab hac hbc ha2a
ha2b ha2c hb2a hb2b hb2c hc2a hc2b hc2c as Li1 [] U3 hnba hU3i1
obtain ⟨g4, t4⟩ := fold3Walk_spec f i1 i2 i3 o1 o2 o3 hab hac hbc h2ab
h2ac h2bc ha2a ha2b ha2c hb2a hb2b hb2c hc2a hc2b hc2c as.length U3
hmk hex
obtain ⟨ka, kb, kc, ka2, kb2, kc2⟩ := fold3_iterate f i1 i2 i3 o1 o2 o3
hab hac hbc h2ab h2ac h2bc ha2a ha2b ha2c hb2a hb2b hb2c hc2a hc2b
hc2c t as bs cs U3 Li1 (TapeSymbol.blank :: []) Li2
(TapeSymbol.blank :: []) Li3 (TapeSymbol.blank :: [])
(TapeSymbol.blank :: Lo1) (TapeSymbol.blank :: Lo2)
(TapeSymbol.blank :: Lo3) hla hlb hlc hU3i1 hU3i2 hU3i3 hU3o1 hU3o2
hU3o3
rw [← hla] at ka kb kc ka2 kb2 kc2
generalize hA : ((fold3Step f i1 i2 i3 o1 o2 o3)^[as.length]) U3 = A
at ka kb kc ka2 kb2 kc2 t4
-- stage 5-7: rewind the outputs
have hnb0 : ∀ x ∈ third0 (foldCells f as bs cs), x ≠ TapeSymbol.blank :=
fun x hx => foldCells_nonblank f as bs cs x ((third_mem _ x).1 hx)
have hnb1 : ∀ x ∈ third1 (foldCells f as bs cs), x ≠ TapeSymbol.blank :=
fun x hx => foldCells_nonblank f as bs cs x ((third_mem _ x).2.1 hx)
have hnb2 : ∀ x ∈ third2 (foldCells f as bs cs), x ≠ TapeSymbol.blank :=
fun x hx => foldCells_nonblank f as bs cs x ((third_mem _ x).2.2 hx)
obtain ⟨g5, t5⟩ := rewindRun_spec o1 (third0 (foldCells f as bs cs))
Lo1 [] TapeSymbol.blank A hnb0 (by rw [ka2]; rfl)
generalize hV1 : Function.update A o1
(cellsTape (TapeSymbol.blank :: Lo1)
(third0 (foldCells f as bs cs) ++ TapeSymbol.blank :: [])) = V1
at t5
have hV1o2 : V1 o2 = A o2 := by
rw [← hV1, Function.update_of_ne h2ab.symm]
obtain ⟨g6, t6⟩ := rewindRun_spec o2 (third1 (foldCells f as bs cs))
Lo2 [] TapeSymbol.blank V1 hnb1 (by rw [hV1o2, kb2]; rfl)
generalize hV2 : Function.update V1 o2
(cellsTape (TapeSymbol.blank :: Lo2)
(third1 (foldCells f as bs cs) ++ TapeSymbol.blank :: [])) = V2
at t6
have hV2o3 : V2 o3 = A o3 := by
rw [← hV2, Function.update_of_ne h2bc.symm, ← hV1,
Function.update_of_ne h2ac.symm]
obtain ⟨g7, t7⟩ := rewindRun_spec o3 (third2 (foldCells f as bs cs))
Lo3 [] TapeSymbol.blank V2 hnb2 (by rw [hV2o3, kc2]; rfl)
generalize hV3 : Function.update V2 o3
(cellsTape (TapeSymbol.blank :: Lo3)
(third2 (foldCells f as bs cs) ++ TapeSymbol.blank :: [])) = V3
at t7
-- assemble
have ch67 := chainStepC g6 t6 g7
have ch57 := chainStepC g5 t5 ch67.1
have ch47 := chainStepC g4 t4 ch57.1
have ch37 := chainStepC g3 t3 ch47.1
have ch27 := chainStepC g2 t2 ch37.1
have ch17 := chainStepC g1 t1 ch27.1
-- the final tape function
have hlen0 := (third_lengths t (foldCells f as bs cs)
(by rw [foldCells_length]; exact hla)).1
have hlen1 := (third_lengths t (foldCells f as bs cs)
(by rw [foldCells_length]; exact hla)).2.1
have hlen2 := (third_lengths t (foldCells f as bs cs)
(by rw [foldCells_length]; exact hla)).2.2
have htp : (((cascLevel f i1 i2 i3 o1 o2 o3).step^[1 + 1 + (1 + 1 +
(1 + 1 + (as.length * 5 + 4 + 1 +
((third0 (foldCells f as bs cs)).length * 4 + 3 + 1 + 1 + 1 +
((third1 (foldCells f as bs cs)).length * 4 + 3 + 1 + 1 + 1 +
((third2 (foldCells f as bs cs)).length * 4 + 3 + 1 +
1))))))])
((cascLevel f i1 i2 i3 o1 o2 o3).startCfg T)).tape = V3 := by
unfold cascLevel
rw [ch17.2, ch27.2, ch37.2, ch47.2, ch57.2, ch67.2]
show (((rewindRun (tapes := tapes) o3).step^[
(third2 (foldCells f as bs cs)).length * 4 + 3 + 1 + 1])
((rewindRun (tapes := tapes) o3).startCfg V2)).tape = V3
rw [t7]
refine ⟨_, ?_, ch17.1, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
· rw [hlen0, hlen1, hlen2, hla]
omega
· rw [htp, ← hV3, Function.update_of_ne hc2a.symm, ← hV2,
Function.update_of_ne hb2a.symm, ← hV1,
Function.update_of_ne ha2a.symm, ka]
· rw [htp, ← hV3, Function.update_of_ne hc2b.symm, ← hV2,
Function.update_of_ne hb2b.symm, ← hV1,
Function.update_of_ne ha2b.symm, kb]
· rw [htp, ← hV3, Function.update_of_ne hc2c.symm, ← hV2,
Function.update_of_ne hb2c.symm, ← hV1,
Function.update_of_ne ha2c.symm, kc]
· rw [htp, ← hV3, Function.update_of_ne h2ac, ← hV2,
Function.update_of_ne h2ab, ← hV1, Function.update_self]
· rw [htp, ← hV3, Function.update_of_ne h2bc, ← hV2,
Function.update_self]
· rw [htp, ← hV3, Function.update_self]
· intro j hji1 hji2 hji3 hjo1 hjo2 hjo3
rw [htp, ← hV3, Function.update_of_ne hjo3, ← hV2,
Function.update_of_ne hjo2, ← hV1, Function.update_of_ne hjo1, ← hA,
fold3Step_other f i1 i2 i3 o1 o2 o3 as.length U3 j hji1 hji2 hji3
hjo1 hjo2 hjo3,
← hU3, Function.update_of_ne hjo3, ← hU2, Function.update_of_ne hjo2,
← hU1, Function.update_of_ne hjo1]
end SipserGacsLautemann