9.5. Principal operations🔗

Arithmetic is coefficientwise where it can be (addition, subtraction, negation, scalar and monomial scaling) and a schoolbook convolution for multiplication. Each operation re-normalizes its result, so the output is again a canonical representative. The standard Add, Sub, Neg, and Mul instances on Hex.DensePoly dispatch to these, so p + q, p - q, -p, and p * q notation works directly.

def

Hex.DensePoly.add.{u} {R : Type u} [Zero R] [DecidableEq R] [Add R]
  (p q : Hex.DensePoly R) : Hex.DensePoly R
Hex.DensePoly.add.{u} {R : Type u}
  [Zero R] [DecidableEq R] [Add R]
  (p q : Hex.DensePoly R) :
  Hex.DensePoly R

Add two dense polynomials coefficientwise.

def

Hex.DensePoly.sub.{u} {R : Type u} [Zero R] [DecidableEq R] [Sub R]
  (p q : Hex.DensePoly R) : Hex.DensePoly R
Hex.DensePoly.sub.{u} {R : Type u}
  [Zero R] [DecidableEq R] [Sub R]
  (p q : Hex.DensePoly R) :
  Hex.DensePoly R

Subtract two dense polynomials coefficientwise.

def

Hex.DensePoly.neg.{u} {R : Type u} [Zero R] [DecidableEq R] [Sub R]
  (p : Hex.DensePoly R) : Hex.DensePoly R
Hex.DensePoly.neg.{u} {R : Type u}
  [Zero R] [DecidableEq R] [Sub R]
  (p : Hex.DensePoly R) : Hex.DensePoly R

Coefficientwise additive inverse, expressed through executable subtraction.

def

Hex.DensePoly.scale.{u} {R : Type u} [Zero R] [DecidableEq R] [Mul R]
  (c : R) (p : Hex.DensePoly R) : Hex.DensePoly R
Hex.DensePoly.scale.{u} {R : Type u}
  [Zero R] [DecidableEq R] [Mul R] (c : R)
  (p : Hex.DensePoly R) : Hex.DensePoly R

Multiply every coefficient by c.

def

Hex.DensePoly.shift.{u} {R : Type u} [Zero R] [DecidableEq R] (n : ℕ)
  (p : Hex.DensePoly R) : Hex.DensePoly R
Hex.DensePoly.shift.{u} {R : Type u}
  [Zero R] [DecidableEq R] (n : ℕ)
  (p : Hex.DensePoly R) : Hex.DensePoly R

Multiply by x^n.

def

Hex.DensePoly.mul.{u} {R : Type u} [Zero R] [DecidableEq R] [Add R]
  [Mul R] (p q : Hex.DensePoly R) : Hex.DensePoly R
Hex.DensePoly.mul.{u} {R : Type u}
  [Zero R] [DecidableEq R] [Add R] [Mul R]
  (p q : Hex.DensePoly R) :
  Hex.DensePoly R

Schoolbook dense polynomial multiplication by direct coefficient convolution.

The inner j-loop reads the loop-invariant coefficient p.coeff i from a single let-bound value (pi) instead of re-projecting it on every (i, j) step, so the compiled inner loop performs one bounds-checked coefficient read per i rather than per (i, j). The let is a zeta reduction away from the bare convolution, so it does not change the value, the coeff_mul spec, or any proof.

Evaluation, composition, and the formal derivative complete the operations. Evaluation and composition both use Horner's method.

def

Hex.DensePoly.eval.{u} {R : Type u} [Zero R] [DecidableEq R] [Add R]
  [Mul R] (p : Hex.DensePoly R) (x : R) : R
Hex.DensePoly.eval.{u} {R : Type u}
  [Zero R] [DecidableEq R] [Add R] [Mul R]
  (p : Hex.DensePoly R) (x : R) : R

Evaluate a polynomial using Horner's method.

def

Hex.DensePoly.compose.{u} {R : Type u} [Zero R] [DecidableEq R] [Add R]
  [Mul R] (p q : Hex.DensePoly R) : Hex.DensePoly R
Hex.DensePoly.compose.{u} {R : Type u}
  [Zero R] [DecidableEq R] [Add R] [Mul R]
  (p q : Hex.DensePoly R) :
  Hex.DensePoly R

Compose polynomials using Horner's method.

def

Hex.DensePoly.derivative.{u} {R : Type u} [Zero R] [DecidableEq R]
  [NatCast R] [Mul R] (p : Hex.DensePoly R) : Hex.DensePoly R
Hex.DensePoly.derivative.{u} {R : Type u}
  [Zero R] [DecidableEq R] [NatCast R]
  [Mul R] (p : Hex.DensePoly R) :
  Hex.DensePoly R

Formal derivative. The coefficient of x^i becomes (i + 1) * a_(i+1).

