Proof internals for simulating CSLib machines on Complexitylib machines

Folding lemmas for the simulator Complexity.FromMultiTape.toTM: the cell layout of a folded two-way tape, and the head moves of the three phases of a simulated step.

def Complexity.FromMultiTape.enc (c : Option Bool) : Γ

Our symbol storing a binary CSLib cell.

Equations

• Complexity.FromMultiTape.enc c = (Complexity.Γw.ofCell c).toΓ

def Complexity.FromMultiTape.fold (z : ℤ) : ℕ

Our cell holding CSLib cell z of a folded tape: 2 z + 1 for z ≥ 0 and -2 z for z < 0.

Equations

• Complexity.FromMultiTape.fold z = if 0 ≤ z then 2 * z.toNat + 1 else 2 * (-z).toNat

theorem Complexity.FromMultiTape.one_le_fold (z : ℤ) : 1 ≤ fold z

Folded cells are never the left-end cell.

theorem Complexity.FromMultiTape.fold_injective : Function.Injective fold

Folding is injective.

theorem Complexity.FromMultiTape.exists_fold_eq {n : ℕ} (hn : 1 ≤ n) : ∃ (z : ℤ), fold z = n

Every cell past the left end is a folded cell.

@[simp]

theorem Complexity.FromMultiTape.enc_ne_start (c : Option Bool) : enc c ≠ Γ.start

Encoded cells are never ▷.

@[simp]

theorem Complexity.FromMultiTape.toCell_enc (c : Option Bool) : (enc c).toCell = c

Decoding an encoded cell recovers it.

@[simp]

theorem Complexity.FromMultiTape.keep_enc (c : Option Bool) : (enc c).keep = Γw.ofCell c

Rewriting an encoded cell stores it again.

theorem Complexity.FromMultiTape.keep_toΓ {r : Γ} (h : r ≠ Γ.start) : r.keep.toΓ = r

Rewriting a symbol other than ▷ leaves it unchanged.

theorem Complexity.FromMultiTape.write_keep {t : Tape} (hC : ∀ (n : ℕ), t.cells n = Γ.start ↔ n = 0) : t.write t.read.keep.toΓ = t

On a tape whose only ▷ is cell 0, rewriting the symbol under the head changes nothing.

structure Complexity.FromMultiTape.FoldRel (t : Tape) (f : ℤ → Option Bool) (z : ℤ) (s : Bool) : Prop

A folded tape simulating the CSLib tape f with head at z; the sign flag s records whether z is negative.

• head : t.head = fold z

  The head is on the folded cell of z.

• sign : s = decide (z < 0)

  The sign flag says whether z is negative.

• start : t.cells 0 = Γ.start

  Cell 0 holds ▷.

• cells (y : ℤ) : t.cells (fold y) = enc (f y)

  Every folded cell stores its CSLib cell.

theorem Complexity.FromMultiTape.FoldRel.start_iff {t : Tape} {f : ℤ → Option Bool} {z : ℤ} {s : Bool} (h : FoldRel t f z s) (n : ℕ) : t.cells n = Γ.start ↔ n = 0

On a folded tape, ▷ sits exactly at cell 0.

theorem Complexity.FromMultiTape.FoldRel.read {t : Tape} {f : ℤ → Option Bool} {z : ℤ} {s : Bool} (h : FoldRel t f z s) : t.read = enc (f z)

A folded tape reads the CSLib symbol under the CSLib head.

theorem Complexity.FromMultiTape.FoldRel.write {t : Tape} {f : ℤ → Option Bool} {z : ℤ} {s : Bool} (h : FoldRel t f z s) (c : Option Bool) : FoldRel (t.write (Γw.ofCell c).toΓ) (Function.update f z c) z s

Writing the encoding of c on a folded tape simulates CSLib's write.

@[simp]

theorem Complexity.FromMultiTape.move_left_head (u : Tape) : (u.move Dir3.left).head = u.head - 1

