lesson5
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
- ...
- Some of these structures share operators: e.g. the operator (_ + _),
introduced for abelian groups (zmodType), is also available for all
the structures that require 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...)
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 subalgebraic structure predicate and use
Defining a mathematical structure in Coq.
This is how mathematical structures are defined in the library.
Unless you need to add a new mathematical structure to the library,
you will only need to read this.
This packaging is very elementary, and the mathematical components
library uses a refinement of this.
Packaging mathematical structures
We briefly explain how to do inheritance with two structures. This is
another simplified version of what happens in the library. The
complete process is described in
Packaging
Mathematical Structures (Garillot, Gonthier, Mahboubi, Rideau)
Inhabiting the mathematical structures hierarchy.
- We now show on the example of integers how to instantiate the
mathematical structures that integers satisfy.
- As a step to minimize the work of the user, the library provides a
way to provide only the mixin. The general pattern is to build the
mixin of a structure, declare the canonical structure associated
with it and go one with creating the next mixin and creating the new
structure. Each time we build a new structure, we provide only the
mixin, as the class can be inferred from the previous canonical
structures
- We now show three different ways to build mixins here and an
additional fourth will be shown in the exercices
- using a reference structure,
- building the required mixin from scratch,
- building a more informative mixin and using it for a weaker structure,
- (in the example) by subtyping.
First we define int
Equality, countable and choice types, by injection
We provide an injection with explicit partial inverse, grom 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. Try to swap any
of the three blocks to see what happen.
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.
Ring and Commutative ring structure, the stronger the better
This time, we will build directly a rich commutative ring mixin first
and use it to instanciate both the ring structure and the commutative
ring struture at the same time. This is not only a structural economy
of space, but a mathematical economy of proofs, since the
commutativity property reduces the number of ring axioms to prove.
Other structures
Extensions of rings
- read the documentation of ssralg and ssrnum (algebraic structures
with order)
Structures for morphisms
Substructures
Naming conventions.
Names in the library are usually obeying one of following the convention:
Or in the presence of a property denoted by a nary or unary predicate:
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, for
ssralg, 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. As in
-
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. 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.
- P -- a characteristic property, often a reflection lemma, as in andP : reflec t (a /\ b) (a && b).
- r -- a right-hand operation, as orb_andr : rightt_distributive orb andb.
- 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.
- 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.
This is design to help search. My own search strategy is usually.
Examples: