Binary addition and comparison inside the polynomial-time algebra

⚠️ Unreviewed by Bolton

Complexitylib.Classes.Containments.Internal.SavitchBits builds a fixed-width counter in the algebra — increment and overflow. A search that accumulates counts needs more: to add two numbers and to compare them. Both are the same shape of computation, a single left-to-right scan over the two operands, and both are written twice here for the same reason the counter was: as a plain recursion, where the arithmetic is proved, and as a scan on a packed state, which is the shape Cobham.iterate_mem_FP iterates.

Numbers are little-endian, least significant bit first, and the two operands are the same width. Addition returns the carry out separately, so nothing is lost to wraparound.

Main definitions

• Complexity.addBitsLE — addition with carry, as a recursion
• Complexity.addBits, Complexity.addCarry — its two components
• Complexity.ltBitsLE, Complexity.ltFlag — comparison
• Complexity.strsOfLen, Complexity.strsLe — the strings of a given length, and up to it
• Complexity.nextStr, Complexity.strIdx — one counter enumerating every short string

Main results

• Complexity.addBitsLE_binValLE — the adder is correct
• Complexity.ltFlag_eq_true_iff — the comparator is correct
• Complexity.addBitsFn_mem_FP, Complexity.ltFlagFn_mem_FP — both are in FP
• Complexity.strsLe_eq_image — the enumeration hits every short string exactly once

The bit operations

def Complexity.majB (c b d : Bool) : Bool

The carry out of a full adder.

Equations

• Complexity.majB c b d = (c && b || (c && d || b && d))

def Complexity.sumB (c b d : Bool) : Bool

The sum bit of a full adder.

Equations

• Complexity.sumB c b d = (c ^^ b ^^ d)

theorem Complexity.majB_sumB (c b d : Bool) : (sumB c b d).toNat + 2 * (majB c b d).toNat = c.toNat + b.toNat + d.toNat

theorem Complexity.binValLE_cons (b : Bool) (w : List Bool) : binValLE (b :: w) = b.toNat + 2 * binValLE w

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

Exclusive or of two flags.

Equations

• Complexity.xorBit x y = Complexity.Cobham.selectHead x (Complexity.notBit y) y

def Complexity.majBit (x y z : List Bool) : List Bool

The carry out, on flags.

Equations

• Complexity.majBit x y z = Complexity.orBit (Complexity.andBit x y) (Complexity.orBit (Complexity.andBit x z) (Complexity.andBit y z))

def Complexity.sumBit (x y z : List Bool) : List Bool

The sum bit, on flags.

Equations

• Complexity.sumBit x y z = Complexity.xorBit (Complexity.xorBit x y) z

@[simp]

theorem Complexity.xorBit_flag (c d : Bool) : xorBit [c] [d] = [c ^^ d]

@[simp]

theorem Complexity.majBit_flag (c b d : Bool) : majBit [c] [b] [d] = [majB c b d]

@[simp]

theorem Complexity.sumBit_flag (c b d : Bool) : sumBit [c] [b] [d] = [sumB c b d]

def Complexity.bit1 (v : List Bool) : List Bool

The leading bit of a string, as a flag, reading past the end as zero.

Equations

• Complexity.bit1 v = List.take 1 (v ++ [false])

@[simp]

theorem Complexity.bit1_nil : bit1 [] = [false]

@[simp]

theorem Complexity.bit1_cons (d : Bool) (t : List Bool) : bit1 (d :: t) = [d]

theorem Complexity.bit1_eq (v : List Bool) : bit1 v = [v.headD false]

Addition as a recursion

def Complexity.addBitsLE : Bool → List Bool → List Bool → Bool × List Bool

Add two little-endian bitstrings with a carry in: the carry out and the sum bits. The second operand is read through headD/drop, so the two are stepped in lockstep.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.addBitsLE x✝¹ [] x✝ = (x✝¹, [])

@[simp]

theorem Complexity.addBitsLE_nil (c : Bool) (v : List Bool) : addBitsLE c [] v = (c, [])

theorem Complexity.addBitsLE_cons {d : Bool} (c b : Bool) (tu tv : List Bool) : addBitsLE c (b :: tu) (d :: tv) = ((addBitsLE (majB c b d) tu tv).1, sumB c b d :: (addBitsLE (majB c b d) tu tv).2)

@[simp]

theorem Complexity.addBitsLE_length (c : Bool) (u v : List Bool) : (addBitsLE c u v).2.length = u.length

