To play this document inside your browser use ALT-N and ALT-P.

## Objective of this course

• 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

## 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
• EM holds
• UIP holds

## 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)

• 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

### 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

## 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

• and eqP is too

## Views are just lemmas

• 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)