Indexed observations, native actions, and Mathlib Tape equivalence on bidirectional tapes

Bolton Bailey's upstream BiTape stores finite data relative to the current head. Its integer view includes blank gaps and negative displacements. The representation relation allows a native integer-indexed tape to have any absolute head position. We also provide the canonical equivalence BiTape.equivTape between BiTape Symbol and Mathlib's _root_.Turing.Tape (Option Symbol).

Main definitions

• Cslib.Turing.BiTape.read: observe the tape at an integer displacement.
• Cslib.Turing.BiTape.step: an optional write followed by a signed move.
• Cslib.Turing.BiTape.Represents: agreement with a native tape and its head position.
• Cslib.Turing.BiTape.equivTape: equivalence between BiTape Symbol and _root_.Turing.Tape (Option Symbol).

Main results

• Cslib.Turing.BiTape.Represents.step: native actions preserve the represented tape.
• Cslib.Turing.BiTape.spaceUsed_step_le: each action adds at most one stored cell.
• Cslib.Turing.BiTape.equivTape_mk₁, equivTape_write, equivTape_move, nth_equivTape: equivTape commutes with tape initialization, writes, head movement, and indexed reads.

References

Ports the additions to Foundations/Data/BiTape.lean and the tape action laws from Computability/Machines/Turing/MultiTape/FiniteTape.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

theorem Cslib.Turing.BiTape.ext {Symbol : Type u_1} {left right : BiTape Symbol} (head : left.head = right.head) (before : left.left = right.left) (after : left.right = right.right) : left = right

A tape is determined by its current symbol and two stored sides.

theorem Cslib.Turing.BiTape.ext_iff {Symbol : Type u_1} {left right : BiTape Symbol} : left = right ↔ left.head = right.head ∧ left.left = right.left ∧ left.right = right.right

def Cslib.Turing.BiTape.read {Symbol : Type u_1} (tape : BiTape Symbol) : ℤ → Option Symbol

Read a cell at an integer displacement from the current head. Negative positions lie to the left; cells outside the finite stored contents are blank.

@[simp]

theorem Cslib.Turing.BiTape.read_zero {Symbol : Type u_1} (tape : BiTape Symbol) : tape.read 0 = tape.head

Reading at displacement 0 is reading the head.

@[simp]

theorem Cslib.Turing.BiTape.read_nil {Symbol : Type u_1} (position : ℤ) : nil.read position = none

The empty tape reads blank at every displacement.

theorem Cslib.Turing.BiTape.read_mk₁ {Symbol : Type u_1} (values : List Symbol) (position : ℤ) : (mk₁ values).read position = if 0 ≤ position then values[position.toNat]? else none

Loading a word puts its first symbol under the head and leaves all negative cells blank.

theorem Cslib.Turing.BiTape.read_moveRight {Symbol : Type u_1} (tape : BiTape Symbol) (position : ℤ) : tape.moveRight.read position = tape.read (position + 1)

Moving the head right shifts the relative reading coordinates by one cell.

theorem Cslib.Turing.BiTape.read_moveLeft {Symbol : Type u_1} (tape : BiTape Symbol) (position : ℤ) : tape.moveLeft.read position = tape.read (position - 1)

Moving the head left shifts the relative reading coordinates by one cell.

theorem Cslib.Turing.BiTape.read_write {Symbol : Type u_1} (tape : BiTape Symbol) (symbol : Option Symbol) (position : ℤ) : (tape.write symbol).read position = if position = 0 then symbol else tape.read position

A write changes exactly the current cell in the integer-indexed view.

def Cslib.Turing.BiTape.step {Symbol : Type u_1} (tape : BiTape Symbol) (action : Option (Option Symbol) × SignType) : BiTape Symbol

Apply the work-tape component of a native multi-tape action.

def Cslib.Turing.BiTape.Represents {Symbol : Type u_1} (tape : BiTape Symbol) (contents : ℤ → Option Symbol) (head : ℤ) : Prop

The finite representation agrees with the native tape at every displacement from its head.

theorem Cslib.Turing.BiTape.represents_nil {Symbol : Type u_1} (head : ℤ) : nil.Represents (fun (x : ℤ) => none) head

