Hoare-style specifications for Turing machines

This file defines Hoare triples for reasoning about TM behavior in terms of tape preconditions and postconditions. This provides a compositional framework for building and verifying complex machines from simpler components.

Main definitions

• TapePred — a predicate on the tape configuration (input, work, output)
• TM.HoareTime — time-bounded Hoare triple: {pre} tm {post} [≤ bound]
• TM.Hoare — unbounded Hoare triple: {pre} tm {post}

Design notes

Hoare triples abstract away the internal state Q, reasoning purely about tape contents and head positions. This makes them ideal for compositional reasoning: the pre/postconditions of composed machines can be stated without reference to the internal state types of the components.

The precondition must imply that the starting configuration has the machine's qstart state. The postcondition holds at halting.

@[reducible, inline]

abbrev Complexity.TapePred (n : ℕ) : Type

A predicate on the tape configuration: input tape, work tapes, output tape.

Equations

• Complexity.TapePred n = (Complexity.Tape → (Fin n → Complexity.Tape) → Complexity.Tape → Prop)

@[reducible, inline]

abbrev Complexity.TM.TapePred (n : ℕ) : Type

A predicate on the tape configuration: input tape, work tapes, output tape.

Equations

• Complexity.TM.TapePred n = Complexity.TapePred n

def Complexity.TM.HoareTime {n : ℕ} (tm : TM n) (pre post : TapePred n) (bound : ℕ) : Prop

Time-bounded Hoare triple: for any tapes satisfying pre, starting from qstart, the machine halts within bound steps with tapes satisfying post.

This is the core specification type for compositional TM reasoning. Captures both correctness (pre/post) and efficiency (time bound).

Equations

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

def Complexity.TM.Hoare {n : ℕ} (tm : TM n) (pre post : TapePred n) : Prop

Unbounded Hoare triple: the machine halts with tapes satisfying post, without a time bound. Useful when only correctness matters.

Equations

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

theorem Complexity.TM.HoareTime.consequence {n : ℕ} {tm : TM n} {pre pre' post post' : TapePred n} {b b' : ℕ} (h : tm.HoareTime pre post b) (hpre : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), pre' inp work out → pre inp work out) (hpost : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), post inp work out → post' inp work out) (hbound : b ≤ b') : tm.HoareTime pre' post' b'

Consequence rule: weaken the precondition and strengthen the postcondition.

theorem Complexity.TM.HoareTime.weaken_pre {n : ℕ} {tm : TM n} {pre pre' post : TapePred n} {b : ℕ} (h : tm.HoareTime pre post b) (hpre : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), pre' inp work out → pre inp work out) : tm.HoareTime pre' post b

Precondition weakening: if pre' implies pre, lift the Hoare triple.

theorem Complexity.TM.HoareTime.strengthen_post {n : ℕ} {tm : TM n} {pre post post' : TapePred n} {b : ℕ} (h : tm.HoareTime pre post b) (hpost : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), post inp work out → post' inp work out) : tm.HoareTime pre post' b

Postcondition strengthening: if post implies post', lift the triple.

theorem Complexity.TM.HoareTime.mono_bound {n : ℕ} {tm : TM n} {pre post : TapePred n} {b b' : ℕ} (h : tm.HoareTime pre post b) (hle : b ≤ b') : tm.HoareTime pre post b'

Time monotonicity: increase the time bound.

theorem Complexity.TM.HoareTime.toHoare {n : ℕ} {tm : TM n} {pre post : TapePred n} {b : ℕ} (h : tm.HoareTime pre post b) : tm.Hoare pre post

Bounded implies unbounded.

theorem Complexity.TM.hoareTime_of_decidesInTime {n : ℕ} {tm : TM n} {L : Language} {T : ℕ → ℕ} (h : tm.DecidesInTime L T) (x : List Bool) : tm.HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = Tape.init (List.map Γ.ofBool x) ∧ (work = fun (x : Fin n) => Tape.init []) ∧ out = Tape.init []) (fun (x_1 : Tape) (x_2 : Fin n → Tape) (out : Tape) => (x ∈ L → out.cells 1 = Γ.one) ∧ (x ∉ L → out.cells 1 = Γ.zero)) (T x.length)

DecidesInTime implies a family of Hoare triples, one per input.

@[reducible, inline]

abbrev Complexity.NTM.TapePred (n : ℕ) : Type

A predicate on the tape configuration: input tape, work tapes, output tape.

Equations

• Complexity.NTM.TapePred n = Complexity.TapePred n

def Complexity.NTM.HoareTime {n : ℕ} (tm : NTM n) (pre post : TapePred n) (bound : ℕ) : Prop

Time-bounded Hoare triple for nondeterministic machines: every choice sequence of the given length reaches a halted configuration satisfying post. NTM.trace already keeps halted configurations fixed, so this also covers machines that halt earlier than the bound.

Equations

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

