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.
Objective of this tutorial
Give you quick access to the
Mathematical Components library
- formalization techniques
- proof language
- familiarize with some theories
There will be two independent parts:
1. An overview of the specfics of the library.
Greatly inspired by Enrico Tassi's and Yves Bertot's
lectures at Math Comp School & Workshop - 2022.
Can be done online.
2. Zooming in on the generation and organization of algebraic hierachies.
You must install mathcomp 2 to follow on your computer.
Disclaimer & Ads:
- We usually do a FIVE DAYS of school with
Yves Bertot, Laurence Rideau, Enrico Tassi and Laurent Thery.
- I tried to reduce it to 3h, so you might only get a feeling.
What is the mathematical components library?
- large, consistent, library organized as a programming language
library (interfaces, overload, naming conventions, ...)
- maintainable in the long term (compact, stable, ...)
- validated on large formalization projects
The mathematical components library was used to formalize the
Odd Order Theorem (Feit Thompson), a 250 pages book.
Such proof amounts to 40k lines
of Coq scripts, on top of 120k lines of mathematical components.
The library has been maintained for more than 10 years now.
Roadmap of the first lesson
- An overview of existing libraries and their contents.
- Searching through the library.
- Naming conventions.
- Writing and reading proof scripts.
- Iterated operators.
An overview of existing libraries and their contents.
mathcomp core
consists of 6 packages:
- mathcomp-ssreflect: bigops, sequences (lists) and tuples,
natural number arithmetic, divisibility and primality,
finite types and sets, quotients, equalities, orders.
- mathcomp-fingroup: basic finite group theory, group morphisms,
permutations, actions and group quotients.
- mathcomp-algebra: hierarchy of algebraic structures,
integer arithmetic, Z/pZ and rational numbers,
univariate polynomials, polynomial arithmetic and fraction fields,
ring quotients, matrices and vector spaces.
- mathcomp-solvable: advanced results in group theory, including
Sylow's theorems and group series.
- mathcomp-field: field theory, finite field theory,
field extension theory, Galois theory and algebraic numbers.
- mathcomp-character: character and representation theory.
Extensions consists of more packages:
- mathcomp-zify: compatibility layer between mathcomp and lia tactics.
- mathcomp-algebra-tactics: compatibility layer between mathcomp and ring/field tactics.
- mathcomp-finmap: finite sets and finite maps.
- mathcomp-real-closed: theory of real closed fields and quantifier elimination.
- mathcomp-multinomials: multivariate polynomials.
- mathcomp-classical: compatibility layer to do classical reasonning on top of mathcomp,
theory of injective, surjective, bijective functions and cardinality.
- mathcomp-analysis: topology, normed vector spaces, real functions,
Bachman-Landau notations, infinite sequences,
measure theory, Lebesgue measure and integral,
nsatz compatibility layer.
Disclaimer: this tutorial is about Mathematical Components version 2.0+alpha1.
The extension libraries are not all available yet. The part one of this course works for both
mathcomp 1 and mathcomp 2 though.
Searching through the library.
- First: use reference documentation
- SSReflect manual
- Book (draft) on the Mathematical Components library
- documentation of the
library
e.g. ssrnat
The headers expose the public definitions and notations.
- Second: use Search using previous information
- patterns, e.g. _ <= _
- names, e.g. "SS"
- constants, e.g. leq
- restrictons, e.g. inside prime.
(See the
naming conventions)
Proof language survival kit (on examples).
Subterm selection mechnalism
- keyed matching drives the search
- specialization via argument passing
- specialization via pattern
- localization via contextual pattern (approximate or precise)
- LHS and RHS notations
Boolean reflection
- when a concept is
computable
we represent it as a
computable function (a program), not as an inductive relation
- Coq knows how to compute, even symbolically, and computation is
a very stable form of automation
- expressions in bool are a
simple
concept in type theory
- Excluded Middle (EM) just holds
- Uniqueness of Identity Proofs holds uniformly
(notes)
Decidable predicates are quite common in both computer
science and mathematics. On this class of predicates the
excluded middle principle needs not to be an axiom; in particular
its computational content can be expressed inside Coq as a program.
Writing this program in Coq may be non trivial (e.g. being a prime
number requires some effort) but once the program is written it
provides notable benefits. First, one can use the program as a
decision procedure for closed terms. Second, the proofs of such
predicate are small. E.g. a proof of
prime 17 = true is just
erefl true.
Last, the proofs of these predicates are irrelevant (i.e. unique).
This means that we can form subtypes without problems. E.g. the
in habitants of the subtype of prime numbers { x | prime x = true }
are pairs, the number (relevant) and the proof (always erefl true).
Hence when we compare these pairs we can ignore the proof part, that is,
prime numbers behave exactly as numbers.
A way to see this is that we are using Coq as a logical framework
and that we are setting up an environment where one can
reason classically (as in set theory, EM, subsets..) but also take
advantage of computations as valid reasoning steps (unlike set theory TT
manipulates effective programs)
The first predicate: leq
- order relation on nat is a program
- .+1 syntax (postfix notations .something are recurrent)
(notes)
We give a taste of boolean reflection by examples
- these examples, to stay simple, are a bit artificial
- in the library the same concepts are defeined in a slightly
different way, but following the same ideas
The first proof about leq
- ... = true to
state
something
- proof by computation
- by [] to say, provable by trivial means (no mean is inside ).
- by tac to say: tac must solve the goal (up to trivial leftovers)
(notes)
Note that 0 <= n is a symbolic expression, n is
unknown, but Coq can still compute its value
Another lemma about leq
- equality as a double implication
(notes)
Again, Coq can compute on symbolic expressions
It is nice to have a lemma, it is even better to don't need it
Connectives for booleans
- since we want statements be in bool, we need to
be able to form longer sentences with our basic
predicates (like leq) and stay in bool
- notations &&, || and ~~
Proofs by truth tables
- we can use EM to reason about boolean predicates
and connectives
- move=> name (alias of intros)
- case:
- naming convention: C suffix
Boolean reflection
- correspondance between Prop and bool
- think of reflect P b as P <-> b
(notes)
Naming convention is key to find lemmas in a large library.
It is worth mentioning here
- C for commutativity
- A for associativity
- K for cancellation
- P for characteristic properties
When doing
truth table
proofs, it is handy to
combine calls to
case with
;, as we do in the last line.
Forward reasoning (dummy examples)
- move=> /view
- have : statement.
- have := proof
- have /view ... : .. := .. and variations
- pose f x y := ...
Forward reasoning tactics (real examples)
- move=> /view
- have : statement.
- have := proof
- have /view ... : .. := .. and variations
- pose f x y := ...
Definition of all
Fixpoint all a s := match s with x :: s' => a x && all a s' | _ => true end.
Definition of count
Fixpoint count a s := match s with x :: s' => a x + count s'| _ => 0 end.
A lemma linking the two concepts
Reading proof scripts.
Look ahead for forward reasoning tactics (pose, have, suff and wlog)
to find key point in a proof.
Let's read a big proof together.
The real MathComp library,
Things to know:
- Search something inside library
- patterns, eg _ <= _
- names, eg "SS"
- constants, eg leq
- n.+1 is a notation for S n (successor of n)
- a < b is a notation for a.+1 <= b
- is_true coercion
(notes)
Unfortunately Search does not work up to
definitions
like commutative. The pattern (_ + _ = _ + _) won't work.
It's sad, it may be fixed one day, but now you know it.
Search for C
if you need a commutativity law.
Equality
- privileged role (many lemmas are stated with = or is_true)
- the eqP view:
is_true (a == b) <-> a = b
- move=> /eqP (both directions, on hyps)
- apply/eqP (both directions, on goal)
- move=> /view name to name after applying the view
- rewrite lem1 lem2 to chain rules
A little bit of gimmicks
- connectives like && have a view as well
- andP and []
- move: to move back down to the goal
Sequences
(notes)
Notations for sequentes are documented the header of the
seq.v file.
rcons is like
cons but the new element is placed in the last position.
Indeed it is not a real constructor, but rather a function that appends the singleton list.
This special case of append has its own name and collection of theorems.
Ad-hoc polymorphic lists
- T : Type |- l : list T v.s. T : eqType |- l : list T
- eqType means: a type with a decidable equality _ == _
(see second lecture).
- if T is an eqType then list T also is an eqType
- x \in l requires the type of x to be an eqType
- overloaded as (_ == _)
(notes)
Ad-hoc polymorphism is a well established concept in object
oriented programming languages and as well in functional
languages equipped with type classes like Haskell.
Whenever T is an eqType, we have a comparison
function for all terms of type T (x in the example above).
Working with the \in notation
- pushing \in with inE
- rewrite flag !
- rewrite !inE idiom
- \notin notation
Big operators
- Big operators provide a library to manipulate iterations in math-comp
- this is an encapsulation of the fold function
Notation
- iteration is provided by the \big notation
- the basic operation is on list
- special notations are introduced for usual case (\sum, \prod, \bigcap ..)
Range
- different ranges are provided
Filtering
- it is possible to filter elements from the range
Switching range
- it is possible to change representation (big_nth, big_mkord).
Big operators and equality
- one can exchange function and/or predicate
Monoid structure
- one can use associativity to reorganize the bigop
Abelian Monoid structure
- one can use communitativity to massage the bigop
Distributivity
- one can exchange sum and product
References for this lesson
- SSReflect manual
- documentation of the
library
- Book (draft) on the Mathematical Components library