Each operation comes with a characterising coefficient law. These are the lemmas downstream proofs rewrite with. The zero-absorption side conditions (hzero) are discharged automatically over any semiring, via the *_semiring/*_ring specializations.

theorem

Hex.DensePoly.coeff_add.{u} {R : Type u} [Zero R] [DecidableEq R]
  [Add R] (p q : Hex.DensePoly R) (n : ℕ)
  (hzero : Zero.zero + Zero.zero = Zero.zero) :
  (p + q).coeff n = p.coeff n + q.coeff n
Hex.DensePoly.coeff_add.{u} {R : Type u}
  [Zero R] [DecidableEq R] [Add R]
  (p q : Hex.DensePoly R) (n : ℕ)
  (hzero :
    Zero.zero + Zero.zero = Zero.zero) :
  (p + q).coeff n = p.coeff n + q.coeff n

Coefficient law for addition. The explicit zero law is needed because the generic Add/Zero interface does not imply 0 + 0 = 0.

theorem

Hex.DensePoly.coeff_mul.{u} {R : Type u} [Zero R] [DecidableEq R]
  [Add R] [Mul R] (p q : Hex.DensePoly R) (n : ℕ) :
  (p * q).coeff n = p.mulCoeffSum q n
Hex.DensePoly.coeff_mul.{u} {R : Type u}
  [Zero R] [DecidableEq R] [Add R] [Mul R]
  (p q : Hex.DensePoly R) (n : ℕ) :
  (p * q).coeff n = p.mulCoeffSum q n

Characterising coefficient law for multiplication: each coefficient of p * q is computed by the same nested schoolbook fold as the executable multiplication loop.

theorem

Hex.DensePoly.coeff_sub.{u} {R : Type u} [Zero R] [DecidableEq R]
  [Sub R] (p q : Hex.DensePoly R) (n : ℕ)
  (hzero : Zero.zero - Zero.zero = Zero.zero) :
  (p - q).coeff n = p.coeff n - q.coeff n
Hex.DensePoly.coeff_sub.{u} {R : Type u}
  [Zero R] [DecidableEq R] [Sub R]
  (p q : Hex.DensePoly R) (n : ℕ)
  (hzero :
    Zero.zero - Zero.zero = Zero.zero) :
  (p - q).coeff n = p.coeff n - q.coeff n

Coefficient law for subtraction. The explicit zero law is needed because the generic Sub/Zero interface does not imply 0 - 0 = 0.

theorem

Hex.DensePoly.coeff_derivative.{u} {R : Type u} [Zero R] [DecidableEq R]
  [NatCast R] [Mul R] (p : Hex.DensePoly R) (n : ℕ)
  (hzero : ↑(n + 1) * Zero.zero = Zero.zero) :
  p.derivative.coeff n = ↑(n + 1) * p.coeff (n + 1)
Hex.DensePoly.coeff_derivative.{u}
  {R : Type u} [Zero R] [DecidableEq R]
  [NatCast R] [Mul R]
  (p : Hex.DensePoly R) (n : ℕ)
  (hzero :
    ↑(n + 1) * Zero.zero = Zero.zero) :
  p.derivative.coeff n =
    ↑(n + 1) * p.coeff (n + 1)

Characterising coefficient law for the formal derivative: the coefficient of x^n in derivative p is (n + 1) * p.coeff (n + 1). The explicit zero law ((n + 1 : Nat) : R) * 0 = 0 is needed because the generic NatCast/Mul/Zero interface does not guarantee it, mirroring the hypothesis on coeff_scale.

9.5.1. Worked example: integer arithmetic🔗

The block below works over DensePoly Int. It builds a quadratic and a monomial, then computes their sum and product, an evaluation, and a derivative.

open Hex Hex.DensePoly

namespace HexPolyChapterArith

-- a = 1 + 2x + 3x²
private def a : DensePoly Int := ofCoeffs #[1, 2, 3]
-- b = x
private def b : DensePoly Int := monomial 1 1

-- The constructors normalize: trailing zeros are
-- dropped, and a monomial stores its one nonzero
-- coefficient at its degree.
#guard a.toArray.toList = [1, 2, 3]
#guard b.toArray.toList = [0, 1]
#guard a.degree? = some 2
#guard a.support = [0, 1, 2]
#guard a.coeff 2 = 3

-- A padded array collapses to the trimmed value.
#guard ofCoeffs #[1, 2, 3, 0, 0] = a
-- The zero constant is the zero polynomial.
#guard C (0 : Int) = (0 : DensePoly Int)

-- (1 + 2x + 3x²) + x = 1 + 3x + 3x²
#guard (a + b).toArray.toList = [1, 3, 3]
-- (1 + 2x + 3x²) · x = x + 2x² + 3x³
#guard (a * b).toArray.toList = [0, 1, 2, 3]
-- Evaluation by Horner: a(2) = 1 + 4 + 12 = 17.
#guard eval a 2 = 17
-- d/dx (1 + 2x + 3x²) = 2 + 6x.
#guard (derivative a).toArray.toList = [2, 6]

end HexPolyChapterArith