A left move decrements the head.

@[simp]

theorem Complexity.FromMultiTape.move_right_head (u : Tape) : (u.move Dir3.right).head = u.head + 1

A right move increments the head.

@[simp]

theorem Complexity.FromMultiTape.move_stay (u : Tape) : u.move Dir3.stay = u

Staying keeps the head.

theorem Complexity.FromMultiTape.fold_moves {t : Tape} (hC : ∀ (n : ℕ), t.cells n = Γ.start ↔ n = 0) {z : ℤ} (hh : t.head = fold z) (m : SignType) : have s := decide (z < 0); have t1 := t.move (Dir3.guard t.read (plan0 s m).2); have r1 := plan1 (plan0 s m).1 s t1.read; have t2 := t1.move (Dir3.guard t1.read r1.2.2); have r2 := plan2 r1.1 r1.2.1 t2.read; have t3 := t2.move (Dir3.guard t2.read r2.2); t3.head = fold (z + ↑m) ∧ (r2.1 = true ↔ z + ↑m < 0)

The head moves of phases 0, 1 and 2 on a folded tape whose only ▷ is cell 0 carry the head from the folded cell of z to that of z + m, and update the sign flag.

def Complexity.FromMultiTape.applyWr (f : ℤ → Option Bool) (z : ℤ) : Option (Option Bool) → ℤ → Option Bool

The CSLib tape after the write wr.

Equations

• Complexity.FromMultiTape.applyWr f z none = f
• Complexity.FromMultiTape.applyWr f z (some c) = Function.update f z c

theorem Complexity.FromMultiTape.FoldRel.writePhase {t : Tape} {f : ℤ → Option Bool} {z : ℤ} {s : Bool} (h : FoldRel t f z s) (wr : Option (Option Bool)) : FoldRel (t.write (writeSym t.read wr).toΓ) (applyWr f z wr) z s

The phase-0 write on a folded tape simulates CSLib's write.

theorem Complexity.FromMultiTape.FoldRel.move_start_iff {t : Tape} {f : ℤ → Option Bool} {z : ℤ} {s : Bool} (h : FoldRel t f z s) (d : Dir3) (n : ℕ) : (t.move d).cells n = Γ.start ↔ n = 0

A moved tape keeps its cells.

theorem Complexity.FromMultiTape.FoldRel.phases {t : Tape} {f : ℤ → Option Bool} {z : ℤ} {s : Bool} (h : FoldRel t f z s) (wr : Option (Option Bool)) (m : SignType) : have t1 := t.writeAndMove (writeSym t.read wr).toΓ (Dir3.guard t.read (plan0 s m).2); have r1 := plan1 (plan0 s m).1 s t1.read; have t2 := t1.writeAndMove t1.read.keep.toΓ (Dir3.guard t1.read r1.2.2); have r2 := plan2 r1.1 r1.2.1 t2.read; have t3 := t2.writeAndMove t2.read.keep.toΓ (Dir3.guard t2.read r2.2); FoldRel t3 (applyWr f z wr) (z + ↑m) r2.1

One simulated step on a folded work tape. Phases 0, 1 and 2 carry a folded tape simulating CSLib tape f with head z to one simulating the CSLib tape after the write wr and the move m.

theorem Complexity.FromMultiTape.moveInputPos_val {m : ℕ} (p : Fin (m + 2)) (s : SignType) : ↑(Turing.moveInputPos p s) = min (↑↑p + ↑s).toNat (m + 1)

The position reached by a CSLib input-head move.

theorem Complexity.FromMultiTape.input_start_iff (x : List Bool) (i : ℕ) : (Tape.init (List.map Γ.ofBool x)).cells i = Γ.start ↔ i = 0

The input tape holds ▷ exactly at cell 0.

