Polynomial-time division and remainder on binary naturals

Schoolbook shift-and-subtract long division over the binary encoding Turing.MultiTapeTM.encNat. The dividend's binary digits are reversed to most-significant-bit-first order and folded with Turing.MultiTapeTM.BinaryDiv.divModStep, which shifts the running remainder by one bit, adds the next dividend bit, and subtracts the divisor whenever it fits. A zero divisor never subtracts, so the quotient stays 0 and the remainder reconstructs the dividend, matching a / 0 = 0 and a % 0 = a.

After consuming any prefix word of the reversed digits, the state (q, r) is the quotient and remainder of Cslib.BitString.binaryValue word by the divisor (BinaryDiv.foldl_divModStep). Both components are therefore at most binaryValue word < 2 ^ word.length, so their binary encodings have length at most word.length, keeping the encoded pair linearly bounded throughout the fold.

Main definitions

• Turing.MultiTapeTM.BinaryDiv.divModStep: one shift-and-subtract step of binary long division.

Main results

• Turing.MultiTapeTM.BinaryDiv.foldl_divModStep: folding divModStep over a most-significant-first bit word computes the quotient and remainder of its binaryValue.
• Turing.MultiTapeTM.BinaryDiv.divMod_eq: folding over a.bits.reverse computes (a / b, a % b).
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.binary_divMod: joint quotient and remainder on encNat.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.binary_div, .binary_mod: binary division and remainder on encNat.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.binary_div', .binary_mod': composition rules for fun_prop and polytime.
• Turing.MultiTapeTM.ComputableInPolyTime.binary_div': named composition rule for plain certificates.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.binary_divMod : ComputableTidilyInPolyTime (fun (p : ℕ × ℕ) => (p.1 / p.2, p.1 % p.2)) (encPair encNat encNat) (encPair encNat encNat)

Compute both quotient and remainder of binary naturals by shift-and-subtract long division.

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

Division of binary naturals.

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

Remainder of binary naturals.

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

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

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

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

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

Divide computed binary values using the shared plain certificate.