Blank finite storage represents the native initial work tape.

theorem Cslib.Turing.BiTape.Represents.head {Symbol : Type u_1} {tape : BiTape Symbol} {contents : ℤ → Option Symbol} {head : ℤ} (h : tape.Represents contents head) : tape.head = contents head

Related tapes present the same symbol to the machine's transition table.

theorem Cslib.Turing.BiTape.Represents.step {Symbol : Type u_1} {tape : BiTape Symbol} {contents : ℤ → Option Symbol} {head : ℤ} (h : tape.Represents contents head) (action : Option (Option Symbol) × SignType) : (tape.step action).Represents (action.1.elim contents fun (symbol : Option Symbol) => Function.update contents head symbol) (head + ↑action.2)

Finite tape updates realize precisely the native write and movement, with no restriction on the head position or on blank gaps within the stored contents.

theorem Cslib.Turing.BiTape.spaceUsed_step_le {Symbol : Type u_1} (tape : BiTape Symbol) (action : Option (Option Symbol) × SignType) : (tape.step action).spaceUsed ≤ tape.spaceUsed + 1

A work-tape action increases the finite representation by at most one cell.

@[simp]

theorem Cslib.Turing.BiTape.write_head_self {Symbol : Type u_1} (tape : BiTape Symbol) : tape.write tape.head = tape

Writing the current head symbol leaves the tape unchanged.

@[simp]

theorem Cslib.Turing.BiTape.head_mk₁ {Symbol : Type u_1} (l : List Symbol) : (mk₁ l).head = l.head?

The tape loaded with a word has the first symbol of the word, if any, under its head.

@[simp]

theorem Cslib.Turing.BiTape.left_mk₁ {Symbol : Type u_1} (l : List Symbol) : (mk₁ l).left = ∅

The tape loaded with a word is empty to the left of its head.

@[simp]

theorem Cslib.Turing.BiTape.right_mk₁ {Symbol : Type u_1} (l : List Symbol) : (mk₁ l).right = StackTape.mapSome l.tail

The tape loaded with a word stores the rest of the word to the right of its head.

@[simp]

theorem Cslib.Turing.BiTape.write_moveLeft_mk₁ {Symbol : Type u_1} (a : Symbol) (l : List Symbol) : (mk₁ l).moveLeft.write (some a) = mk₁ (a :: l)

Moving left on the tape loaded with l and writing a gives the tape loaded with a :: l.

def Cslib.Turing.BiTape.equivTape {Symbol : Type u_1} : BiTape Symbol ≃ Turing.Tape (Option Symbol)

Canonical equivalence between BiTape Symbol and Mathlib's _root_.Turing.Tape (Option Symbol).

@[simp]

theorem Cslib.Turing.BiTape.head_equivTape {Symbol : Type u_1} (tape : BiTape Symbol) : (equivTape tape).head = tape.head

equivTape preserves the head symbol.

@[simp]

theorem Cslib.Turing.BiTape.left_equivTape {Symbol : Type u_1} (tape : BiTape Symbol) : (equivTape tape).left = StackTape.equivListBlank tape.left

The left side of equivTape tape is the ListBlank of the left side of tape.

@[simp]

theorem Cslib.Turing.BiTape.right_equivTape {Symbol : Type u_1} (tape : BiTape Symbol) : (equivTape tape).right = StackTape.equivListBlank tape.right

The right side of equivTape tape is the ListBlank of the right side of tape.

@[simp]

theorem Cslib.Turing.BiTape.head_equivTape_symm {Symbol : Type u_1} (tape : Turing.Tape (Option Symbol)) : (equivTape.symm tape).head = tape.head

The inverse of equivTape preserves the head symbol.

@[simp]

theorem Cslib.Turing.BiTape.left_equivTape_symm {Symbol : Type u_1} (tape : Turing.Tape (Option Symbol)) : (equivTape.symm tape).left = StackTape.equivListBlank.symm tape.left

The left side of equivTape.symm tape is the stack tape of the left side of tape.

@[simp]

