Length tests and bitwise operations inside the algebra

Two utilities the algebra needs for block-structured data: comparing the lengths of two strings, and taking the bitwise exclusive-or of two strings of equal length.

Both are built from the dispatchers of Complexitylib.Classes.P.Cobham.Internal.Blocks: a length comparison is a drop followed by an emptiness test, and the exclusive-or is one limited recursion whose step reads the matching bit of the second argument through a ruler cut to the right width.

Main definitions

• Cobham.lenLeFlag, Cobham.lenEqFlag — length comparison flags
• Cobham.xorSuffix — exclusive-or of a string with the matching suffix of a second string

Main results

• Cobham.lenLeFlag_eq_true_iff, Cobham.lenEqFlag_eq_true_iff
• Cobham.lenLeFlag_mem, Cobham.lenEqFlag_mem
• Cobham.andBit_eq_true_iff — conjunction of flags

theorem Complexity.Cobham.andBit_eq_true_iff {x y : List Bool} (hx : x = [true] ∨ x = [false]) (hy : y = [true] ∨ y = [false]) : andBit x y = [true] ↔ x = [true] ∧ y = [true]

Conjunction of two flags is [true] exactly when both are.

theorem Complexity.Cobham.orBit_eq_true_iff {x y : List Bool} (hx : x = [true] ∨ x = [false]) (hy : y = [true] ∨ y = [false]) : orBit x y = [true] ↔ x = [true] ∨ y = [true]

Disjunction of two flags is [true] exactly when one is.

theorem Complexity.Cobham.orBit_flag {x y : List Bool} (hx : x = [true] ∨ x = [false]) (hy : y = [true] ∨ y = [false]) : orBit x y = [true] ∨ orBit x y = [false]

Disjunction of flags is a flag.

theorem Complexity.Cobham.orBit_length (x y : List Bool) : (orBit x y).length = 1

A disjunction is always exactly one bit long.

theorem Complexity.Cobham.notBit_eq_true_iff {x : List Bool} (hx : x = [true] ∨ x = [false]) : notBit x = [true] ↔ x = [false]

Negation of a flag.

def Complexity.Cobham.lenLeFlag (a b : List Bool) : List Bool

The flag |b| ≤ |a|: nothing is left of b after dropping |a| bits.

Equations

• Complexity.Cobham.lenLeFlag a b = Complexity.notBit (Complexity.nonemptyFlag (List.drop a.length b))

def Complexity.Cobham.lenEqFlag (a b : List Bool) : List Bool

The flag |a| = |b|.

Equations

• Complexity.Cobham.lenEqFlag a b = Complexity.andBit (Complexity.Cobham.lenLeFlag a b) (Complexity.Cobham.lenLeFlag b a)

theorem Complexity.Cobham.lenLeFlag_flag (a b : List Bool) : lenLeFlag a b = [true] ∨ lenLeFlag a b = [false]

@[simp]

theorem Complexity.Cobham.lenLeFlag_eq_true_iff (a b : List Bool) : lenLeFlag a b = [true] ↔ b.length ≤ a.length

theorem Complexity.Cobham.lenEqFlag_flag (a b : List Bool) : lenEqFlag a b = [true] ∨ lenEqFlag a b = [false]

@[simp]

theorem Complexity.Cobham.lenEqFlag_eq_true_iff (a b : List Bool) : lenEqFlag a b = [true] ↔ a.length = b.length

theorem Complexity.Cobham.lenLeFlag_mem {n : ℕ} {ga gb : (Fin n → List Bool) → List Bool} (ha : Cobham ga) (hb : Cobham gb) : Cobham fun (v : Fin n → List Bool) => lenLeFlag (ga v) (gb v)

The length tests are in the algebra.

theorem Complexity.Cobham.lenEqFlag_mem {n : ℕ} {ga gb : (Fin n → List Bool) → List Bool} (ha : Cobham ga) (hb : Cobham gb) : Cobham fun (v : Fin n → List Bool) => lenEqFlag (ga v) (gb v)

Exclusive-or

def Complexity.Cobham.xorSuffix : List Bool → List Bool → List Bool

Exclusive-or of a with the suffix of b of the same length. The bit of b paired with the head of a sits at index |b| - |x| - 1, which is the length of b.drop (|x| + 1) — a ruler the algebra can build from the recursion's own tail.

Equations

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

@[simp]

theorem Complexity.Cobham.xorSuffix_nil (b : List Bool) : xorSuffix [] b = []

@[simp]

theorem Complexity.Cobham.xorSuffix_length (a b : List Bool) : (xorSuffix a b).length = a.length

theorem Complexity.Cobham.xorSuffix_eq_zipWith (a b : List Bool) (h : a.length ≤ b.length) : xorSuffix a b = List.zipWith xor a (List.drop (b.length - a.length) b)

The exclusive-or is the pointwise one against the matching suffix.

theorem Complexity.Cobham.xorSuffix_eq_zipWith_of_length (a b : List Bool) (h : a.length = b.length) : xorSuffix a b = List.zipWith xor a b

Two strings of equal length are combined bit by bit.

theorem Complexity.Cobham.xorSuffix_mem {n : ℕ} {ga gb : (Fin n → List Bool) → List Bool} (ha : Cobham ga) (hb : Cobham gb) : Cobham fun (v : Fin n → List Bool) => xorSuffix (ga v) (gb v)

The exclusive-or is in the algebra.

Equality of strings

def Complexity.Cobham.allZeroFlag : List Bool → List Bool

Flag: every bit of x is false.

Equations

• Complexity.Cobham.allZeroFlag [] = [true]
• Complexity.Cobham.allZeroFlag (true :: tail) = [false]
• Complexity.Cobham.allZeroFlag (false :: x_1) = Complexity.Cobham.allZeroFlag x_1

@[simp]

theorem Complexity.Cobham.allZeroFlag_nil : allZeroFlag [] = [true]

theorem Complexity.Cobham.allZeroFlag_flag (x : List Bool) : allZeroFlag x = [true] ∨ allZeroFlag x = [false]

@[simp]

theorem Complexity.Cobham.allZeroFlag_eq_true_iff (x : List Bool) : allZeroFlag x = [true] ↔ ∀ b ∈ x, b = false

theorem Complexity.Cobham.allZeroFlag_mem_one : Cobham fun (v : Fin 1 → List Bool) => allZeroFlag (v 0)

The all-zero test is in the algebra.

theorem Complexity.Cobham.allZeroFlag_mem {n : ℕ} {g : (Fin n → List Bool) → List Bool} (hg : Cobham g) : Cobham fun (v : Fin n → List Bool) => allZeroFlag (g v)

def Complexity.Cobham.eqFlag (a b : List Bool) : List Bool

Flag: the two strings are equal.

Equations

• Complexity.Cobham.eqFlag a b = Complexity.andBit (Complexity.Cobham.lenEqFlag a b) (Complexity.Cobham.allZeroFlag (Complexity.Cobham.xorSuffix a b))

theorem Complexity.Cobham.eqFlag_flag (a b : List Bool) : eqFlag a b = [true] ∨ eqFlag a b = [false]

@[simp]

theorem Complexity.Cobham.eqFlag_eq_true_iff (a b : List Bool) : eqFlag a b = [true] ↔ a = b

theorem Complexity.Cobham.eqFlag_mem {n : ℕ} {ga gb : (Fin n → List Bool) → List Bool} (ha : Cobham ga) (hb : Cobham gb) : Cobham fun (v : Fin n → List Bool) => eqFlag (ga v) (gb v)

String equality is in the algebra.