We describe here best practices for contributing to the library. In particular we explain what conventions are used in the library. When contributing, you should comply to these conventions to get your code integrated to the library.
This file is not comprehensive yet and might still contain mistakes or unclear indications, please consider contributing to its improvement.
- One important guideline is to structure proofs in blocks, i.e.,
forward steps, to limit the scope of errors.
- See G. Gonthier, A. Mahboubi, "An introduction to small scale reflection in Coq", p.103 for an illustration
- A line should have no more than 80 characters. If a line is longer than that, it should be cut semantically. If there is no way to make a semantic cut (e.g. the user provides an explicit term that is too long to fit on one line), then just cut it over several lines to make it readable.
- Lines end with a point
.
and only have;
inside them. - Lines that close a goal must start with a terminator (
by
orexact
). You should consider using an editor that highlights those terminators in a specific color (e.g. red). - Chaining too many optional rewrites makes error detection hard. The idiom is
rewrite conditional_rule ?simplify_side_condition // next_rule.
- Do not use
Focus
or{}
, use the relevant indentation, along with terminators likeby
orexact
.
We write
move=>
andmove:
(no space betweenmove
and=>
or:
)apply/
andapply:
(no space betweenapply
and/
or:
)rewrite /definition
(there is a space betweenrewrite
and an unfold)
-
When two subgoals are created, the first subgoal is indented by 2 spaces, the second is not. Use
last first
to bring the smallest/less meaningful goal first, and keep the main flow of the proof unindented. -
When more than two subgoals are created, bullets are used
-
for the first level,+
for the second and*
for the third as in:tactic. - tactic. + tactic. * tactic. * tactic. * tactic. + tactic. + tactic. - tactic - tactic
If all the subgoals have the same importance, use bullets for all of them, however, if one goal is more important than the others (i.e. is main flow of the proof). Then you might remove the bullet for this last one and unindent it as in:
tactic. - tactic. (* secondary subgoal 1 *) - tactic. (* secondary subgoal 2 *) tactic. (* third subgoal is the main one *)
- Universal quantifications with dependent variable should appear on the left hand side of the colon, until we reach the first non dependent variables. e.g.
Lemma example x y : x < y -> x >= y = false
- Operators are surrounded by space, for example
n*m
should be writtenn * m
. This particular example can be problematic if matrix.v is imported because then,M *m N
is matrix product.
-
There is a number of "macros" that are available to state lemmas, like
commutative
,associative
,... (seessrfun.v
) -
There are also macros that are available to localize a statement, like
{in A, P}
,... (seessrbool.v
)
- Variable/hypothesis names follow the following conventions.
- Hypothesis should not be named
H
,H'
,... (these collide with subgroup variable conventions) but have meaningful names. For example, an hypothesisn > 0
should be namedn_gt0
. - Induction Hypotheses are prefixed by
IH
orih
(e.g. induction hypothesis onn
is calledIHn
). - Natural numbers and integers should be named
m
,n
,p
,d
, ... - Elements of another ring should be named
x
,y
,z
,u
,v
,w
, ... - Polynomials should be named by lower case letter
p
,q
,r
... (to avoid collision with properties namedP
,Q
, ...) - Matrices should be named
A
,B
, ...,M
,N
, ... - Polymorphic variables should be named
x
, ...
- Hypothesis should not be named
- Variables/hypotheses that do not survive the line can be introduced using
?
. - Variables/hypotheses with a very short scope (~ 1-5 lines) can have a short name.
- Variables/hypotheses with a longer scope (> 5 lines) must have a meaningful name.
Names in the library usually obey one of the following conventions:
(condition_)?mainSymbol_suffixes
mainSymbol_suffixes(_condition)?
Or in the presence of a property denoted by an n-ary 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 (e.g., 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.)
- one of the main symbols of the theory at hand (e.g., it will be
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
forinjective
,id
for "identity", etc.) or an abbreviation.
There is an underscore before suffixes
when suffixes
starts with a one-letter small identifier (i.e., not a capital letter or a number or a longer identifier such as if
). Since the intent is to make the suffixes
readable enough, there are exceptions for short names (e.g., lern1
).
Abbreviations are in the header of the file which introduces them. We list here the main abbreviations.
A
-- associativity, as inandbA : associative andb
AC
-- right commutativityACA
-- self-interchange (inner commutativity), e.g.,orbACA : (a || b) || (c || d) = (a || c) || (b || d)
b
-- a boolean argument, as inandbb : idempotent andb
C
-- commutativity, as inandbC : commutative andb
-- alternatively, predicate or set complement, as inpredC
-- alternatively, constantCA
-- left commutativityD
-- predicate or set difference, as inpredD
E
-- elimination lemma, as innegbFE : ~~ b = false -> b
F
orf
-- boolean false, as inandbF : b && false = false
F
-- alternatively, about a finite typeg
-- a group argument.I
-- left/right injectivity, as inaddbI : right_injective addb
-- alternatively predicate or set intersection, as inpredI
l
-- the left-hand of an operation, as inandb_orl : left_distributive andb orb
ltr_norml x y : (`|x| < y) = (- y < x < y)
L
-- the left-hand of a relation, as inltn_subrL : n - m < n = (0 < m) && (0 < n)
LR
-- moving an operator from the left-hand to the right-hand of an relation, as inleq_subLR : (m - n <= p) = (m <= n + p)
N
orn
-- boolean negation, as inandbN : a && (~~ a) = false
n
-- alternatively, it is a natural number argumentN
-- alternatively ring negation, as inmulNr : (- x) * y = - (x * y)
P
-- a characteristic property, often a reflection lemma, as inandP : reflect (a /\ b) (a && b)
r
-- a right-hand operation, as inorb_andr : right_distributive orb andb
ler_normr x y : (x <= `|y|) = (x <= y) || (x <= - y)
- alternatively, it is a ring argument
R
-- the right-hand of a relation, as inltn_subrR : n < n - m = false
RL
-- moving an operator from the right-hand to the left-hand of an relation, as inltn_subRL : (n < p - m) = (m + n < p)
T
ort
-- boolean truth, as inandbT: right_id true andb
T
-- alternatively, total setU
-- predicate or set union, as inpredU
W
-- weakening, as inin1W : {in D, forall x, P} -> forall x, P
0
-- ring or nat 0, or empty set, as inaddr0 : x + 0 = x
1
-- ring; nat or group 1, as inmulr1 : x * 1 = x
D
-- addition, as inlinearD : f (u + v) = f u + f v
B
-- subtraction, as inopprB : - (x - y) = y - x
M
-- multiplication, as ininvfM : (x * y)^-1 = x^-1 * y^-1
Mn
-- ring nat multiplication, as inraddfMn : f (x *+ n) = f x *+ n
V
-- multiplicative inverse, as inmulVr : x^-1 * x = 1
X
-- exponentiation, as inrmorphXn : f (x ^+ n) = f x ^+ n
Xn
-- nat exponentiationXz
-- int exponentiation
Z
-- (left) module scaling, as inlinearZ : f (a *: v) = s *: f v
z
-- an int argumentp
-- positive number, as inltr_pM2l x : 0 < x -> {mono *%R x : x y / x < y}
n
-- negative numberw
-- non strict (weak) monotony, as inler_wpM2r x : 0 <= x -> {homo *%R^~ x : y z / y <= z}
wp
-- non-negative numberwn
-- non-positive number
- For the infix membership predicate
_ \in _
, the prefixin_
is used for lemmas that unfold specific predicates, possibly propagating the infix membership (e.g,in_cons
orin_set0
). These lemmas are generally part of theinE
multirule. Other lemmas involving the infix membership predicated use the generic prefixmem_
(e.g.,mem_head
ormem_map
).
Search _ "prefix" "suffix"* (symbol|pattern)* in library.
(for coq < 8.12)Search "prefix" "suffix"* (symbol|pattern)* inside library.
(for coq >= 8.12)
- types of mathematical structures
- Mixed case, the first letter lowercase and the first letter of each internal
word capitalized, end with
Type
- e.g.,
unitRingType
- Mixed case, the first letter lowercase and the first letter of each internal
word capitalized, end with
- HB structures
- Mixed case, the first letter of each internal word capitalized
- e.g.,
UnitRing
- interfaces (mixins, factories)
- when the interface sits at the bottom of a hierarchy: mixed case, starts
with
is
orhas
, the first letter of each internal word capitalized- e.g.,
hasChoice
,isZsemimodule
- e.g.,
- when the interface extends a structure
A
into a structureB
usingC
:A_C_isB
orA_C_hasB
whereB
andC
are mixed case, the first letter of each internal word capitalized- e.g.,
Zsemimodule_isZmodule
,SemiRing_hasCommutativeMul
,Lattice_Meet_isDistrLattice
- exceptions:
Choice_
,Equality_
can be omitted
- e.g.,
- when the interface sits at the bottom of a hierarchy: mixed case, starts
with
- Coq modules
- Mixed case, the first letter of each internal word capitalized
- e.g.,
NumDomain
inssrnum.v
- The following are considered as single words and are abbreviated when used as prefixes
- Z-module becomes
zmod
/Zmod
, e.g.,ZmodType
inssralg.v
,normedZmodType
inssrnum.v
- L-module becomes
lmod
/Lmod
- L-algebra becomes
lalg
/Lalg
- Z-module becomes
- Partial order is abbreviated to
porder
orPOrder
, e.g.,porderType
,CanPOrderMixin
inorder.v
Definitions and lemmas should never be removed or renamed without warning users:
they should be deprecated first, during at least one release.
We use the pragma deprecated
to implement deprecation of definitions and lemmas;
see the many examples in the source code.
We try to keep deprecation warnings for at least two years unless we need to remove them
(for example because of a name clash, and in any case after at least one release); after this period, deprecation warnings
might disappear at any moment, making the deletion or the renaming definitive.
See this wiki entry
First
From HB Require Import structures.
The structure names can be found in the header comments, for instance,
the eqType
structure is defined in
eqtype.v
.
Basic information about structures can be obtained via HB.about
, for
instance
HB.about eqType.
Factories enabling to build a structure can be discovered with
HB.howto
, for instance
HB.howto eqType.
tells us that eqType
instances can be built with hasDecEq.Build
.
(Note that by default HB.howto
may not return all the available factories;
it might be necessary to increase the depth search using a natural number
as in HB.howto xyzType 5
.)
One can then
HB.about hasDecEq.Build.
to learn that hasDecEq.Build
is expecting a type T
, a predicate
eq_op : rel T
(implicit argument, as indicated by the square
brackets) and proof of Equality.axiom eq_op
. One can thus
instantiate an eqType
on some type T
with
HB.instance Definition _ := hasDecEq.Build T proof_of_Equality_axiom.
or
HB.instance Definition _ := @hasDecEq.Build T eq_op proof_of_Equality_axiom.
which should output a few lines among which:
module_T__canonical__eqtype_Equality is defined
(beware that the output may not be visible by default with VSCoq). Absence of such a line indicates failure of the command.
In addition to the regular factories, listed by HB.howto
, the
library defines some aliases (aka feather factories). Those aliases
are documented in the header comments. For instance, an eqType
instance on some type T
can be derived from some T'
already
equipped with an eqType
structure, given a function f : T -> T'
and a proof injf : injective f
HB.instance Definition _ := Equality.copy T (inj_type injf).
Instances a type is already equipped with can be listed with
HB.about
, for instance
HB.about bool.
lists all the structures bool
is already equipped with.
A graph of the hierarchy can be obtained with
HB.graph "hierarchy.dot".
then
tred hierarchy.dot | xdot
or
tred hierarchy.dot | dot -Tpng > hierarchy.png
See the documentation of Hierarchy Builder.