What the block scanners compute — proof internals #

The two total parsers of a self-delimiting block — Cobham.fstBlock decodes the leading block's payload, Cobham.sndBlock returns the suffix after it — and the control states their scanners share. Complexity.pairSplitCoreTM handles only valid pair inputs, so the total decoders need machines of their own; those are Internal.SndBlock, Internal.FstBlock and Internal.Cat, one per machine.

source

def Complexity.Cobham.fstBlock :

List Bool → List Bool

Decode the payload of the leading self-delimiting block: read doubled bits until the [false, true] separator. On a valid pair pair x y this returns x (see fstBlock_pair); on malformed input it returns the bits decoded so far. This total, incremental form is what the fstBlockTM scanner computes.

Equations

Instances For

source

def Complexity.Cobham.sndBlock (z : List Bool) :

List Bool

Take the suffix after the leading self-delimiting block (the second unpair? component), or [] if the input is not a valid block. On encodeVec of a nonempty vector this returns the head component v 0.

Equations

Complexity.Cobham.sndBlock z = match Complexity.unpair? z with | some (fst, s) => s | none => []

Instances For

source

@[simp]

theorem Complexity.Cobham.fstBlock_pair (x y : List Bool) :

fstBlock (pair x y) = x

source

@[simp]

theorem Complexity.Cobham.sndBlock_pair (x y : List Bool) :

sndBlock (pair x y) = y

source

theorem Complexity.Cobham.fstBlock_encodeVec_succ {n : ℕ} (v : Fin (n + 1) → List Bool) :

fstBlock (encodeVec v) = encodeVec (Fin.tail v)

Stripping the head component of an encoded vector yields the encoded tail. (Not a simp lemma: simp already reaches this via encodeVec_succ and fstBlock_pair.)

source