Testing a leading bit — proof internals

Every other FP primitive the Cobham proof uses — Complexity.takeLen, List.reverse, Complexity.pair, Cobham.mulUnpair — fixes its output's length from its inputs' lengths alone, so none of them can react to a bit's value. Complexity.headFlag closes that gap by turning a bit test into a length: the answer is carried by whether the result is empty. Its two-state transducer moves off the left-end marker, then emits one bit exactly when the first input bit matches.

Main results

• Complexity.headFlag_mem_FP — the leading-bit test is in FP

def Complexity.headFlag (target : Bool) (x : List Bool) : List Bool

[false] when x begins with target, and [] otherwise: a bit test whose answer is carried by the length of the result.

Equations

• Complexity.headFlag target x = if x.head? = some target then [false] else []

inductive Complexity.HeadPhase : Type

Control states of the head-bit flag machine.

• skip : HeadPhase

  Advance past the left-end markers.

• test : HeadPhase

  Read the first input bit.

• done : HeadPhase

  Halted.

@[implicit_reducible]

instance Complexity.instDecidableEqHeadPhase : DecidableEq HeadPhase

Equations

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

@[implicit_reducible]

instance Complexity.instFintypeHeadPhase : Fintype HeadPhase

Equations

• Complexity.instFintypeHeadPhase = { elems := {Complexity.HeadPhase.skip, Complexity.HeadPhase.test, Complexity.HeadPhase.done}, complete := ⋯ }

def Complexity.headFlagTM (target : Bool) : TM 0

Read the first input bit and emit one output bit exactly when it is target. Two steps: skip moves off the left-end markers, test reads the bit and either writes or not.

Equations

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

theorem Complexity.headFlagTM_computesInTime (target : Bool) : (headFlagTM target).ComputesInTime (headFlag target) fun (x : ℕ) => 2

headFlagTM target computes headFlag target in two steps.

theorem Complexity.headFlag_mem_FP (target : Bool) : headFlag target ∈ FP

A bit test, as a length.