Binary string encodings on Turing-machine tapes

Generic predicates and lemmas for tapes containing canonical binary strings. Tape.HasBinaryPrefix describes a string being written from left to right, Tape.HasBinaryString describes the same contents after rewinding the head to cell one, Tape.HasBinaryContent forgets the head while an in-place arithmetic cursor moves, and Tape.HasBinarySuffix describes a read cursor at the beginning of a remaining suffix. These shapes are shared by deterministic and nondeterministic machine constructions.

def Complexity.Tape.HasBinaryPrefix (t : Tape) (bits : List Bool) : Prop

A tape while a binary string is being written: cells 1..|bits| contain the bits, the head is at the next cell, and the remaining tail is blank.

Equations

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

def Complexity.Tape.HasBinaryString (t : Tape) (bits : List Bool) : Prop

A completed binary string: the bits are present and the head has been rewound to cell one.

Equations

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

def Complexity.Tape.HasBinaryContent (t : Tape) (bits : List Bool) : Prop

Canonical binary contents independently of the tape head. This is the stable invariant for in-place arithmetic cursors that scan and rewind.

Equations

• t.HasBinaryContent bits = ((∀ (i : ℕ) (h : i < bits.length), t.cells (i + 1) = Complexity.Γ.ofBool bits[i]) ∧ ∀ (i : ℕ), bits.length ≤ i → t.cells (i + 1) = Complexity.Γ.blank)

def Complexity.Tape.HasBinarySuffix (t : Tape) (bits : List Bool) : Prop

A read cursor at the beginning of a remaining binary suffix. The suffix starts under the current off-marker head, is followed immediately by blank, and the tape has no stray left markers.

Equations

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

def Complexity.Tape.HasBoundedBinaryString (t : Tape) (B : ℕ) : Prop

A completed binary string whose length is at most B.

Equations

• t.HasBoundedBinaryString B = ∃ (bits : List Bool), bits.length ≤ B ∧ t.HasBinaryString bits

theorem Complexity.Tape.HasBinaryString.hasBinaryContent {t : Tape} {bits : List Bool} (h : t.HasBinaryString bits) : t.HasBinaryContent bits

A completed binary string has the same canonical contents after forgetting its parked head.

theorem Complexity.Tape.HasBinaryContent.hasBinaryString {t : Tape} {bits : List Bool} (h : t.HasBinaryContent bits) (hhead : t.head = 1) : t.HasBinaryString bits

Canonical contents become a completed binary string when the head is at cell one.

theorem Complexity.Tape.HasBinaryContent.move {t : Tape} {bits : List Bool} (h : t.HasBinaryContent bits) (dir : Dir3) : (t.move dir).HasBinaryContent bits

Moving a cursor preserves its canonical binary contents.

theorem Complexity.Tape.HasBinaryContent.cells_ne_start {t : Tape} {bits : List Bool} (h : t.HasBinaryContent bits) (j : ℕ) : 1 ≤ j → t.cells j ≠ Γ.start

Canonical binary contents contain no stray left marker after cell zero.

theorem Complexity.Tape.HasBinaryContent.write_set {t : Tape} {bits : List Bool} {i : ℕ} (bit : Bool) (h : t.HasBinaryContent bits) (hhead : t.head = i + 1) (hi : i < bits.length) : (t.write (Γ.ofBool bit)).HasBinaryContent (bits.set i bit)

Overwriting one in-range binary cell preserves canonical contents and updates exactly that bit.

theorem Complexity.Tape.write_move_cell0 {t : Tape} (symbol : Γ) (dir : Dir3) (h0 : t.cells 0 = Γ.start) : ((t.write symbol).move dir).cells 0 = Γ.start

Writing away from cell zero and then moving preserves the left marker.

theorem Complexity.Tape.hasOutput_of_hasBinaryString {t : Tape} {bits : List Bool} (h : t.HasBinaryString bits) : t.HasOutput bits

A completed binary tape encodes exactly bits as its output string.

theorem Complexity.Tape.cells_ne_start_of_hasBinaryString {t : Tape} {bits : List Bool} (h : t.HasBinaryString bits) (j : ℕ) : j ≥ 1 → t.cells j ≠ Γ.start

A completed binary tape never contains ▷ after the left-end marker.

theorem Complexity.Tape.eq_init_move_right_of_hasBinaryString {t : Tape} {bits : List Bool} (h : t.HasBinaryString bits) (h0 : t.cells 0 = Γ.start) : t = (init (List.map Γ.ofBool bits)).move Dir3.right

A completed binary tape with the left marker at cell 0 is exactly the standard initialized tape for those bits, moved to cell 1.

theorem Complexity.Tape.HasBinaryPrefix.cells_eq_init {t : Tape} {bits : List Bool} (h : t.HasBinaryPrefix bits) (h0 : t.cells 0 = Γ.start) : t.cells = (init (List.map Γ.ofBool bits)).cells

A binary prefix with the left marker at cell zero has exactly the canonical initialized cell contents, independently of its current head.

theorem Complexity.Tape.exists_eq_init_move_right_of_hasBoundedBinaryString {t : Tape} {B : ℕ} (h : t.HasBoundedBinaryString B) (h0 : t.cells 0 = Γ.start) : ∃ (bits : List Bool), bits.length ≤ B ∧ t = (init (List.map Γ.ofBool bits)).move Dir3.right

