(edits are also saved when you close the window). Finally you can
Roadmap for the lesson:
- introduction to HB
- 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
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.
- 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
- by quotienting (out of scope of the tutorial).
Let's open an module and redefine 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:
**
Reasoning modulo p.
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.
Application to building the field of Gauss integers
- First we define a predicate for the algebraic numbers which are Gaussian integers.
We prove that Gaussian integers form a subring
- Finally, we define the type of Gaussian Integer, as a sigma type of algebraic numbers. We soon prove that this is in fact a sub type.
- We provide the subtype property, this makes it possible to use the generic operator
val
to get an algC from a Gaussian Integer.
- Moreover provide a commutative ring structure to the type GI, using the subring canonical property for the predicate gaussInteger