Documentation

Transfer.Examples.CoqEAL.ComputePolynomial

Computing with Mathlib's Polynomial through a CompPoly refinement #

Mathlib's Polynomial R is the proof-oriented object — a Finsupp, with the operations that matter for evaluation noncomputable. CompPoly's CPolynomial R is the computation-oriented refinement: an Array-backed representation (CPolynomial.Raw R := Array R) with a RingEquiv to Polynomial R (CompPoly.CPolynomial.ringEquiv, forward map toPoly).

This is the CoqEAL data refinement, and the Kaliszyk–O'Connor move that ReprTransfer records: compute with a classical object by running the computational representation and certifying the result against the classical one through the isomorphism. Here the classical object is Mathlib's Polynomial ℤ; the computation runs in CPolynomial ℤ; and coeff_toPoly / toPoly_mul certify that a coefficient computed by array arithmetic is the coefficient of the Mathlib product.

The ReprTransfer view: CPolynomial's * realizes Polynomial's * along the decoder toPoly — a BinOpHomOn (a homomorphism on the whole domain, no injectivity needed), the map-level rung of the transfer hierarchy.

source
@[reducible, inline]
abbrev Transfer.Param.CoqEAL.CP :
Type

The computational (array-backed) polynomial carrier over ℤ.

Equations
Instances For
    source
    def Transfer.Param.CoqEAL.poly1 :
    CP

    2X + 1, stored as an array.

    Equations
    Instances For
      source
      def Transfer.Param.CoqEAL.poly2 :
      CP

      3X + 1, stored as an array.

      Equations
      Instances For

        Compute #

        (2X + 1)(3X + 1) = 6X² + 5X + 1, by array arithmetic — #guard forces the computation and asserts each coefficient.

        Certify against Mathlib's Polynomial #

        source
        theorem Transfer.Param.CoqEAL.toPoly_mul' (a b : CP) :
        CompPoly.CPolynomial.toPoly (a * b) = CompPoly.CPolynomial.toPoly a * CompPoly.CPolynomial.toPoly b

        toPoly is a *-homomorphism into Mathlib's Polynomial (the map_mul of ringEquiv).

        source
        theorem Transfer.Param.CoqEAL.coeff_eq (a : CP) (i : ℕ) :
        CompPoly.CPolynomial.coeff a i = (CompPoly.CPolynomial.toPoly a).coeff i

        A coefficient computed on the array representation equals the coefficient of the Mathlib polynomial it denotes.

        The ReprTransfer realization #

        source
        theorem Transfer.Param.CoqEAL.polyMulRealization :
        ReprTransfer.BinOpHomOn CompPoly.CPolynomial.toPoly (fun (x : CompPoly.CPolynomial ℤ) => True) (fun (x1 x2 : CompPoly.CPolynomial ℤ) => x1 * x2) fun (x1 x2 : Polynomial ℤ) => x1 * x2

        CPolynomial's * realizes Mathlib Polynomial's * along the decoder toPoly: decoding the computed product equals the Mathlib product of the decoded operands, on the whole domain. This is the map-level BinOpHomOn — the field-arithmetic realizations (STARK / Baby Bear) share this rung.