Tape contents

Holds τ p l: the tape τ holds the list l from cell p. The lemmas relate it to appending, to writing a cell (Function.update) and to reading the cell under a head.

@[reducible, inline]

abbrev MIPRE.TM.Interp.Tape : Type

A work tape.

Equations

• MIPRE.TM.Interp.Tape = (ℤ → Option MIPRE.TM.Interp.Sym)

def MIPRE.TM.Interp.Holds (τ : Tape) (p : ℤ) (l : List Sym) : Prop

The tape holds l from cell p.

Equations

• MIPRE.TM.Interp.Holds τ p l = ∀ (k : ℕ) (hk : k < l.length), τ (p + ↑k) = some l[k]

@[simp]

theorem MIPRE.TM.Interp.Holds.nil {τ : Tape} {p : ℤ} : Holds τ p []

theorem MIPRE.TM.Interp.Holds.cons_iff {τ : Tape} {p : ℤ} {s : Sym} {l : List Sym} : Holds τ p (s :: l) ↔ τ p = some s ∧ Holds τ (p + 1) l

theorem MIPRE.TM.Interp.Holds.cons {τ : Tape} {p : ℤ} {s : Sym} {l : List Sym} (h0 : τ p = some s) (h : Holds τ (p + 1) l) : Holds τ p (s :: l)

theorem MIPRE.TM.Interp.Holds.head {τ : Tape} {p : ℤ} {s : Sym} {l : List Sym} (h : Holds τ p (s :: l)) : τ p = some s

theorem MIPRE.TM.Interp.Holds.tail {τ : Tape} {p : ℤ} {s : Sym} {l : List Sym} (h : Holds τ p (s :: l)) : Holds τ (p + 1) l

theorem MIPRE.TM.Interp.Holds.append_iff {τ : Tape} {p : ℤ} {l₁ l₂ : List Sym} : Holds τ p (l₁ ++ l₂) ↔ Holds τ p l₁ ∧ Holds τ (p + ↑l₁.length) l₂

theorem MIPRE.TM.Interp.Holds.append {τ : Tape} {p : ℤ} {l₁ l₂ : List Sym} (h₁ : Holds τ p l₁) (h₂ : Holds τ (p + ↑l₁.length) l₂) : Holds τ p (l₁ ++ l₂)

theorem MIPRE.TM.Interp.Holds.of_append_left {τ : Tape} {p : ℤ} {l₁ l₂ : List Sym} (h : Holds τ p (l₁ ++ l₂)) : Holds τ p l₁

theorem MIPRE.TM.Interp.Holds.of_append_right {τ : Tape} {p : ℤ} {l₁ l₂ : List Sym} (h : Holds τ p (l₁ ++ l₂)) : Holds τ (p + ↑l₁.length) l₂

theorem MIPRE.TM.Interp.Holds.update_of_not_mem {τ : Tape} {p : ℤ} {l : List Sym} (h : Holds τ p l) {q : ℤ} (s : Option Sym) (hq : q < p ∨ p + ↑l.length ≤ q) : Holds (Function.update τ q s) p l

Writing outside the held region keeps it.

theorem MIPRE.TM.Interp.Holds.congr {τ : Tape} {p : ℤ} {τ' : Tape} {l : List Sym} (h : Holds τ p l) (hagree : ∀ (q : ℤ), p ≤ q → q < p + ↑l.length → τ' q = τ q) : Holds τ' p l

Two tapes agreeing on the held region hold the same.

theorem MIPRE.TM.Interp.Holds.singleton_iff {τ : Tape} {p : ℤ} {s : Sym} : Holds τ p [s] ↔ τ p = some s

theorem MIPRE.TM.Interp.holds_update_self (τ : Tape) (p : ℤ) (s : Sym) : Holds (Function.update τ p (some s)) p [s]

Writing a symbol at the head, then holding it: Holds (update τ p (some s)) p [s].

def MIPRE.TM.Interp.BlankFrom (τ : Tape) (p : ℤ) (n : ℕ) : Prop

The cells of [p, p + n) are blank.

Equations

• MIPRE.TM.Interp.BlankFrom τ p n = ∀ (q : ℤ), p ≤ q → q < p + ↑n → τ q = none

def MIPRE.TM.Interp.BlankBeyond (τ : Tape) (p : ℤ) : Prop

The tape is blank from p on.

Equations

• MIPRE.TM.Interp.BlankBeyond τ p = ∀ (q : ℤ), p ≤ q → τ q = none

def MIPRE.TM.Interp.BlankBefore (τ : Tape) (p : ℤ) : Prop

The tape is blank before p.

Equations

• MIPRE.TM.Interp.BlankBefore τ p = ∀ q < p, τ q = none

def MIPRE.TM.Interp.bits : List Bool → List Sym

The bits of a bit string as symbols.

Equations

• MIPRE.TM.Interp.bits = List.map fun (b : Bool) => if b = true then MIPRE.TM.Interp.Sym.one else MIPRE.TM.Interp.Sym.zero

@[simp]

theorem MIPRE.TM.Interp.bits_nil : bits [] = []

@[simp]

theorem MIPRE.TM.Interp.bits_cons (b : Bool) (l : List Bool) : bits (b :: l) = (if b = true then Sym.one else Sym.zero) :: bits l

@[simp]

theorem MIPRE.TM.Interp.bits_append (l₁ l₂ : List Bool) : bits (l₁ ++ l₂) = bits l₁ ++ bits l₂

@[simp]

theorem MIPRE.TM.Interp.length_bits (l : List Bool) : (bits l).length = l.length