sgl_casc_loop
DefinitionDefinition code
import Definitions.Def_sgl_casc_level
import Definitions.Def_sgl_verifier_constructions
import Definitions.Def_sgl_left_loop
/-!
# The cascade loop
One depth mark per level: each round of the loop consumes a mark and runs
one cascade level, the direction chosen by which triple currently carries
votes. The two directions are the same machine with its tape arguments
swapped, so both branches of the dispatch share a state type and one level
lemma serves both.
The loop is analysed by peeling: a round that ends `true` restarts the
body, and a `HaltsExactly` run from the restarted configuration lifts to
one from the round's start. This avoids fixing per-round costs up front —
each level is cheaper than the last.
-/
namespace SipserGacsLautemann
variable {tapes : Nat} {S : Type}
/-- **Peel composition.** A `true` round followed by a halting run of the
loop is a halting run of the loop. -/
theorem repeatUntilFalse_shift (body : TypedMachine tapes S)
(c : TypedConfiguration tapes S) (a k : Nat) (v : Bool)
(hround : HaltsExactly body c a true)
(hrest : HaltsExactly body.repeatUntilFalse
⟨body.start, ((body.step^[a]) c).tape⟩ k v) :
HaltsExactly body.repeatUntilFalse c (a + 1 + k) v := by
have hpeel := body.repeatUntilFalse_round c a hround
constructor
· rw [show a + 1 + k = k + (a + 1) by omega, Function.iterate_add_apply,
hpeel]
exact hrest.halts
· intro j hj
rcases Nat.lt_or_ge j (a + 1) with hlt | hge
· exact body.repeatUntilFalse_round_fresh c a hround j hlt
· obtain ⟨t, ht⟩ := Nat.exists_eq_add_of_le hge
have htk : t < k := by omega
rw [ht, Nat.add_comm, Function.iterate_add_apply, hpeel]
exact hrest.fresh t htk
/-- The tape family after a peeled round, for reuse. -/
theorem repeatUntilFalse_shift_tape (body : TypedMachine tapes S)
(c : TypedConfiguration tapes S) (a k : Nat)
(hround : HaltsExactly body c a true) :
((body.repeatUntilFalse.step^[a + 1 + k]) c) =
((body.repeatUntilFalse.step^[k])
⟨body.start, ((body.step^[a]) c).tape⟩) := by
have hpeel := body.repeatUntilFalse_round c a hround
rw [show a + 1 + k = k + (a + 1) by omega, Function.iterate_add_apply,
hpeel]
/-- One level of vote combination. -/
def foldLevel (l : List TapeSymbol) : List TapeSymbol :=
foldCells (fun x y z => majorityVoteConstruction x y z)
(third0 l) (third1 l) (third2 l)
/-- The round body's inner machine: fold whichever triple carries votes
onto the other. -/
noncomputable def cascInner (A1 A2 A3 B1 B2 B3 : Fin tapes) :=
(TypedMachine.test (notBlankAt A1)).andThen fun v =>
if v then
cascLevel (fun x y z => majorityVoteConstruction x y z)
A1 A2 A3 B1 B2 B3
else
cascLevel (fun x y z => majorityVoteConstruction x y z)
B1 B2 B3 A1 A2 A3
/-- The loop body: consume one depth mark, then run one level. -/
noncomputable def cascBody (dt A1 A2 A3 B1 B2 B3 : Fin tapes) :=
leftBody dt (cascInner A1 A2 A3 B1 B2 B3)
/-- The cascade loop. -/
noncomputable def cascLoop (dt A1 A2 A3 B1 B2 B3 : Fin tapes) :=
(cascBody dt A1 A2 A3 B1 B2 B3).repeatUntilFalse
/-- The loop invariant: `rounds` depth marks remain, one triple carries the
level's votes rewound to their runs' starts, the other waits at its
frontier. -/
def CascInv (dt A1 A2 A3 B1 B2 B3 : Fin tapes) (rounds : Nat)
(lvl : List TapeSymbol) (par : Bool) (T : Fin tapes → Tape) : Prop :=
(∃ Ld Rd, T dt = cellsTape
(List.replicate rounds (TapeSymbol.bit true) ++
TapeSymbol.blank :: Ld) Rd) ∧
(∀ x ∈ lvl, x ≠ TapeSymbol.blank) ∧
lvl.length = 3 ^ (rounds + 1) ∧
(if par then
((∃ L1, T A1 = cellsTape L1 (third0 lvl ++ TapeSymbol.blank :: [])) ∧
(∃ L2, T A2 = cellsTape L2 (third1 lvl ++ TapeSymbol.blank :: [])) ∧
(∃ L3, T A3 = cellsTape L3 (third2 lvl ++ TapeSymbol.blank :: [])) ∧
(∃ M1, T B1 = cellsTape M1 []) ∧
(∃ M2, T B2 = cellsTape M2 []) ∧
(∃ M3, T B3 = cellsTape M3 []))
else
((∃ L1, T B1 = cellsTape L1 (third0 lvl ++ TapeSymbol.blank :: [])) ∧
(∃ L2, T B2 = cellsTape L2 (third1 lvl ++ TapeSymbol.blank :: [])) ∧
(∃ L3, T B3 = cellsTape L3 (third2 lvl ++ TapeSymbol.blank :: [])) ∧
(∃ M1, T A1 = cellsTape M1 []) ∧
(∃ M2, T A2 = cellsTape M2 []) ∧
(∃ M3, T A3 = cellsTape M3 []))) ∧
(∀ x ∈ foldLevel lvl, x ≠ TapeSymbol.blank) ∧
(foldLevel lvl).length = 3 ^ (rounds + 0)
/-- A run of positive length starts with a non-blank head. -/
theorem run_head_nonblank (l : List TapeSymbol) (R : List TapeSymbol)
(L : List TapeSymbol) (hne : l ≠ [])
(hnb : ∀ x ∈ l, x ≠ TapeSymbol.blank) :
(cellsTape L (l ++ TapeSymbol.blank :: R)).head ≠ TapeSymbol.blank := by
cases l with
| nil => exact absurd rfl hne
| cons a l' =>
show ((a :: l' ++ TapeSymbol.blank :: R).headD TapeSymbol.blank) ≠
TapeSymbol.blank
exact hnb a (by simp)
set_option maxHeartbeats 4000000 in
/-- **One round.** With at least one depth mark left, the body consumes it,
folds the live triple onto the waiting one, and re-establishes the
invariant one level down with the roles swapped. -/
theorem cascRound (dt A1 A2 A3 B1 B2 B3 : Fin tapes)
(hd1 : dt ≠ A1) (hd2 : dt ≠ A2) (hd3 : dt ≠ A3)
(hd4 : dt ≠ B1) (hd5 : dt ≠ B2) (hd6 : dt ≠ B3)
(hA12 : A1 ≠ A2) (hA13 : A1 ≠ A3) (hA23 : A2 ≠ A3)
(hB12 : B1 ≠ B2) (hB13 : B1 ≠ B3) (hB23 : B2 ≠ B3)
(hAB11 : A1 ≠ B1) (hAB12 : A1 ≠ B2) (hAB13 : A1 ≠ B3)
(hAB21 : A2 ≠ B1) (hAB22 : A2 ≠ B2) (hAB23 : A2 ≠ B3)
(hAB31 : A3 ≠ B1) (hAB32 : A3 ≠ B2) (hAB33 : A3 ≠ B3)
(rounds : Nat) (lvl : List TapeSymbol) (par : Bool)
(T : Fin tapes → Tape)
(hInv : CascInv dt A1 A2 A3 B1 B2 B3 (rounds + 1) lvl par T) :
∃ cb : Nat,
cb ≤ 27 * 3 ^ rounds + 40 ∧
HaltsExactly (cascBody dt A1 A2 A3 B1 B2 B3)
((cascBody dt A1 A2 A3 B1 B2 B3).startCfg T) cb true ∧
CascInv dt A1 A2 A3 B1 B2 B3 rounds (foldLevel lvl) (!par)
((((cascBody dt A1 A2 A3 B1 B2 B3).step^[cb])
((cascBody dt A1 A2 A3 B1 B2 B3).startCfg T)).tape) := by
classical
obtain ⟨⟨Ld, Rd, hdt⟩, hnb, hlen, hpar, hnbF, hlenF⟩ := hInv
-- the tape family after the depth-mark consumption
set T1 := Function.update T dt (moveDir HeadMove.left (T dt)) with hT1
have hT1dt : T1 dt = cellsTape
(List.replicate rounds (TapeSymbol.bit true) ++
TapeSymbol.blank :: Ld)
(TapeSymbol.bit true ::
(Rd.headD TapeSymbol.blank :: Rd.tail)) := by
rw [hT1, Function.update_self, hdt]
rw [show List.replicate (rounds + 1) (TapeSymbol.bit true) =
TapeSymbol.bit true :: List.replicate rounds (TapeSymbol.bit true)
from rfl]
rw [cellsTape_moveLeft_headD]
rfl
have hmark : (T1 dt).head ≠ TapeSymbol.blank := by
rw [hT1dt]
show (TapeSymbol.bit true ::
(Rd.headD TapeSymbol.blank :: Rd.tail)).headD TapeSymbol.blank ≠
TapeSymbol.blank
simp
-- lengths of the level thirds
have hlvl3 : lvl.length = 3 * 3 ^ (rounds + 1) := by
rw [hlen]
ring
obtain ⟨hth0, hth1, hth2⟩ := third_lengths (3 ^ (rounds + 1)) lvl hlvl3
have hth0len3 : (third0 lvl).length = 3 * 3 ^ rounds := by
rw [hth0]
ring
have hth1len3 : (third1 lvl).length = 3 * 3 ^ rounds := by
rw [hth1]
ring
have hth2len3 : (third2 lvl).length = 3 * 3 ^ rounds := by
rw [hth2]
ring
have hnb0 : ∀ x ∈ third0 lvl, x ≠ TapeSymbol.blank :=
fun x hx => hnb x ((third_mem lvl x).1 hx)
have hth0ne : third0 lvl ≠ [] := by
intro h
rw [h] at hth0
simp at hth0
have hpos : 0 < 3 ^ (rounds + 1) := Nat.pow_pos (by omega)
omega
-- the two directions share everything but the branch
cases par with
| true =>
obtain ⟨⟨L1, hA1⟩, ⟨L2, hA2⟩, ⟨L3, hA3⟩, ⟨M1, hB1⟩, ⟨M2, hB2⟩,
⟨M3, hB3⟩⟩ := hpar
have hT1A1 : T1 A1 = cellsTape L1
(third0 lvl ++ TapeSymbol.blank :: []) := by
rw [hT1, Function.update_of_ne hd1.symm, hA1]
have hT1A2 : T1 A2 = cellsTape L2
(third1 lvl ++ TapeSymbol.blank :: []) := by
rw [hT1, Function.update_of_ne hd2.symm, hA2]
have hT1A3 : T1 A3 = cellsTape L3
(third2 lvl ++ TapeSymbol.blank :: []) := by
rw [hT1, Function.update_of_ne hd3.symm, hA3]
have hT1B1 : T1 B1 = cellsTape M1 [] := by
rw [hT1, Function.update_of_ne hd4.symm, hB1]
have hT1B2 : T1 B2 = cellsTape M2 [] := by
rw [hT1, Function.update_of_ne hd5.symm, hB2]
have hT1B3 : T1 B3 = cellsTape M3 [] := by
rw [hT1, Function.update_of_ne hd6.symm, hB3]
-- the level, live triple A onto B
obtain ⟨clev, hclevb, glev, ki1, ki2, ki3, ko1, ko2, ko3, koth⟩ :=
cascLevel_spec (fun x y z => majorityVoteConstruction x y z)
A1 A2 A3 B1 B2 B3 hA12 hA13 hA23 hB12 hB13 hB23
hAB11.symm hAB21.symm hAB31.symm
hAB12.symm hAB22.symm hAB32.symm
hAB13.symm hAB23.symm hAB33.symm
(3 ^ rounds) (third0 lvl) (third1 lvl) (third2 lvl)
hth0len3 hth1len3 hth2len3 hnb0 T1 L1 L2 L3 M1 M2 M3
hT1A1 hT1A2 hT1A3 hT1B1 hT1B2 hT1B3
-- the dispatch: the test reads a vote, so the `true` branch runs
have htest := TypedMachine.test_spec (notBlankAt A1) T1
have htmark : (T1 A1).head ≠ TapeSymbol.blank := by
rw [hT1A1]
exact run_head_nonblank (third0 lvl) [] L1 hth0ne hnb0
rw [notBlankAt_true A1 T1 htmark] at htest
have htestt : (((TypedMachine.test (notBlankAt A1)).step^[1])
((TypedMachine.test (notBlankAt A1)).startCfg T1)).tape = T1 := by
rw [Function.iterate_one]
funext j
simp [TypedMachine.step, TypedMachine.test, TypedMachine.startCfg,
Tape.write_head_self, Tape.move]
have hinner := chainStepD
(M₂ := fun v =>
if v then
cascLevel (fun x y z => majorityVoteConstruction x y z)
A1 A2 A3 B1 B2 B3
else
cascLevel (fun x y z => majorityVoteConstruction x y z)
B1 B2 B3 A1 A2 A3)
htest htestt (by simpa using glev)
-- the body round
obtain ⟨gbody, tbody⟩ := leftBody_mark dt
(cascInner A1 A2 A3 B1 B2 B3) T
((((cascLevel (fun x y z => majorityVoteConstruction x y z)
A1 A2 A3 B1 B2 B3).step^[clev])
((cascLevel (fun x y z => majorityVoteConstruction x y z)
A1 A2 A3 B1 B2 B3).startCfg T1)).tape)
(1 + 1 + clev) hmark (by rw [← hT1]; exact hinner.1)
(by
rw [← hT1]
have h2 := hinner.2
unfold cascInner
rw [h2]
rfl)
refine ⟨_, ?_, gbody, ?_⟩
· have := hclevb
omega
· unfold cascBody
rw [tbody]
refine ⟨⟨Ld, TapeSymbol.bit true ::
(Rd.headD TapeSymbol.blank :: Rd.tail), ?_⟩, hnbF,
(by simpa using hlenF), ?_, ?_, ?_⟩
· rw [koth dt hd1 hd2 hd3 hd4 hd5 hd6, hT1dt]
· show if (!true) = true then _ else _
simp only [Bool.not_true, if_neg (by decide : ¬false = true)]
refine ⟨⟨TapeSymbol.blank :: M1, ?_⟩, ⟨TapeSymbol.blank :: M2, ?_⟩,
⟨TapeSymbol.blank :: M3, ?_⟩, ⟨(third0 lvl).reverse ++ L1, ?_⟩,
⟨(third1 lvl).reverse ++ L2, ?_⟩,
⟨(third2 lvl).reverse ++ L3, ?_⟩⟩
· rw [ko1]
rfl
· rw [ko2]
rfl
· rw [ko3]
rfl
· rw [ki1]
rfl
· rw [ki2]
rfl
· rw [ki3]
rfl
· intro x hx
exact foldCells_nonblank _ _ _ _ x hx
· have h3 : (foldLevel lvl).length = 3 * 3 ^ rounds := by
rw [show (foldLevel lvl).length = (third0 lvl).length from
foldCells_length _ _ _ _]
exact hth0len3
obtain ⟨g0, _, _⟩ := third_lengths (3 ^ rounds) (foldLevel lvl) h3
rw [show (foldLevel (foldLevel lvl)).length =
(third0 (foldLevel lvl)).length from foldCells_length _ _ _ _]
simpa using g0
| false =>
obtain ⟨⟨L1, hB1⟩, ⟨L2, hB2⟩, ⟨L3, hB3⟩, ⟨M1, hA1⟩, ⟨M2, hA2⟩,
⟨M3, hA3⟩⟩ := hpar
have hT1B1 : T1 B1 = cellsTape L1
(third0 lvl ++ TapeSymbol.blank :: []) := by
rw [hT1, Function.update_of_ne hd4.symm, hB1]
have hT1B2 : T1 B2 = cellsTape L2
(third1 lvl ++ TapeSymbol.blank :: []) := by
rw [hT1, Function.update_of_ne hd5.symm, hB2]
have hT1B3 : T1 B3 = cellsTape L3
(third2 lvl ++ TapeSymbol.blank :: []) := by
rw [hT1, Function.update_of_ne hd6.symm, hB3]
have hT1A1 : T1 A1 = cellsTape M1 [] := by
rw [hT1, Function.update_of_ne hd1.symm, hA1]
have hT1A2 : T1 A2 = cellsTape M2 [] := by
rw [hT1, Function.update_of_ne hd2.symm, hA2]
have hT1A3 : T1 A3 = cellsTape M3 [] := by
rw [hT1, Function.update_of_ne hd3.symm, hA3]
obtain ⟨clev, hclevb, glev, ki1, ki2, ki3, ko1, ko2, ko3, koth⟩ :=
cascLevel_spec (fun x y z => majorityVoteConstruction x y z)
B1 B2 B3 A1 A2 A3 hB12 hB13 hB23 hA12 hA13 hA23
hAB11 hAB12 hAB13 hAB21 hAB22 hAB23 hAB31 hAB32 hAB33
(3 ^ rounds) (third0 lvl) (third1 lvl) (third2 lvl)
hth0len3 hth1len3 hth2len3 hnb0 T1 L1 L2 L3 M1 M2 M3
hT1B1 hT1B2 hT1B3 hT1A1 hT1A2 hT1A3
have htest := TypedMachine.test_spec (notBlankAt A1) T1
have htblank : (T1 A1).head = TapeSymbol.blank := by
rw [hT1A1]
rfl
rw [notBlankAt_false A1 T1 htblank] at htest
have htestt : (((TypedMachine.test (notBlankAt A1)).step^[1])
((TypedMachine.test (notBlankAt A1)).startCfg T1)).tape = T1 := by
rw [Function.iterate_one]
funext j
simp [TypedMachine.step, TypedMachine.test, TypedMachine.startCfg,
Tape.write_head_self, Tape.move]
have hinner := chainStepD
(M₂ := fun v =>
if v then
cascLevel (fun x y z => majorityVoteConstruction x y z)
A1 A2 A3 B1 B2 B3
else
cascLevel (fun x y z => majorityVoteConstruction x y z)
B1 B2 B3 A1 A2 A3)
htest htestt (by simpa using glev)
obtain ⟨gbody, tbody⟩ := leftBody_mark dt
(cascInner A1 A2 A3 B1 B2 B3) T
((((cascLevel (fun x y z => majorityVoteConstruction x y z)
B1 B2 B3 A1 A2 A3).step^[clev])
((cascLevel (fun x y z => majorityVoteConstruction x y z)
B1 B2 B3 A1 A2 A3).startCfg T1)).tape)
(1 + 1 + clev) hmark (by rw [← hT1]; exact hinner.1)
(by
rw [← hT1]
have h2 := hinner.2
unfold cascInner
rw [h2]
rfl)
refine ⟨_, ?_, gbody, ?_⟩
· have := hclevb
omega
· unfold cascBody
rw [tbody]
refine ⟨⟨Ld, TapeSymbol.bit true ::
(Rd.headD TapeSymbol.blank :: Rd.tail), ?_⟩, hnbF,
(by simpa using hlenF), ?_, ?_, ?_⟩
· rw [koth dt hd4 hd5 hd6 hd1 hd2 hd3, hT1dt]
· show if (!false) = true then _ else _
simp only [Bool.not_false, if_pos rfl]
refine ⟨⟨TapeSymbol.blank :: M1, ?_⟩, ⟨TapeSymbol.blank :: M2, ?_⟩,
⟨TapeSymbol.blank :: M3, ?_⟩, ⟨(third0 lvl).reverse ++ L1, ?_⟩,
⟨(third1 lvl).reverse ++ L2, ?_⟩,
⟨(third2 lvl).reverse ++ L3, ?_⟩⟩
· rw [ko1]
rfl
· rw [ko2]
rfl
· rw [ko3]
rfl
· rw [ki1]
rfl
· rw [ki2]
rfl
· rw [ki3]
rfl
· intro x hx
exact foldCells_nonblank _ _ _ _ x hx
· have h3 : (foldLevel lvl).length = 3 * 3 ^ rounds := by
rw [show (foldLevel lvl).length = (third0 lvl).length from
foldCells_length _ _ _ _]
exact hth0len3
obtain ⟨g0, _, _⟩ := third_lengths (3 ^ rounds) (foldLevel lvl) h3
rw [show (foldLevel (foldLevel lvl)).length =
(third0 (foldLevel lvl)).length from foldCells_length _ _ _ _]
simpa using g0
/-- Which triple is live after `r` more levels. -/
def parAfter (r : Nat) (p : Bool) : Bool :=
if r % 2 = 0 then p else !p
theorem parAfter_succ (r : Nat) (p : Bool) :
parAfter (r + 1) p = parAfter r (!p) := by
unfold parAfter
by_cases h : r % 2 = 0
· rw [if_pos h, if_neg (by omega)]
· rw [if_neg h, if_pos (by omega), Bool.not_not]
set_option maxHeartbeats 4000000 in
/-- **The cascade loop runs to the bottom.** From the invariant with
`rounds` marks, the loop halts `false`, having folded `rounds` levels; the
final level list — three votes — sits on the triple the parity names. -/
theorem cascLoop_run (dt A1 A2 A3 B1 B2 B3 : Fin tapes)
(hd1 : dt ≠ A1) (hd2 : dt ≠ A2) (hd3 : dt ≠ A3)
(hd4 : dt ≠ B1) (hd5 : dt ≠ B2) (hd6 : dt ≠ B3)
(hA12 : A1 ≠ A2) (hA13 : A1 ≠ A3) (hA23 : A2 ≠ A3)
(hB12 : B1 ≠ B2) (hB13 : B1 ≠ B3) (hB23 : B2 ≠ B3)
(hAB11 : A1 ≠ B1) (hAB12 : A1 ≠ B2) (hAB13 : A1 ≠ B3)
(hAB21 : A2 ≠ B1) (hAB22 : A2 ≠ B2) (hAB23 : A2 ≠ B3)
(hAB31 : A3 ≠ B1) (hAB32 : A3 ≠ B2) (hAB33 : A3 ≠ B3) :
∀ (rounds : Nat) (lvl : List TapeSymbol) (par : Bool)
(T : Fin tapes → Tape),
CascInv dt A1 A2 A3 B1 B2 B3 rounds lvl par T →
∃ cost : Nat,
cost ≤ 14 * 3 ^ (rounds + 1) + 50 * (rounds + 1) ∧
HaltsExactly (cascLoop dt A1 A2 A3 B1 B2 B3)
((cascLoop dt A1 A2 A3 B1 B2 B3).startCfg T) cost false ∧
(if parAfter rounds par then
((∃ L1, (((cascLoop dt A1 A2 A3 B1 B2 B3).step^[cost])
((cascLoop dt A1 A2 A3 B1 B2 B3).startCfg T)).tape A1 =
cellsTape L1 (third0 (foldLevel^[rounds] lvl) ++
TapeSymbol.blank :: [])) ∧
(∃ L2, (((cascLoop dt A1 A2 A3 B1 B2 B3).step^[cost])
((cascLoop dt A1 A2 A3 B1 B2 B3).startCfg T)).tape A2 =
cellsTape L2 (third1 (foldLevel^[rounds] lvl) ++
TapeSymbol.blank :: [])) ∧
(∃ L3, (((cascLoop dt A1 A2 A3 B1 B2 B3).step^[cost])
((cascLoop dt A1 A2 A3 B1 B2 B3).startCfg T)).tape A3 =
cellsTape L3 (third2 (foldLevel^[rounds] lvl) ++
TapeSymbol.blank :: [])) ∧
(∃ M1, (((cascLoop dt A1 A2 A3 B1 B2 B3).step^[cost])
((cascLoop dt A1 A2 A3 B1 B2 B3).startCfg T)).tape B1 =
cellsTape M1 []) ∧
(∃ M2, (((cascLoop dt A1 A2 A3 B1 B2 B3).step^[cost])
((cascLoop dt A1 A2 A3 B1 B2 B3).startCfg T)).tape B2 =
cellsTape M2 []) ∧
(∃ M3, (((cascLoop dt A1 A2 A3 B1 B2 B3).step^[cost])
((cascLoop dt A1 A2 A3 B1 B2 B3).startCfg T)).tape B3 =
cellsTape M3 []))
else
((∃ L1, (((cascLoop dt A1 A2 A3 B1 B2 B3).step^[cost])
((cascLoop dt A1 A2 A3 B1 B2 B3).startCfg T)).tape B1 =
cellsTape L1 (third0 (foldLevel^[rounds] lvl) ++
TapeSymbol.blank :: [])) ∧
(∃ L2, (((cascLoop dt A1 A2 A3 B1 B2 B3).step^[cost])
((cascLoop dt A1 A2 A3 B1 B2 B3).startCfg T)).tape B2 =
cellsTape L2 (third1 (foldLevel^[rounds] lvl) ++
TapeSymbol.blank :: [])) ∧
(∃ L3, (((cascLoop dt A1 A2 A3 B1 B2 B3).step^[cost])
((cascLoop dt A1 A2 A3 B1 B2 B3).startCfg T)).tape B3 =
cellsTape L3 (third2 (foldLevel^[rounds] lvl) ++
TapeSymbol.blank :: [])) ∧
(∃ M1, (((cascLoop dt A1 A2 A3 B1 B2 B3).step^[cost])
((cascLoop dt A1 A2 A3 B1 B2 B3).startCfg T)).tape A1 =
cellsTape M1 []) ∧
(∃ M2, (((cascLoop dt A1 A2 A3 B1 B2 B3).step^[cost])
((cascLoop dt A1 A2 A3 B1 B2 B3).startCfg T)).tape A2 =
cellsTape M2 []) ∧
(∃ M3, (((cascLoop dt A1 A2 A3 B1 B2 B3).step^[cost])
((cascLoop dt A1 A2 A3 B1 B2 B3).startCfg T)).tape A3 =
cellsTape M3 []))) ∧
(∀ x ∈ foldLevel^[rounds] lvl, x ≠ TapeSymbol.blank) ∧
(foldLevel^[rounds] lvl).length = 3 ^ 1 := by
intro rounds
induction rounds with
| zero =>
intro lvl par T hInv
obtain ⟨⟨Ld, Rd, hdt⟩, hnb, hlen, hpar, hnbF, hlenF⟩ := hInv
have hblank : ((Function.update T dt
(moveDir HeadMove.left (T dt))) dt).head = TapeSymbol.blank := by
rw [Function.update_self, hdt]
rw [show List.replicate 0 (TapeSymbol.bit true) ++
TapeSymbol.blank :: Ld = TapeSymbol.blank :: Ld from rfl]
rw [cellsTape_moveLeft_headD]
rfl
obtain ⟨gexit, texit⟩ := leftBody_blank dt
(cascInner A1 A2 A3 B1 B2 B3) T hblank
have hloop : HaltsExactly (cascLoop dt A1 A2 A3 B1 B2 B3)
((cascLoop dt A1 A2 A3 B1 B2 B3).startCfg T)
(1 + 1 + (1 + 1 + (0 + 1 + 0))) false := by
constructor
· show (cascLoop dt A1 A2 A3 B1 B2 B3).result
(((leftBody dt (cascInner A1 A2 A3 B1 B2
B3)).repeatUntilFalse.step^[1 + 1 + (1 + 1 + (0 + 1 + 0))])
((leftBody dt (cascInner A1 A2 A3 B1 B2
B3)).startCfg T)).state = some false
exact ((leftBody dt (cascInner A1 A2 A3 B1 B2
B3)).repeatUntilFalse_exit _ _ gexit)
· intro j hj
show (cascLoop dt A1 A2 A3 B1 B2 B3).result
(((leftBody dt (cascInner A1 A2 A3 B1 B2
B3)).repeatUntilFalse.step^[j])
((leftBody dt (cascInner A1 A2 A3 B1 B2
B3)).startCfg T)).state = none
exact TypedMachine.repeatUntilFalse_pre_fresh _ _ _ _ gexit j hj
have htape : (((cascLoop dt A1 A2 A3 B1 B2 B3).step^[
1 + 1 + (1 + 1 + (0 + 1 + 0))])
((cascLoop dt A1 A2 A3 B1 B2 B3).startCfg T)).tape =
Function.update T dt (moveDir HeadMove.left (T dt)) := by
show (((leftBody dt (cascInner A1 A2 A3 B1 B2
B3)).repeatUntilFalse.step^[1 + 1 + (1 + 1 + (0 + 1 + 0))])
((leftBody dt (cascInner A1 A2 A3 B1 B2 B3)).startCfg T)).tape =
Function.update T dt (moveDir HeadMove.left (T dt))
rw [TypedMachine.repeatUntilFalse_iterate_fresh _ _ _ gexit.fresh]
exact texit
refine ⟨1 + 1 + (1 + 1 + (0 + 1 + 0)), by omega, hloop, ?_, hnb,
(by simpa using hlen)⟩
rw [htape]
show if parAfter 0 par then _ else _
rw [show parAfter 0 par = par from rfl]
cases par with
| true =>
obtain ⟨⟨L1, hA1⟩, ⟨L2, hA2⟩, ⟨L3, hA3⟩, ⟨M1, hB1⟩, ⟨M2, hB2⟩,
⟨M3, hB3⟩⟩ := hpar
simp only [if_pos rfl, Function.iterate_zero_apply]
exact ⟨⟨L1, by rw [Function.update_of_ne hd1.symm]; exact hA1⟩,
⟨L2, by rw [Function.update_of_ne hd2.symm]; exact hA2⟩,
⟨L3, by rw [Function.update_of_ne hd3.symm]; exact hA3⟩,
⟨M1, by rw [Function.update_of_ne hd4.symm]; exact hB1⟩,
⟨M2, by rw [Function.update_of_ne hd5.symm]; exact hB2⟩,
⟨M3, by rw [Function.update_of_ne hd6.symm]; exact hB3⟩⟩
| false =>
obtain ⟨⟨L1, hB1⟩, ⟨L2, hB2⟩, ⟨L3, hB3⟩, ⟨M1, hA1⟩, ⟨M2, hA2⟩,
⟨M3, hA3⟩⟩ := hpar
simp only [if_neg (by decide : ¬false = true),
Function.iterate_zero_apply]
exact ⟨⟨L1, by rw [Function.update_of_ne hd4.symm]; exact hB1⟩,
⟨L2, by rw [Function.update_of_ne hd5.symm]; exact hB2⟩,
⟨L3, by rw [Function.update_of_ne hd6.symm]; exact hB3⟩,
⟨M1, by rw [Function.update_of_ne hd1.symm]; exact hA1⟩,
⟨M2, by rw [Function.update_of_ne hd2.symm]; exact hA2⟩,
⟨M3, by rw [Function.update_of_ne hd3.symm]; exact hA3⟩⟩
| succ rounds ih =>
intro lvl par T hInv
obtain ⟨cb, hcb, ground, hInv'⟩ := cascRound dt A1 A2 A3 B1 B2 B3
hd1 hd2 hd3 hd4 hd5 hd6 hA12 hA13 hA23 hB12 hB13 hB23 hAB11 hAB12
hAB13 hAB21 hAB22 hAB23 hAB31 hAB32 hAB33 rounds lvl par T hInv
obtain ⟨cost', hcost', hrest, hfacts, hnb', hlen'⟩ := ih
(foldLevel lvl) (!par)
((((cascBody dt A1 A2 A3 B1 B2 B3).step^[cb])
((cascBody dt A1 A2 A3 B1 B2 B3).startCfg T)).tape) hInv'
have hshift := repeatUntilFalse_shift
(cascBody dt A1 A2 A3 B1 B2 B3)
((cascLoop dt A1 A2 A3 B1 B2 B3).startCfg T) cb cost' false
ground hrest
have hshiftt : (((cascLoop dt A1 A2 A3 B1 B2 B3).step^[
cb + 1 + cost'])
((cascLoop dt A1 A2 A3 B1 B2 B3).startCfg T)) =
(((cascLoop dt A1 A2 A3 B1 B2 B3).step^[cost'])
((cascLoop dt A1 A2 A3 B1 B2 B3).startCfg
((((cascBody dt A1 A2 A3 B1 B2 B3).step^[cb])
((cascBody dt A1 A2 A3 B1 B2 B3).startCfg T)).tape))) :=
repeatUntilFalse_shift_tape
(cascBody dt A1 A2 A3 B1 B2 B3)
((cascLoop dt A1 A2 A3 B1 B2 B3).startCfg T) cb cost' ground
refine ⟨cb + 1 + cost', ?_, hshift, ?_, ?_, ?_⟩
· have h1 : (3:Nat) ^ (rounds + 2) = 9 * 3 ^ rounds := by ring
have h2 : (3:Nat) ^ (rounds + 1) = 3 * 3 ^ rounds := by ring
omega
· rw [show (parAfter (rounds + 1) par) = parAfter rounds (!par) from
parAfter_succ rounds par]
rw [show foldLevel^[rounds + 1] lvl =
foldLevel^[rounds] (foldLevel lvl) from
Function.iterate_succ_apply foldLevel rounds lvl]
show if parAfter rounds (!par) then _ else _
cases hp : parAfter rounds (!par) with
| true =>
rw [hp] at hfacts
simp only [if_pos rfl] at hfacts ⊢
obtain ⟨⟨L1, k1⟩, ⟨L2, k2⟩, ⟨L3, k3⟩, ⟨M1, m1⟩, ⟨M2, m2⟩,
⟨M3, m3⟩⟩ := hfacts
exact ⟨⟨L1, by rw [hshiftt]; exact k1⟩,
⟨L2, by rw [hshiftt]; exact k2⟩,
⟨L3, by rw [hshiftt]; exact k3⟩,
⟨M1, by rw [hshiftt]; exact m1⟩,
⟨M2, by rw [hshiftt]; exact m2⟩,
⟨M3, by rw [hshiftt]; exact m3⟩⟩
| false =>
rw [hp] at hfacts
simp only [if_neg (by decide : ¬false = true)] at hfacts ⊢
obtain ⟨⟨L1, k1⟩, ⟨L2, k2⟩, ⟨L3, k3⟩, ⟨M1, m1⟩, ⟨M2, m2⟩,
⟨M3, m3⟩⟩ := hfacts
exact ⟨⟨L1, by rw [hshiftt]; exact k1⟩,
⟨L2, by rw [hshiftt]; exact k2⟩,
⟨L3, by rw [hshiftt]; exact k3⟩,
⟨M1, by rw [hshiftt]; exact m1⟩,
⟨M2, by rw [hshiftt]; exact m2⟩,
⟨M3, by rw [hshiftt]; exact m3⟩⟩
· rw [show foldLevel^[rounds + 1] lvl =
foldLevel^[rounds] (foldLevel lvl) from
Function.iterate_succ_apply foldLevel rounds lvl]
exact hnb'
· rw [show foldLevel^[rounds + 1] lvl =
foldLevel^[rounds] (foldLevel lvl) from
Function.iterate_succ_apply foldLevel rounds lvl]
exact hlen'
end SipserGacsLautemann