sgl_capped_adv
DefinitionDefinition code
import Definitions.Def_sgl_left_loop
/-!
# The capped advance
Move the source head forward by `min i n · n`, where `i` arrives in unary on
its own tape and `n` is the length of the ruler's run. The minimum is taken
by the simultaneous walk, whose consumed marks the left loop then walks back,
paying one full ruler-guided advance per mark.
-/
namespace SipserGacsLautemann
variable {tapes : Nat}
/-- The simultaneous walk's left contexts, made explicit — the marks it
consumed are what the left loop walks back over. -/
theorem simulStep_iterate_left (a b : Fin tapes) (hab : a ≠ b) :
∀ (r : Nat) (T : Fin tapes → Tape) (La Ra Lb Rb : List TapeSymbol),
r ≤ Ra.length → r ≤ Rb.length →
T a = cellsTape La Ra → T b = cellsTape Lb Rb →
(((simulStep a b)^[r]) T) a =
cellsTape ((Ra.take r).reverse ++ La) (Ra.drop r) ∧
(((simulStep a b)^[r]) T) b =
cellsTape ((Rb.take r).reverse ++ Lb) (Rb.drop r) := by
intro r
induction r with
| zero =>
intro T La Ra Lb Rb _ _ ha hb
exact ⟨by simpa using ha, by simpa using hb⟩
| succ r ih =>
intro T La Ra Lb Rb hra hrb ha hb
cases Ra with
| nil => simp at hra
| cons ca Ra' =>
cases Rb with
| nil => simp at hrb
| cons cb Rb' =>
rw [Function.iterate_succ_apply]
obtain ⟨ha', hb'⟩ := simulStep_tapes a b hab T La (ca :: Ra')
Lb (cb :: Rb') ha hb
obtain ⟨hA, hB⟩ := ih (simulStep a b T) (ca :: La) Ra'
(cb :: Lb) Rb' (by simpa using hra) (by simpa using hrb)
(by simpa using ha') (by simpa using hb')
refine ⟨?_, ?_⟩
· rw [hA]
congr 1
simp
· rw [hB]
congr 1
simp
/-- The advance: take the minimum, restore the ruler — a rewind, since the
consumed prefix is one non-blank run — then one ruler-guided advance of the
source per consumed mark. -/
noncomputable def cappedAdvance (idx ruler src : Fin tapes) :=
(simulWalk idx ruler).andThen fun _ =>
(rewindRun ruler).andThen fun _ =>
leftLoop idx
((guidedWalk ruler src HeadMove.right none).andThen fun _ =>
rewindRun ruler)
/-! ## The inner advance, in the loop's contract shape -/
/-- The per-round effect: the guide's leftward step absorbed, the source
advanced one ruler-length. -/
def advEffect (idx ruler src : Fin tapes) (n : Nat)
(U : Fin tapes → Tape) : Fin tapes → Tape :=
Function.update
(Function.update U idx (moveDir HeadMove.left (U idx)))
src ((moveDir HeadMove.right)^[n] (U src))
set_option maxHeartbeats 4000000 in
/-- **One round's body.** On the stepped tape the ruler-guided advance runs
and the ruler is restored. -/
theorem innerAdv_spec (idx ruler src : Fin tapes)
(hir : idx ≠ ruler) (his : idx ≠ src) (hrs : ruler ≠ src)
(rcells Lr Rr : List TapeSymbol)
(hnb : ∀ c ∈ rcells, c ≠ TapeSymbol.blank)
(U : Fin tapes → Tape)
(hruler : U ruler = cellsTape (TapeSymbol.blank :: Lr)
(rcells ++ TapeSymbol.blank :: Rr)) :
HaltsExactly
((guidedWalk ruler src HeadMove.right none).andThen fun _ =>
rewindRun ruler)
(((guidedWalk ruler src HeadMove.right none).andThen fun _ =>
rewindRun ruler).startCfg
(Function.update U idx (moveDir HeadMove.left (U idx))))
(rcells.length * 5 + 4 + 1 + (rcells.length * 4 + 3 + 1 + 1)) true ∧
((((guidedWalk ruler src HeadMove.right none).andThen fun _ =>
rewindRun ruler).step^[
rcells.length * 5 + 4 + 1 + (rcells.length * 4 + 3 + 1 + 1)])
(((guidedWalk ruler src HeadMove.right none).andThen fun _ =>
rewindRun ruler).startCfg
(Function.update U idx (moveDir HeadMove.left (U idx))))).tape =
advEffect idx ruler src rcells.length U := by
classical
set U1 := Function.update U idx (moveDir HeadMove.left (U idx)) with hU1
have hU1r : U1 ruler = cellsTape (TapeSymbol.blank :: Lr)
(rcells ++ TapeSymbol.blank :: Rr) := by
rw [hU1, Function.update_of_ne (Ne.symm hir)]
exact hruler
obtain ⟨h1a, h1b⟩ := guidedStep_skip_iterate ruler src hrs rcells U1
(TapeSymbol.blank :: Lr) (TapeSymbol.blank :: Rr) (by rw [hU1r])
obtain ⟨hW, hWt⟩ := guidedWalk_spec ruler src hrs HeadMove.right none
rcells.length U1
(guidedStep_skip_marks ruler src hrs rcells U1
(TapeSymbol.blank :: Lr) (TapeSymbol.blank :: Rr) hnb (by rw [hU1r]))
(by rw [h1a]; rfl)
set U2 := ((guidedStep ruler src HeadMove.right none)^[rcells.length]) U1
with hU2
have hU2r : U2 ruler = cellsTape (rcells.reverse ++ TapeSymbol.blank :: Lr)
(TapeSymbol.blank :: Rr) := h1a
obtain ⟨hR, hRt⟩ := rewindRun_spec ruler rcells Lr Rr TapeSymbol.blank U2
hnb (by rw [hU2r])
have hch := chainStepC hW hWt hR
refine ⟨hch.1, ?_⟩
have hfin : (((guidedWalk ruler src HeadMove.right none).andThen fun _ =>
rewindRun ruler).step^[_])
(((guidedWalk ruler src HeadMove.right none).andThen fun _ =>
rewindRun ruler).startCfg U1) = _ := hch.2
rw [hfin]
have hIR : ∀ {S₁ S₂ : Type} (bb : Bool) (c : TypedConfiguration tapes S₂),
(TypedConfiguration.inRight (S₁ := S₁) bb c).tape = c.tape :=
fun _ _ => rfl
rw [hIR, hRt]
funext j
by_cases hj : j = ruler
· rw [hj, Function.update_self]
show cellsTape (TapeSymbol.blank :: Lr)
(rcells ++ TapeSymbol.blank :: Rr) = advEffect idx ruler src
rcells.length U ruler
rw [advEffect, Function.update_of_ne hrs,
Function.update_of_ne (Ne.symm hir)]
exact hruler.symm
· rw [Function.update_of_ne hj]
by_cases hj2 : j = src
· rw [hj2]
show U2 src = advEffect idx ruler src rcells.length U src
rw [h1b, advEffect, Function.update_self, hU1]
rw [Function.update_of_ne (Ne.symm his)]
· show U2 j = advEffect idx ruler src rcells.length U j
rw [hU2,
guidedStep_other ruler src HeadMove.right none rcells.length U1 j hj
hj2, advEffect, Function.update_of_ne hj2]
/-- The round effect, iterated: the source accumulates, the ruler stands
still, the guide steps left once a round, and everything else is untouched. -/
theorem advEffect_iterate (idx ruler src : Fin tapes)
(hir : idx ≠ ruler) (his : idx ≠ src) (hrs : ruler ≠ src) (n : Nat) :
∀ (k : Nat) (U : Fin tapes → Tape),
((advEffect idx ruler src n)^[k] U) src =
((moveDir HeadMove.right)^[k * n]) (U src) ∧
((advEffect idx ruler src n)^[k] U) ruler = U ruler ∧
((advEffect idx ruler src n)^[k] U) idx =
((moveDir HeadMove.left)^[k]) (U idx) ∧
(∀ j, j ≠ idx → j ≠ ruler → j ≠ src →
((advEffect idx ruler src n)^[k] U) j = U j) := by
intro k
induction k with
| zero => intro U; exact ⟨by simp, rfl, rfl, fun _ _ _ _ => rfl⟩
| succ k ih =>
intro U
rw [Function.iterate_succ_apply]
obtain ⟨hs, hr, hi, ho⟩ := ih (advEffect idx ruler src n U)
have hstep_src : (advEffect idx ruler src n U) src =
((moveDir HeadMove.right)^[n]) (U src) := by
rw [advEffect, Function.update_self]
have hstep_ruler : (advEffect idx ruler src n U) ruler = U ruler := by
rw [advEffect, Function.update_of_ne hrs,
Function.update_of_ne (Ne.symm hir)]
have hstep_idx : (advEffect idx ruler src n U) idx =
moveDir HeadMove.left (U idx) := by
rw [advEffect, Function.update_of_ne his, Function.update_self]
refine ⟨?_, ?_, ?_, ?_⟩
· rw [hs, hstep_src, ← Function.iterate_add_apply]
congr 1
ring
· rw [hr, hstep_ruler]
· rw [hi, hstep_idx]
exact (Function.iterate_succ_apply (moveDir HeadMove.left) k
(U idx)).symm
· intro j hji hjr hjs
rw [ho j hji hjr hjs]
show (Function.update (Function.update U idx
(moveDir HeadMove.left (U idx))) src _) j = U j
rw [Function.update_of_ne hjs, Function.update_of_ne hji]
/-- Crossing a run leftward: the run's cells return to the right context in
their original order, and the head lands on the blank below the run. -/
theorem moveLeft_cross_run (cs : List TapeSymbol) :
∀ (L R' : List TapeSymbol) (r : TapeSymbol),
((moveDir HeadMove.left)^[cs.length])
(cellsTape (cs.reverse ++ TapeSymbol.blank :: L) (r :: R')) =
cellsTape (TapeSymbol.blank :: L) (cs ++ r :: R') := by
induction cs using List.reverseRecOn with
| nil => intro L R' r; simp
| append_singleton cs' c ih =>
intro L R' r
have hlen : (cs' ++ [c]).length = cs'.length + 1 := by simp
rw [hlen, Function.iterate_succ_apply]
have hrev : (cs' ++ [c]).reverse ++ TapeSymbol.blank :: L =
c :: (cs'.reverse ++ TapeSymbol.blank :: L) := by simp
have hstep : moveDir HeadMove.left
(cellsTape ((cs' ++ [c]).reverse ++ TapeSymbol.blank :: L)
(r :: R')) =
cellsTape (cs'.reverse ++ TapeSymbol.blank :: L)
(c :: r :: R') := by
rw [hrev, cellsTape_moveLeft_headD]
rfl
rw [hstep]
have := ih L (r :: R') c
rw [this]
simp
set_option maxHeartbeats 4000000 in
/-- **The capped advance.** The source moves `min i n · n` cells right, the
ruler is restored exactly, the index tape ends parked on its origin blank,
and nothing else moves. -/
theorem cappedAdvance_spec (idx ruler src : Fin tapes)
(hir : idx ≠ ruler) (his : idx ≠ src) (hrs : ruler ≠ src)
(i : Nat) (rcells Li Ri Lr Rr : List TapeSymbol)
(hnbr : ∀ c ∈ rcells, c ≠ TapeSymbol.blank)
(T : Fin tapes → Tape)
(hidx : T idx = cellsTape (TapeSymbol.blank :: Li)
(List.replicate i (TapeSymbol.bit true) ++ TapeSymbol.blank :: Ri))
(hruler : T ruler = cellsTape (TapeSymbol.blank :: Lr)
(rcells ++ TapeSymbol.blank :: Rr)) :
∃ cost : Nat,
cost ≤ (min i rcells.length) * (9 * rcells.length + 25) + 16 ∧
HaltsExactly (cappedAdvance idx ruler src)
((cappedAdvance idx ruler src).startCfg T) cost false ∧
(∃ X : List TapeSymbol,
(((cappedAdvance idx ruler src).step^[cost])
((cappedAdvance idx ruler src).startCfg T)).tape idx =
cellsTape Li (TapeSymbol.blank :: X)) ∧
(((cappedAdvance idx ruler src).step^[cost])
((cappedAdvance idx ruler src).startCfg T)).tape ruler =
cellsTape (TapeSymbol.blank :: Lr) (rcells ++ TapeSymbol.blank :: Rr) ∧
(((cappedAdvance idx ruler src).step^[cost])
((cappedAdvance idx ruler src).startCfg T)).tape src =
((moveDir HeadMove.right)^[(min i rcells.length) * rcells.length])
(T src) ∧
(∀ j, j ≠ idx → j ≠ ruler → j ≠ src →
(((cappedAdvance idx ruler src).step^[cost])
((cappedAdvance idx ruler src).startCfg T)).tape j = T j) := by
classical
set m := min i rcells.length with hm
set n := rcells.length with hn
have hmi : m ≤ i := Nat.min_le_left _ _
have hmn : m ≤ n := Nat.min_le_right _ _
have hnbi : ∀ c ∈ List.replicate i (TapeSymbol.bit true),
c ≠ TapeSymbol.blank := by
intro c hc
rw [List.eq_of_mem_replicate hc]
simp
-- stage 1: the simultaneous walk
obtain ⟨g1, s1⟩ := simulWalk_spec idx ruler hir
(List.replicate i (TapeSymbol.bit true)) rcells
(TapeSymbol.blank :: Li) Ri (TapeSymbol.blank :: Lr) Rr T hnbi hnbr
hidx hruler
rw [show (List.replicate i (TapeSymbol.bit true)).length = i from
List.length_replicate] at g1 s1
rw [← hn, ← hm] at g1 s1
set T1 := ((simulStep idx ruler)^[m]) T with hT1
-- stage 2: values after the walk
obtain ⟨hI1, hR1⟩ := simulStep_iterate_left idx ruler hir m T
(TapeSymbol.blank :: Li)
(List.replicate i (TapeSymbol.bit true) ++ TapeSymbol.blank :: Ri)
(TapeSymbol.blank :: Lr) (rcells ++ TapeSymbol.blank :: Rr)
(by simp; omega) (by simp; omega) hidx hruler
have htakeI : (List.replicate i (TapeSymbol.bit true) ++
TapeSymbol.blank :: Ri).take m =
List.replicate m (TapeSymbol.bit true) := by
rw [List.take_append_of_le_length (by simp; omega), List.take_replicate]
congr 1
omega
have hdropI : (List.replicate i (TapeSymbol.bit true) ++
TapeSymbol.blank :: Ri).drop m =
List.replicate (i - m) (TapeSymbol.bit true) ++
TapeSymbol.blank :: Ri := by
rw [List.drop_append_of_le_length (by simp; omega), List.drop_replicate]
have htakeR : (rcells ++ TapeSymbol.blank :: Rr).take m = rcells.take m :=
List.take_append_of_le_length (by omega)
have hdropR : (rcells ++ TapeSymbol.blank :: Rr).drop m =
rcells.drop m ++ TapeSymbol.blank :: Rr :=
List.drop_append_of_le_length (by omega)
rw [htakeI, hdropI] at hI1
rw [htakeR, hdropR] at hR1
-- stage 3: restore the ruler
have hnbTake : ∀ c ∈ rcells.take m, c ≠ TapeSymbol.blank := by
intro c hc
exact hnbr c (List.mem_of_mem_take hc)
have hconsD : rcells.drop m ++ TapeSymbol.blank :: Rr =
(rcells.drop m ++ TapeSymbol.blank :: Rr).headD TapeSymbol.blank ::
(rcells.drop m ++ TapeSymbol.blank :: Rr).tail := by
cases hD : rcells.drop m with
| nil => simp
| cons c rest => simp
obtain ⟨g2, s2⟩ := rewindRun_spec ruler (rcells.take m) Lr
((rcells.drop m ++ TapeSymbol.blank :: Rr).tail)
((rcells.drop m ++ TapeSymbol.blank :: Rr).headD TapeSymbol.blank) T1
hnbTake (by
show ((simulStep idx ruler)^[m]) T ruler = _
rw [hR1, ← hconsD])
set D := rcells.drop m ++ TapeSymbol.blank :: Rr with hD
set T2 := Function.update T1 ruler
(cellsTape (TapeSymbol.blank :: Lr)
(rcells.take m ++ D.headD TapeSymbol.blank :: D.tail)) with hT2
have hT2r : T2 ruler = cellsTape (TapeSymbol.blank :: Lr)
(rcells ++ TapeSymbol.blank :: Rr) := by
rw [hT2, Function.update_self, ← hconsD, hD, ← List.append_assoc,
List.take_append_drop]
-- stage 4: the left loop
set Inv : (Fin tapes → Tape) → Prop :=
fun U => U ruler = cellsTape (TapeSymbol.blank :: Lr)
(rcells ++ TapeSymbol.blank :: Rr) with hInv
set f := advEffect idx ruler src n with hf
set cb := n * 5 + 4 + 1 + (n * 4 + 3 + 1 + 1) with hcb
have hbodyC : ∀ U, Inv U →
HaltsExactly ((guidedWalk ruler src HeadMove.right none).andThen fun _ =>
rewindRun ruler)
(((guidedWalk ruler src HeadMove.right none).andThen fun _ =>
rewindRun ruler).startCfg
(Function.update U idx (moveDir HeadMove.left (U idx)))) cb true ∧
((((guidedWalk ruler src HeadMove.right none).andThen fun _ =>
rewindRun ruler).step^[cb])
(((guidedWalk ruler src HeadMove.right none).andThen fun _ =>
rewindRun ruler).startCfg
(Function.update U idx (moveDir HeadMove.left (U idx))))).tape =
f U := by
intro U hU
have := innerAdv_spec idx ruler src hir his hrs rcells Lr Rr hnbr U hU
rw [← hn] at this
exact this
have hpresC : ∀ U, Inv U → Inv (f U) := by
intro U hU
show (f U) ruler = _
rw [hf, advEffect, Function.update_of_ne hrs,
Function.update_of_ne (Ne.symm hir)]
exact hU
have hfgC : ∀ U, Inv U → (f U) idx =
(Function.update U idx (moveDir HeadMove.left (U idx))) idx := by
intro U _
rw [hf, advEffect, Function.update_of_ne his, Function.update_self]
have hT2idx : T2 idx = cellsTape
(List.replicate m (TapeSymbol.bit true) ++ TapeSymbol.blank :: Li)
(List.replicate (i - m) (TapeSymbol.bit true) ++
TapeSymbol.blank :: Ri) := by
rw [hT2, Function.update_of_ne hir]
show ((simulStep idx ruler)^[m]) T idx = _
rw [hI1, List.reverse_replicate]
obtain ⟨g3, s3⟩ := leftLoop_spec_inv idx
((guidedWalk ruler src HeadMove.right none).andThen fun _ =>
rewindRun ruler) Inv f cb hbodyC hpresC hfgC m Li
(List.replicate (i - m) (TapeSymbol.bit true) ++ TapeSymbol.blank :: Ri)
T2 hT2r hT2idx
-- the chain
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
-- stage 5: final values
obtain ⟨hFsrc, hFruler, hFidx, hFoth⟩ :=
advEffect_iterate idx ruler src hir his hrs n m T2
have hT2src : T2 src = T src := by
rw [hT2, Function.update_of_ne (Ne.symm hrs)]
show ((simulStep idx ruler)^[m]) T src = T src
exact simulStep_other idx ruler m T src (Ne.symm his) (Ne.symm hrs)
have hT2oth : ∀ j, j ≠ idx → j ≠ ruler → j ≠ src → T2 j = T j := by
intro j hji hjr hjs
rw [hT2, Function.update_of_ne hjr]
exact simulStep_other idx ruler m T j hji hjr
set F := ((f^[m]) T2) with hF
set FIN := Function.update F idx (moveDir HeadMove.left (F idx)) with hFIN
have hfin : (((cappedAdvance idx ruler src).step^[
m * 5 + 4 + 1 + ((List.take m rcells).length * 4 + 3 + 1 + 1 + 1 +
(m * (1 + 1 + (1 + 1 + (cb + 1 + 0)) + 1) +
(1 + 1 + (1 + 1 + (0 + 1 + 0)))))])
((cappedAdvance idx ruler src).startCfg T)).tape = FIN := by
have hk : ((cappedAdvance idx ruler src).step^[
m * 5 + 4 + 1 + ((List.take m rcells).length * 4 + 3 + 1 + 1 + 1 +
(m * (1 + 1 + (1 + 1 + (cb + 1 + 0)) + 1) +
(1 + 1 + (1 + 1 + (0 + 1 + 0)))))])
((cappedAdvance idx ruler src).startCfg T) = _ := k1.2
rw [hk, hIR, k2.2, hIR]
exact s3
refine ⟨_, ?_, k1.1, ?_, ?_, ?_, ?_⟩
· have hlen : (List.take m rcells).length = m := by
rw [List.length_take]
omega
rw [hlen]
have heq : m * 5 + 4 + 1 + (m * 4 + 3 + 1 + 1 + 1 +
(m * (1 + 1 + (1 + 1 + (cb + 1 + 0)) + 1) +
(1 + 1 + (1 + 1 + (0 + 1 + 0))))) = m * (9 * n + 25) + 16 := by
rw [hcb]
ring
rw [heq]
· -- idx parked on its origin blank
have hconsR : List.replicate (i - m) (TapeSymbol.bit true) ++
TapeSymbol.blank :: Ri =
(List.replicate (i - m) (TapeSymbol.bit true) ++
TapeSymbol.blank :: Ri).headD TapeSymbol.blank ::
(List.replicate (i - m) (TapeSymbol.bit true) ++
TapeSymbol.blank :: Ri).tail := by
cases hcase : List.replicate (i - m) (TapeSymbol.bit true) with
| nil => simp
| cons c rest => simp
exact ⟨_, by
rw [hfin, hFIN, Function.update_self]
show moveDir HeadMove.left (F idx) = _
rw [hFidx, hT2idx, hconsR]
have hcross := moveLeft_cross_run
(List.replicate m (TapeSymbol.bit true)) Li
((List.replicate (i - m) (TapeSymbol.bit true) ++
TapeSymbol.blank :: Ri).tail)
((List.replicate (i - m) (TapeSymbol.bit true) ++
TapeSymbol.blank :: Ri).headD TapeSymbol.blank)
rw [List.length_replicate, List.reverse_replicate] at hcross
rw [hcross, cellsTape_moveLeft_headD]
rfl⟩
· -- the ruler restored
rw [hfin, hFIN, Function.update_of_ne (Ne.symm hir)]
show F ruler = _
rw [hFruler]
exact hT2r
· -- the source advanced
rw [hfin, hFIN, Function.update_of_ne (Ne.symm his)]
show F src = _
rw [hFsrc, hT2src]
· -- everything else
intro j hji hjr hjs
rw [hfin, hFIN, Function.update_of_ne hji]
show F j = _
rw [hFoth j hji hjr hjs]
exact hT2oth j hji hjr hjs
end SipserGacsLautemann