CoqEAL Karatsuba polynomial multiplication, ported to Lean #
CoqEAL's karatsuba is the headline algorithm refinement of the library: a fast
polynomial multiply proven to refine the schoolbook product. This file ports the
algebraic core of that refinement onto CompPoly's computable CPolynomial R, and
registers it in the engine's @[transfer] registry (Transfer.Base.Core).
What is proved #
The Karatsuba trick rewrites a single split product
(lo + Xᵏ·hi) · (lo' + Xᵏ·hi')
= z₀ + Xᵏ·z₁ + X²ᵏ·z₂
with z₀ = lo·lo', z₂ = hi·hi', and z₁ = (lo+hi)·(lo'+hi') − z₀ − z₂ — i.e.
three multiplications instead of four. karatsubaMul is exactly this
recombination on the four halves, and karatsubaMul_eq proves it equals the
product of the two reconstructed polynomials.
The proof transfers the goal across CompPoly's RingEquiv
CPolynomial R ≃+* Polynomial R (CPolynomial.ringEquiv, whose underlying map
toPoly is injective) to Mathlib's Polynomial R, where the recombination
identity is a commutative-ring fact discharged by ring. The transfer is sound
because toPoly is a ring homomorphism on +, -, *, ^ (CompPoly's
toPoly_add / toPoly_sub / toPoly_mul / toPoly_pow), so no coefficient
reasoning is duplicated and canonicalization (trailing-zero trimming) is handled
inside those CompPoly lemmas.
Scope #
This is the one-level Karatsuba step, taking the four halves as explicit
arguments. A full karatsubaMul' : CPolynomial R → CPolynomial R → CPolynomial R
would (a) split each input at a chosen degree k (a divByMonic/modByMonic
or array-extract operation on the canonical representation), (b) recurse on
the three half-products, and (c) terminate by a decreasing-degree measure with a
base case below a cutoff. The splitting and the recursion/termination (matching CoqEAL's
Rmorph_karatsuba over MathComp {poly R}) are not part of this file, which
proves the algebraic identity and karatsubaMul = (· * ·) for the structured
(already split) case. KaratsubaRec supplies the splitting and the fuel
recursion.
Registry entry #
karatsuba_repr is tagged @[transfer] in the refine direction (structured
product ↦ Karatsuba recombination), so repr_transfer automatically rewrites a
CPolynomial product presented in split form (lo + Xᵏ·hi)·(lo' + Xᵏ·hi') to
its three-multiplication Karatsuba form.
One-level Karatsuba recombination on the four halves of a split product.
Given the low/high halves lo, hi of p = lo + Xᵏ·hi and lo', hi' of
q = lo' + Xᵏ·hi', this computes the product p · q using only three
half-multiplications (z₀, z₂, and the middle (lo+hi)·(lo'+hi'))
instead of the four a naive cross product would use:
z₀ + Xᵏ·z₁ + X²ᵏ·z₂ with z₁ = (lo+hi)·(lo'+hi') − z₀ − z₂.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Correctness of the Karatsuba step. The recombination equals the product
of the two reconstructed polynomials lo + Xᵏ·hi and lo' + Xᵏ·hi'.
Proved by transferring across the ring equivalence
CPolynomial.ringEquiv : CPolynomial R ≃+* Polynomial R (injective toPoly)
to Mathlib Polynomial R, where the identity is a ring fact. This is the
Karatsuba algebraic identity in full; the recursion/termination/splitting is
the named residual (see the module docstring).
Registry entry (refinement direction). Tagged @[transfer] so that
repr_transfer rewrites a structured CPolynomial product
(lo + Xᵏ·hi)·(lo' + Xᵏ·hi') to its Karatsuba three-multiplication form
karatsubaMul k lo hi lo' hi'. This makes Karatsuba a registered refinement
in the transfer engine, alongside the field-kernel and SeqPoly
add refinements.