Arithmetic in the ambient model: increment, unary conversion, multiplication, polynomials

The arithmetic the wrapper decider (Halting/Wrapper.lean) and the compressor's decider (Halting/Compressor.lean) need, each with its cost:

• Prog.incProg: the successor of a canonical binary numeral (Data.inc, with Data.inc_bits : inc n.bits = (n + 1).bits), used to enumerate the bit queries;
• Prog.toUnaryProg: a binary numeral to unary (encode n ↦ ofNat n), by the fold k ↦ 2k + b over the bits from the most significant one, doubling the unary accumulator with revOntoProg;
• Prog.mulProg: multiplication of unary numerals, by repeated addProg;
• Prog.polyProg cs: the Horner evaluation c₀ + m (c₁ + m (…)) of a polynomial given by its coefficient list, on a unary input; hornerCoeffs and Data.polyEval_hornerCoeffs connect it to Polynomial.eval, so that the wrapper can compute the paper's poly(n, λ) bounds.

Costs are polynomial in the values (the unary numerals are as long as the values); the polynomial evaluation is bounded by an explicit Polynomial ℕ in the argument (Prog.polyProg_runs), which is what the time accounting downstream composes.

The successor of a binary numeral

def MIPRE.Cost.Data.inc : BitStr → BitStr

The successor of a binary numeral, least significant bit first.

Equations

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

theorem MIPRE.Cost.Data.bitsVal_inc (l : BitStr) : bitsVal (inc l) = bitsVal l + 1

theorem MIPRE.Cost.Data.inc_ne_nil (l : BitStr) : inc l ≠ []

theorem MIPRE.Cost.Data.inc_canon (l : BitStr) (hl : l = [] ∨ List.getLast? l = some true) : List.getLast? (inc l) = some true

theorem MIPRE.Cost.Data.inc_bits (n : ℕ) : inc n.bits = (n + 1).bits

The successor on canonical binary numerals is the successor.

def MIPRE.Cost.Data.incAcc : BitStr → BitStr → BitStr × BitStr

The first phase of the increment: (rest, acc) ↦ (acc', rest') with acc'.reverse ++ rest' = acc.reverse ++ inc rest.

Equations

• MIPRE.Cost.Data.incAcc [] x✝ = (true :: x✝, [])
• MIPRE.Cost.Data.incAcc (false :: r) x✝ = (true :: x✝, r)
• MIPRE.Cost.Data.incAcc (true :: r) x✝ = MIPRE.Cost.Data.incAcc r (false :: x✝)

theorem MIPRE.Cost.Data.incAcc_spec (l acc : BitStr) : List.reverse (incAcc l acc).1 ++ (incAcc l acc).2 = List.reverse acc ++ inc l

theorem MIPRE.Cost.Data.incAcc_length (l acc : BitStr) : List.length (incAcc l acc).1 + List.length (incAcc l acc).2 ≤ List.length l + List.length acc + 1

theorem MIPRE.Cost.Data.size_encode_append (l₁ l₂ : BitStr) : (encode (l₁ ++ l₂)).size + 1 = (encode l₁).size + (encode l₂).size

theorem MIPRE.Cost.Data.size_encode_reverse (l : BitStr) : (encode (List.reverse l)).size = (encode l).size

Binary to unary

def MIPRE.Cost.Data.msbFold : List Bool → ℕ → ℕ

The fold k ↦ 2k + b over bits, most significant first.

Equations

• MIPRE.Cost.Data.msbFold [] x✝ = x✝
• MIPRE.Cost.Data.msbFold (b :: r) x✝ = MIPRE.Cost.Data.msbFold r (2 * x✝ + b.toNat)

theorem MIPRE.Cost.Data.msbFold_append_singleton (l : List Bool) (b : Bool) (k : ℕ) : msbFold (l ++ [b]) k = 2 * msbFold l k + b.toNat

theorem MIPRE.Cost.Data.msbFold_reverse (l : BitStr) (k : ℕ) : msbFold (List.reverse l) k = k * 2 ^ List.length l + bitsVal l

