The closure library, part IV: binary numbers

Programs on binary numbers presented as bit strings (LSB first, as in Nat.bits), used by the bit-query program of the recursive compression argument: the zero test (isZeroProg) and decrement (decProg). Decrement flips the leading falses to true and the first true to false; it may leave a non-canonical representation (trailing falses), which is why the specifications are in terms of the value bitsVal of a bit string rather than Nat.bits.

Costs: every list walk is quadratic in this model (the loop state is rebuilt each iteration, copying the tail), so bounds have the form (iterations + 1) · (S + c) with S dominating the sizes involved.

Bit strings as data

@[simp]

theorem MIPRE.Cost.Data.ofBool_false : ofBool false = nil

@[simp]

theorem MIPRE.Cost.Data.ofBool_true : ofBool true = nil.cons nil

@[simp]

theorem MIPRE.Cost.encode_bool (b : Bool) : encode b = Data.ofBool b

@[simp]

theorem MIPRE.Cost.encode_bitStr_nil : encode [] = Data.nil

@[simp]

theorem MIPRE.Cost.encode_bitStr_cons (b : Bool) (l : BitStr) : encode (b :: l) = (Data.ofBool b).cons (encode l)

theorem MIPRE.Cost.encode_bitStr_eq_list (l : BitStr) : encode l = Data.list (List.map Data.ofBool l)

theorem MIPRE.Cost.size_encode_replicate_true (j : ℕ) : (encode (List.replicate j true)).size = 4 * j + 1

theorem MIPRE.Cost.size_encode_replicate_false_append (j : ℕ) (rest : BitStr) : (encode (List.replicate j false ++ true :: rest)).size = 2 * j + (encode rest).size + 4

theorem MIPRE.Cost.size_encode_false_cons_replicate_true (j : ℕ) : (encode (false :: List.replicate j true)).size = 4 * j + 3

def MIPRE.Cost.bitsVal (l : BitStr) : ℕ

The value of a bit string (LSB first), canonical or not.

Equations

• MIPRE.Cost.bitsVal l = List.foldr Nat.bit 0 l

@[simp]

theorem MIPRE.Cost.bitsVal_nil : bitsVal [] = 0

@[simp]

theorem MIPRE.Cost.bitsVal_cons (b : Bool) (l : BitStr) : bitsVal (b :: l) = Nat.bit b (bitsVal l)

theorem MIPRE.Cost.bitsVal_bits (n : ℕ) : bitsVal n.bits = n

theorem MIPRE.Cost.bitsVal_eq_zero_iff (l : BitStr) : bitsVal l = 0 ↔ List.any l id = false

theorem MIPRE.Cost.bitsVal_replicate_true_append (j : ℕ) (rest : BitStr) : bitsVal (List.replicate j true ++ false :: rest) + 1 = bitsVal (List.replicate j false ++ true :: rest)

theorem MIPRE.Cost.exists_split_of_any (l : BitStr) (h : List.any l id = true) : ∃ (j : ℕ) (rest : List Bool), l = List.replicate j false ++ true :: rest

A bit string with a true bit splits as false^j ++ true :: rest.

Zero test

def MIPRE.Cost.Prog.isZeroBody : Prog

Body of isZeroProg: walk the bits; stop with nil (zero) at the end, with cons nil nil (nonzero) at the first true bit.

Equations

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

def MIPRE.Cost.Prog.isZeroProg : Prog

isZeroProg on a bit string computes encode (l.any id): nil iff the value is zero.

Equations

• MIPRE.Cost.Prog.isZeroProg = MIPRE.Cost.Prog.isZeroBody.loop

theorem MIPRE.Cost.Prog.isZeroBody_wellScoped : WellScoped 1 isZeroBody

theorem MIPRE.Cost.Prog.isZeroProg_wellScoped : WellScoped 1 isZeroProg

theorem MIPRE.Cost.Prog.isZeroBody_stop : Eval [encode []] isZeroBody (Data.nil.cons Data.nil) 4

