Inner-Block Realizability

This file shows that any TM0RealizesBlockSep Γ sep f can be lifted to operate on an inner block of a two-separator tape, preserving the prefix.

Main definitions

• TM0RealizesInnerBlockSep Γ sep₁ sep₂ f: the machine applies f to the inner block between sep₂ and sep₁, preserving the prefix before sep₂.

Main result

• tm0RealizesBlockSep_toInnerOuterSep: any TM0RealizesBlockSep Γ sep₂ f can be lifted to TM0RealizesInnerBlockSep Γ sep₁ sep₂ f when the outer separator is non-default.
• tm0RealizesBlockSep_toInnerDefault: default-boundary version of the same prefix/suffix lift.

Strategy

The construction composes five sub-machines (three distinct):

1. Reverse (sep₁-delimited): reverses the outer block, bringing inner.reverse to the front where the left boundary is blank.
2. Reverse (sep₂-delimited): un-reverses the inner block back to inner.
3. Apply f (sep₂-delimited): applies f to the inner block.
4. Reverse (sep₂-delimited): reverses f(inner) back.
5. Reverse (sep₁-delimited): reverses the outer block, restoring prefix.

Steps 2–4 are composed into reverse ∘ f ∘ reverse via tm0RealizesBlockSep_comp, producing a single TM0RealizesBlockSep Γ sep₂ machine. The full construction is then a three-machine composition: reverse(sep₁) → revFRev(sep₂) → reverse(sep₁).

Inner Block Realizability Definition

def TM0RealizesInnerBlockSep (Γ : Type) [Inhabited Γ] (sep₁ sep₂ : Γ) (f : List Γ → List Γ) : Prop

A TM0 machine that applies f to the inner block of a two-separator tape.

Given tape pfx ++ [sep₂] ++ inner ++ [sep₁] ++ suffix, produces pfx ++ [sep₂] ++ f(inner) ++ [sep₁] ++ suffix.

The prefix pfx, both separators sep₁ and sep₂, and the suffix are all preserved. Only the inner block between sep₂ and sep₁ is modified.

Equations

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

def TM0RealizesInnerBlockSepAnySuffix (Γ : Type) [Inhabited Γ] (sep₁ sep₂ : Γ) (f : List Γ → List Γ) : Prop

Strong suffix version of TM0RealizesInnerBlockSep.

The machine applies f to the block between sep₂ and sep₁, preserving the entire suffix after sep₁ without requiring it to be blank-free.

Equations

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

theorem tm0RealizesInnerBlockSep_of_anySuffix {Γ : Type} [Inhabited Γ] {sep₁ sep₂ : Γ} {f : List Γ → List Γ} (hf : TM0RealizesInnerBlockSepAnySuffix Γ sep₁ sep₂ f) : TM0RealizesInnerBlockSep Γ sep₁ sep₂ f

Forget that an inner-block machine is suffix-opaque.

def TM0RealizesInnerBlockDefaultSep (Γ : Type) [Inhabited Γ] (sep₂ : Γ) (f : List Γ → List Γ) : Prop

A default-delimited version of TM0RealizesInnerBlockSep.

This is the shape needed by invariant while-loop bodies: the whole active block is default-delimited, and an internal separator sep₂ splits the preserved prefix from the inner block transformed by f.

Equations

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

def TM0RealizesInnerBlockDefaultViaSep (Γ : Type) [Inhabited Γ] (tmp sep₂ : Γ) (f : List Γ → List Γ) : Prop

Default-delimited inner-block realizability using a temporary non-default outer separator.

The extra separator tmp is not part of the input/output tape. It is the marker used internally to turn the outer default boundary into a real separator, run the non-default prefix/suffix lift, then restore the boundary to default. The contract records exactly the freshness facts needed for that construction.

Equations

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

List Reversal Helpers

theorem reverse_append_cons {α : Type} (l₁ : List α) (a : α) (l₂ : List α) : (l₁ ++ a :: l₂).reverse = l₂.reverse ++ a :: l₁.reverse

Reversing l₁ ++ a :: l₂ gives l₂.reverse ++ a :: l₁.reverse.