theorem Complexity.FromMultiTape.input_blank_iff (x : List Bool) (i : ℕ) : (Tape.init (List.map Γ.ofBool x)).cells (i + 1) = Γ.blank ↔ x.length ≤ i

Past ▷, the input tape is blank exactly after the input.

theorem Complexity.FromMultiTape.input_toCell {k : ℕ} {S : Type} {x : List Bool} (d : Turing.Cfg k Bool S x) : ((Tape.init (List.map Γ.ofBool x)).cells ↑d.inputPos).toCell = d.inputSymbol

The symbol under our input head decodes to CSLib's input symbol.

theorem Complexity.FromMultiTape.input_phases {x : List Bool} {t : Tape} (hc : t.cells = (Tape.init (List.map Γ.ofBool x)).cells) (p : Fin (x.length + 2)) (hp : t.head = ↑p) (m : SignType) : have t1 := t.move (Dir3.guard t.read Dir3.stay); have t2 := t1.move (Dir3.guard t1.read Dir3.stay); have t3 := t2.move (Dir3.guard t2.read (inputPlan t.read m)); t3.cells = t.cells ∧ t3.head = ↑(Turing.moveInputPos p m)

One simulated step on the input tape. Phases 0, 1 and 2 move our input head from CSLib's input position p to the position reached by CSLib's clamped move m.

structure Complexity.FromMultiTape.OutRel (t : Tape) (out : List Bool) : Prop

Our output tape holds the CSLib output out after ▷, with the head just past it.

• head : t.head = out.length + 1

  The head is just past the output.

• start_iff (n : ℕ) : t.cells n = Γ.start ↔ n = 0

  ▷ sits exactly at cell 0.

• cells (i : ℕ) (h : i < out.length) : t.cells (i + 1) = Γ.ofBool out[i]

  Cells 1, …, |out| hold the output.

theorem Complexity.FromMultiTape.idle_phase {t : Tape} (hC : ∀ (n : ℕ), t.cells n = Γ.start ↔ n = 0) (hh : t.head ≠ 0) : t.writeAndMove t.read.keep.toΓ (Dir3.guard t.read Dir3.stay) = t

A tape whose only ▷ is cell 0, with its head off cell 0, stays put in the idle phases.

theorem Complexity.FromMultiTape.OutRel.phase0 {t : Tape} {out : List Bool} (h : OutRel t out) (e : Option Bool) : OutRel (t.writeAndMove (outSym t.read e).toΓ (Dir3.guard t.read (outDir e))) (out ++ e.toList)

One simulated step on the output tape. Phase 0 appends the emitted bit e; phases 1 and 2 leave the tape alone.

theorem Complexity.FromMultiTape.toTM_step {k : ℕ} {S : Type} [DecidableEq S] [Fintype S] (M : Turing.MultiTapeTM k Bool S) (c : Cfg k (St k S)) (h : c.state ≠ St.halt) : (toTM M).step c = some { state := (δ M c.state c.input.read (fun (i : Fin k) => (c.work i).read) c.output.read).1, input := c.input.move (δ M c.state c.input.read (fun (i : Fin k) => (c.work i).read) c.output.read).2.2.2.1, work := fun (i : Fin k) => (c.work i).writeAndMove ((δ M c.state c.input.read (fun (i : Fin k) => (c.work i).read) c.output.read).2.1 i).toΓ ((δ M c.state c.input.read (fun (i : Fin k) => (c.work i).read) c.output.read).2.2.2.2.1 i), output := c.output.writeAndMove (δ M c.state c.input.read (fun (i : Fin k) => (c.work i).read) c.output.read).2.2.1.toΓ (δ M c.state c.input.read (fun (i : Fin k) => (c.work i).read) c.output.read).2.2.2.2.2 }

One step of the simulator from a configuration that has not halted.

structure Complexity.FromMultiTape.Sim {k : ℕ} {S : Type} (x : List Bool) (c : Cfg k (St k S)) (d : Turing.Cfg k Bool S x) : Prop