theorem Complexity.addBitsLE_binValLE (c : Bool) (u v : List Bool) (h : v.length = u.length) : binValLE (addBitsLE c u v).2 + (addBitsLE c u v).1.toNat * 2 ^ u.length = binValLE u + binValLE v + c.toNat

The adder is correct.

Addition as a scan

def Complexity.addStep : List Bool × List Bool × List Bool × List Bool → List Bool × List Bool × List Bool × List Bool

One step of the addition scan: the carry, the bits emitted so far, and the two operands still to read.

Equations

• Complexity.addStep (c, acc, [], v) = (c, acc, [], v)
• Complexity.addStep (c, acc, b :: tu, v) = (Complexity.majBit c [b] (Complexity.bit1 v), acc ++ Complexity.sumBit c [b] (Complexity.bit1 v), tu, List.drop 1 v)

@[simp]

theorem Complexity.addStep_nil (c acc v : List Bool) : addStep (c, acc, [], v) = (c, acc, [], v)

theorem Complexity.addStep_flag (c b : Bool) (acc tu v : List Bool) : addStep ([c], acc, b :: tu, v) = ([majB c b (v.headD false)], acc ++ [sumB c b (v.headD false)], tu, List.drop 1 v)

theorem Complexity.addStep_iterate_run (c : Bool) (acc u v : List Bool) (h : v.length = u.length) : addStep^[u.length] ([c], acc, u, v) = ([(addBitsLE c u v).1], acc ++ (addBitsLE c u v).2, [], [])

The scan computes the sum.

theorem Complexity.addStep_iterate_length (c : Bool) (acc u v : List Bool) (n : ℕ) : (addStep^[n] ([c], acc, u, v)).1.length = 1 ∧ (addStep^[n] ([c], acc, u, v)).2.1.length + (addStep^[n] ([c], acc, u, v)).2.2.1.length ≤ acc.length + u.length ∧ (addStep^[n] ([c], acc, u, v)).2.2.2.length ≤ v.length

The scan never has more in hand than it started with.

The packed scan

def Complexity.addPack (c acc ru rv : List Bool) : List Bool

The packed scan state.

Equations

• Complexity.addPack c acc ru rv = Complexity.pair c (Complexity.pair acc (Complexity.pair ru rv))

@[simp]

theorem Complexity.addPack_length (c acc ru rv : List Bool) : (addPack c acc ru rv).length = 2 * c.length + 2 * acc.length + 2 * ru.length + rv.length + 6

def Complexity.addStepP (z : List Bool) : List Bool

One step of the packed scan.

Equations

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

theorem Complexity.addStepP_pack (c acc ru rv : List Bool) : addStepP (addPack c acc ru rv) = addPack (addStep (c, acc, ru, rv)).1 (addStep (c, acc, ru, rv)).2.1 (addStep (c, acc, ru, rv)).2.2.1 (addStep (c, acc, ru, rv)).2.2.2

The packed step is the unpacked step.

theorem Complexity.addStepP_iterate (s : List Bool × List Bool × List Bool × List Bool) (n : ℕ) : addStepP^[n] (addPack s.1 s.2.1 s.2.2.1 s.2.2.2) = addPack (addStep^[n] s).1 (addStep^[n] s).2.1 (addStep^[n] s).2.2.1 (addStep^[n] s).2.2.2

The packed iteration is the unpacked one.

theorem Complexity.addStepP_iterate_args (c acc ru rv : List Bool) (n : ℕ) : addStepP^[n] (addPack c acc ru rv) = addPack (addStep^[n] (c, acc, ru, rv)).1 (addStep^[n] (c, acc, ru, rv)).2.1 (addStep^[n] (c, acc, ru, rv)).2.2.1 (addStep^[n] (c, acc, ru, rv)).2.2.2

The verdicts

def Complexity.addRun (u v : List Bool) : List Bool

The packed addition run to completion.

Equations

• Complexity.addRun u v = Complexity.addStepP^[u.length] (Complexity.addPack [false] [] u v)

def Complexity.addBits (u v : List Bool) : List Bool

The sum bits of u and v.

Equations

• Complexity.addBits u v = Complexity.pairFst (Complexity.pairSnd (Complexity.addRun u v))

def Complexity.addCarry (u v : List Bool) : List Bool

The carry out of u + v.

Equations

• Complexity.addCarry u v = Complexity.pairFst (Complexity.addRun u v)

theorem Complexity.addRun_eq (u v : List Bool) (h : v.length = u.length) : addRun u v = addPack [(addBitsLE false u v).1] (addBitsLE false u v).2 [] []

@[simp]

theorem Complexity.addBits_eq (u v : List Bool) (h : v.length = u.length) : addBits u v = (addBitsLE false u v).2

