Polynomial-time arithmetic on binary integers

Polynomial-time certificates for arithmetic on the binary sign-magnitude integers Turing.MultiTapeTM.encIntBin. The sign bit and the magnitude are read off the code directly. Every other operation is an ordinary functional program over the sign and the magnitude, by cases on the signs, built from the binary natural arithmetic of Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/Binary.lean; no new machine is involved. A result is assembled from a sign and a magnitude by Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_signMagnitude, which clears the sign of a zero magnitude. Integers of equal sign add their magnitudes; otherwise the smaller magnitude is subtracted from the larger one, which keeps its sign. A product multiplies the magnitudes, and is negative when exactly one factor is. Lists are summed and powers taken by left folds, with the binary length bounds of Int.size_natAbs_add_le and Int.size_natAbs_mul_le.

Main results

• Turing.MultiTapeTM.ComputableInPolyTime.intBin_mul': multiply two plain-certified binary integers from the same complete input encoding.

• Turing.MultiTapeTM.ComputableInPolyTime.intBin_prod_range: the product of a plain-certified family of binary integers over a computed unary range.

• Int.size_natAbs_add_le, Int.size_natAbs_sub_le, Int.size_natAbs_mul_le, Int.size_natAbs_pow_le, Int.size_natAbs_sum_le, Int.size_natAbs_prod_le: binary lengths of magnitudes of sums, differences, products, powers, list sums and list products.

• Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_isNeg, .intBin_natAbs: the sign and the binary magnitude.

• Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_signMagnitude, .intBin_natCast: integers from a sign and a binary magnitude, and from binary naturals.

• Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_isZero, .intBin_isPos, .intBin_sign, .intBin_toNat: sign tests, the sign and truncation at zero.

• Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_neg, .intBin_add, .intBin_sub, .intBin_mul, .intBin_pow: ring operations, powers to a unary exponent.

• Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_lt, .intBin_le: comparisons.

• Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_sum, .intBin_prod: the sum and product of a list.

• Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_add', .intBin_sub', .intBin_mul', .intBin_pow', .intBin_lt', .intBin_le': composition rules for fun_prop.

theorem Int.size_natAbs_add_le (a b : ℤ) : (a + b).natAbs.size ≤ max a.natAbs.size b.natAbs.size + 1

The magnitude of a sum is at most one binary digit longer than the longer magnitude of the summands.

theorem Int.size_natAbs_sub_le (a b : ℤ) : (a - b).natAbs.size ≤ max a.natAbs.size b.natAbs.size + 1

The magnitude of a difference is at most one binary digit longer than the longer magnitude of the operands.

theorem Int.size_natAbs_mul_le (a b : ℤ) : (a * b).natAbs.size ≤ a.natAbs.size + b.natAbs.size

The magnitude of a product is at most as long as the magnitudes of the factors together.

theorem Int.size_natAbs_pow_le (a : ℤ) (k : ℕ) : (a ^ k).natAbs.size ≤ k * a.natAbs.size + 1

The magnitude of a power is at most the exponent times the magnitude of the base, plus one for the zeroth power.

theorem Int.size_natAbs_sum_le {l : List ℤ} {b : ℕ} (h : ∀ z ∈ l, z.natAbs.size ≤ b) : l.sum.natAbs.size ≤ b + l.length.size

A sum of integers whose magnitudes have binary length at most b has a magnitude of binary length at most b plus the binary length of the number of summands.

theorem Int.size_natAbs_prod_le (l : List ℤ) : l.prod.natAbs.size ≤ (List.map (fun (z : ℤ) => z.natAbs.size) l).sum + 1

A product of integers has a magnitude of binary length at most the sum of the binary lengths of the magnitudes of the factors, plus one for the empty product.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_isNeg : ComputableTidilyInPolyTime (fun (z : ℤ) => decide (z < 0)) encIntBin encBool

The sign of a binary integer: whether it is negative.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_natAbs : ComputableTidilyInPolyTime Int.natAbs encIntBin encNat

The magnitude of a binary integer, as a binary natural.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_signMagnitude : ComputableTidilyInPolyTime (fun (p : Bool × ℕ) => if p.1 = true then -↑p.2 else ↑p.2) (encPair encBool encNat) encIntBin

Assemble a binary integer from a sign and a binary magnitude. A negative sign on a zero magnitude is dropped, so the code stays unique.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_natCast : ComputableTidilyInPolyTime (fun (n : ℕ) => ↑n) encNat encIntBin

A binary natural as a binary integer.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_neg : ComputableTidilyInPolyTime (fun (z : ℤ) => -z) encIntBin encIntBin

Negation of binary integers flips the sign of a nonzero magnitude.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_add : ComputableTidilyInPolyTime (fun (p : ℤ × ℤ) => p.1 + p.2) (encPair encIntBin encIntBin) encIntBin

Addition of binary integers, by cases on the signs of the summands.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_mul : ComputableTidilyInPolyTime (fun (p : ℤ × ℤ) => p.1 * p.2) (encPair encIntBin encIntBin) encIntBin

Multiplication of binary integers: the magnitudes multiply, and the product is negative when exactly one factor is.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_sub : ComputableTidilyInPolyTime (fun (p : ℤ × ℤ) => p.1 - p.2) (encPair encIntBin encIntBin) encIntBin

Subtraction of binary integers, as addition of the negation.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_isZero : ComputableTidilyInPolyTime (fun (z : ℤ) => decide (z = 0)) encIntBin encBool

Test whether a binary integer is zero: its magnitude has no digits.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_isPos : ComputableTidilyInPolyTime (fun (z : ℤ) => decide (0 < z)) encIntBin encBool