theorem MIPRE.Cost.Prog.isZeroBody_false (l : BitStr) : Eval [encode (false :: l)] isZeroBody ((Data.nil.cons Data.nil).cons (encode l)) ((encode l).size + 7)

theorem MIPRE.Cost.Prog.isZeroBody_true (l : BitStr) : Eval [encode (true :: l)] isZeroBody (Data.nil.cons (Data.nil.cons Data.nil)) 7

theorem MIPRE.Cost.Prog.isZeroProg_runs (l : BitStr) (env : Env) (S : ℕ) (hS : (encode l).size ≤ S) : ∃ t ≤ (List.length l + 1) * (S + 8), Eval (encode l :: env) isZeroProg (encode (List.any l id)) t

Decrement

def MIPRE.Cost.Prog.decBody : Prog

Body of the first phase of decProg: on state cons bits acc, a leading false bit is turned into a true pushed on acc; at the first true bit the loop stops with the pair cons (false :: acc) rest, which the second phase (revOntoProg) reverses onto rest.

Equations

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

def MIPRE.Cost.Prog.decProg : Prog

decProg on the bits of a nonzero number computes the bits of its predecessor.

Equations

• MIPRE.Cost.Prog.decProg = ((MIPRE.Cost.Prog.var 0).cons MIPRE.Cost.Prog.nil).let_ (MIPRE.Cost.Prog.decBody.loop.let_ MIPRE.Cost.Prog.revOntoProg)

theorem MIPRE.Cost.Prog.decBody_wellScoped : WellScoped 1 decBody

theorem MIPRE.Cost.Prog.decProg_wellScoped : WellScoped 1 decProg

theorem MIPRE.Cost.Prog.decBody_false (l acc : BitStr) : Eval [(encode (false :: l)).cons (encode acc)] decBody ((Data.nil.cons Data.nil).cons ((encode l).cons (encode (true :: acc)))) ((encode l).size + (encode acc).size + 14)

theorem MIPRE.Cost.Prog.decBody_true (l acc : BitStr) : Eval [(encode (true :: l)).cons (encode acc)] decBody (Data.nil.cons ((encode (false :: acc)).cons (encode l))) ((encode l).size + (encode acc).size + 10)

theorem MIPRE.Cost.Prog.decLoop_runs (j : ℕ) (rest : BitStr) (i : ℕ) (env : Env) (S : ℕ) (hS : 2 * j + (encode rest).size + 4 + (4 * i + 1) + 2 * j ≤ S) : ∃ t ≤ (j + 1) * (S + 15), Eval ((encode (List.replicate j false ++ true :: rest)).cons (encode (List.replicate i true)) :: env) decBody.loop ((encode (false :: List.replicate (i + j) true)).cons (encode rest)) t

The first phase of decProg on false^j ++ true :: rest with accumulator true^i. The slack S must cover the growth of the accumulator: each converted bit adds two nodes.

theorem MIPRE.Cost.Prog.decProg_runs (j : ℕ) (rest : BitStr) : ∃ t ≤ (j + 2) * (10 * (2 * j + (encode rest).size + 4) + 60), decProg.Runs (encode (List.replicate j false ++ true :: rest)) (encode (List.replicate j true ++ false :: rest)) t

The next level index

theorem MIPRE.Cost.encode_two_mul_add_one (n : ℕ) : encode (2 * n + 1) = (Data.nil.cons Data.nil).cons (encode n)

theorem MIPRE.Cost.size_two_mul_add_one (n : ℕ) : (2 * n + 1).size = n.size + 1

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

n ↦ 2 n + 1 on binary numerals: prepend a true bit. This is the "next level" map of the recursive compression argument (the paper's n + 1 would need a carry propagation; 2 n + 1 is one node).

Equations

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

@[simp]

theorem MIPRE.Cost.PolyTimeFun.next_apply (n : ℕ) : next.toFun n = 2 * n + 1