To play this document inside your browser use ALT-N and ALT-P. If you get stack overflow errors, try to use Google Chrome or Chromium with the command line option --js-flags="--harmony-tailcalls".

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 course

Give you access to the Mathematical Components library

  • formalization principles
  • 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

(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 2 lessons

  • boolean reflection (small scale reflection)
  • the ssreflect proof language (SSReflect)
  • basic libraries (ssrbool, ssrnat, seq)

Disclaimer: 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, I'll focus on intuition rather than technical details

Boolean reflection

  • when a concept is computable, lets 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
  • functions (to 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.

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)

Another lemma about leq

  • equality as a double implication
  • naming convention

Lets (not) use these lemmas

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

Connectives can be booleans too

Proofs by truth tables

  • we can use EM to reason about boolean predicates and connectives
  • case:
  • bookkeeping /=
  • 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

Bookkeeping 101

  • defective case (stack model, the top implicit tactic argument)
  • tactic=>
  • tactic: (caveat: tactic != apply or exact)
  • rename, reorder

(notes)
We say that the goal (under the horizontal bar) is a stack, since items can only be accessed accorrding to a stack discipline. If the goal is forall x y, x = 1 + 2 * y -> odd x one has to deal with x and y before accessing x = 1 + 2 * y.

Recap: formalization approach and basic tactics

  • boolean predicates and connectives
  • think up to computation
  • case, elim, move, :, =>, basic rewrite
  • if-is-then-else, .+1
  • naming convetion

The real MathComp library

Things to know:

  • Search head_symbol (pat _ term) "string" name
  • (a < b) is a notation for (a.+1 <= b)
  • == stands for computable equality (overloaded)
  • != is ~~ (_ == _)
  • is_true coercion

Equality

  • privileged role (many lemmas are stated with = or is_true)
  • the eqP view: is_true (a == b) <-> a = b
  • => /eqP (both directions)
  • => -> (on the fly rewrite, subst)
  • notation .*2

Infix == is overloaded

  • and eqP is too

Views are just lemmas

(plus some automatic adaptors)

  • lemmas like A -> B can be used as views too
  • boolean connectives have associated views
  • => [ ... ]

The reflect predicate

  • reflect P b is the preferred way to state that the predicate P (in Prop) is logically equivalent to b=true

Proving the reflection lemma for eqn

  • the convenience lemma iffP
  • the congr tactic
  • trivial branches //
  • loaded induction elim: n m

rewrite, one command to rule them all

  • rewrite
  • side condition and // ?
  • rewrite a boolean predicate (is_true hides an eqaution)

References for this lesson