To play this document inside your browser use ALT-N and ALT-P. You can save your edits inside your browser and load them back (edits are also saved when you close the window). Finally you can download the file for offline editing.

The algebra library

  • This is a central part of the mathematical components library.
  • This library register a various range of (mathematical) structures.
    • types with decidable equality: eqType
    • types with a finite number of elements: finType
    • finite groups: finGroupType
    • abelian (not possibly finite) groups: zmodType
    • rings: ringType
    • rings with invertible elements: unitRingType
    • commutative rings: comRingType
    • integral domains: idomainType
    • fields: fieldType
    • left modules: lmodType
    • left algebra: lalgType
    • algebra: algType
    • finite dimensional vector spaces: vectType
    • ...

  • These structures share operators: e.g. the operator (_ + _), introduced for abelian groups (zmodType), is also available for all the structures that inherit it (rings, domains, fields, etc...)

  • All of these structures are discrete: they all have decidable equality: the operator (_ == _) is available on all of them.

  • Here is a picture of the begining of the hierarchy

    Extensive documentation in the header of:

  • In addition there are structures for maps (additive morphisms, ring morphisms, etc...), and substructures (subgroup, subsemiring, subring, subfield, etc...)

  • From math-comp 2.0 alpha, structures are generated by the external tool Hierarchy Builder

Roadmap for the lesson:

  • introduction of the general definition pattern for algebraic structures
  • instantiation of a structure in the library
  • exploration of the theory provided by this structure and naming conventions
  • creation of a algebraic substructure and predicate and their use

Defining a mathematical structure in Coq.

This is how mathematical structures are defined in the library. We define structures as sets of mixins (they look more like traits in object oriented slang)

Defining a mathematical hierarchy in Coq.

Adding a structure is adding more mixins and packaging them into structures.

Adding alternative definitions of structures to the hierarchy.

We need a factory and builders

Hierarchy Builder (HB) now automatically recognizes that hasPredOnC can define a Funny.type and only that, hence the failing structure definition. Now, one can use the factory hasPredOnC instead of hasFunnyPred to define a Funny.type.

Inhabiting the mathematical structures hierarchy.

  • We now show on the example of integers how to instantiate the mathematical structures that integers satisfy.

  • In order to minimize the work of the user, the library lets you inhabit structures by instanciating mixins and factory, one at a time. Each time we want to build structures, we only declare the mixin/factory as an HB.instance. One or several structures will be automatically instantiated.

  • We catagorize five different ways to build structures. Th three first will be shown here. The fourth will be shown in the exercices, and the fifth one won't be shown.

    • using a partially isomorphic structure (and providing the witness).
    • by instanciating just the required mixin from scratch,
    • by instanciating a factory to create one or several structures,
    • by subtyping (in the exercise session),
    • by quotienting (out of scope of the school).

First we define int

Equality, countable and choice types, by injection

We provide an injection with explicit partial inverse, from int to nat + nat, this will be enough to provide the mixins for equality, countable and choice types.

We create the mixins for equality, countable and choice types from this injection, and gradually inhabit the hierarchy.

Abelian group structure, from scratch

We now create the abelian group structure of integers (here called Z-module), from scratch, introducing the operators and proving exactly the required properties.

Remark: we may develop here a piece of abelian group theory which is specific to the theory of integers. E.g.

Ring and Commutative ring structure, the stronger the better

This time, we will build directly a rich commutative ring factory first and use it to instanciate both the ring structure and the commutative ring struture at the same time. This is not only an economy of space, but an economy of proofs, since the commutativity property reduces the number of ring axioms to prove.

Other structures and instances

About other algebraic structures:

  • read the documentation of ssralg and ssrnum (algebraic structures with order and absolute value)

  • Canonical instances in the library are:
    • integers (int) (forms an integral domain)
    • rationals (rat) (forms an archimedian field)
    • algebraic numbers (algC) (forms an algebraically closed field)
    • polynomials {poly R} (forms an integral domain under sufficient hypothesis on the base ring)
    • matrices 'M[R]_(m, n) (forms a module / a finite dimension vector space)
    • square matrices 'M[R]_n (forms an algebra, if n := m.+1)

Group theory (not in this course):

  • see fingroup, perm, action, ...

Structures for morphisms:

** Structure preserving predicates:

Naming conventions.

The two most important things to get your way out of a situation:

  • Knowing your math
  • Searching the library for what you think you know

For that you have the ssreflect Search command. To use its full power, one should combine seach by identifier (Coq definition), pattern (partial terms) and name (a string contained in the name of the theorem).