Test whether a binary integer is positive.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_sign : ComputableTidilyInPolyTime Int.sign encIntBin encIntBin

The sign of a binary integer, as a binary integer.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_toNat : ComputableTidilyInPolyTime Int.toNat encIntBin encNat

Truncate a binary integer at zero, as a binary natural.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_lt : ComputableTidilyInPolyTime (fun (p : ℤ × ℤ) => decide (p.1 < p.2)) (encPair encIntBin encIntBin) encBool

Strict comparison of binary integers, through the sign of their difference.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_le : ComputableTidilyInPolyTime (fun (p : ℤ × ℤ) => decide (p.1 ≤ p.2)) (encPair encIntBin encIntBin) encBool

Comparison of binary integers.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_pow : ComputableTidilyInPolyTime (fun (p : ℤ × ℕ) => p.1 ^ p.2) (encPair encIntBin encUnary) encIntBin

A power of a binary integer to a unary exponent, by repeated multiplication.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_sum : ComputableTidilyInPolyTime List.sum (encList encIntBin) encIntBin

The sum of a list of binary integers, by a left fold of binary additions.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_prod : ComputableTidilyInPolyTime List.prod (encList encIntBin) encIntBin

The product of a list of binary integers, by a left fold of binary multiplications.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_add' {α : Type} {input : α ↪ List Bool} {left right : α → ℤ} (hleft : ComputableTidilyInPolyTime left input encIntBin) (hright : ComputableTidilyInPolyTime right input encIntBin) : ComputableTidilyInPolyTime (fun (a : α) => left a + right a) input encIntBin

Add computed binary integers, fixing their intermediate encodings for proof search.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_sub' {α : Type} {input : α ↪ List Bool} {left right : α → ℤ} (hleft : ComputableTidilyInPolyTime left input encIntBin) (hright : ComputableTidilyInPolyTime right input encIntBin) : ComputableTidilyInPolyTime (fun (a : α) => left a - right a) input encIntBin

Subtract computed binary integers, fixing their intermediate encodings.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_mul' {α : Type} {input : α ↪ List Bool} {left right : α → ℤ} (hleft : ComputableTidilyInPolyTime left input encIntBin) (hright : ComputableTidilyInPolyTime right input encIntBin) : ComputableTidilyInPolyTime (fun (a : α) => left a * right a) input encIntBin

Multiply computed binary integers, fixing their intermediate encodings.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_pow' {α : Type} {input : α ↪ List Bool} {base : α → ℤ} {exponent : α → ℕ} (hbase : ComputableTidilyInPolyTime base input encIntBin) (hexponent : ComputableTidilyInPolyTime exponent input encUnary) : ComputableTidilyInPolyTime (fun (a : α) => base a ^ exponent a) input encIntBin

Raise a computed binary integer to a computed unary exponent, fixing the intermediate encodings.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_lt' {α : Type} {input : α ↪ List Bool} {left right : α → ℤ} (hleft : ComputableTidilyInPolyTime left input encIntBin) (hright : ComputableTidilyInPolyTime right input encIntBin) : ComputableTidilyInPolyTime (fun (a : α) => decide (left a < right a)) input encBool

Strictly compare computed binary integers, fixing their intermediate encodings.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_le' {α : Type} {input : α ↪ List Bool} {left right : α → ℤ} (hleft : ComputableTidilyInPolyTime left input encIntBin) (hright : ComputableTidilyInPolyTime right input encIntBin) : ComputableTidilyInPolyTime (fun (a : α) => decide (left a ≤ right a)) input encBool

Compare computed binary integers, fixing their intermediate encodings.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_prod_range {α : Type} {enc : α ↪ List Bool} {f : α × ℕ → ℤ} {r : α → ℕ} (hf : ComputableTidilyInPolyTime f (encPair enc encUnary) encIntBin) (hr : ComputableTidilyInPolyTime r enc encUnary) : ComputableTidilyInPolyTime (fun (a : α) => ∏ i ∈ Finset.range (r a), f (a, i)) enc encIntBin

Multiply a uniformly computed family of binary integers over a computed unary range.

theorem Turing.MultiTapeTM.ComputableInPolyTime.intBin_mul' {α : Type} {input : α ↪ List Bool} {left right : α → ℤ} (hleft : ComputableInPolyTime left input encIntBin) (hright : ComputableInPolyTime right input encIntBin) : ComputableInPolyTime (fun (a : α) => left a * right a) input encIntBin

Multiply computed binary integers, preserving the complete input encoding.

theorem Turing.MultiTapeTM.ComputableInPolyTime.intBin_natCast : ComputableInPolyTime (fun (n : ℕ) => ↑n) encNat encIntBin

The cast of a binary natural number to a binary integer.

theorem Turing.MultiTapeTM.ComputableInPolyTime.intBin_toNat : ComputableInPolyTime Int.toNat encIntBin encNat

Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_toNat for plain certificates.

theorem Turing.MultiTapeTM.ComputableInPolyTime.intBin_sub : ComputableInPolyTime (fun (p : ℤ × ℤ) => p.1 - p.2) (encPair encIntBin encIntBin) encIntBin

Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_sub for plain certificates.

theorem Turing.MultiTapeTM.ComputableInPolyTime.intBin_prod_range {α : Type} {enc : α ↪ List Bool} {f : α × ℕ → ℤ} {r : α → ℕ} (hf : ComputableInPolyTime f (encPair enc encUnary) encIntBin) (hr : ComputableInPolyTime r enc encUnary) : ComputableInPolyTime (fun (a : α) => ∏ i ∈ Finset.range (r a), f (a, i)) enc encIntBin

Turing.MultiTapeTM.ComputableTidilyInPolyTime.intBin_prod_range for plain certificates.