theorem MIPRE.Cost.Data.msbFold_le (l : List Bool) (k : ℕ) : k ≤ msbFold l k

Polynomials by their coefficients

def MIPRE.Cost.Data.polyEval : List ℕ → ℕ → ℕ

Horner evaluation of a coefficient list: polyEval [c₀, c₁, …] m = c₀ + m (c₁ + m (…)).

Equations

• MIPRE.Cost.Data.polyEval [] x✝ = 0
• MIPRE.Cost.Data.polyEval (c :: cs) x✝ = c + x✝ * MIPRE.Cost.Data.polyEval cs x✝

theorem MIPRE.Cost.Data.polyEval_range_map (f : ℕ → ℕ) (k m : ℕ) : polyEval (List.map f (List.range k)) m = ∑ i ∈ Finset.range k, f i * m ^ i

noncomputable def MIPRE.Cost.hornerCoeffs (p : Polynomial ℕ) : List ℕ

The coefficient list of a polynomial over ℕ, least significant first and padded to natDegree + 1 entries: the form Horner evaluation consumes (Data.polyEval). Mathlib's Polynomial.coeffList is the big-endian list without the padding.

Equations

• MIPRE.Cost.hornerCoeffs p = List.map (⇑p.coeff) (List.range (p.natDegree + 1))

theorem MIPRE.Cost.Data.polyEval_hornerCoeffs (p : Polynomial ℕ) (m : ℕ) : polyEval (hornerCoeffs p) m = Polynomial.eval m p

def MIPRE.Cost.Prog.tacticCost_omega' : Lean.ParserDescr

Close a cost bound after the run has been built: unfold the sizes of the small constants and of unary numerals, and let omega finish.

Equations

• MIPRE.Cost.Prog.tacticCost_omega' = Lean.ParserDescr.node `MIPRE.Cost.Prog.tacticCost_omega' 1024 (Lean.ParserDescr.nonReservedSymbol "cost_omega'" false)

The increment program

def MIPRE.Cost.Prog.incBody : Prog

Body of the first phase of incProg, on the state cons rest acc: at the end or at a false bit, stop with (true :: acc, rest); at a true bit, move a false onto acc.

Equations

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

def MIPRE.Cost.Prog.incProg : Prog

incProg on the bits of n computes the bits of n + 1.

Equations

• MIPRE.Cost.Prog.incProg = ((MIPRE.Cost.Prog.var 0).cons MIPRE.Cost.Prog.nil).let_ (MIPRE.Cost.Prog.incBody.loop.let_ MIPRE.Cost.Prog.revOntoProg)

theorem MIPRE.Cost.Prog.incBody_wellScoped : WellScoped 1 incBody

theorem MIPRE.Cost.Prog.incProg_wellScoped : WellScoped 1 incProg

theorem MIPRE.Cost.Prog.incBody_nil (acc : BitStr) : ∃ t ≤ (encode acc).size + 20, Eval [(encode []).cons (encode acc)] incBody (Data.nil.cons ((encode (true :: acc)).cons (encode []))) t

theorem MIPRE.Cost.Prog.incBody_false (r acc : BitStr) : ∃ t ≤ (encode r).size + (encode acc).size + 20, Eval [(encode (false :: r)).cons (encode acc)] incBody (Data.nil.cons ((encode (true :: acc)).cons (encode r))) t

theorem MIPRE.Cost.Prog.incBody_true (r acc : BitStr) : ∃ t ≤ (encode r).size + (encode acc).size + 20, Eval [(encode (true :: r)).cons (encode acc)] incBody ((Data.nil.cons Data.nil).cons ((encode r).cons (encode (false :: acc)))) t

theorem MIPRE.Cost.Prog.incLoop_runs (l acc : BitStr) (env : Env) (S : ℕ) (hS : (encode l).size + (encode acc).size + 3 * List.length l ≤ S) : ∃ t ≤ (List.length l + 1) * (S + 21), Eval ((encode l).cons (encode acc) :: env) incBody.loop ((encode (Data.incAcc l acc).1).cons (encode (Data.incAcc l acc).2)) t