The two first methods are straightforward to use (except if you instanciate your patterns more than necessary), but searching by name requires to be aware of naming conventions.

Names in the library are usually obeying one of following the convention 

  • (condition_)?mainSymbol_suffixes
  • mainSymbol_suffixes(_condition)?

Or in the presence of a property denoted by a nary or unary predicate: 

  • naryPredicate_mainSymbol+
  • mainSymbol_unaryPredicate

Where :

  • mainSymbol is the most meaningful part of the lemma. It generally is the head symbol of the right-hand side of an equation or the head symbol of a theorem. It can also simply be the main object of study, head symbol or not. It is usually either

    • one of the main symbols of the theory at hand. For example, it will be opp, add, mul, etc...

    • or a special canonical operation, such as a ring morphism or a subtype predicate. e.g. linear, raddf, rmorph, rpred, etc ...

  • condition is used when the lemma applies under some hypothesis.

  • suffixes are there to refine what shape and/or what other symbols the lemma has. It can either be the name of a symbol (add, mul, etc...), or the (short) name of a predicate (inj for injectivity, id for identity, ...) or an abbreviation.

Abbreviations are in the header of the file which introduce them. We list here the main abbreviations.

  • A -- associativity, as in andbA : associative andb.
  • AC -- right commutativity.
  • ACA -- self-interchange (inner commutativity), e.g., orbACA : (a || b) || (c || d) = (a || c) || (b || d).
  • b -- a boolean argument, as in andbb : idempotent andb.
  • C -- commutativity, as in andbC : commutative andb, or predicate complement, as in predC.
  • CA -- left commutativity.
  • D -- predicate difference, as in predD.
  • E -- elimination, as in negbFE : ~~ b = false -> b.
  • F or f -- boolean false, as in andbF : b && false = false.
  • I -- left/right injectivity, as in addbI : right_injective addb or predicate intersection, as in predI.
  • l -- a left-hand operation, as andb_orl : left_distributive andb orb.
  • N or n -- boolean negation, as in andbN : a && (~~ a) = false.
  • n -- alternatively, it is a natural number argument
  • P -- a characteristic property, often a reflection lemma, as in andP : reflect (a /\ b) (a && b).
  • r -- a right-hand operation, as orb_andr : right_distributive orb andb.
    • - alternatively, it is a ring argument
  • T or t -- boolean truth, as in andbT: right_id true andb.
  • U -- predicate union, as in predU.
  • W -- weakening, as in in1W : {in D, forall x, P} -> forall x, P.
  • 0 -- ring 0, as in addr0 : x + 0 = x.
  • 1 -- ring 1, as in mulr1 : x * 1 = x.
  • D -- ring addition, as in linearD : f (u + v) = f u + f v.
  • B -- ring subtraction, as in opprB : - (x - y) = y - x.
  • M -- ring multiplication, as in invfM : (x * y)^-1 = x^-1 * y^-1.
  • Mn -- ring by nat multiplication, as in raddfMn : f (x *+ n) = f x *+ n.
  • mx -- a matrix argument
  • N -- ring opposite, as in mulNr : (- x) * y = - (x * y).
  • V -- ring inverse, as in mulVr : x^-1 * x = 1.
  • X -- ring exponentiation, as in rmorphX : f (x ^+ n) = f x ^+ n.
  • Z -- (left) module scaling, as in linearZ : f (a *: v) = s *: f v.
  • z -- a int operation

My most used search pattern 

Search "prefix" "suffix"* (symbol|pattern)* in library.

Examples

Revisiting an exercise from session 2

Instead of reasonning using (_ %| _) and (_ %% _), we switch to 'Z_p

More about structure preserving predicates.

There is a notion of subobject for a few algebraic concepts.

See the [hierarchy.dot], use [HB.about], [HB.howto] or read documentation headers to discover other substructure preserving predicates.

A reminder on subtyping.

  • In Coq, sT := {x : T | P x} is a way to form a sigma-type. We say it is a subtype if there is only one element it sT for each element in T. This happens when P is a boolean predicate. Another way to form a subtype is to create a record : Record sT := ST {x : T; px : P x}.

  • In mathcomp, to deal with subtypes independently from how they are formed, we have a structure.

  • The most important operators to know on subtypes are val : sT -> T, insub : T -> option sT and insubd : sT -> T -> sT.

  • And the most important theorems to know are val_inj, val_eqE, val_insubd, insubdK and insub

Substructures

Substructures are subtypes that happen to have the same structure as their base type.

There are special factories to instantiate them easily.

Moreover, when a predicate is declared as a structure preserving predicate, we can use it to declare a substructure automatically (see exercise session).