Indexed observations and Mathlib ListBlank equivalence for finite stack tapes

These additions give Bolton Bailey's upstream StackTape an indexed view that reads blank outside its stored list, together with the canonical equivalence with Mathlib's quotient one-sided tape _root_.Turing.ListBlank (Option Symbol).

Main definitions

• Cslib.Turing.StackTape.read: observe the tape at a natural-number displacement.
• Cslib.Turing.StackTape.ofList: fold a list of optional symbols onto an empty stack tape.
• Cslib.Turing.StackTape.equivListBlank: equivalence between StackTape Symbol and _root_.Turing.ListBlank (Option Symbol).

Main results

• Cslib.Turing.StackTape.read_eq_getElem?: agreement with padded list lookup.
• Cslib.Turing.StackTape.read_mapSome: loading a word preserves its indexed symbols.
• Cslib.Turing.StackTape.equivListBlank_cons, head_equivListBlank, tail_equivListBlank, nth_equivListBlank: equivListBlank commutes with stack-tape operations and indexed reads.

References

Ports the additions to Foundations/Data/StackTape.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, retaining the upstream tape representation.

theorem Cslib.Turing.StackTape.ext {Symbol : Type u_1} {left right : StackTape Symbol} (h : left.toList = right.toList) : left = right

Equality of stored lists determines equality of stack tapes.

theorem Cslib.Turing.StackTape.ext_iff {Symbol : Type u_1} {left right : StackTape Symbol} : left = right ↔ left.toList = right.toList

@[simp]

theorem Cslib.Turing.StackTape.tail_toList {Symbol : Type u_1} (tape : StackTape Symbol) : tape.tail.toList = tape.toList.tail

The stored list of tail is the tail of the stored list.

theorem Cslib.Turing.StackTape.cons_toList {Symbol : Type u_1} (symbol : Option Symbol) (tape : StackTape Symbol) : (cons symbol tape).toList = if (symbol.isSome || !tape.toList.isEmpty) = true then symbol :: tape.toList else []

Prepending retains blank cells only when there is stored data beyond them.

def Cslib.Turing.StackTape.read {Symbol : Type u_1} : StackTape Symbol → ℕ → Option Symbol

Read a cell, treating every position beyond the finite representation as blank.

@[simp]

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

Reading at 0 is reading the head.

@[simp]

theorem Cslib.Turing.StackTape.read_succ {Symbol : Type u_1} (tape : StackTape Symbol) (position : ℕ) : tape.read (position + 1) = tape.tail.read position

Reading at position + 1 is reading the tail at position.

@[simp]

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

The empty stack tape reads blank everywhere.

theorem Cslib.Turing.StackTape.read_eq_getElem? {Symbol : Type u_1} (tape : StackTape Symbol) (position : ℕ) : tape.read position = tape.toList[position]?.join

The indexed view agrees with the stored list, with absent cells read as blanks.

@[simp]

theorem Cslib.Turing.StackTape.read_mapSome {Symbol : Type u_1} (values : List Symbol) (position : ℕ) : (mapSome values).read position = values[position]?

The tape loaded with a word reads its symbol at each position, and blank past its end.

@[simp]

theorem Cslib.Turing.StackTape.cons_none_nil {Symbol : Type u_1} : cons none nil = nil

Prepending a blank to the empty stack tape leaves it empty.

def Cslib.Turing.StackTape.ofList {Symbol : Type u_1} (values : List (Option Symbol)) : StackTape Symbol

Construct a StackTape from an arbitrary list of optional symbols by folding cons.

@[simp]

theorem Cslib.Turing.StackTape.ofList_nil {Symbol : Type u_1} : ofList [] = nil

ofList turns the empty list into the empty stack tape.

@[simp]

theorem Cslib.Turing.StackTape.ofList_cons {Symbol : Type u_1} (a : Option Symbol) (l : List (Option Symbol)) : ofList (a :: l) = cons a (ofList l)

ofList turns list prepending into cons.

@[simp]

theorem Cslib.Turing.StackTape.ofList_replicate_none {Symbol : Type u_1} (n : ℕ) : ofList (List.replicate n none) = nil

A list of blanks gives the empty stack tape.

theorem Cslib.Turing.StackTape.ofList_append_replicate_none {Symbol : Type u_1} (l : List (Option Symbol)) (n : ℕ) : ofList (l ++ List.replicate n none) = ofList l

Trailing blanks do not change ofList.

@[simp]

theorem Cslib.Turing.StackTape.ofList_toList {Symbol : Type u_1} (tape : StackTape Symbol) : ofList tape.toList = tape