The first phase of the increment, on (rest, acc).

theorem MIPRE.Cost.Prog.incProg_runs (l : BitStr) : ∃ t ≤ (List.length l + 2) * (8 * (encode l).size + 8 * List.length l + 60), incProg.Runs (encode l) (encode (Data.inc l)) t

incProg computes the successor of a binary numeral.

theorem MIPRE.Cost.Prog.incProg_runs_nat (n : ℕ) : ∃ t ≤ (n.size + 2) * (8 * esize n + 8 * n.size + 60), incProg.Runs (encode n) (encode (n + 1)) t

The successor on canonical numerals, as a run on encode n.

Binary to unary

def MIPRE.Cost.Prog.toUnaryBody : Prog

Body of toUnaryProg, on the state cons rest acc (rest the remaining bits, most significant first; acc a unary numeral): double acc and add the next bit.

Equations

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

def MIPRE.Cost.Prog.toUnaryProg : Prog

toUnaryProg on encode n computes ofNat n.

Equations

• MIPRE.Cost.Prog.toUnaryProg = (MIPRE.Cost.Prog.callVar 0 MIPRE.Cost.Prog.revProg).let_ (((MIPRE.Cost.Prog.var 0).cons MIPRE.Cost.Prog.nil).let_ MIPRE.Cost.Prog.toUnaryBody.loop)

theorem MIPRE.Cost.Prog.toUnaryBody_wellScoped : WellScoped 1 toUnaryBody

theorem MIPRE.Cost.Prog.toUnaryProg_wellScoped : WellScoped 1 toUnaryProg

theorem MIPRE.Cost.Prog.toUnaryBody_nil (k : ℕ) : ∃ t ≤ 2 * k + 20, Eval [(encode []).cons (Data.ofNat k)] toUnaryBody (Data.nil.cons (Data.ofNat k)) t

theorem MIPRE.Cost.Prog.double_runs (k : ℕ) (env : Env) : ∃ t ≤ (k + 1) * (4 * k + 14), Eval ((Data.ofNat k).cons (Data.ofNat k) :: env) revOntoProg (Data.ofNat (2 * k)) t

The doubling of a unary numeral by revOntoProg.

theorem MIPRE.Cost.Prog.toUnaryBody_step (b : Bool) (r : BitStr) (k : ℕ) : ∃ t ≤ (k + 1) * (4 * k + 14) + (encode r).size + 8 * k + 64, Eval [(encode (b :: r)).cons (Data.ofNat k)] toUnaryBody ((Data.nil.cons Data.nil).cons ((encode r).cons (Data.ofNat (2 * k + b.toNat)))) t

theorem MIPRE.Cost.Prog.toUnaryLoop_runs (l : List Bool) (k : ℕ) (env : Env) (N : ℕ) (hN : Data.msbFold l k = N) (S : ℕ) (hS : (encode l).size ≤ S) : ∃ t ≤ (l.length + 1) * ((N + 1) * (4 * N + 14) + S + 8 * N + 65), Eval ((encode l).cons (Data.ofNat k) :: env) toUnaryBody.loop (Data.ofNat N) t

The unary fold over the bits, most significant first: from (rest, ofNat k) to ofNat (msbFold rest k), in time (|rest| + 1) · B for B a bound depending on the final value N = msbFold rest k.

theorem MIPRE.Cost.Prog.toUnaryProg_runs (n : ℕ) : ∃ t ≤ (n.size + 2) * ((n + 1) * (4 * n + 14) + 7 * esize n + 8 * n + 90), toUnaryProg.Runs (encode n) (Data.ofNat n) t

toUnaryProg converts a binary numeral to unary.

Multiplication of unary numerals

def MIPRE.Cost.Prog.mulBody : Prog

Body of the multiplication loop, on the state cons bRest acc, with the first factor a one variable further out: at the end stop with acc, otherwise add a to acc.

Equations

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

def MIPRE.Cost.Prog.mulProg : Prog

