lesson2

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

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

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

save script

load script