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 school

Give you access to the Mathematical Components library

  • formalization techniques
  • proof language
  • familiarize with some theories

Why another library? Why another language?

  • 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

Captatio benevolentiae: this is not standard Coq

  • things are done differently, very differently, than usual
  • it is not easy to appreciate the benefits on small examples, but we will try hard ;-)
  • not enough time to explain eveything, we may focus on intuition rather than technical details (aka handwaving)

(notes)
The mathematical components library was used to formalize the Odd Order Theorem (Feit Thompson) , literally 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

  • formalization technique: boolean reflection (aka small scale reflection)
  • proof language: basic SSReflect (part 1)
  • libraries: conventions, notations, ad-hoc polymorphism

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)
Decideable predicates are quite common in both computer science and mathematics. On this class or 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
  • if-is-then syntax (simply a 2-way match-with-end)
  • .+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
  • naming convention

(notes)
Again, Coq can compute on symbolic expressions

It is nice to have a lemma, it is even better to don't need it

  • elim with naming and automatic clear of n
  • indentation for subgoals
  • no need to mention lemmas proved by computation
  • apply, rewrite

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
  • case:
  • move=> /=
  • naming convention: C suffix

(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
When doing truth table proofs, it is handy to combine calls to case with ;, as we do in the last line.

Recap: formalization approach and basic tactics

  • boolean predicates and connectives
  • think up to computation
  • case, elim, move, rewrite
  • if-is-then-else, .+1, &&, ||, ~~
  • naming convetions C, foo0n, foon0, fooSS

The real MathComp library

Things to know:

  • Search something inside library
    • patterns, eg _ <= _
    • names, eg "SS"
    • constants, eg leq
  • a < b is a notation for a.+1 <= b
  • _ == _ stands for computable equality (overloaded)
  • _ != _ is ~~ (_ == _)
  • is_true coercion
  • rewrite /concept to unfold

(notes)
Unfortunately Search does not work up to definitions like commutative. The pattern (_ + _ = _ + _) won't work. It's sad, it may be fidex 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
  • notation .*2
  • 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

Forward steps:

  • have
  • move: (f x)
  • move=> {}H

(notes)
Unlike with _ /\ _ we rarely use split to prove a conjunction. It is typically simpler to rewrite _ && _ to true.

Sequences

  • many notations

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

Polymorphic lists

  • no assumptions on T
  • we can use => ... // to kill a goal
  • we can use => ... /= to simplify a goal

Ad-hoc polymorphic lists

  • T : Type |- l : list T v.s. T : eqType |- l : list T
  • eqType means: a type with a decidable equality _ == _
  • 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

References for this lesson