Hoare-style composition rules for TM combinators

This file provides Hoare-triple composition rules for all four TM combinators. Each rule specifies how pre/postconditions and time bounds compose.

Main results

• seqTM_hoareTime — sequential composition: time b₁ + 1 + b₂
• phaseTransition_eq_self_of_reads_ne_start — identify a stable phase boundary
• complementTM_hoareTime — complement flips output cell 1: time b + p_bound + 4
• ifTM_hoareTime — if-then-else branching: time b_test + p_bound + max b_then b_else + 5
• loopTM_hoareTime — loop invariant with variant: time (k + 1) * b_iter

Tape transition effects

All combinators apply transitionTape / transitionInput at phase boundaries. A current read other than ▷ is exactly what their fixed-point rules require; parked tapes, or AllTapesWF together with positive-head facts, provide common stronger certificates.

theorem Complexity.TM.seqTM_hoareTime {n : ℕ} (tm₁ tm₂ : TM n) {pre mid mid' post : TapePred n} {b₁ b₂ : ℕ} (h₁ : tm₁.HoareTime pre mid b₁) (h_trans : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), mid inp work out → mid' (transitionInput inp) (fun (i : Fin n) => transitionTape (work i)) (transitionTape out)) (h₂ : tm₂.HoareTime mid' post b₂) : (tm₁.seqTM tm₂).HoareTime pre post (b₁ + 1 + b₂)

Sequential composition of Hoare triples.

theorem Complexity.TM.phaseTransition_eq_self_of_reads_ne_start {n : ℕ} {inp out : Tape} {work : Fin n → Tape} (hinput : inp.read ≠ Γ.start) (hwork : ∀ (i : Fin n), (work i).read ≠ Γ.start) (houtput : out.read ≠ Γ.start) : transitionInput inp = inp ∧ (fun (i : Fin n) => transitionTape (work i)) = work ∧ transitionTape out = out

The input, work family, and output transition maps are jointly the identity when every tape is reading something other than the left-end marker. This shared read-local boundary certificate matches the transition shape accepted by both time-only and time-space sequential composition; it deliberately does not require parked heads or global tape well-formedness.

def Complexity.TM.AllTapesWF {n : ℕ} (inp : Tape) (work : Fin n → Tape) (out : Tape) : Prop

Well-formedness condition on all tapes: cells 0 = start and cells ≥ 1 ≠ start.

Equations

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

theorem Complexity.TM.AllTapesWF.transition {n : ℕ} {inp : Tape} {work : Fin n → Tape} {out : Tape} (h : AllTapesWF inp work out) : (transitionInput inp).head ≥ 1 ∧ (∀ j ≥ 1, (transitionInput inp).cells j ≠ Γ.start) ∧ (∀ (i : Fin n), (transitionTape (work i)).head ≥ 1) ∧ (∀ (i : Fin n), ∀ j ≥ 1, (transitionTape (work i)).cells j ≠ Γ.start) ∧ (transitionTape out).cells = out.cells ∧ (transitionTape out).head ≥ 1

AllTapesWF is preserved through the standard combinator phase transition (transitionTape / transitionInput).

theorem Complexity.TM.complementTM_hoareTime {n : ℕ} (tm : TM n) {pre : TapePred n} {b p_bound : ℕ} {cell1_pred : Γ → Prop} (h_tm : tm.HoareTime pre (fun (x : Tape) (x_1 : Fin n → Tape) (out : Tape) => out.cells 0 = Γ.start ∧ (∀ j ≥ 1, out.cells j ≠ Γ.start) ∧ out.head ≤ p_bound ∧ cell1_pred (out.cells 1)) b) : tm.complementTM.HoareTime pre (fun (x : Tape) (x_1 : Fin n → Tape) (out : Tape) => ∃ (g : Γ), cell1_pred g ∧ out.cells 1 = (flipBit g).toΓ) (b + p_bound + 4)

Complement Hoare triple. If tm satisfies a Hoare triple whose postcondition provides output WF (for rewind), a head bound, and a property of output cell 1, then complementTM tm satisfies a triple where output cell 1 is flipped. Time: b + p_bound + 4.

theorem Complexity.TM.ifTM_hoareTime {n : ℕ} (tmTest tmThen tmElse : TM n) {pre mid_test mid_then mid_else post_then post_else post : TapePred n} {b_test b_then b_else p_bound : ℕ} (h_test : tmTest.HoareTime pre mid_test b_test) (h_wf : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), mid_test inp work out → AllTapesWF inp work out) (h_head : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), mid_test inp work out → out.head ≤ p_bound) (h_to_then : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), mid_test inp work out → out.cells 1 = Γ.one → mid_then (transitionInput inp) (fun (i : Fin n) => transitionTape (work i)) { head := 1, cells := out.cells }) (h_to_else : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), mid_test inp work out → out.cells 1 ≠ Γ.one → mid_else (transitionInput inp) (fun (i : Fin n) => transitionTape (work i)) { head := 1, cells := out.cells }) (h_then : tmThen.HoareTime mid_then post_then b_then) (h_else : tmElse.HoareTime mid_else post_else b_else) (h_post_then : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), post_then inp work out → post (transitionInput inp) (fun (i : Fin n) => transitionTape (work i)) (transitionTape out)) (h_post_else : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), post_else inp work out → post (transitionInput inp) (fun (i : Fin n) => transitionTape (work i)) (transitionTape out)) : (tmTest.ifTM tmThen tmElse).HoareTime pre post (b_test + p_bound + max b_then b_else + 5)

If-then-else Hoare triple. Composes test, then-branch, and else-branch Hoare triples. The test postcondition must include AllTapesWF (for rewind) and a head bound. Branch routing maps the test postcondition to the branch precondition on transitioned tapes (output gets head = 1, cells preserved).

Time: b_test + p_bound + max b_then b_else + 5 (test + transition + rewind + check + branch + halt).

theorem Complexity.TM.loopTM_hoareTime {n : ℕ} (tmBody tmTest : TM n) {inv post : TapePred n} {b_iter k : ℕ} {variant : Tape → (Fin n → Tape) → Tape → ℕ} (h_variant_bound : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), inv inp work out → variant inp work out ≤ k) (h_iter : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), inv inp work out → (∃ (c' : Cfg n (tmBody.loopTM tmTest).Q), ∃ t ≤ b_iter, (tmBody.loopTM tmTest).reachesIn t { state := (tmBody.loopTM tmTest).qstart, input := inp, work := work, output := out } c' ∧ (tmBody.loopTM tmTest).halted c' ∧ post c'.input c'.work c'.output) ∨ ∃ (inp' : Tape) (work' : Fin n → Tape) (out' : Tape), ∃ t ≤ b_iter, (tmBody.loopTM tmTest).reachesIn t { state := (tmBody.loopTM tmTest).qstart, input := inp, work := work, output := out } { state := (tmBody.loopTM tmTest).qstart, input := inp', work := work', output := out' } ∧ inv inp' work' out' ∧ variant inp' work' out' < variant inp work out) : (tmBody.loopTM tmTest).HoareTime inv post ((k + 1) * b_iter)

Loop invariant rule. Each iteration (≤ b_iter steps) either halts with post or returns to the loop start with inv preserved and variant decreased. The variant is bounded by k under inv, giving total time (k + 1) * b_iter.