lesson2

To play this document inside your browser use ALT-N and ALT-P. If you get stack overflow errors, try to use Google Chrome or Chromium with the command line option --js-flags="--harmony-tailcalls".

You can save your edits inside your browser and load them back (edits are also saved when you close the window). Finally you can download the file for offline editing.

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

(notes)

Notations for sequentes are documented the header of the seq.v file. rcons is like cons but the new element is placed in the last position. Indeed it is not a real constructor, but rather a function that appends the singleton list. This special case of append has its own name and collection of theorems.

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

(notes)

Had-hoc polymorphism is a well established concept in object oriented programming languages and as well in functional languages equipped with type classes like Haskell. Whenever T is an eqType, we have a comparison function for all terms of type T (x in the example above).

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

Module myreflect1.

Inductive reflect (P : Prop) (b : bool) : Prop :=
  | ReflectT (p : P) (e : b = true)
  | ReflectF (np : ~ P) (e : b = false).

Fixpoint eqn m n :=
  match m, n with
  | 0, 0 => true
  | j.+1,k.+1 => eqn j k
  | _, _ => false
  end.
Arguments eqn !m !n.

Axiom eqP : forall m n, reflect (m = n) (eqn m n).

Lemma test_reflect1 m n : ~~ (eqn m n) || (n <= m <= n).
Proof.
case: (eqn m n) => /=.
(* case: (eqP m n) => [Enm -> | nE_mn ->] /=. *)
Admitted.

End myreflect1.

(*
Module myreflect2.

Inductive reflect (P : Prop) : bool-> Prop :=
  | ReflectT (p : P) : reflect P true
  | ReflectF (np : ~ P) : reflect P false.

Fixpoint eqn m n :=
  match m, n with
  | 0, 0 => true
  | j.+1,k.+1 => eqn j k
  | _, _ => false
  end.
Arguments eqn !m !n.

Axiom eqP : forall m n, reflect (m = n) (eqn m n).
Arguments eqP {m n}.

Lemma test_reflect1 m n : ~~ (eqn m n) || (n <= m <= n).
Proof.
case: (@eqP m n) => [Enm | nE_mn ] /=.
by case: eqP => [->|] //=; rewrite leqnn.
Qed.

End myreflect2.

Check (_ =P _).
Check eqP.

Inductive leq_xor_gtn m n : bool -> bool -> Prop :=
  | LeqNotGtn of m <= n : leq_xor_gtn m n true false
  | GtnNotLeq of n < m  : leq_xor_gtn m n false true.

Axiom leqP : forall m n : nat, leq_xor_gtn m n (m <= n) (n < m).

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
remark how the goal is used as a work space

Rewrite on steroids

keyed matching
instantiation
localization

References for this lesson:

SSReflect manual
documentation of the library
- in particular seq

Demo:

you should be now able to read this proof