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

save script
Goals
Messages