mulProg on cons (ofNat a) (ofNat b) computes ofNat (a * b).

Equations

• MIPRE.Cost.Prog.mulProg = MIPRE.Cost.Prog.elim 0 MIPRE.Cost.Prog.nil (((MIPRE.Cost.Prog.var 1).cons MIPRE.Cost.Prog.nil).let_ MIPRE.Cost.Prog.mulBody.loop)

theorem MIPRE.Cost.Prog.mulProg_wellScoped : WellScoped 1 mulProg

theorem MIPRE.Cost.Prog.mulBody_nil (a acc : ℕ) (rest : Env) : ∃ t ≤ 2 * acc + 20, Eval ((Data.ofNat 0).cons (Data.ofNat acc) :: Data.ofNat a :: rest) mulBody (Data.nil.cons (Data.ofNat acc)) t

theorem MIPRE.Cost.Prog.mulBody_step (a b' acc : ℕ) (rest : Env) : ∃ t ≤ (a + 1) * (4 * a + 2 * acc + 15) + 4 * a + 4 * acc + 2 * b' + 40, Eval ((Data.ofNat (b' + 1)).cons (Data.ofNat acc) :: Data.ofNat a :: rest) mulBody ((Data.nil.cons Data.nil).cons ((Data.ofNat b').cons (Data.ofNat (a + acc)))) t

theorem MIPRE.Cost.Prog.mulLoop_runs (a b acc : ℕ) (rest : Env) (P : ℕ) (hP : acc + a * b ≤ P) : ∃ t ≤ (b + 1) * ((a + 1) * (4 * a + 2 * P + 15) + 4 * a + 4 * P + 2 * b + 41), Eval ((Data.ofNat b).cons (Data.ofNat acc) :: Data.ofNat a :: rest) mulBody.loop (Data.ofNat (acc + a * b)) t

The multiplication loop: from (ofNat b, ofNat acc) with a one variable out, to ofNat (acc + a b).

theorem MIPRE.Cost.Prog.mulProg_runs (a b : ℕ) : ∃ t ≤ (b + 1) * ((a + 1) * (4 * a + 2 * (a * b) + 15) + 4 * a + 4 * (a * b) + 2 * b + 41) + 2 * b + 10, mulProg.Runs ((Data.ofNat a).cons (Data.ofNat b)) (Data.ofNat (a * b)) t

mulProg multiplies unary numerals.

Polynomials, by Horner's rule

def MIPRE.Cost.Prog.polyProg : List ℕ → Prog

Horner evaluation of the coefficient list cs on a unary input m: polyProg (c :: cs) computes c + m · polyProg cs.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Cost.Prog.polyProg [] = MIPRE.Cost.Prog.nil

theorem MIPRE.Cost.Prog.polyProg_wellScoped (cs : List ℕ) : WellScoped 1 (polyProg cs)

theorem MIPRE.Cost.Prog.polyProg_runs (cs : List ℕ) : ∃ (Q : Polynomial ℕ), ∀ (m : ℕ) (env : Env), ∃ t ≤ Polynomial.eval m Q, Eval (Data.ofNat m :: env) (polyProg cs) (Data.ofNat (Data.polyEval cs m)) t

polyProg cs evaluates the polynomial, within a cost polynomial in the argument.

Evaluating a fixed polynomial, primitively recursively

The answer-length budget of the tabulation is bound.eval (n + λ) for the fixed polynomial bound of MIPRE.GapCompression, so MIPRE.Halting.tab_computable needs a polynomial's evaluation to be primitive recursive in its argument. It goes through this file's own Data.polyEval and hornerCoeffs rather than Mathlib's Polynomial API: the coefficient list is fixed data, and Horner's rule on a fixed list is a fixed composition of + and *.

theorem MIPRE.Cost.primrec_polyEval (L : List ℕ) : Primrec (Data.polyEval L)

theorem MIPRE.Cost.primrec_poly_eval (p : Polynomial ℕ) : Primrec fun (m : ℕ) => Polynomial.eval m p