Polynomial-time comparison of binary natural numbers

The comparison scans coefficient bits directly, padding only by the supplied bit-string lengths. It never expands a binary number to unary.

def MIPRE.Cost.compareStep (acc : Bool) (p : Bool × Bool) : Bool

Equations

• MIPRE.Cost.compareStep acc p = if p.1 = true then if p.2 = true then acc else false else if p.2 = true then true else acc

theorem MIPRE.Cost.compare_fold (a b : BitStr) (acc : Bool) (h : List.length a = List.length b) : List.foldl compareStep acc (List.zip a b) = true ↔ bitsVal a < bitsVal b ∨ bitsVal a = bitsVal b ∧ acc = true

theorem MIPRE.Cost.bitsVal_append_false (a : BitStr) (n : ℕ) : bitsVal (a ++ List.replicate n false) = bitsVal a

theorem MIPRE.Cost.esize_bool_le (b : Bool) : esize b ≤ 3

noncomputable def MIPRE.Cost.compareStepProg : PolyTimeFun (Bool × Bool × Bool) Bool

Equations

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

theorem MIPRE.Cost.compareStepProg_apply (b : Bool) (p : Bool × Bool) : compareStepProg.toFun (b, p) = compareStep b p

noncomputable def MIPRE.Cost.PolyTimeFun.leBits : PolyTimeFun (BitStr × BitStr) Bool

Compare arbitrary little-endian strings, allowing leading zeroes.

Equations

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

@[simp]

theorem MIPRE.Cost.PolyTimeFun.leBits_apply (p : BitStr × BitStr) : leBits.toFun p = decide (bitsVal p.1 ≤ bitsVal p.2)

noncomputable def MIPRE.Cost.PolyTimeFun.leNat : PolyTimeFun (ℕ × ℕ) Bool

Binary natural comparison, with a global polynomial cost in the encodings.

Equations

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

@[simp]

theorem MIPRE.Cost.PolyTimeFun.leNat_apply (p : ℕ × ℕ) : leNat.toFun p = decide (p.1 ≤ p.2)