ofList recovers a stack tape from its stored list.

@[simp]

theorem Cslib.Turing.StackTape.ofList_map_some {Symbol : Type u_1} (l : List Symbol) : ofList (List.map some l) = mapSome l

ofList of the symbols of a word wrapped in some is mapSome of the word.

@[simp]

theorem Cslib.Turing.StackTape.listBlank_mk_toList_ofList {Symbol : Type u_1} (l : List (Option Symbol)) : Turing.ListBlank.mk (ofList l).toList = Turing.ListBlank.mk l

The stored list of ofList l gives the same ListBlank as l.

def Cslib.Turing.StackTape.equivListBlank {Symbol : Type u_1} : StackTape Symbol ≃ Turing.ListBlank (Option Symbol)

Canonical equivalence between StackTape Symbol and Mathlib's _root_.Turing.ListBlank (Option Symbol).

@[simp]

theorem Cslib.Turing.StackTape.equivListBlank_nil {Symbol : Type u_1} : equivListBlank nil = default

equivListBlank sends the empty stack tape to the blank ListBlank.

@[simp]

theorem Cslib.Turing.StackTape.equivListBlank_symm_default {Symbol : Type u_1} : equivListBlank.symm default = nil

The inverse of equivListBlank sends the blank ListBlank to the empty stack tape.

@[simp]

theorem Cslib.Turing.StackTape.equivListBlank_symm_mk {Symbol : Type u_1} (l : List (Option Symbol)) : equivListBlank.symm (Turing.ListBlank.mk l) = ofList l

The inverse of equivListBlank sends the ListBlank of a list l to ofList l.

@[simp]

theorem Cslib.Turing.StackTape.equivListBlank_ofList {Symbol : Type u_1} (l : List (Option Symbol)) : equivListBlank (ofList l) = Turing.ListBlank.mk l

equivListBlank sends ofList l to the ListBlank of l.

@[simp]

theorem Cslib.Turing.StackTape.equivListBlank_cons {Symbol : Type u_1} (a : Option Symbol) (tape : StackTape Symbol) : equivListBlank (cons a tape) = Turing.ListBlank.cons a (equivListBlank tape)

equivListBlank turns stack-tape cons into ListBlank.cons.

@[simp]

theorem Cslib.Turing.StackTape.equivListBlank_symm_cons {Symbol : Type u_1} (a : Option Symbol) (lb : Turing.ListBlank (Option Symbol)) : equivListBlank.symm (Turing.ListBlank.cons a lb) = cons a (equivListBlank.symm lb)

The inverse of equivListBlank turns ListBlank.cons into stack-tape cons.

@[simp]

theorem Cslib.Turing.StackTape.head_equivListBlank {Symbol : Type u_1} (tape : StackTape Symbol) : (equivListBlank tape).head = tape.head

equivListBlank preserves the head.

@[simp]

theorem Cslib.Turing.StackTape.head_equivListBlank_symm {Symbol : Type u_1} (lb : Turing.ListBlank (Option Symbol)) : (equivListBlank.symm lb).head = lb.head

The inverse of equivListBlank preserves the head.

@[simp]

theorem Cslib.Turing.StackTape.tail_equivListBlank {Symbol : Type u_1} (tape : StackTape Symbol) : (equivListBlank tape).tail = equivListBlank tape.tail

equivListBlank commutes with taking the tail.

@[simp]

theorem Cslib.Turing.StackTape.tail_equivListBlank_symm {Symbol : Type u_1} (lb : Turing.ListBlank (Option Symbol)) : (equivListBlank.symm lb).tail = equivListBlank.symm lb.tail

The inverse of equivListBlank commutes with taking the tail.

@[simp]

theorem Cslib.Turing.StackTape.equivListBlank_mapSome {Symbol : Type u_1} (l : List Symbol) : equivListBlank (mapSome l) = Turing.ListBlank.mk (List.map some l)

equivListBlank sends mapSome l to the ListBlank of l.map some.

@[simp]

theorem Cslib.Turing.StackTape.nth_equivListBlank {Symbol : Type u_1} (tape : StackTape Symbol) (n : ℕ) : (equivListBlank tape).nth n = tape.read n

Reading the ListBlank at n is reading the tape at n.

@[simp]

theorem Cslib.Turing.StackTape.read_equivListBlank_symm {Symbol : Type u_1} (lb : Turing.ListBlank (Option Symbol)) (n : ℕ) : (equivListBlank.symm lb).read n = lb.nth n

Reading the stack tape equivListBlank.symm lb at n is reading lb at n.