Polynomial-time arithmetic on binary naturals

Polynomial-time certificates for arithmetic on the binary encoding Turing.MultiTapeTM.encNat (digits least significant first), the binary counterparts of the unary certificates in Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat.lean. Addition and multiplication are Christian Reitwiessner's degree-bounded machines (Turing.MultiTapeTM.computableTidilyInDegree_add, Turing.MultiTapeTM.computableTidilyInDegree_mul). A list is summed by a left fold whose accumulator grows by at most one digit more than the length of the element added. Powers of two are computed from a unary exponent by repeated doubling. Strict comparison is the linear-time zip transducer of Turing.MultiTapeTM.computableInTimeAndSpace_natLt. The verifiers and reductions of the number problems (Cslib.Complexity.SubsetSum and its relatives) are built from these.

Truncated subtraction is schoolbook subtraction: a left fold over the digit pairs of both operands keeps a borrow and appends one difference digit per position. A final borrow means that the difference is negative; otherwise the digits are read back as a natural (Turing.MultiTapeTM.ofBits, certified by Turing.MultiTapeTM.Decoder.nat), dropping trailing zeros. General powers to a unary exponent are computed by repeated multiplication.

Main definitions

• Turing.MultiTapeTM.BinarySub.subStep: one round of schoolbook subtraction with a borrow.

Main results

• Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsToNat: binary decoding of arbitrary words.
• Nat.size_add_le: a sum has at most one binary digit more than its summands together.
• Nat.lt_iff_exists_testBit: strict order through the highest differing bit.
• Nat.size_add_le_max, Nat.size_mul_le, Nat.size_pow_le, Nat.size_sum_le: binary lengths of sums, products, powers and list sums.
• Turing.MultiTapeTM.BinarySub.sub_eq: truncated subtraction through the final borrow.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.binary_add, .binary_mul: addition and multiplication.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.binary_sum: the sum of a list.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.binary_two_pow: 2 ^ k in binary, from k in unary.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.binary_lt, .binary_le: comparisons.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.binary_sub: truncated subtraction.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.binary_pow: a power to a unary exponent.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.binary_add', .binary_lt', .binary_le': composition rules for fun_prop.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.binary_mul', .binary_sub', .binary_pow': composition rules for fun_prop.
• Turing.MultiTapeTM.ComputableInPolyTime.binary_bitwise, .binary_and, .binary_or, .binary_xor, .binary_and', .binary_or', .binary_xor': bitwise operations on binary naturals, and their composition rules.
• Turing.MultiTapeTM.ComputableInPolyTime.binary_size, .binary_min_unary, .binary_min_unary', .binary_shiftRight, .binary_shiftRight': bit-length in unary, capping a binary natural by a unary bound, and binary right shift.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.binary_testBit: a bit of a binary number at a unary position.

theorem Nat.size_add_le (m n : ℕ) : (m + n).size ≤ m.size + n.size + 1

The binary length of a sum is at most the binary lengths of the summands together, plus one.

theorem Nat.size_add_le_max (m n : ℕ) : (m + n).size ≤ max m.size n.size + 1

The binary length of a sum is at most one more than the longer binary length of the summands.

theorem Nat.size_sum_le {l : List ℕ} {b : ℕ} (h : ∀ n ∈ l, n.size ≤ b) : l.sum.size ≤ b + l.length.size

A sum of naturals of binary length at most b has binary length at most b plus the binary length of the number of summands.

theorem Nat.size_le_self (n : ℕ) : n.size ≤ n

A binary length is at most the number itself.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsToNat : ComputableTidilyInPolyTime ofBits encBits encNat

Decode arbitrary little-endian bit words to binary naturals.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.natBits : ComputableTidilyInPolyTime Nat.bits encNat encBits

The binary digits of a natural number, as a raw bit string.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.binary_add : ComputableTidilyInPolyTime (fun (p : ℕ × ℕ) => p.1 + p.2) (encPair encNat encNat) encNat

Addition of binary naturals.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.binary_mul : ComputableTidilyInPolyTime (fun (p : ℕ × ℕ) => p.1 * p.2) (encPair encNat encNat) encNat

Multiplication of binary naturals.

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

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

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.binary_sum : ComputableTidilyInPolyTime List.sum (encList encNat) encNat

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

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.binary_two_pow : ComputableTidilyInPolyTime (fun (k : ℕ) => 2 ^ k) encUnary encNat

2 ^ k in binary, from k in unary, by doubling.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.binary_lt : ComputableTidilyInPolyTime (fun (p : ℕ × ℕ) => decide (p.1 < p.2)) (encPair encNat encNat) encBool

Strict comparison of binary naturals, from the linear zip-transducer certificate.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.binary_le : ComputableTidilyInPolyTime (fun (p : ℕ × ℕ) => decide (p.1 ≤ p.2)) (encPair encNat encNat) encBool

Comparison of binary naturals.

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

Strictly compare computed binary values, fixing their intermediate encodings.

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

Compare computed binary values, fixing their intermediate encodings.

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

Multiply computed binary values, fixing their intermediate encodings for proof search.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.binary_pow : ComputableTidilyInPolyTime (fun (p : ℕ × ℕ) => p.1 ^ p.2) (encPair encNat encUnary) encNat

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

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

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

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.binary_sub : ComputableTidilyInPolyTime (fun (p : ℕ × ℕ) => p.1 - p.2) (encPair encNat encNat) encNat

Truncated subtraction of binary naturals, reusing the shared plain schoolbook certificate.

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

