Blocks, flags, and bit dispatch — proof internals

The string toolkit the simulation of a machine inside Cobham's algebra is written in. None of it appears in the statement of CobhamFP_eq_FP; it is the vocabulary of the proof.

• Dispatch — Complexity.caseBit selects on a leading bit and returns nothing on the empty string; Complexity.caseBit₀ reads "no bit" as false. Both are needed: the partial one to read off the end of a string, the total one so that a flag (a one-bit string) is always genuinely one bit.
• Flags — Complexity.andBit, orBit, notBit, bitAt, Complexity.nonemptyFlag and Complexity.matchPrefix, the Boolean layer a machine's finite transition table is written in. matchPrefix unfolds into |c| bit tests for each fixed constant c, so it is a finite composition — the induction is at the meta level, not inside the algebra.
• Blocks — Complexity.padTo pads a field to one ruler's width and Complexity.blockAt reads field i back, so a packed configuration needs no self-delimiting decoder inside the algebra. The padding algebra (padTo_append_padTo, take_padTo, drop_padTo, padTo_drop) says that re-padding commutes with the edits a simulated step performs.

def Complexity.caseBit (s x y : List Bool) : List Bool

Bit dispatch: select x or y according to the leading bit of s, returning the empty string when s is empty.

This is the branching primitive of the algebra. It is definable by a single limited recursion on notation (Cobham.caseBit) because the step functions of recNotation are already selected by the bit being peeled — dispatching on a bit costs nothing beyond the recursion that is there anyway.

Equations

• Complexity.caseBit [] x y = []
• Complexity.caseBit (b :: tail) x y = bif b then x else y

@[simp]

theorem Complexity.caseBit_nil (x y : List Bool) : caseBit [] x y = []

@[simp]

theorem Complexity.caseBit_cons (b : Bool) (s x y : List Bool) : caseBit (b :: s) x y = bif b then x else y

theorem Complexity.caseBit_length_le (s x y : List Bool) : (caseBit s x y).length ≤ (x ++ y).length

Bit dispatch never returns more than its two branches together.

def Complexity.caseBit₀ (s x y : List Bool) : List Bool

Total bit dispatch: like caseBit, but the empty string selects the false branch instead of returning nothing.

Both variants are needed. caseBit is the partial reader used when running off the end of a string must produce nothing (Cobham.takePrefix reads bits this way); caseBit₀ is the total one used for Boolean logic, where "no bit" has to mean false so that flags are always exactly [true] or [false].

Equations

• Complexity.caseBit₀ [] x y = y
• Complexity.caseBit₀ (b :: tail) x y = bif b then x else y

@[simp]

theorem Complexity.caseBit₀_nil (x y : List Bool) : caseBit₀ [] x y = y

@[simp]

theorem Complexity.caseBit₀_cons (b : Bool) (s x y : List Bool) : caseBit₀ (b :: s) x y = bif b then x else y

theorem Complexity.caseBit₀_length_le (s x y : List Bool) : (caseBit₀ s x y).length ≤ (x ++ y).length

Total bit dispatch never returns more than its two branches together.

Flags

A flag is a one-bit string, [true] or [false]. The connectives below are each one caseBit₀, so they are in the algebra as soon as caseBit₀ is, and they are how the finite case analysis of a machine's transition function gets written inside it. Because they are built on the total dispatcher, every flag these produce is genuinely one bit — never empty — so they compose.

def Complexity.andBit (x y : List Bool) : List Bool

Conjunction of flags.

Equations

• Complexity.andBit x y = Complexity.caseBit₀ x (Complexity.caseBit₀ y [true] [false]) [false]

def Complexity.orBit (x y : List Bool) : List Bool

Disjunction of flags.

Equations

• Complexity.orBit x y = Complexity.caseBit₀ x [true] (Complexity.caseBit₀ y [true] [false])

def Complexity.notBit (x : List Bool) : List Bool

Negation of a flag.

Equations

• Complexity.notBit x = Complexity.caseBit₀ x [false] [true]

def Complexity.bitAt (r x : List Bool) : List Bool

The bit of x at the position marked by the ruler r, as a flag; false when the position is past the end of x.

Equations

• Complexity.bitAt r x = Complexity.caseBit₀ (List.drop r.length x) [true] [false]

@[simp]

theorem Complexity.bitAt_nil_left (x : List Bool) : bitAt [] x = caseBit₀ x [true] [false]

theorem Complexity.bitAt_length (r x : List Bool) : (bitAt r x).length = 1

A flag is exactly one bit long.

def Complexity.padTo (r x : List Bool) : List Bool

Pad (or truncate) x to exactly the width of the ruler r, filling with zeros.

Fixed-width blocks are how a simulated machine's configuration is packed into the single string a member of the class returns: every field occupies |r| bits, so field i is recovered by dropping i rulers and taking one — no self-delimiting decoder is needed inside the algebra.

Equations

• Complexity.padTo r x = List.take r.length (x ++ List.replicate r.length false)

@[simp]

theorem Complexity.padTo_length (r x : List Bool) : (padTo r x).length = r.length

A padded block always has exactly the ruler's width.

