lesson1
To play this document inside your browser use ALT-N and ALT-P.
Objective of this course
Give you access to the Mathematical Components library
- formalization principles
- proof language
- familiarize with some theories
MathComp website
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
- the ssreflect tactic language
- 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
- if-is-then syntax (simply a 2-way match-with-end)
- .+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
- if-is-then-else, .+1
- naming convetion
Now we use 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_true coercion
- != is ~~ (_ == _)
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 aconnectives 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: