Lesson 3: Mathematics Verification

Advanced Topics

Some possible topics for Friday are:

• deep specification
• user interfaces, notations, interactive books
• collaborative development / ecosystem / impact
• proof automation / Machine Learning
• higher mathematical structures / HoTT (Homotophy Type Theory)
• proof by refinement
• advanced program logics
• models, axioms, proof relevance

The Mathematical Components Library

• https://math-comp.github.io/
• Developed first for the 4 color theorem, then for the Feit-Thompsom proof.
• High-quality, large set of advanced techniques and theorems
• Large development effort, co-development with Coq, refactoring very costly
• Powerful but lacking documentation thus it feels hard to use
• Indeed, it is not a straightforward step for a mathematician.

Lean's mathlib

• https://leanprover-community.github.io/mathlib_docs/
• Lean is a recent re-implementation of Coq's type theory by Leo de Moura and collaborators
• Type theories almost compatible, front-ends follow the same spirit, but significant differences.
• Built on many ideas from math-comp
• Made very popular for mathematicians thanks to great communication and community.
• Math marketing effort mainly led by Kevin Buzzard
• New version (Lean 4) vs mathlib (Lean 3)
• It is also not a straightforward step for a mathematician.
• https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-developments/

Challenges of doing mathematics in type theory

• general usability: search, tactics, documentation, notations
• organization of mathematical structures: base type theory is not well-suited for encoding complex mathematical

Plan + an example:

In today's brief introduction we will cover some examples and structures from the mathematical components library, in particular, we will present the basic algebraic structures (commutative groups, rings), matrices, and polynomials. The library includes many more structures and results, including a new library on analysis. We start by explaining an example on numbers:

Base useful libraries

In this lesson, we will use a large number of "basic" data structures and theories which are by no means trivial, and play an essential role in the developments. In particular:

• eqType, choiceType: types with choice and decidable equality
• nat: mathcomp's Peano numbers + their large theory, including modular arithmetic, prime numbers, etc...
• seq A: mathcomp's lists (or sequences) + their large theory
• finType: finite types
• orderType: types with different orders
• subType P A: subTypes of A convertibles to A. For example the set of all even natural numbers: { x : nat | even x }.

Using subtypes we can define:

• ordinals 'I_n, in particular 'I_n := { x : nat | x < n }
• tuples n-tuple A, lists of size n, or tuples
• {ffun T → U} finitely supported functions (a tuple of cardinality #|T| .

Of particular interest are the finitely supported functions. Similarly to other "classical" principles, Coq's logic doesn't prove the principle of functional extensionality for all functions:

However, a lot of reasoning in mathematics depends on this being true. mathcomp is pretty careful as to use datatypes that validate this principle, for example finitely supported functions are implemented in a way such that we can prove extensionality

Finite sets do validate this principle too

Mathematical Structures

While type theory does provide us a convenient way to write low-level proofs and check them, when doing mathematics formally we need to organize and validate a large ontology of mathematical object with complex relations among them. For example, a ring may be a group, and it may be so in more than one. Similarly subgroups are groups, and some particular instances of objects, like matrices, may form structures only in some cases. Good support for inference and synthesis of these relations is essential, as you will find that stating a theorem often involves the same object but viewed from several different points of view. Thus, in order to keep definitions and statement manageable, the meta information about objects must be used by Coq automatically. A lot of research has been put into building good support for such structures. Math-comp provides great support by using a Coq inference feature called "Canonical Structures", and automatic (safe) type castings. Both features live at the level of elaboration and not in the kernel.

Canonical Structures

As we have seen, it is customary to pack the definition of an structure and its properties into a record. For example, types with decidable equality are packed as `eqType`, which thanks to a coercion can be used a `Type`. However, it is very common that we will have the following situation: (∀ {T : eqType}, (x y : T), ...) 3 4 That is to say, x y have type ?T.(type) (due to the coercion), as ?T is implicit and just a meta-variable at this point. Thus, we got a unification problem ?T.(type) = nat, which is hard to solve as it would mean we need to synthesize an implementation de eqType for nat on on the fly. Instead, we can tell Coq to consider a hint when this kind of unification problem appears. What we can say to Coq is that indeed, every unification problem that that has the shape of ?T : eqType |- ?T.(type) = nat , should be solved by using the existing nat_eqP instance. "Canonical" structures provides us the way to indicate this.

Coercions

Coercions allow the type inference to relate to different types by inserting (or synthesising) a type casting from a type to another. A good example is just the above equation. We have T : eqType and we need in (x : T) that T is a Type however it is an eqType. But Coq knows how to repair this, and will insert the .(type) projection so we now have (x : T.(type), with this correctly typing.

Status in Coq

As of today, defining our own structures requires too much boiler-plate. Lean has better support for this (with trade-offs) , whereas Coq has an experimental plugin called hierarchy builder that greatly helps.

Algebra

Equipped with this, we proceed to present some of the core algebraic structures of math comp: Abelian groups, rings, and commutative rings.

zmodType is the type of Abelian groups over choiceTypes:
Record mixin_of (V : Type) : Type := Mixin {
  zero : V;
  opp : V → V;
  add : V → V → V;
  _ : associative add;
  _ : commutative add;
  _ : left_id zero add;
  _ : left_inverse zero opp add
}.

- The operators exported are [0] [x + y] [- x] , a few derived ones are defined too, like [x *+ n].
- Suffix for theory is [r], so [addr0], [addrA], etc...

ringType: (non-commutative) rings over a commutative abelian group

Big Operators

Another very important tool is the one of "big operators", which are usually operators such as sum or max but applied over a collection of objects. They will appear in many places as for example matrix multiplication is defined that way, etc...

Matrices

Matrices in math-comp are implemented by a finitely supported finitely-supported function from their indexes to the value. Matrices will inherit some of the algebraic properties iff Matrices are extensional so that allows to do many proofs easily! The down side is due to locking these matrices don't computer well.

Polynomials

Last, we will explore a bit {poly R} the type of polynomials with coefficients in R

• 'X^i is the variable
• p.i is evaluation (Horner scheme)
• polynomials have the corresponding ring structure