Canonical binary arithmetic

The parameter algorithms use binary integers, even when their values are much larger than the available work space. These programs manipulate binary digits directly. In particular, converting a bit string to a natural number normalizes its encoding without expanding its value to unary.

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

Prepend a digit, suppressing the noncanonical representation of zero.

Equations

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

@[simp]

theorem MIPRE.Cost.PolyTimeFun.natBit_apply (p : Bool × ℕ) : natBit.toFun p = Nat.bit p.1 p.2

theorem MIPRE.Cost.esize_natBit_le (b : Bool) (n : ℕ) : esize (Nat.bit b n) ≤ esize n + 4

noncomputable def MIPRE.Cost.PolyTimeFun.bitsValue : PolyTimeFun BitStr ℕ

Read and normalize an arbitrary little-endian bit string.

Equations

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

@[simp]

theorem MIPRE.Cost.PolyTimeFun.bitsValue_apply (l : BitStr) : bitsValue.toFun l = bitsVal l

def MIPRE.Cost.decBits : BitStr → BitStr

Binary borrow, used on the nonzero canonical representation.

Equations

• MIPRE.Cost.decBits [] = []
• MIPRE.Cost.decBits (true :: l) = false :: l
• MIPRE.Cost.decBits (false :: l) = true :: MIPRE.Cost.decBits l

theorem MIPRE.Cost.decBits_split (j : ℕ) (rest : BitStr) : decBits (List.replicate j false ++ true :: rest) = List.replicate j true ++ false :: rest

theorem MIPRE.Cost.split_bits_of_ne_zero (n : ℕ) (hn : n ≠ 0) : ∃ (j : ℕ) (rest : List Bool), n.bits = List.replicate j false ++ true :: rest

theorem MIPRE.Cost.bitsVal_decBits (n : ℕ) : bitsVal (decBits n.bits) = n - 1

noncomputable def MIPRE.Cost.PolyTimeFun.predBits : PolyTimeFun ℕ BitStr

The existing borrow machine, with its missing zero case supplied. Its output need not be canonical; bitsValue subsequently normalizes it.

Equations

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

@[simp]

theorem MIPRE.Cost.PolyTimeFun.predBits_apply (n : ℕ) : predBits.toFun n = decBits n.bits

noncomputable def MIPRE.Cost.PolyTimeFun.predN : PolyTimeFun ℕ ℕ

Saturating predecessor of a binary integer.

Equations

• MIPRE.Cost.PolyTimeFun.predN = (MIPRE.Cost.PolyTimeFun.bitsValue.comp MIPRE.Cost.PolyTimeFun.predBits).congr (fun (n : ℕ) => n - 1) MIPRE.Cost.PolyTimeFun.predN._proof_1

@[simp]

theorem MIPRE.Cost.PolyTimeFun.predN_apply (n : ℕ) : predN.toFun n = n - 1

theorem MIPRE.Cost.fold_addUnary (u : Unary) (n : ℕ) : List.foldl (fun (k : ℕ) (x : Unit) => k + 1) n u = n + List.length u

noncomputable def MIPRE.Cost.PolyTimeFun.addUnary : PolyTimeFun (ℕ × Unary) ℕ

Add a unary offset to a binary integer.

Equations

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

@[simp]

theorem MIPRE.Cost.PolyTimeFun.addUnary_apply (p : ℕ × Unary) : addUnary.toFun p = p.1 + List.length p.2

theorem MIPRE.Cost.fold_subUnary (u : Unary) (n : ℕ) : List.foldl (fun (k : ℕ) (x : Unit) => k - 1) n u = n - List.length u

noncomputable def MIPRE.Cost.PolyTimeFun.subUnary : PolyTimeFun (ℕ × Unary) ℕ

Subtract a unary offset from a binary integer, saturating at zero. The intermediate values are bounded by the initial integer, in binary size.

Equations

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

@[simp]

theorem MIPRE.Cost.PolyTimeFun.subUnary_apply (p : ℕ × Unary) : subUnary.toFun p = p.1 - List.length p.2