To play this document inside your browser use ALTN and ALTP.
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
Roadmap of the first 2 lessons
 the small scale reflection approach (ssr)
 the ssreflect tactic language (ssr)
 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
The SSR approach
 when a concept is
computable
, lets represent it as a
computable function, 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
A taste of boolean reflection by examples
 these examples are artificial
 in the library things are done in a slightly different way
The first predicate
 order ralation on nat is a program
 ifisthen syntax (simply a 2way matchwithend)
 .+1 syntax (postfix notations .something are recurrent)
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
Bookkeeping 101
 defective case (stack model, the top implicit tactic argument)
 tactic=>
 tactic: (caveat: tactic != apply or exact)

rename
, reorder
Recap (ssr approach and basic tactics)
 boolean predicates and connectives
 think
up to
computation
 case, elim, move, :, =>, basic rewrite
 ifisthenelse, .+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
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
 SSReflect manual
 documentation of the
library
 Book (draft) on the Mathematical Components library