lesson2
Recap:
- => intro pattern (names, views, //, /=, {}, )
- rewrite lem -lem // /= /def
- naming convention: addnC, eqP, orbN, orNb, ...
- notations: .+1, if-is-then-else
- reflect P b
Lessons learnt yesterday
- Search _ (_ + _) in ssrnat.
- Search _ addn
C
in ssrnat.
- Use the HTML doc!
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 s := if s is x :: s' then a x && all s' else true.
Definition of count
Fixpoint count 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
Last, (_ =P _)
- Just eqP but with the right implicit arguments
Rewrite on steroids
- keyed matching
- instantiation
- localization
References for this lesson:
Demo:
- you should be now able to read this proof