@[simp]

theorem Complexity.addCarry_eq (u v : List Bool) (h : v.length = u.length) : addCarry u v = [(addBitsLE false u v).1]

theorem Complexity.addBits_binValLE (u v : List Bool) (h : v.length = u.length) (hc : addCarry u v = [false]) : binValLE (addBits u v) = binValLE u + binValLE v

What the packed addition computes.

theorem Complexity.addBits_length (u v : List Bool) (h : v.length = u.length) : (addBits u v).length = u.length

Addition is polynomial-time

theorem Complexity.addStepP_mem_FP : addStepP ∈ FP

theorem Complexity.addRunFn_mem_FP {a b : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) : (fun (z : List Bool) => addRun (a z) (b z)) ∈ FP

theorem Complexity.addBitsFn_mem_FP {a b : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) : (fun (z : List Bool) => addBits (a z) (b z)) ∈ FP

theorem Complexity.addCarryFn_mem_FP {a b : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) : (fun (z : List Bool) => addCarry (a z) (b z)) ∈ FP

Comparison as a recursion

def Complexity.ltBitsLE : Bool → List Bool → List Bool → Bool

Scan two little-endian bitstrings from the bottom, keeping the verdict of the highest position at which they have differed so far.

Equations

• Complexity.ltBitsLE x✝¹ [] x✝ = x✝¹
• Complexity.ltBitsLE x✝¹ (b :: tu) x✝ = Complexity.ltBitsLE (if b = x✝.headD false then x✝¹ else x✝.headD false) tu (List.drop 1 x✝)

@[simp]

theorem Complexity.ltBitsLE_nil (f : Bool) (v : List Bool) : ltBitsLE f [] v = f

theorem Complexity.ltBitsLE_cons (f b : Bool) (tu v : List Bool) : ltBitsLE f (b :: tu) v = ltBitsLE (if b = v.headD false then f else v.headD false) tu (List.drop 1 v)

theorem Complexity.ltBitsLE_spec (f : Bool) (u v : List Bool) (h : v.length = u.length) : ltBitsLE f u v = if binValLE u < binValLE v then true else if binValLE v < binValLE u then false else f

The comparator is correct.

Comparison as a scan

def Complexity.ltStep : List Bool × List Bool × List Bool → List Bool × List Bool × List Bool

One step of the comparison scan.

Equations

• Complexity.ltStep (f, [], v) = (f, [], v)
• Complexity.ltStep (f, b :: tu, v) = (Complexity.Cobham.selectHead (Complexity.Cobham.eqFlag [b] (Complexity.bit1 v)) f (Complexity.bit1 v), tu, List.drop 1 v)

@[simp]

theorem Complexity.ltStep_nil (f v : List Bool) : ltStep (f, [], v) = (f, [], v)

theorem Complexity.ltStep_flag (f b : Bool) (tu v : List Bool) : ltStep ([f], b :: tu, v) = ([if b = v.headD false then f else v.headD false], tu, List.drop 1 v)

theorem Complexity.ltStep_iterate_run (f : Bool) (u v : List Bool) (h : v.length = u.length) : ltStep^[u.length] ([f], u, v) = ([ltBitsLE f u v], [], [])

The scan computes the comparison.

theorem Complexity.ltStep_iterate_length (f : Bool) (u v : List Bool) (n : ℕ) : (ltStep^[n] ([f], u, v)).1.length = 1 ∧ (ltStep^[n] ([f], u, v)).2.1.length ≤ u.length ∧ (ltStep^[n] ([f], u, v)).2.2.length ≤ v.length

The packed comparison

def Complexity.ltPack (f ru rv : List Bool) : List Bool

The packed comparison state.

Equations

• Complexity.ltPack f ru rv = Complexity.pair f (Complexity.pair ru rv)

@[simp]

theorem Complexity.ltPack_length (f ru rv : List Bool) : (ltPack f ru rv).length = 2 * f.length + 2 * ru.length + rv.length + 4

def Complexity.ltStepP (z : List Bool) : List Bool

One step of the packed comparison.

Equations

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

theorem Complexity.ltStepP_pack (f ru rv : List Bool) : ltStepP (ltPack f ru rv) = ltPack (ltStep (f, ru, rv)).1 (ltStep (f, ru, rv)).2.1 (ltStep (f, ru, rv)).2.2

theorem Complexity.ltStepP_iterate (s : List Bool × List Bool × List Bool) (n : ℕ) : ltStepP^[n] (ltPack s.1 s.2.1 s.2.2) = ltPack (ltStep^[n] s).1 (ltStep^[n] s).2.1 (ltStep^[n] s).2.2