theorem Complexity.NTM.HoareTime.consequence {n : ℕ} {tm : NTM n} {pre pre' post post' : TapePred n} {b : ℕ} (h : tm.HoareTime pre post b) (hpre : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), pre' inp work out → pre inp work out) (hpost : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), post inp work out → post' inp work out) : tm.HoareTime pre' post' b

Consequence rule for NTM Hoare triples.

theorem Complexity.NTM.HoareTime.weaken_pre {n : ℕ} {tm : NTM n} {pre pre' post : TapePred n} {b : ℕ} (h : tm.HoareTime pre post b) (hpre : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), pre' inp work out → pre inp work out) : tm.HoareTime pre' post b

Precondition weakening for NTM Hoare triples.

theorem Complexity.NTM.HoareTime.strengthen_post {n : ℕ} {tm : NTM n} {pre post post' : TapePred n} {b : ℕ} (h : tm.HoareTime pre post b) (hpost : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), post inp work out → post' inp work out) : tm.HoareTime pre post' b

Postcondition strengthening for NTM Hoare triples.

theorem Complexity.NTM.HoareTime.mono_bound {n : ℕ} {tm : NTM n} {pre post : TapePred n} {b b' : ℕ} (h : tm.HoareTime pre post b) (hle : b ≤ b') : tm.HoareTime pre post b'

Time monotonicity for NTM Hoare triples. Since NTM.trace is fixed after halting, a proof for b steps also gives a proof for any larger bound.

theorem Complexity.NTM.HoareTime.consequence_bound {n : ℕ} {tm : NTM n} {pre pre' post post' : TapePred n} {b b' : ℕ} (h : tm.HoareTime pre post b) (hpre : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), pre' inp work out → pre inp work out) (hpost : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), post inp work out → post' inp work out) (hbound : b ≤ b') : tm.HoareTime pre' post' b'

Consequence rule plus time-bound weakening for NTM Hoare triples.

theorem Complexity.NTM.exists_first_halt_time_of_trace_halted {n : ℕ} (tm : NTM n) (T : ℕ) (choices : Fin T → Bool) (c : Cfg n tm.Q) (hhalt : tm.halted (tm.trace T choices c)) : ∃ (t : ℕ) (ht : t ≤ T), tm.halted (tm.trace t (fun (i : Fin t) => choices (Fin.castLE ht i)) c) ∧ ∀ (s : ℕ) (hs : s < t), ¬tm.halted (tm.trace s (fun (i : Fin s) => choices (Fin.castLE ⋯ i)) c)

If a finite NTM trace is halted at time T, then it has a least halted prefix time. This is useful for phase-composed machines: Hoare-time facts give halting by a fixed bound, while phase exits need the first local halt time.

theorem Complexity.NTM.HoareTime.exists_first_halt_time {n : ℕ} {tm : NTM n} {pre post : TapePred n} {bound : ℕ} (h : tm.HoareTime pre post bound) {inp : Tape} {work : Fin n → Tape} {out : Tape} (hpre : pre inp work out) (choices : Fin bound → Bool) : ∃ (t : ℕ) (ht : t ≤ bound), tm.halted (tm.trace t (fun (i : Fin t) => choices (Fin.castLE ht i)) { state := tm.qstart, input := inp, work := work, output := out }) ∧ ∀ (s : ℕ) (hs : s < t), ¬tm.halted (tm.trace s (fun (i : Fin s) => choices (Fin.castLE ⋯ i)) { state := tm.qstart, input := inp, work := work, output := out })

Hoare-time corollary of exists_first_halt_time_of_trace_halted: every all-path halting proof yields a least halting prefix for each fixed choice sequence.

theorem Complexity.NTM.HoareTime.exists_first_halt_time_with_post {n : ℕ} {tm : NTM n} {pre post : TapePred n} {bound : ℕ} (h : tm.HoareTime pre post bound) {inp : Tape} {work : Fin n → Tape} {out : Tape} (hpre : pre inp work out) (choices : Fin bound → Bool) : ∃ (t : ℕ) (ht : t ≤ bound), have c0 := { state := tm.qstart, input := inp, work := work, output := out }; tm.halted (tm.trace t (fun (i : Fin t) => choices (Fin.castLE ht i)) c0) ∧ post (tm.trace t (fun (i : Fin t) => choices (Fin.castLE ht i)) c0).input (tm.trace t (fun (i : Fin t) => choices (Fin.castLE ht i)) c0).work (tm.trace t (fun (i : Fin t) => choices (Fin.castLE ht i)) c0).output ∧ ∀ (s : ℕ) (hs : s < t), ¬tm.halted (tm.trace s (fun (i : Fin s) => choices (Fin.castLE ⋯ i)) c0)

Hoare-time first-halt extraction, preserving the Hoare postcondition at the first halted prefix.

theorem Complexity.TM.HoareTime.toNTM {n : ℕ} {tm : TM n} {pre post : TapePred n} {b : ℕ} (h : tm.HoareTime pre post b) : tm.toNTM.HoareTime pre post b

A deterministic Hoare triple lifts to an NTM Hoare triple for TM.toNTM. The bound is unchanged because toNTM ignores the choice bit.