theorem forall_mem_append_cons {α : Type} {P : α → Prop} {a : α} {l₁ l₂ : List α} : (∀ g ∈ l₁ ++ a :: l₂, P g) ↔ (∀ g ∈ l₁, P g) ∧ P a ∧ ∀ g ∈ l₂, P g

All elements of l₁ ++ a :: l₂ satisfy P iff elements of l₁, a, and elements of l₂ all satisfy P.

Boundary replacement helper

inductive BoundaryReplaceSt : Type

• scan : BoundaryReplaceSt
• goLeft : BoundaryReplaceSt
• rewind : BoundaryReplaceSt
• done : BoundaryReplaceSt

instance instDecidableEqBoundaryReplaceSt : DecidableEq BoundaryReplaceSt

Equations

• instDecidableEqBoundaryReplaceSt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance instFintypeBoundaryReplaceSt : Fintype BoundaryReplaceSt

Equations

• instFintypeBoundaryReplaceSt = { elems := { val := ↑BoundaryReplaceSt.enumList, nodup := BoundaryReplaceSt.enumList_nodup }, complete := instFintypeBoundaryReplaceSt._proof_1 }

instance instInhabitedBoundaryReplaceSt : Inhabited BoundaryReplaceSt

Equations

• instInhabitedBoundaryReplaceSt = { default := BoundaryReplaceSt.scan }

