Recap
Proof language
- : name, to prepare the goal for a tactic
- => name /view // /= {name} [], to post-process the goal
- rewrite lem -lem // /= /def
- apply: lem
Library
- naming convention: addnC, eqP, orbN, orNb, ...
- notations: .+1, if-is-then-else
- Search _ (_ + _) in ssrnat
- Search _ addn "C" in ssrnat
- Use the HTML doc!
Approach
- boolean predicates
- reflect P b to link bool with Prop
Today
- The seq library
- forward reasoning with have
- spec lemmas
- rewrite patterns
Sequences
- an alias for lists (used to be differnt)
- many notations
Polymorphic lists
- This statement makes no assumptions on T
- recap: // /= ->
Had-hoc polymorphism
- T : Type |- l : list T
- T : eqType |- l : list T
- eqType means: a type with a decidable equality (_ == _)
The \in notation
- overloaded as (_ == _)
- pushing \in with inE
- computable.
- rewrite !inE
Forward reasoning
- have
- have :=
- have + views
- do I need eqType here?
Definition of all
Fixpoint all a s := if s is x :: s' then a x && all a s' else true.
Definition of count
Fixpoint count a s := if s is x :: s' then a x + count s' else 0.
A lemma linking the two concepts
Spec lemmas
- Inductive predicates to drive the proof
Let's try out leqP on an ugly goal
- matching of indexes
- generalization of unresolved implicits
- instantiation by matching
Another commodity: ifP
- a spec lemma for if-then-else
- handy with case, since matching spares you to write
the expressions involved
Rewrite on steroids
- keyed matching
- instantiation
- localization
References for this lesson:
Demo:
- you should be now able to read this proof