The simulation relation between our configuration c and a CSLib configuration d on input x, at the start of a simulated step.

• input_head : c.input.head = ↑d.inputPos

  The input head is on CSLib's input position.

• input_cells : c.input.cells = (Tape.init (List.map Γ.ofBool x)).cells

  The input tape is untouched.

• work (j : Fin k) : FoldRel (c.work j) (d.workTapes j) (d.workTapePos j) (decide (d.workTapePos j < 0))

  Each work tape folds its CSLib work tape.

• output : OutRel c.output d.output

  The output tape holds CSLib's output.

theorem Complexity.FromMultiTape.Sim.input_read {k : ℕ} {S : Type} {x : List Bool} {c : Cfg k (St k S)} {d : Turing.Cfg k Bool S x} (h : Sim x c d) : c.input.read.toCell = d.inputSymbol

Under the simulation relation, our input head reads CSLib's input symbol.

theorem Complexity.FromMultiTape.Sim.work_read {k : ℕ} {S : Type} {x : List Bool} {c : Cfg k (St k S)} {d : Turing.Cfg k Bool S x} (h : Sim x c d) : (fun (j : Fin k) => (c.work j).read.toCell) = d.workTapeSymbols

Under the simulation relation, our work heads read CSLib's work symbols.

theorem Complexity.FromMultiTape.cslib_step_eq {k : ℕ} {S : Type} (M : Turing.MultiTapeTM k Bool S) {x : List Bool} {d : Turing.Cfg k Bool S x} {q : S} (h : d.state = some q) : Turing.MultiTapeTM.step d = { state := (M.tr q d.inputSymbol d.workTapeSymbols).state, inputPos := Turing.moveInputPos d.inputPos (M.tr q d.inputSymbol d.workTapeSymbols).inputTape, workTapes := fun (i : Fin k) => applyWr (d.workTapes i) (d.workTapePos i) ((M.tr q d.inputSymbol d.workTapeSymbols).workTapes i).1, workTapePos := fun (i : Fin k) => d.workTapePos i + ↑((M.tr q d.inputSymbol d.workTapeSymbols).workTapes i).2, output := d.output ++ (M.tr q d.inputSymbol d.workTapeSymbols).output.toList }

One CSLib step from a running configuration, field by field.

theorem Complexity.FromMultiTape.Sim.step_run {k : ℕ} {S : Type} [DecidableEq S] [Fintype S] {M : Turing.MultiTapeTM k Bool S} {x : List Bool} {c : Cfg k (St k S)} {d : Turing.Cfg k Bool S x} (h : Sim x c d) {q q' : S} (hq : d.state = some q) (hc : c.state = St.run q fun (j : Fin k) => decide (d.workTapePos j < 0)) (hq' : (M.tr q d.inputSymbol d.workTapeSymbols).state = some q') : ∃ (c' : Cfg k (toTM M).Q), (toTM M).reachesIn 3 c c' ∧ Sim x c' (Turing.MultiTapeTM.step d) ∧ c'.state = St.run q' fun (j : Fin k) => decide ((Turing.MultiTapeTM.step d).workTapePos j < 0)

One simulated step. From the simulation relation at a CSLib step that does not halt, three steps of the simulator restore the relation.

theorem Complexity.FromMultiTape.Sim.step_halt {k : ℕ} {S : Type} [DecidableEq S] [Fintype S] {M : Turing.MultiTapeTM k Bool S} {x : List Bool} {c : Cfg k (St k S)} {d : Turing.Cfg k Bool S x} (h : Sim x c d) {q : S} (hq : d.state = some q) (hc : c.state = St.run q fun (j : Fin k) => decide (d.workTapePos j < 0)) (hq' : (M.tr q d.inputSymbol d.workTapeSymbols).state = none) : ∃ (c' : Cfg k (toTM M).Q), (toTM M).reachesIn 1 c c' ∧ c'.state = St.halt ∧ OutRel c'.output (Turing.MultiTapeTM.step d).output

