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 CslibFrontier/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.ComputableInPolyTime.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

• 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.ComputableInPolyTime.intBin_isNeg, .intBin_natAbs: the sign and the binary magnitude.
• Turing.MultiTapeTM.ComputableInPolyTime.intBin_signMagnitude, .intBin_natCast: integers from a sign and a binary magnitude, and from binary naturals.
• Turing.MultiTapeTM.ComputableInPolyTime.intBin_isZero, .intBin_isPos, .intBin_sign, .intBin_toNat: sign tests, the sign and truncation at zero.
• Turing.MultiTapeTM.ComputableInPolyTime.intBin_neg, .intBin_add, .intBin_sub, .intBin_mul, .intBin_pow: ring operations, powers to a unary exponent.
• Turing.MultiTapeTM.ComputableInPolyTime.intBin_lt, .intBin_le: comparisons.
• Turing.MultiTapeTM.ComputableInPolyTime.intBin_sum, .intBin_prod, .intBin_finset_prod, .intBin_prod_range: the sum and product of a list, the product of a fixed finite family, and the product of a computed family over a unary range.
• Turing.MultiTapeTM.ComputableInPolyTime.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.ComputableInPolyTime.intBin_isNeg : ComputableInPolyTime (fun (z : ℤ) => decide (z < 0)) encIntBin encBool

Whether a binary integer is negative: the sign bit of its code.

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

The binary magnitude of a binary integer: its code without the sign bit.

theorem Turing.MultiTapeTM.ComputableInPolyTime.intBin_signMagnitude : ComputableInPolyTime (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.ComputableInPolyTime.intBin_natCast : ComputableInPolyTime (fun (n : ℕ) => ↑n) encNat encIntBin

A binary natural as a binary integer: a nonnegative sign bit in front of its digits.

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

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

theorem Turing.MultiTapeTM.ComputableInPolyTime.intBin_add : ComputableInPolyTime (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.ComputableInPolyTime.intBin_mul : ComputableInPolyTime (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.ComputableInPolyTime.intBin_sub : ComputableInPolyTime (fun (p : ℤ × ℤ) => p.1 - p.2) (encPair encIntBin encIntBin) encIntBin

Subtraction of binary integers, as addition of the negation.

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

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

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

Test whether a binary integer is positive.

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

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

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

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

theorem Turing.MultiTapeTM.ComputableInPolyTime.intBin_lt : ComputableInPolyTime (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.ComputableInPolyTime.intBin_le : ComputableInPolyTime (fun (p : ℤ × ℤ) => decide (p.1 ≤ p.2)) (encPair encIntBin encIntBin) encBool

Comparison of binary integers.

theorem Turing.MultiTapeTM.ComputableInPolyTime.intBin_pow : ComputableInPolyTime (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.ComputableInPolyTime.intBin_sum : ComputableInPolyTime List.sum (encList encIntBin) encIntBin

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

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

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

theorem Turing.MultiTapeTM.ComputableInPolyTime.intBin_add' {α : 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

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

theorem Turing.MultiTapeTM.ComputableInPolyTime.intBin_sub' {α : 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

Subtract computed binary integers, fixing their intermediate encodings.

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, fixing their intermediate encodings.

theorem Turing.MultiTapeTM.ComputableInPolyTime.intBin_pow' {α : Type} {input : α ↪ List Bool} {base : α → ℤ} {exponent : α → ℕ} (hbase : ComputableInPolyTime base input encIntBin) (hexponent : ComputableInPolyTime exponent input encUnary) : ComputableInPolyTime (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.ComputableInPolyTime.intBin_lt' {α : Type} {input : α ↪ List Bool} {left right : α → ℤ} (hleft : ComputableInPolyTime left input encIntBin) (hright : ComputableInPolyTime right input encIntBin) : ComputableInPolyTime (fun (a : α) => decide (left a < right a)) input encBool

Compare two computed binary integers with <, fixing their intermediate encodings.

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

Compare two computed binary integers with ≤, fixing their intermediate encodings.

theorem Turing.MultiTapeTM.ComputableInPolyTime.intBin_finset_prod {α : Type} {ι : Type u_1} {enc : α ↪ List Bool} (s : Finset ι) {f : ι → α → ℤ} (hf : ∀ i ∈ s, ComputableInPolyTime (f i) enc encIntBin) : ComputableInPolyTime (fun (a : α) => ∏ i ∈ s, f i a) enc encIntBin

Multiply a fixed finite family of computed binary integers.

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

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

Tidy forms

Tidy proofs in Lyubashevsky.Efficient, Lyubashevsky.NativeExtract and ExactOne.DrawingPolyTime still compose these rules; each is the plain rule above.

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

Turing.MultiTapeTM.ComputableInPolyTime.intBin_natAbs for tidy certificates.

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

Turing.MultiTapeTM.ComputableInPolyTime.intBin_natCast for tidy certificates.

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

Turing.MultiTapeTM.ComputableInPolyTime.intBin_sub for tidy certificates.

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

Turing.MultiTapeTM.ComputableInPolyTime.intBin_mul for tidy certificates.

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

Turing.MultiTapeTM.ComputableInPolyTime.intBin_pow for tidy certificates.

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

Turing.MultiTapeTM.ComputableInPolyTime.intBin_sum for tidy certificates.

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

Turing.MultiTapeTM.ComputableInPolyTime.intBin_add' for tidy certificates.

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

Turing.MultiTapeTM.ComputableInPolyTime.intBin_sub' for tidy certificates.

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

Turing.MultiTapeTM.ComputableInPolyTime.intBin_mul' for tidy certificates.