Unrestricted depth-three lower bound: tape copy

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/TapeCopy.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical proofs are retained.

inductive Complexity.DepthThreeLowerBound.TapeCopy.State : Type

Control states of the copy routine.

• start : State
• scan : State
• rewind : State
• done : State

@[instance_reducible]

instance Complexity.DepthThreeLowerBound.TapeCopy.instDecidableEqState : DecidableEq State

Equations

• Complexity.DepthThreeLowerBound.TapeCopy.instDecidableEqState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Complexity.DepthThreeLowerBound.TapeCopy.instInhabitedState : Inhabited State

Equations

• Complexity.DepthThreeLowerBound.TapeCopy.instInhabitedState = { default := Complexity.DepthThreeLowerBound.TapeCopy.instInhabitedState.default }

@[instance_reducible]

instance Complexity.DepthThreeLowerBound.TapeCopy.instFintypeState : Fintype State

Equations

• One or more equations did not get rendered due to their size.

def Complexity.DepthThreeLowerBound.TapeCopy.onPair {α : Type uDepth1} (src dst : TapeRegister) (base : TapeRegister → α) (s d : α) : TapeRegister → α

Replace the values at two selected registers, giving priority to the first.

Equations

• Complexity.DepthThreeLowerBound.TapeCopy.onPair src dst base s d r = if r = src then s else if r = dst then d else base r

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeCopy.onPair_src {α : Type uDepth2} (src dst : TapeRegister) (base : TapeRegister → α) (s d : α) : onPair src dst base s d src = s

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeCopy.onPair_dst {α : Type uDepth3} {src dst : TapeRegister} (hne : src ≠ dst) (base : TapeRegister → α) (s d : α) : onPair src dst base s d dst = d

theorem Complexity.DepthThreeLowerBound.TapeCopy.onPair_other {α : Type uDepth4} (src dst : TapeRegister) (base : TapeRegister → α) (s d : α) (r : TapeRegister) (hs : r ≠ src) (hd : r ≠ dst) : onPair src dst base s d r = base r

def Complexity.DepthThreeLowerBound.TapeCopy.emit {Q : Type uDepth5} (src dst : TapeRegister) (q : Q) (h : TapeHeads) (s d : TapeSymbol) (m : HeadMove) : Option (Q × TapeHeads × TapeMoves)

Write the two selected tape heads and move them together.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.DepthThreeLowerBound.TapeCopy.code (src dst : TapeRegister) : TapeMultiProgram State

Transition function of the copy routine.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DepthThreeLowerBound.TapeCopy.code src dst Complexity.DepthThreeLowerBound.TapeCopy.State.done x✝ = none

