Documentation

Transfer.Examples.ExampleField

A self-contained example field for the Trocq engine demos #

The Trocq parametricity engine in this directory (Related/RelatedBinOp, the transfer/rcongr/param_* tactics, the @[transfer]/@[param] databases) is field-agnostic: it transfers any registered commuting square enc (op x y) = bop (enc x) (enc y) regardless of what the carrier is.

The demos need one concrete field with two registered operations. This module provides them — F, bbFieldMul, bbFieldAdd, bbFieldMul_eq, bbFieldAdd_eq — built only from Mathlib. F is ZMod p for the Baby Bear prime p = 2^31 - 2^27 + 1, and the two example operations are named op-tree heads distinct from the abstract */+, each proved equal to the abstract operation — exactly the shape the transfer engine consumes.

The operations here are an illustrative instance of a registered RelatedBinOp. A realization by compiled machine-word arithmetic, where bbFieldMul_eq is an encode/compute/decode theorem, has the same shape, and the engine treats it in the same way.

source
def Transfer.ExampleField.exampleFieldPrime :
ℕ

The Baby Bear prime 2^31 - 2^27 + 1.

Equations
Instances For
    source
    instance Transfer.ExampleField.instNeZeroNatExampleFieldPrime :
    NeZero exampleFieldPrime
    source
    @[reducible, inline]
    abbrev Transfer.ExampleField.F :
    Type

    The example carrier F = ZMod p (a commutative ring; primality is not asserted, see the note above). Built from Mathlib alone.

    Equations
    Instances For
      source
      def Transfer.ExampleField.bbFieldMul (a b : F) :
      F

      An example binary operation registered as realizing abstract *. It is a distinct op-tree head from HMul.hMul, proved equal to * by bbFieldMul_eq.

      Equations
      Instances For
        source
        def Transfer.ExampleField.bbFieldAdd (a b : F) :
        F

        An example binary operation registered as realizing abstract +. Distinct op-tree head from HAdd.hAdd, proved equal to + by bbFieldAdd_eq.

        Equations
        Instances For
          source
          theorem Transfer.ExampleField.bbFieldMul_eq (a b : F) :
          bbFieldMul a b = a * b

          bbFieldMul realizes the abstract field product.

          source
          theorem Transfer.ExampleField.bbFieldAdd_eq (a b : F) :
          bbFieldAdd a b = a + b

          bbFieldAdd realizes the abstract field sum.