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).

  • rewrite and set subterm selection mechanism.
  • The role of booleans, reflection and views.
  • have and pose forward reasoning tactics.
  • Big operators and canonical instances.

    We skip details about:

  • The tacticials => and : and all the special modifiers in all their generality.
  • SSReflect apply and elim.

    You may use any tactic you like to perform the latter operations. You can call me during the exercise session if you want details about them.


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



Polymorphic lists

  • no assumptions on T


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