To play this document inside your browser use ALT-N and ALT-P.
If you get stack overflow
errors, try to use
Google Chrome
or Chromium
with the command line option --js-flags="--harmony-tailcalls".
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.
Extensive documentation in the header of:
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.
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) and in the Mathematical Components Book.
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.
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.
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.
The two most important things to get your way out of a situation:
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.
(condition_)?mainSymbol_suffixes
mainSymbol_suffixes(_condition)?
Or in the presence of a property denoted by a nary or unary predicate:
naryPredicate_mainSymbol+
mainSymbol_unaryPredicate
mainSymbolis 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
opp
, add
, mul
, etc...
canonicaloperation, such as a ring morphism or a subtype predicate. e.g.
linear
, raddf
, rmorph
, rpred
, etc ...
conditionis used when the lemma applies under some hypothesis.
suffixesare 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.
andbA : associative andb.
orbACA : (a || b) || (c || d) = (a || c) || (b || d).
andbb : idempotent andb.
andbC : commutative andb
,
or predicate complement, as in predC.
predD.
negbFE : ~~ b = false -> b
.
andbF : b && false = false.
addbI : right_injective addb
or predicate intersection, as in predI.
andb_orl : left_distributive andb orb.
andbN : a && (~~ a) = false.
andP : reflect (a /\ b) (a && b)
.
orb_andr : right_distributive orb andb.
andbT: right_id true andb.
predU
.
in1W : {in D, forall x, P} -> forall x, P.
addr0 : x + 0 = x.
mulr1 : x * 1 = x.
linearD : f (u + v) = f u + f v.
opprB : - (x - y) = y - x.
invfM : (x * y)^-1 = x^-1 * y^-1.
raddfMn : f (x *+ n) = f x *+ n.
mulNr : (- x) * y = - (x * y).
mulVr : x^-1 * x = 1.
rmorphX : f (x ^+ n) = f x ^+ n.
linearZ : f (a *: v) = s *: f v.
Search _ "prefix" "suffix"* (symbol|pattern)* in library.
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}
.
val : sT -> T
, insub : T -> option sT
and
insubd : sT -> T -> sT
.
val_inj, val_eqE, val_insubd, insubdK
and insub