theorem Complexity.ltStepP_iterate_args (f ru rv : List Bool) (n : ℕ) : ltStepP^[n] (ltPack f ru rv) = ltPack (ltStep^[n] (f, ru, rv)).1 (ltStep^[n] (f, ru, rv)).2.1 (ltStep^[n] (f, ru, rv)).2.2

def Complexity.ltRun (u v : List Bool) : List Bool

The packed comparison run to completion.

Equations

• Complexity.ltRun u v = Complexity.ltStepP^[u.length] (Complexity.ltPack [false] u v)

def Complexity.ltFlag (u v : List Bool) : List Bool

Is u below v, as a flag.

Equations

• Complexity.ltFlag u v = Complexity.pairFst (Complexity.ltRun u v)

theorem Complexity.ltFlag_eq (u v : List Bool) (h : v.length = u.length) : ltFlag u v = [ltBitsLE false u v]

theorem Complexity.ltFlag_eq_true_iff (u v : List Bool) (h : v.length = u.length) : ltFlag u v = [true] ↔ binValLE u < binValLE v

The flag decides the comparison.

theorem Complexity.ltFlag_flag (u v : List Bool) (h : v.length = u.length) : ltFlag u v = [true] ∨ ltFlag u v = [false]

Comparison is polynomial-time

theorem Complexity.ltStepP_mem_FP : ltStepP ∈ FP

theorem Complexity.ltFlagFn_mem_FP {a b : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) : (fun (z : List Bool) => ltFlag (a z) (b z)) ∈ FP

The larger of two numbers

def Complexity.maxBits (u v : List Bool) : List Bool

The larger of two equal-width numbers.

Equations

• Complexity.maxBits u v = Complexity.Cobham.selectHead (Complexity.ltFlag u v) v u

theorem Complexity.maxBits_eq (u v : List Bool) (h : v.length = u.length) : maxBits u v = if binValLE u < binValLE v then v else u

theorem Complexity.maxBitsFn_mem_FP {a b : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) : (fun (z : List Bool) => maxBits (a z) (b z)) ∈ FP

Arithmetic without overflow

theorem Complexity.binValLE_addBits (u v : List Bool) (h : v.length = u.length) (hlt : binValLE u + binValLE v < 2 ^ u.length) : binValLE (addBits u v) = binValLE u + binValLE v

Adding below the width is exact.

theorem Complexity.binValLE_maxBits (u v : List Bool) (h : v.length = u.length) : binValLE (maxBits u v) = max (binValLE u) (binValLE v)

theorem Complexity.maxBits_length (u v : List Bool) (h : v.length = u.length) : (maxBits u v).length = u.length

theorem Complexity.bumpOver_eq_false_of_lt {w : List Bool} (h : binValLE w + 1 < 2 ^ w.length) : bumpOver w = false

Powers of two as bitstrings

theorem Complexity.binValLE_replicate_false (n : ℕ) : binValLE (List.replicate n false) = 0

theorem Complexity.padTo_nil (r : List Bool) : padTo r [] = List.replicate r.length false

theorem Complexity.binValLE_replicate_false_append (n : ℕ) (z : List Bool) : binValLE (List.replicate n false ++ z) = 2 ^ n * binValLE z

def Complexity.twoPowBits (t : ℕ) : List Bool

The bitstring of 2 ^ t, one bit wider than t bits so that it can be compared with a doubled t + 1-bit count.

Equations

• Complexity.twoPowBits t = List.replicate t false ++ [true, false]

@[simp]

theorem Complexity.twoPowBits_length (t : ℕ) : (twoPowBits t).length = t + 2

@[simp]

theorem Complexity.binValLE_twoPowBits (t : ℕ) : binValLE (twoPowBits t) = 2 ^ t

theorem Complexity.two_pow_lt_two_mul_iff (t : ℕ) (w : List Bool) (hw : w.length = t + 1) : 2 ^ t < 2 * binValLE w ↔ ltFlag (twoPowBits t) (false :: w) = [true]

The threshold comparison, as the algebra performs it. A count w of t + 1 bits exceeds half of 2 ^ t exactly when the doubled count is above 2 ^ t.

Selection on a literal flag

@[simp]

theorem Complexity.selectHead_cons_true (x y : List Bool) : Cobham.selectHead [true] x y = x

@[simp]

theorem Complexity.selectHead_cons_false (x y : List Bool) : Cobham.selectHead [false] x y = y

Emptiness and the leading bit

def Complexity.emptyFlag (y : List Bool) : List Bool

Is the string empty, as a flag.