Subtract computed binary values, truncating at zero and fixing their intermediate encodings.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.binary_testBit {α : Type} {input : α ↪ List Bool} {n i : α → ℕ} (hn : ComputableTidilyInPolyTime n input encNat) (hi : ComputableTidilyInPolyTime i input encUnary) : ComputableTidilyInPolyTime (fun (a : α) => (n a).testBit (i a)) input encBool

Read the bit of a computed binary number at a computed unary position.

theorem Turing.MultiTapeTM.ComputableInPolyTime.binary_bitwise (op : Bool → Bool → Bool) (h0 : op false false = false) : ComputableInPolyTime (fun (p : ℕ × ℕ) => Nat.bitwise op p.1 p.2) (encPair encNat encNat) encNat

Any zero-preserving bitwise operation on binary naturals is polynomial-time.

theorem Turing.MultiTapeTM.ComputableInPolyTime.binary_and : ComputableInPolyTime (fun (p : ℕ × ℕ) => p.1 &&& p.2) (encPair encNat encNat) encNat

Bitwise AND of binary naturals.

theorem Turing.MultiTapeTM.ComputableInPolyTime.binary_or : ComputableInPolyTime (fun (p : ℕ × ℕ) => p.1 ||| p.2) (encPair encNat encNat) encNat

Bitwise OR of binary naturals.

theorem Turing.MultiTapeTM.ComputableInPolyTime.binary_xor : ComputableInPolyTime (fun (p : ℕ × ℕ) => p.1 ^^^ p.2) (encPair encNat encNat) encNat

Bitwise XOR of binary naturals.

theorem Turing.MultiTapeTM.ComputableInPolyTime.binary_and' {α : Type} {input : α ↪ List Bool} {left right : α → ℕ} (hleft : ComputableInPolyTime left input encNat) (hright : ComputableInPolyTime right input encNat) : ComputableInPolyTime (fun (a : α) => left a &&& right a) input encNat

Bitwise AND of computed binary naturals.

theorem Turing.MultiTapeTM.ComputableInPolyTime.binary_or' {α : Type} {input : α ↪ List Bool} {left right : α → ℕ} (hleft : ComputableInPolyTime left input encNat) (hright : ComputableInPolyTime right input encNat) : ComputableInPolyTime (fun (a : α) => left a ||| right a) input encNat

Bitwise OR of computed binary naturals.

theorem Turing.MultiTapeTM.ComputableInPolyTime.binary_xor' {α : Type} {input : α ↪ List Bool} {left right : α → ℕ} (hleft : ComputableInPolyTime left input encNat) (hright : ComputableInPolyTime right input encNat) : ComputableInPolyTime (fun (a : α) => left a ^^^ right a) input encNat

Bitwise XOR of computed binary naturals.

theorem Turing.MultiTapeTM.ComputableInPolyTime.binary_size : ComputableInPolyTime Nat.size encNat encUnary

The bit-length Nat.size n of a binary natural, returned in unary.

theorem Turing.MultiTapeTM.ComputableInPolyTime.binary_min_unary : ComputableInPolyTime (fun (p : ℕ × ℕ) => min p.1 p.2) (encPair encUnary encNat) encUnary

The smaller of a unary natural and a binary natural, returned in unary by saturating binary decoding.

theorem Turing.MultiTapeTM.ComputableInPolyTime.binary_min_unary' {α : Type} {input : α ↪ List Bool} {left right : α → ℕ} (hleft : ComputableInPolyTime left input encUnary) (hright : ComputableInPolyTime right input encNat) : ComputableInPolyTime (fun (a : α) => min (left a) (right a)) input encUnary

Cap a computed binary natural by a computed unary bound, returning the result in unary.

theorem Turing.MultiTapeTM.ComputableInPolyTime.binary_shiftRight : ComputableInPolyTime (fun (p : ℕ × ℕ) => p.1 >>> p.2) (encPair encNat encNat) encNat

Right shift of binary naturals, by dropping at most the dividend's bit length of low-order digits.

theorem Turing.MultiTapeTM.ComputableInPolyTime.binary_shiftRight' {α : Type} {input : α ↪ List Bool} {left right : α → ℕ} (hleft : ComputableInPolyTime left input encNat) (hright : ComputableInPolyTime right input encNat) : ComputableInPolyTime (fun (a : α) => left a >>> right a) input encNat

Right shift of computed binary naturals.

theorem Turing.MultiTapeTM.ComputableInPolyTime.binary_lt' {α : Type} {input : α ↪ List Bool} {left right : α → ℕ} (hleft : ComputableInPolyTime left input encNat) (hright : ComputableInPolyTime right input encNat) : ComputableInPolyTime (fun (a : α) => decide (left a < right a)) input encBool

The strict order of two computed numbers in binary.

Plain polynomial-time automation

theorem Turing.MultiTapeTM.ComputableInPolyTime.binary_two_pow : ComputableInPolyTime (fun (k : ℕ) => 2 ^ k) encUnary encNat

2 ^ k in binary, from k in unary, by doubling.

theorem Turing.MultiTapeTM.ComputableInPolyTime.binary_sub' {α : Type} {input : α ↪ List Bool} {left right : α → ℕ} (hleft : ComputableInPolyTime left input encNat) (hright : ComputableInPolyTime right input encNat) : ComputableInPolyTime (fun (a : α) => left a - right a) input encNat

Subtract computed binary values using the shared plain certificate.

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

Turing.MultiTapeTM.ComputableTidilyInPolyTime.binary_pow' for plain certificates.