The halting step. From the simulation relation at a CSLib step that halts, one step of the simulator halts with CSLib's final output.

theorem Complexity.FromMultiTape.init_move (l : List Γ) (d : Dir3) : (Tape.init l).move (Dir3.guard (Tape.init l).read d) = { head := 1, cells := (Tape.init l).cells }

The first move off ▷ on an initialized tape.

theorem Complexity.FromMultiTape.init_writeAndMove (l : List Γ) (s : Γ) (d : Dir3) : (Tape.init l).writeAndMove s (Dir3.guard (Tape.init l).read d) = { head := 1, cells := (Tape.init l).cells }

The first step on an initialized tape: the write is dropped and the head moves off ▷.

theorem Complexity.FromMultiTape.init_nil_start_iff (n : ℕ) : (Tape.init []).cells n = Γ.start ↔ n = 0

The blank tape holds ▷ exactly at cell 0.

@[reducible, inline]

abbrev Complexity.FromMultiTape.initD {k : ℕ} {S : Type} (M : Turing.MultiTapeTM k Bool S) (x : List Bool) : Turing.Cfg k Bool S x

The CSLib initial configuration on input x.

Equations

• Complexity.FromMultiTape.initD M x = Turing.MultiTapeTM.initCfg x

theorem Complexity.FromMultiTape.sim_init {k : ℕ} {S : Type} [DecidableEq S] [Fintype S] (M : Turing.MultiTapeTM k Bool S) (x : List Bool) : ∃ (c : Cfg k (toTM M).Q), (toTM M).reachesIn 1 ((toTM M).initCfg x) c ∧ Sim x c (initD M x) ∧ c.state = St.run M.q₀ fun (j : Fin k) => decide ((initD M x).workTapePos j < 0)

The first step. One step of the simulator moves every head off ▷ and establishes the simulation relation with CSLib's initial configuration.

theorem Complexity.FromMultiTape.sim_run {k : ℕ} {S : Type} [DecidableEq S] [Fintype S] (M : Turing.MultiTapeTM k Bool S) (x : List Bool) (n : ℕ) : (Turing.MultiTapeTM.runFrom (initD M x) n).state ≠ none → ∃ (c : Cfg k (toTM M).Q) (q : S), (toTM M).reachesIn (3 * n + 1) ((toTM M).initCfg x) c ∧ Sim x c (Turing.MultiTapeTM.runFrom (initD M x) n) ∧ (Turing.MultiTapeTM.runFrom (initD M x) n).state = some q ∧ c.state = St.run q fun (j : Fin k) => decide ((Turing.MultiTapeTM.runFrom (initD M x) n).workTapePos j < 0)

The run. While CSLib has not halted after n steps, the simulator reaches, after 3 n + 1 steps, a configuration related to CSLib's.

theorem Complexity.FromMultiTape.toTM_decides {k : ℕ} {S : Type} [DecidableEq S] [Fintype S] (M : Turing.MultiTapeTM k Bool S) {L : Language} {t s : List Bool → ℕ} (hM : M.ComputesFunInTimeAndSpace (Function.Embedding.refl (List Bool)) { toFun := fun (b : Bool) => [b], inj' := toTM_decides._proof_1 } (Turing.MultiTapeTM.indicator L) t s) (x : List Bool) : ∃ (c' : Cfg k (toTM M).Q), ∃ T ≤ 3 * t x, (toTM M).reachesIn T ((toTM M).initCfg x) c' ∧ (toTM M).halted c' ∧ (x ∈ L → c'.output.cells 1 = Γ.one) ∧ (x ∉ L → c'.output.cells 1 = Γ.zero)

The simulator decides what CSLib decides. If M computes the indicator of L within time t, the simulator decides L within time 3 t.