Equations

• Complexity.emptyFlag y = Complexity.Cobham.lenLeFlag [] y

@[simp]

theorem Complexity.emptyFlag_nil : emptyFlag [] = [true]

theorem Complexity.emptyFlag_cons (b : Bool) (y : List Bool) : emptyFlag (b :: y) = [false]

theorem Complexity.emptyFlag_pair (a b : List Bool) : emptyFlag (pair a b) = [false]

theorem Complexity.emptyFlagFn_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => emptyFlag (a z)) ∈ FP

def Complexity.dropOne (y : List Bool) : List Bool

Drop the leading bit.

Equations

• Complexity.dropOne y = List.drop 1 y

theorem Complexity.dropOneFn_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => dropOne (a z)) ∈ FP

The strings of a given length

def Complexity.strsOfLen (ℓ : ℕ) : Finset (List Bool)

The bitstrings of length exactly ℓ.

Equations

• Complexity.strsOfLen ℓ = Finset.image (Complexity.bitsOfLenLE ℓ) (Finset.range (2 ^ ℓ))

@[simp]

theorem Complexity.mem_strsOfLen {ℓ : ℕ} {l : List Bool} : l ∈ strsOfLen ℓ ↔ l.length = ℓ

def Complexity.strsLe (m : ℕ) : Finset (List Bool)

The bitstrings of length at most m.

Equations

• Complexity.strsLe m = (Finset.range (m + 1)).biUnion Complexity.strsOfLen

@[simp]

theorem Complexity.mem_strsLe {m : ℕ} {l : List Bool} : l ∈ strsLe m ↔ l.length ≤ m

theorem Complexity.strsLe_nonempty (m : ℕ) : (strsLe m).Nonempty

Enumerating every short string with one counter

A search that sums over all strings of length at most m must visit each exactly once. One counter suffices: order the strings by length and then by value, so the successor of the all-ones string of length ℓ is the all-zeros string of length ℓ + 1. The position of a string in that order is Complexity.strIdx, and it increases by one at every step, which is what makes the enumeration a bijection.

def Complexity.strIdx (w : List Bool) : ℕ

The position of a string in the order: by length first, then by value.

Equations

• Complexity.strIdx w = 2 ^ w.length - 1 + Complexity.binValLE w

def Complexity.nextStr (w : List Bool) : List Bool

The next string in the order.

Equations

• Complexity.nextStr w = if Complexity.bumpOver w = true then List.replicate (w.length + 1) false else Complexity.bumpBits w

@[simp]

theorem Complexity.strIdx_nil : strIdx [] = 0

theorem Complexity.strIdx_lower (w : List Bool) : 2 ^ w.length - 1 ≤ strIdx w

theorem Complexity.strIdx_upper (w : List Bool) : strIdx w + 2 ≤ 2 ^ (w.length + 1)

theorem Complexity.strIdx_nextStr (w : List Bool) : strIdx (nextStr w) = strIdx w + 1

The counter steps one place along the order.

theorem Complexity.strIdx_iterate (i : ℕ) : strIdx (nextStr^[i] []) = i

theorem Complexity.strIdx_injective {w w' : List Bool} (h : strIdx w = strIdx w') : w = w'

theorem Complexity.strIdx_lt_iff (m : ℕ) (w : List Bool) : strIdx w < 2 ^ (m + 1) - 1 ↔ w.length ≤ m

theorem Complexity.strsLe_eq_image (m : ℕ) : strsLe m = Finset.image (fun (i : ℕ) => nextStr^[i] []) (Finset.range (2 ^ (m + 1) - 1))

The counter enumerates every short string exactly once.

theorem Complexity.nextStr_injOn (m : ℕ) : Set.InjOn (fun (i : ℕ) => nextStr^[i] []) ↑(Finset.range (2 ^ (m + 1) - 1))

theorem Complexity.bitsOfLenLE_zero (ℓ : ℕ) : bitsOfLenLE ℓ 0 = List.replicate ℓ false

theorem Complexity.strsOfLen_eq_image (ℓ : ℕ) : strsOfLen ℓ = Finset.image (fun (i : ℕ) => bumpBits^[i] (List.replicate ℓ false)) (Finset.range (2 ^ ℓ))

The counter enumerates the strings of one length too, starting from the zeros.

theorem Complexity.bumpBits_injOn (ℓ : ℕ) : Set.InjOn (fun (i : ℕ) => bumpBits^[i] (List.replicate ℓ false)) ↑(Finset.range (2 ^ ℓ))

theorem Complexity.nextStrFn_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => nextStr (a z)) ∈ FP