Bounded completed binary tapes expose exact initialized tape shape for some string whose length satisfies the same bound.

theorem Complexity.Tape.init_nil_move_right_hasBinaryPrefix_nil : ((init []).move Dir3.right).HasBinaryPrefix []

A freshly initialized empty tape, moved right past ▷, is an empty binary prefix.

theorem Complexity.Tape.init_move_right_hasBinaryString (bits : List Bool) : ((init (List.map Γ.ofBool bits)).move Dir3.right).HasBinaryString bits

A standard initialized binary tape moved right to its first data cell is a completed binary string.

theorem Complexity.Tape.HasBinaryPrefix.read_blank {t : Tape} {bits : List Bool} (h : t.HasBinaryPrefix bits) : t.read = Γ.blank

The head of an appendable binary prefix reads its first trailing blank.

theorem Complexity.Tape.HasBinaryPrefix.hasOutput {t : Tape} {bits : List Bool} (h : t.HasBinaryPrefix bits) : t.HasOutput bits

An appendable binary prefix already contains the advertised delimited output, independently of its current head.

theorem Complexity.Tape.init_move_right_hasBinarySuffix (bits : List Bool) : ((init (List.map Γ.ofBool bits)).move Dir3.right).HasBinarySuffix bits

A freshly initialized binary tape starts with its whole string as the remaining suffix.

theorem Complexity.Tape.HasBinaryString.hasBinarySuffix {t : Tape} {bits : List Bool} (h : t.HasBinaryString bits) : t.HasBinarySuffix bits

A completed binary string exposes the same bits as its remaining suffix.

theorem Complexity.Tape.HasOutput.hasBinarySuffix {t : Tape} {bits : List Bool} (h : t.HasOutput bits) (hhead : t.head = 1) (hinv : t.StartInvariant) : t.HasBinarySuffix bits

A delimited output parked at cell one is a binary suffix cursor when the tape has no stray left-end markers.

theorem Complexity.Tape.HasBinarySuffix.read_cons {t : Tape} {bit : Bool} {bits : List Bool} (h : t.HasBinarySuffix (bit :: bits)) : t.read = Γ.ofBool bit

The first symbol of a nonempty binary suffix is under the tape head.

theorem Complexity.Tape.HasBinarySuffix.move_right_cons {t : Tape} {bit : Bool} {bits : List Bool} (h : t.HasBinarySuffix (bit :: bits)) : (t.move Dir3.right).HasBinarySuffix bits

Moving right after reading the first bit exposes the remaining suffix.

theorem Complexity.Tape.HasBinarySuffix.read_nil {t : Tape} (h : t.HasBinarySuffix []) : t.read = Γ.blank

An empty remaining suffix reads the terminating blank.

theorem Complexity.Tape.HasBinarySuffix.read_ne_start {t : Tape} {bits : List Bool} (h : t.HasBinarySuffix bits) : t.read ≠ Γ.start

A binary suffix cursor never reads the left-end marker.

theorem Complexity.Tape.hasBinaryPrefix_write_bit {t : Tape} {bits : List Bool} (bit : Bool) (h : t.HasBinaryPrefix bits) : (t.writeAndMove (Γ.ofBool bit) Dir3.right).HasBinaryPrefix (bits ++ [bit])

Writing the next bit extends a binary prefix by one cell.

theorem Complexity.Tape.HasBinaryContent.write_append {t : Tape} {bits : List Bool} (bit : Bool) (h : t.HasBinaryContent bits) (hhead : t.head = bits.length + 1) : (t.write (Γ.ofBool bit)).HasBinaryContent (bits ++ [bit])

Writing at the first blank appends one canonical binary cell.

theorem Complexity.Tape.hasBinaryPrefix_write_bit_cell0 {t : Tape} {bits : List Bool} (bit : Bool) (h : t.HasBinaryPrefix bits) (h0 : t.cells 0 = Γ.start) : (t.writeAndMove (Γ.ofBool bit) Dir3.right).cells 0 = Γ.start

Writing the next bit preserves the left-end marker cell.

theorem Complexity.Tape.cells_ne_start_of_hasBinaryPrefix {t : Tape} {bits : List Bool} (h : t.HasBinaryPrefix bits) (j : ℕ) : j ≥ 1 → t.cells j ≠ Γ.start

A binary prefix never contains ▷ after the left-end marker.

theorem Complexity.Tape.hasBinaryPrefix_of_hasBinaryString {t t' : Tape} {bits : List Bool} (hstring : t.HasBinaryString bits) (hhead : t'.head = bits.length + 1) (hcells : t'.cells = t.cells) : t'.HasBinaryPrefix bits

Moving a completed binary string's head to the first blank, without changing its cells, yields the corresponding appendable prefix.

theorem Complexity.Tape.hasBinaryString_of_hasBinaryPrefix {t t' : Tape} {bits : List Bool} (hprefix : t.HasBinaryPrefix bits) (hhead : t'.head = 1) (hcells : t'.cells = t.cells) : t'.HasBinaryString bits

Rewinding a binary prefix to cell one yields a completed binary string.