noncomputable def boundaryReplaceMachine {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (target repl : Γ) : Turing.TM0.Machine Γ BoundaryReplaceSt

Scan to the first occurrence of target, replace it by repl, then rewind to the left edge of the active block.

Equations

• One or more equations did not get rendered due to their size.
• boundaryReplaceMachine target repl BoundaryReplaceSt.goLeft a = some (BoundaryReplaceSt.rewind, Turing.TM0.Stmt.move Turing.Dir.left)
• boundaryReplaceMachine target repl BoundaryReplaceSt.done a = none

theorem boundaryReplace_rewind_loop {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (target repl : Γ) (revBlock acc : List Γ) (hrevBlock : ∀ x ∈ revBlock, x ≠ default) : Turing.Reaches (Turing.TM0.step (boundaryReplaceMachine target repl)) { q := BoundaryReplaceSt.rewind, Tape := { head := revBlock.headI, left := Turing.ListBlank.mk revBlock.tail, right := Turing.ListBlank.mk acc } } { q := BoundaryReplaceSt.rewind, Tape := { head := default, left := Turing.ListBlank.mk [], right := Turing.ListBlank.mk (revBlock.reverse ++ acc) } }

theorem boundaryReplace_scan_gen {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (target repl : Γ) (block suffix revL : List Γ) (hblock_default : ∀ g ∈ block, g ≠ default) (hblock_target : ∀ g ∈ block, g ≠ target) (hrevL_default : ∀ g ∈ revL, g ≠ default) : Turing.Reaches (Turing.TM0.step (boundaryReplaceMachine target repl)) { q := BoundaryReplaceSt.scan, Tape := { head := (block ++ target :: suffix).headI, left := Turing.ListBlank.mk revL, right := Turing.ListBlank.mk (block ++ target :: suffix).tail } } { q := BoundaryReplaceSt.done, Tape := Turing.Tape.mk₁ (revL.reverse ++ block ++ repl :: suffix) }

theorem boundaryReplace_reaches {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (target repl : Γ) (block suffix : List Γ) (hblock_default : ∀ g ∈ block, g ≠ default) (hblock_target : ∀ g ∈ block, g ≠ target) : Turing.Reaches (Turing.TM0.step (boundaryReplaceMachine target repl)) (Turing.TM0.init (block ++ target :: suffix)) { q := BoundaryReplaceSt.done, Tape := Turing.Tape.mk₁ (block ++ repl :: suffix) }

theorem tm0_boundaryReplace {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (target repl : Γ) (block suffix : List Γ) : (∀ g ∈ block, g ≠ default) → (∀ g ∈ block, g ≠ target) → (TM0Seq.evalCfg (boundaryReplaceMachine target repl) (block ++ target :: suffix)).Dom ∧ ∀ (h : (TM0Seq.evalCfg (boundaryReplaceMachine target repl) (block ++ target :: suffix)).Dom), ((TM0Seq.evalCfg (boundaryReplaceMachine target repl) (block ++ target :: suffix)).get h).Tape = Turing.Tape.mk₁ (block ++ repl :: suffix)

theorem tm0RealizesBlock_toBlockSep {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] {sep : Γ} {f : List Γ → List Γ} (hf : TM0RealizesBlock Γ f) : TM0RealizesBlockSep Γ sep f

Any default-delimited block machine can be run before an arbitrary non-default separator by temporarily replacing that separator with default, running the machine, and restoring the separator.

theorem tm0RealizesBlockAnySuffix_toBlockSepAnySuffix {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] {sep : Γ} {f : List Γ → List Γ} (hf : TM0RealizesBlockAnySuffix Γ f) : TM0RealizesBlockSepAnySuffix Γ sep f

Any strong default-delimited block machine can be run before an arbitrary non-default separator by temporarily replacing that separator with default, running the machine, and restoring the separator.

Unlike tm0RealizesBlock_toBlockSep, this preserves an entirely opaque suffix: the wrapped machine must already be a strong TM0RealizesBlockAnySuffix machine, and the boundary replacement machines only touch the first boundary cell.

Composition: reverse ∘ f ∘ reverse

theorem tm0RealizesBlockSep_revFRev {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] {sep : Γ} {f : List Γ → List Γ} (hf : TM0RealizesBlockSep Γ sep f) (hf_nd : ∀ (block : List Γ), (∀ g ∈ block, g ≠ default) → ∀ g ∈ f block, g ≠ default) (hf_nsep : ∀ (block : List Γ), (∀ g ∈ block, g ≠ sep) → ∀ g ∈ f block, g ≠ sep) : TM0RealizesBlockSep Γ sep (List.reverse ∘ f ∘ List.reverse)

If f is TM0RealizesBlockSep Γ sep, then reverse ∘ f ∘ reverse is also TM0RealizesBlockSep Γ sep, provided f preserves the non-defaultness and non-separator properties.

This is a reusable sub-machine composition: it takes any block-sep-realizable function and produces a machine for the "conjugated" function reverse ∘ f ∘ reverse.

theorem tm0RealizesBlockSepAnySuffix_revFRev {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] {sep : Γ} {f : List Γ → List Γ} (hf : TM0RealizesBlockSepAnySuffix Γ sep f) (hf_nd : ∀ (block : List Γ), (∀ g ∈ block, g ≠ default) → ∀ g ∈ f block, g ≠ default) (hf_nsep : ∀ (block : List Γ), (∀ g ∈ block, g ≠ sep) → ∀ g ∈ f block, g ≠ sep) : TM0RealizesBlockSepAnySuffix Γ sep (List.reverse ∘ f ∘ List.reverse)

Strong suffix version of tm0RealizesBlockSep_revFRev. This is the form needed by prefix/suffix lifting when the preserved suffix after sep may itself contain default.

theorem tm0_appendList_blockSep_anySuffix {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] {sep : Γ} (suf : List Γ) (hsuf_nd : ∀ g ∈ suf, g ≠ default) (hsuf_nsep : ∀ g ∈ suf, g ≠ sep) : TM0RealizesBlockSepAnySuffix Γ sep fun (block : List Γ) => block ++ suf

Appending a fixed non-default, non-separator list is realizable before a separator, with no invariant on the suffix. This follows by reversing the active block, prepending the reversed fixed suffix, and reversing back.

theorem tm0_appendList_blockSep {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] {sep : Γ} (suf : List Γ) (hsuf_nd : ∀ g ∈ suf, g ≠ default) (hsuf_nsep : ∀ g ∈ suf, g ≠ sep) : TM0RealizesBlockSep Γ sep fun (block : List Γ) => block ++ suf

Main Theorem: Lifting to Inner Block

theorem tm0RealizesBlockSep_toInner_nondefault {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] {sep₁ sep₂ : Γ} {f : List Γ → List Γ} (hsep₁ : sep₁ ≠ default) (hsep₂ : sep₂ ≠ default) (h₁₂ : sep₁ ≠ sep₂) (hf : TM0RealizesBlockSep Γ sep₂ f) (hf_nd : ∀ (block : List Γ), (∀ g ∈ block, g ≠ default) → ∀ g ∈ f block, g ≠ default) (hf_nsep : ∀ (block : List Γ), (∀ g ∈ block, g ≠ sep₂) → ∀ g ∈ f block, g ≠ sep₂) : TM0RealizesInnerBlockSep Γ sep₁ sep₂ f

theorem tm0RealizesBlockSepAnySuffix_toInner {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] {sep₁ sep₂ : Γ} {f : List Γ → List Γ} (hsep₂ : sep₂ ≠ default) (h₁₂ : sep₁ ≠ sep₂) (hf : TM0RealizesBlockSepAnySuffix Γ sep₂ f) (hf_nd : ∀ (block : List Γ), (∀ g ∈ block, g ≠ default) → ∀ g ∈ f block, g ≠ default) (hf_nsep : ∀ (block : List Γ), (∀ g ∈ block, g ≠ sep₂) → ∀ g ∈ f block, g ≠ sep₂) : TM0RealizesInnerBlockSepAnySuffix Γ sep₁ sep₂ f

Strong suffix version of the prefix/suffix lift.

This is the construction that works uniformly for sep₁ = default and sep₁ ≠ default: after reversing the outer block, the middle machine runs on inner.reverse ++ sep₂ :: pfx.reverse ++ sep₁ :: suffix, so the hypothesis on f must be TM0RealizesBlockSepAnySuffix.

theorem tm0RealizesBlockSep_toInnerOuterSep {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] {sep₁ sep₂ : Γ} {f : List Γ → List Γ} (hsep₁ : sep₁ ≠ default) (hsep₂ : sep₂ ≠ default) (h₁₂ : sep₁ ≠ sep₂) (hf : TM0RealizesBlockSep Γ sep₂ f) (hf_nd : ∀ (block : List Γ), (∀ g ∈ block, g ≠ default) → ∀ g ∈ f block, g ≠ default) (hf_nsep : ∀ (block : List Γ), (∀ g ∈ block, g ≠ sep₂) → ∀ g ∈ f block, g ≠ sep₂) : TM0RealizesInnerBlockSep Γ sep₁ sep₂ f

Separator-delimited version of the default-boundary lift.

This is the form to use when the outer delimiter after the inner block should be a real separator sep₁, not the tape blank. The tape shape is pfx ++ sep₂ :: inner ++ sep₁ :: suffix.

theorem tm0RealizesBlockSep_toInnerDefaultViaSep {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] {tmp sep₂ : Γ} {f : List Γ → List Γ} (htmp : tmp ≠ default) (hsep₂ : sep₂ ≠ default) (htmp₂ : tmp ≠ sep₂) (hf : TM0RealizesBlockSep Γ sep₂ f) (hf_nd : ∀ (block : List Γ), (∀ g ∈ block, g ≠ default) → ∀ g ∈ f block, g ≠ default) (hf_nsep : ∀ (block : List Γ), (∀ g ∈ block, g ≠ sep₂) → ∀ g ∈ f block, g ≠ sep₂) : TM0RealizesInnerBlockDefaultViaSep Γ tmp sep₂ f

Default-boundary inner-block lift through a temporary real separator.

Operationally this is:

1. rewrite the boundary default after inner to tmp;
2. use tm0RealizesBlockSep_toInner_nondefault with outer separator tmp;
3. rewrite the resulting boundary tmp back to default.

The freshness assumptions on tmp are carried by TM0RealizesInnerBlockDefaultViaSep, because the temporary marker must not be confused with data in the prefix, inner block, or transformed inner block.

theorem tm0RealizesBlockSep_toInnerDefault {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] {sep₂ : Γ} {f : List Γ → List Γ} (hsep₂ : sep₂ ≠ default) (hf : TM0RealizesBlockSep Γ sep₂ f) (hf_nd : ∀ (block : List Γ), (∀ g ∈ block, g ≠ default) → ∀ g ∈ f block, g ≠ default) (hf_nsep : ∀ (block : List Γ), (∀ g ∈ block, g ≠ sep₂) → ∀ g ∈ f block, g ≠ sep₂) : TM0RealizesInnerBlockDefaultSep Γ sep₂ f

Default-delimited inner-block lift with no suffix after the final blank.

The construction is the same three-machine composition: reverse before the outer default, run reverse ∘ f ∘ reverse before the internal separator, then reverse before the outer default again. The middle phase is applied to a list without the trailing default; evalCfg_append_default identifies that with the actual intermediate tape.