theorem Complexity.DepthThreeLowerBound.TapeCopy.step_emit {Q : Type uDepth6} (P : TapeMultiProgram Q) {src dst : TapeRegister} (hne : src ≠ dst) (T : TapeTapes) (S D : Turing.Tape TapeSymbol) (q q' : Q) (s d : TapeSymbol) (m : HeadMove) (h : P q (TapeMultiProgram.heads (onPair src dst T S D)) = emit src dst q' (TapeMultiProgram.heads (onPair src dst T S D)) s d m) : P.step (TapeMultiProgram.cfg q (onPair src dst T S D)) = some (TapeMultiProgram.cfg q' (onPair src dst T (m.apply (Turing.Tape.write s S)) (m.apply (Turing.Tape.write d D))))

theorem Complexity.DepthThreeLowerBound.TapeCopy.step_start {src dst : TapeRegister} (hne : src ≠ dst) (T : TapeTapes) (S D : Turing.Tape TapeSymbol) : (code src dst).step (TapeMultiProgram.cfg State.start (onPair src dst T S D)) = some (TapeMultiProgram.cfg State.scan (onPair src dst T (Turing.Tape.move Turing.Dir.right S) (Turing.Tape.move Turing.Dir.right D)))

theorem Complexity.DepthThreeLowerBound.TapeCopy.step_scan_bit {src dst : TapeRegister} (hne : src ≠ dst) (T : TapeTapes) (S D : Turing.Tape TapeSymbol) (b : Bool) (hS : S.head = rawInputSymbol b) : (code src dst).step (TapeMultiProgram.cfg State.scan (onPair src dst T S D)) = some (TapeMultiProgram.cfg State.scan (onPair src dst T (Turing.Tape.move Turing.Dir.right S) (Turing.Tape.move Turing.Dir.right (Turing.Tape.write (rawInputSymbol b) D))))

theorem Complexity.DepthThreeLowerBound.TapeCopy.step_scan_end {src dst : TapeRegister} (hne : src ≠ dst) (T : TapeTapes) (S D : Turing.Tape TapeSymbol) (hS : S.head = cleanAtom TapeAtom.endMark) : (code src dst).step (TapeMultiProgram.cfg State.scan (onPair src dst T S D)) = some (TapeMultiProgram.cfg State.rewind (onPair src dst T S (Turing.Tape.write (cleanAtom TapeAtom.endMark) D)))

theorem Complexity.DepthThreeLowerBound.TapeCopy.step_rewind_move {src dst : TapeRegister} (hne : src ≠ dst) (T : TapeTapes) (S D : Turing.Tape TapeSymbol) (hS : S.head.1 ≠ TapeAtom.home) : (code src dst).step (TapeMultiProgram.cfg State.rewind (onPair src dst T S D)) = some (TapeMultiProgram.cfg State.rewind (onPair src dst T (Turing.Tape.move Turing.Dir.left S) (Turing.Tape.move Turing.Dir.left D)))

theorem Complexity.DepthThreeLowerBound.TapeCopy.step_rewind_home {src dst : TapeRegister} (hne : src ≠ dst) (T : TapeTapes) (S D : Turing.Tape TapeSymbol) (hS : S.head.1 = TapeAtom.home) : (code src dst).step (TapeMultiProgram.cfg State.rewind (onPair src dst T S D)) = some (TapeMultiProgram.cfg State.done (onPair src dst T S D))

theorem Complexity.DepthThreeLowerBound.TapeCopy.write_mk₂ (L R : List TapeSymbol) (a : TapeSymbol) : Turing.Tape.write a (Turing.Tape.mk₂ L R) = Turing.Tape.mk₂ L (a :: R.tail)

theorem Complexity.DepthThreeLowerBound.TapeCopy.runs_scan {src dst : TapeRegister} (hne : src ≠ dst) (T : TapeTapes) (bits : List Bool) (L R : List TapeSymbol) (hR : R.tail = []) : RunsIn (code src dst).step (TapeMultiProgram.cfg State.scan (onPair src dst T (Turing.Tape.mk₂ L (encodeInput bits ++ [cleanAtom TapeAtom.endMark])) (Turing.Tape.mk₂ L R))) (TapeMultiProgram.cfg State.rewind (onPair src dst T (Turing.Tape.mk₂ ((encodeInput bits).reverse ++ L) [cleanAtom TapeAtom.endMark]) (Turing.Tape.mk₂ ((encodeInput bits).reverse ++ L) [cleanAtom TapeAtom.endMark]))) (bits.length + 1)

theorem Complexity.DepthThreeLowerBound.TapeCopy.runs_rewind {src dst : TapeRegister} (hne : src ≠ dst) (T : TapeTapes) (bits : List Bool) (a : TapeSymbol) (R : List TapeSymbol) (ha : a.1 ≠ TapeAtom.home) : RunsIn (code src dst).step (TapeMultiProgram.cfg State.rewind (onPair src dst T (Turing.Tape.mk₂ (encodeInput bits ++ [cleanAtom TapeAtom.home]) (a :: R)) (Turing.Tape.mk₂ (encodeInput bits ++ [cleanAtom TapeAtom.home]) (a :: R)))) (TapeMultiProgram.cfg State.done (onPair src dst T (Turing.Tape.mk₂ [] (cleanAtom TapeAtom.home :: ((encodeInput bits).reverse ++ a :: R))) (Turing.Tape.mk₂ [] (cleanAtom TapeAtom.home :: ((encodeInput bits).reverse ++ a :: R))))) (bits.length + 2)

theorem Complexity.DepthThreeLowerBound.TapeCopy.runs_copy {src dst : TapeRegister} (hne : src ≠ dst) (T : TapeTapes) (bits : List Bool) : RunsIn (code src dst).step (TapeMultiProgram.cfg State.start (onPair src dst T (wordTape bits) (wordTape []))) (TapeMultiProgram.cfg State.done (onPair src dst T (wordTape bits) (wordTape bits))) (2 * bits.length + 4)

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeCopy.step_done (src dst : TapeRegister) (T : TapeTapes) : (code src dst).step (TapeMultiProgram.cfg State.done T) = none