Documentation

Transfer.Examples.CoqEAL.SeqMatrix

CoqEAL seqmatrix, ported to Lean — List (List R) refines the entry function #

CoqEAL's seqmatrix refines MathComp matrices 'M[R]_(m,n) to lists of lists seq (seq R). Here we port the data-refinement core of that example: a matrix-as-rows List (List R) refines the abstract entry function ℕ → ℕ → R (absent entries are 0), and the concrete row-wise list addition addMx refines the abstract entrywise addition — the CoqEAL Radd_seqmx refinement square.

This mirrors the companion SeqPoly.lean (seqpoly add) one dimension up: the inner row addition reuses the same addSeq-style coefficientwise add, and the outer addMx zips rows. The refinement mechanism — a relation between an abstract and a concrete representation, plus transfer of operations — is the same ReprTransfer layer; this file is one worked instance over the seqmatrix representation. SeqMatrixMul refines the multiplication; the CoqEAL aggregator records the suite's frontier.

source
def Transfer.Examples.CoqEAL.SeqMatrix.entry {R : Type u_1} [AddZeroClass R] (m : List (List R)) (i j : ℕ) :
R

The CoqEAL seqmatrix refinement relation: a row-major list of lists denotes the abstract entry function (absent rows and entries are 0).

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

    The concrete (computational) row addition on coefficient lists — the inner addSeq-style coefficientwise add, shared with the seqpoly example.

    Equations
    Instances For
      source
      theorem Transfer.Examples.CoqEAL.SeqMatrix.getD_addSeq {R : Type u_1} [AddZeroClass R] (p q : List R) (j : ℕ) :
      (addSeq p q).getD j 0 = p.getD j 0 + q.getD j 0

      The inner row-refinement square: the concrete row add refines pointwise add.

      source
      def Transfer.Examples.CoqEAL.SeqMatrix.addMx {R : Type u_1} [AddZeroClass R] :
      List (List R) → List (List R) → List (List R)

      The concrete (computational) matrix addition on lists of rows.

      Equations
      Instances For
        source
        theorem Transfer.Examples.CoqEAL.SeqMatrix.entry_addMx {R : Type u_1} [AddZeroClass R] (m n : List (List R)) (i j : ℕ) :
        entry (addMx m n) i j = entry m i j + entry n i j

        The CoqEAL Radd_seqmx refinement square. The concrete row-wise list addition refines the abstract entrywise matrix addition.

        source
        theorem Transfer.Examples.CoqEAL.SeqMatrix.entry_addMx_fun {R : Type u_1} [AddZeroClass R] (m n : List (List R)) :
        entry (addMx m n) = fun (i j : ℕ) => entry m i j + entry n i j

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