2.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 invoke 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.

Kernel-facing specification: a single padded walk of the two coefficient lists. Compiled code uses Hex.DensePoly.addImpl, the value-equal, one-allocation Array.ofFn loop selected by Hex.DensePoly.add_eq_impl.

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.

Like Hex.DensePoly.add, this is a kernel-reduction-friendly specification. Compiled code uses Hex.DensePoly.subImpl, the value-equal Array.ofFn loop selected by Hex.DensePoly.sub_eq_impl.

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.

Kernel-facing specification (one Hex.DensePoly.sub against the zero polynomial); compiled code uses Hex.DensePoly.negImpl, the value-equal Array.map pass selected by Hex.DensePoly.neg_eq_impl.

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.

Kernel-facing specification: one map over the reference coefficient list. Compiled code uses Hex.DensePoly.scaleImpl, the value-equal Array.map pass selected by Hex.DensePoly.scale_eq_impl.

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.

Kernel-facing specification: one replicate-append of the reference coefficient list. Compiled code uses Hex.DensePoly.shiftImpl, the value-equal Array.append implementation selected by Hex.DensePoly.shift_eq_impl.

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.

This definition is the kernel-reduction-friendly specification: the accumulator is a plain list walked head-first, so reducing a concrete product costs one cons-step per (i, j) coefficient pair instead of an O(size) list traversal per Array access. Compiled code instead runs the in-place Array loop Hex.DensePoly.mulImpl, selected by Hex.DensePoly.mul_eq_impl.

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.

Kernel-facing specification: one cons walk of the coefficient list, highest degree innermost. Compiled code uses Hex.DensePoly.evalImpl, the value-equal downward Array.foldr loop with no intermediate list or reverse allocation, selected by Hex.DensePoly.eval_eq_impl.

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.

Kernel-facing specification: one cons walk of the coefficient list. Compiled code uses Hex.DensePoly.composeImpl, the value-equal downward Array.foldr loop selected by Hex.DensePoly.compose_eq_impl.

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).

Kernel-facing specification: one cons walk of the coefficient tail. Compiled code uses Hex.DensePoly.derivativeImpl, the value-equal Array.ofFn loop selected by Hex.DensePoly.derivative_eq_impl.

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 Hex.DensePoly.coeff_scale.

2.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 := #p[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 literal with padding collapses to the trimmed value.
#guard #p[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