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

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

(_ == _) 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 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:

save script
Goals
Messages