theorem Cslib.Turing.BiTape.right_equivTape_symm {Symbol : Type u_1} (tape : Turing.Tape (Option Symbol)) : (equivTape.symm tape).right = StackTape.equivListBlank.symm tape.right

The right side of equivTape.symm tape is the stack tape of the right side of tape.

@[simp]

theorem Cslib.Turing.BiTape.equivTape_nil {Symbol : Type u_1} : equivTape nil = default

equivTape sends the empty tape to the blank Mathlib tape.

@[simp]

theorem Cslib.Turing.BiTape.equivTape_symm_default {Symbol : Type u_1} : equivTape.symm default = nil

The inverse of equivTape sends the blank Mathlib tape to the empty tape.

@[simp]

theorem Cslib.Turing.BiTape.equivTape_mk₁ {Symbol : Type u_1} (l : List Symbol) : equivTape (mk₁ l) = Turing.Tape.mk₁ (List.map some l)

equivTape sends the tape loaded with a word l to Mathlib's Tape.mk₁ (l.map some).

@[simp]

theorem Cslib.Turing.BiTape.equivTape_symm_mk₁ {Symbol : Type u_1} (l : List Symbol) : equivTape.symm (Turing.Tape.mk₁ (List.map some l)) = mk₁ l

The inverse of equivTape sends Mathlib's Tape.mk₁ (l.map some) to the tape loaded with l.

@[simp]

theorem Cslib.Turing.BiTape.equivTape_write {Symbol : Type u_1} (tape : BiTape Symbol) (a : Option Symbol) : equivTape (tape.write a) = Turing.Tape.write a (equivTape tape)

equivTape commutes with writing.

@[simp]

theorem Cslib.Turing.BiTape.equivTape_symm_write {Symbol : Type u_1} (tape : Turing.Tape (Option Symbol)) (a : Option Symbol) : equivTape.symm (Turing.Tape.write a tape) = (equivTape.symm tape).write a

The inverse of equivTape commutes with writing.

@[simp]

theorem Cslib.Turing.BiTape.equivTape_moveLeft {Symbol : Type u_1} (tape : BiTape Symbol) : equivTape tape.moveLeft = Turing.Tape.move Turing.Dir.left (equivTape tape)

equivTape turns moveLeft into Mathlib's move to the left.

@[simp]

theorem Cslib.Turing.BiTape.equivTape_moveRight {Symbol : Type u_1} (tape : BiTape Symbol) : equivTape tape.moveRight = Turing.Tape.move Turing.Dir.right (equivTape tape)

equivTape turns moveRight into Mathlib's move to the right.

@[simp]

theorem Cslib.Turing.BiTape.equivTape_move {Symbol : Type u_1} (tape : BiTape Symbol) (d : Turing.Dir) : equivTape (tape.move d) = Turing.Tape.move d (equivTape tape)

equivTape commutes with moving the head in either direction.

@[simp]

theorem Cslib.Turing.BiTape.equivTape_symm_move {Symbol : Type u_1} (tape : Turing.Tape (Option Symbol)) (d : Turing.Dir) : equivTape.symm (Turing.Tape.move d tape) = (equivTape.symm tape).move d

The inverse of equivTape commutes with moving the head in either direction.

@[simp]

theorem Cslib.Turing.BiTape.equivTape_optionMove {Symbol : Type u_1} (tape : BiTape Symbol) (d : Option Turing.Dir) : equivTape (tape.optionMove d) = d.elim (equivTape tape) fun (d : Turing.Dir) => Turing.Tape.move d (equivTape tape)

equivTape commutes with an optional head move, where none leaves the tape in place.

@[simp]

theorem Cslib.Turing.BiTape.nth_equivTape {Symbol : Type u_1} (tape : BiTape Symbol) (i : ℤ) : (equivTape tape).nth i = tape.read i

Reading the Mathlib tape at i is reading the tape at displacement i.

@[simp]

theorem Cslib.Turing.BiTape.read_equivTape_symm {Symbol : Type u_1} (tape : Turing.Tape (Option Symbol)) (i : ℤ) : (equivTape.symm tape).read i = tape.nth i

Reading equivTape.symm tape at displacement i is reading tape at i.