Documentation

Transfer.Examples.CoqEAL.SeqPoly

CoqEAL seqpoly, ported to Lean — List R refines the coefficient function #

CoqEAL's seqpoly refines MathComp polynomials {poly R} to lists seq R. Here we port the data-refinement core of that example into the ReprTransfer framework: a coefficient list List R refines the abstract coefficient function ℕ → R, and the concrete list addition addSeq refines the abstract coefficient-wise addition — the CoqEAL Radd_seqpoly refinement square.

The refinement mechanism — a relation between an abstract and a concrete representation, plus transfer of operations — is the ReprTransfer layer; this file is one worked instance over the seqpoly representation. The CoqEAL aggregator records the suite's frontier (the general-size algorithms and the normal-form theory).

source
def Transfer.Examples.CoqEAL.SeqPoly.coeff {R : Type u_1} [AddZeroClass R] (l : List R) (i : ℕ) :
R

The CoqEAL seqpoly refinement relation: a coefficient list denotes the abstract coefficient function (absent coefficients are 0).

Equations
Instances For
    source
    def Transfer.Examples.CoqEAL.SeqPoly.addSeq {R : Type u_1} [AddZeroClass R] :
    List R → List R → List R

    The concrete (computational) polynomial addition on coefficient lists.

    Equations
    Instances For
      source
      theorem Transfer.Examples.CoqEAL.SeqPoly.coeff_addSeq {R : Type u_1} [AddZeroClass R] (p q : List R) (i : ℕ) :
      coeff (addSeq p q) i = coeff p i + coeff q i

      The CoqEAL Radd_seqpoly refinement square. The concrete list addition refines the abstract coefficient-wise addition.

      source
      theorem Transfer.Examples.CoqEAL.SeqPoly.coeff_addSeq_fun {R : Type u_1} [AddZeroClass R] (p q : List R) :
      coeff (addSeq p q) = fun (i : ℕ) => coeff p i + coeff q i

      Functional form of the refinement square — the commuting square the ReprTransfer registry consumes (concrete add ↦ abstract pointwise add).