theorem Complexity.padTo_eq_append (r x : List Bool) (h : x.length ≤ r.length) : padTo r x = x ++ List.replicate (r.length - x.length) false

Padding a short string appends zeros.

def Complexity.blockAt (r x : List Bool) (i : ℕ) : List Bool

The i-th block of x, when x is a concatenation of blocks each as wide as the ruler r.

Equations

• Complexity.blockAt r x i = List.take r.length (List.drop (i * r.length) x)

@[simp]

theorem Complexity.blockAt_zero_append (r a x : List Bool) (h : a.length = r.length) : blockAt r (a ++ x) 0 = a

Block zero of a block-aligned string is its first block.

theorem Complexity.blockAt_succ_append (r a x : List Bool) (h : a.length = r.length) (i : ℕ) : blockAt r (a ++ x) (i + 1) = blockAt r x i

Later blocks of a block-aligned string are the blocks of its tail.

Padding algebra

A simulated step reads a padded block, edits it, and re-pads. These three lemmas say that the padding is invisible to that: re-padding commutes with the edits, so the encoded step can be reasoned about on raw contents.

theorem Complexity.padTo_append_replicate (r z : List Bool) (m : ℕ) : padTo r (z ++ List.replicate m false) = padTo r z

Extra zero padding is invisible to padTo.

theorem Complexity.padTo_append_padTo (r y x : List Bool) (hx : x.length ≤ r.length) : padTo r (y ++ padTo r x) = padTo r (y ++ x)

Re-padding a padded block is the same as padding its raw content.

theorem Complexity.take_padTo (r x : List Bool) (n : ℕ) (hn : n ≤ x.length) (hx : x.length ≤ r.length) : List.take n (padTo r x) = List.take n x

Taking from within the content of a padded block ignores the padding.

theorem Complexity.drop_padTo (r x : List Bool) (n : ℕ) (hn : n ≤ x.length) (hx : x.length ≤ r.length) : List.drop n (padTo r x) = List.drop n x ++ List.replicate (r.length - x.length) false

Dropping from a padded block leaves the padding trailing at the end.

theorem Complexity.padTo_drop (r x : List Bool) (n : ℕ) (hn : n ≤ x.length) (hx : x.length ≤ r.length) : padTo r (List.drop n (padTo r x)) = padTo r (List.drop n x)

Dropping from a padded block and re-padding ignores the padding.

theorem Complexity.blockAt_flatten (r : List Bool) (bs : List (List Bool)) : (∀ (b : List Bool), b ∈ bs → b.length = r.length) → ∀ (i : ℕ) (hi : i < bs.length), blockAt r bs.flatten i = bs[i]

Reading a field out of a block-aligned record. When bs is a list of blocks all as wide as the ruler r, block i of their concatenation is bs[i]. This is what makes Cobham.blockFn a field accessor.

def Complexity.nonemptyFlag (x : List Bool) : List Bool

Flag: is x nonempty? The partial dispatcher returns [] on the empty string, and [] reads as false to the flag connectives — so this is the one place caseBit rather than caseBit₀ is what is wanted.

Without it matchPrefix could not tell "the head bit is 0" from "there is no head bit", and would report a match of [0] against [].

Equations

• Complexity.nonemptyFlag x = Complexity.caseBit x [true] [true]

@[simp]

theorem Complexity.nonemptyFlag_nil : nonemptyFlag [] = []

@[simp]

theorem Complexity.nonemptyFlag_cons (b : Bool) (x : List Bool) : nonemptyFlag (b :: x) = [true]

def Complexity.matchPrefix : List Bool → List Bool → List Bool

Flag: does x begin with the fixed constant c? Unfolds into |c| bit tests joined by andBit, so for each constant it is a finite composition — no recursion on notation is needed.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.matchPrefix [] x✝ = [true]

@[simp]

theorem Complexity.matchPrefix_nil (x : List Bool) : matchPrefix [] x = [true]

@[simp]

theorem Complexity.matchPrefix_cons (b : Bool) (c x : List Bool) : matchPrefix (b :: c) x = andBit (nonemptyFlag x) (andBit (bif b then bitAt [] x else notBit (bitAt [] x)) (matchPrefix c x.tail))

theorem Complexity.matchPrefix_append (c y : List Bool) : matchPrefix c (c ++ y) = [true]

A constant is matched by anything it prefixes.

theorem Complexity.matchPrefix_nil_right (b : Bool) (c : List Bool) : matchPrefix (b :: c) [] = [false]

Nothing but the empty constant matches the empty string. (Not a simp lemma: simp unfolds the left-hand side past this shape.)

theorem Complexity.andBit_flag (x y : List Bool) : andBit x y = [true] ∨ andBit x y = [false]

Conjunction always returns a genuine one-bit flag, whatever it is given.

theorem Complexity.matchPrefix_flag (c x : List Bool) : matchPrefix c x = [true] ∨ matchPrefix c x = [false]

The match test always returns a genuine one-bit flag.

theorem Complexity.matchPrefix_eq_true_iff (c x : List Bool) : matchPrefix c x = [true] ↔ c <+: x

The match test is exactly the prefix test. This is what makes a table of constant patterns behave like a case analysis: the entry whose pattern is a prefix of the key fires, and no other does.