Lesson 3: Mathematics Verification

From mathcomp Require Import all_ssreflect all_algebra.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Definition sorry {T} : T. Admitted.

Seminar tomorrow:

Flèche: Incremental Validation for Hybrid Proof Documents
  • user interfaces, notations, interactive books
  • formal model interpreter + algebraic effects: easy to maintain
  • implementation: jsCoq 2 + coq-lsp

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
  • 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 + accesibility
  • 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:

Today 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 can start by having a look to a "real" proof on numbers:
Lemma prime_above m : {p | m < p & prime p}.
have /pdivP[p pr_p p_dv_m1]: 1 < m`! + 1 by rewrite addn1 ltnS fact_gt0.
∃ p ⇒ //; rewrite ltnNge; apply: contraL p_dv_m1 ⇒ p_le_m.
by rewrite dvdn_addr ?dvdn_fact ?prime_gt0 // gtnNdvd ?prime_gt1.
Qed.

Extensionality

Let's do a quick recap of what we discussed yesterday:
  • characteristic P predicates and reflection, classical interfaces
  • object-oriented programming with Canonical structures (eqType, finType)
  • inference and view techniques
  • finite types and their theory.
Finite types do allow for some quite powerful patterns, in particular, we have the type of finitely-supported functions:
Section FFun.
Variable (n : nat).
Variable (value : finType).
Definition my_map := {ffun 'I_n → value}.
We can use this function normally, in particular let's define update and try prove a lemma about it
Definition update : sorry := sorry.
Similarly to other "classical" principles, Coq's logic doesn't prove the principle of functional extensionality for all functions:
Axiom funext : ∀ T U (f g : T → U), (∀ x, f x = g x) → f = g.
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
Section ExtIntro.
Variable (T : finType) (U : Type).

Lemma ffun_ext_show (f g : {ffun T → U}) : f = g.
Proof. apply/ffunP. move⇒ x. Abort.
How does this work? It does work because we implement a {ffun } using a tuple over the index of the elements!

Finite Sets

We can use {ffun ...} to implement many other things, in particular finite sets.
Implicit Types (A B : {set T}).

Lemma fset_ext_show (A B : {set T}) : A = B.
Proof. apply/setP. move⇒ x. Abort.
We can prove some things about sets now!
Lemma setUC A B : A :|: B = B :|: A.
Proof. Admitted.

Lemma setIC A B : A :&: B = B :&: A.
Proof. Admitted.

Also note that sets of sets and functions spaces are themselves finite types!
End ExtIntro.
End FFun.

Matrices

Definition matrix n m R := {ffun 'I_n → 'I_m → R}.

Lemma matrixP n m R (A B : matrix n m R) : (A = B) ↔ (A =2 B).
Proof. Admitted.

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.

Algebra

Equipped with this, we proceed to present some of the core algebraic structures of math comp: Abelian groups, rings, and commutative rings.
Open Scope ring_scope.
Import GRing.Theory.

Section AEx.

Variable (A : zmodType).
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...

Lemma demo_A (x y : A) : x + y + 0 = y + 0 + x.
Proof. Admitted.

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

Lemma demo_R (x y : R) : x + y + 0 = y + 0 + x.
Proof. Admitted.

Variable (C : comRingType).
Lemma demo_C (x y : C) : x + y + 0 = y + 0 + x.
Proof. Admitted.

Variable (L : lmodType R).
Lemma demo_l (a : R) (x y : L) : a *: (x + y) = a *: x + a *:y.
Proof. Admitted.

End AEx.

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.

Lemma matrix_1 :
  let A : 'M[nat]_(2,2) := \matrix_(i < 2, j < 2) (i + j)%nat in
  let B : 'M[nat]_(2,2) := \matrix_(i < 2, j < 2) (i + j)%nat in
  A = B.
Proof. Admitted.

Lemma matrix_struct_1 (T : zmodType) n m (A B : 'M[T]_(n,m)) : A + B = B + A.
Proof. Admitted.

Lemma matrix_struct_1' (T : zmodType) n m (A B : 'M[T]_(n,m)) : A + B = B + A.
Proof. Admitted.

Lemma matrix_struct_2 (T : ringType) n (A B C : 'M[T]_(n.+1,n.+1)) : A × B × C = A × (B × C).
Proof. Admitted.

Lemma tr_tr (T : zmodType) m n (A : 'M[T]_(n,m)) : A = A^T^T.
Proof. Admitted.

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
Lemma poly_1 (A : ringType) (x y z : A) :
  (Poly [:: x; y; z])`_1 = y.
Proof. by rewrite coef_Poly. Admitted.

Lemma poly_2 (A : ringType) (p q : {poly A}) : p + q = q + p.
Proof. Admitted.

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...
Lemma big_swap_(A : zmodType) (x y : A → A) i l : \sum_(i <- l) x i + y i = \sum_(i <- l) y i + x i.
Proof. Admitted.