lesson4

To play this document inside your browser use ALT-N and ALT-P. 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.

From elpi Require Import elpi.
From HB Require Import structures.
From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Recap of lesson 1

Proof language

move=> name /view // /= [..|..] to name/change the goal
: name, : (lem arg)
rewrite lem -lem
apply: lem
apply/view

Library

naming convention: addnC, eqP, orbN, orNb, ...
notations: .+1, if-is-then-else
Search (_ + _) inside ssrnat
Search addn "C" inside ssrnat
Use the HTML doc!

Approach

boolean predicates
reflect P b to link bool with Prop

Today

the SSReflect proof language (part 2)
- stack model and views
- rewrite idioms and patterns
- forward reasoning with have
spec lemmas
- reflect
- fooP
- idioms

Bookkeeping 101

the goal is a stack
defective case/elim (the top implicit tactic argument)
tactical => for post processing
tactical : for pre processing
rename, reorder

Lemma negb_and :
  forall b c, ~~ (b && c) = ~~ b || ~~ c.
Proof.
(*
move=> b. move=> c. move: b. move: c. (* up and down *)
move=> c b. move: b c.  (* reverse order, it's a stack *)
move=> b; case: b. move=> c; case: c. (* no need to name _top_, it's the default subject *)
*)
by case; case. Qed.

(notes)

We say that the goal (under the horizontal bar) is a stack, since items can only be accessed accorrding to a stack discipline. If the goal is forall x y, x = 1 + 2 * y -> odd x one has to deal with x and y before accessing x = 1 + 2 * y.

Induction

elim with generalization
in x * alternative
rewrite (lem args) to specialize a lemma

Lemma induction_fold (l : seq nat) x :
  foldl addn x l = x + foldl addn 0 l.
Proof.
(*
elim: l => [|y ys IH] /=. (* first attempt *)
  by rewrite addn0.
(* we are stuck *)
#*)
elim: l x => [|y ys IH] x /=. (* better attempt, generalize and re-introduce x *)
  by rewrite addn0.
by rewrite IH (IH y) addnA. (* IH is now quantified *)
Qed.

(notes)

Recall that elim (or case) actually operate on the top of the stack, which is the last item generalized by :.

Views are just lemmas (plus some automatic adaptors)

lemmas like A -> B can be used as views too
boolean connectives have associated views (P suffix)


Lemma test_leqW i j k :
  (i <= k) && (k.+1 <= j) -> i <= j.+1.
Proof.
(* move=> /andP H; case: H. move=> /leqW leq_ik1. *)
move=> /andP[/leqW leq_ik1 /leqW leq_k1j1]. (* process fully, then name *)
by apply: leq_trans leq_ik1 leq_k1j1.
Qed.

(notes)

There is nothin special with the /andP[H1 H2] we did in lesson 1, it is just the composition of /view followed by a case split [] (in this case only one branch)

`rewrite`, one command to rule them all

1/3 of the lines of Math Comp proofs are rewrite
side conditions handling via // and ?
rewrite a boolean predicate (is_true hides an eqaution)


Lemma test_leq_cond p : prime p -> p.-1.+1 + p = p.*2.
Proof.
(*
move=> pr_p.
Search predn inside ssrnat.
rewrite prednK. (* main step *)
  by rewrite addnn. (* side condition *)
Search prime leq 0.
by apply: prime_gt0. (* conclusion *)
#*)
(* idiomatic use of conditional rewrite rules *)
by move=> pr_p; rewrite prednK ?addnn // prime_gt0.
Qed.

`rewrite` and subterm selection

keyed matching drives the search
specialization via argument passing
specialization via pattern
localization via contextual pattern (approximate or precise)
LHS and RHS notations

Lemma subterm_selection n m :
  n + (m * 2).+1 = n * (m + m.+1).
Proof.
rewrite addnC.
rewrite (addnC m).
rewrite [_ + m]addnC.
rewrite [in n * _]addnC.
rewrite [X in _ = _ * X]addnC.
rewrite [in RHS]addnC.
Abort.

Lemma occurrence_selection n m :
  n + m = n + m.
Proof.
rewrite addnC. (* all occurrecens of the rule are replaced *)
rewrite [in RHS]addnC. (* limit to RHS of the goal *)
Abort.

Lemma no_pattern_from_the_rewrite_rule n : n + 0 = n.
Proof.
rewrite -[n in RHS]addn0. (* precise patterns for ambiguous rules *)
Abort.

(notes)

The details can be found in the reference manual or in the paper

The reflect predicate

reflect P b is the preferred way to state that the predicate P (in Prop) is logically equivalent to b = true

Module reflect_for_eqP.

Print reflect.

(* we use this boolean predicate in the examples below *)
Fixpoint eqn m n :=
  match m, n with
  | 0, 0 => true
  | j.+1,k.+1 => eqn j k
  | _, _ => false
  end.
Arguments eqn !m !n.

Proving the reflection lemma for `eqn`

the convenience lemma iffP
the congr tactic
trivial branches => //
rewrite on the fly ->
first by
congr

Lemma myeqP m n : reflect (m = n) (eqn m n).
Proof.
(*
apply: (iffP idP) => [|->]; last by elim: n.
elim: m n; first by case.
move=> n IHn m eq_n1m.
case: m eq_n1m => // m eq_n1m1. (* case with generalization *)
congr (_.+1). (* cleanup of the goal *)
by apply: IHn.
#*)
apply: (iffP idP) => [|->]; last by elim: n.
by elim: m n => [|m IHm] // [|n] // /IHm->.
Qed.

Lemma test_myeqP n m : (eqn n m) -> m = n.
Proof. by move=> /myeqP ->. Qed.

End reflect_for_eqP.

Spec lemmas

Inductive predicates to drive the proof:
- you chose how many branches
- you chose which equations are automatically applied
- you chose which extra assumption a branch has
of syntax for inductives


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 uses the same discipline of rewrite

Bonus (time permitting):

generalization of unresolved implicits after /leq_trans
specialization of the top stack item via /(_ arg)

Lemma test_leqP m n1 n2 :
  (m <= (if n1 < n2 then n1 else n2)) =
  (m <= n1) && (m <= n2) && ((n1 < n2) || (n2 <= n1)).
Proof.
(* the indexes of <tt>leqP</tt> give rise to patterns, which are matched
   right to left. So the first one is <tt>_ < _</tt> which finds <tt>n1 < n2</tt>
   and replaces it with <tt>false</tt> in the first branch and <tt>true</tt> in the
   second. Then it is the turn of <tt>n2 <= n1</tt>.
   
   use: Set Debug "ssreflect". for a slow motion *)
case: leqP => [leqn21 | /ltnW ltn12 ]; rewrite /= andbT.
  by rewrite andb_idl // => /leq_trans /(_ leqn21).
by rewrite andb_idr // => /leq_trans->.
Qed.

(notes)

While I presonally find /leq_trans too clever and likely unnecessary, it is used in the library, hence this slide

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

Lemma test_ifP n m : if n <= m then 0 <= m - n else m - n == 0.
Proof.
case: ifP => //.
(* MC idiom: don't introduce hyps if not necessary *)
by move=> /negbT; rewrite subn_eq0 leqNgt negbK=> /ltnW.
Qed.

Forward reasoning

have : statement.
have := proof
have /view ... : .. := .. and variations

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

Lemma all_count (T : Type) (a : pred T) s :
  all a s = (count a s == size s).
Proof.
(* common start *)
elim: s => //= x s.

(* first try at using EM *)
have EM_a : a x || ~~ a x.
  by apply: orbN.
move: EM_a => /orP EM_a. case: EM_a => [-> | /negbTE-> ] //= _.

(*
(* second try using views and have *)
have /orP[ ax | /negbTE n_ax ] : a x || ~~ a x by case: (a x).
  by rewrite ax.
rewrite n_ax /= => ?.
#*)

(*
(* this is the best way of doing it *)
have [ax//|n_ax ?] := boolP (a x).
#*)

(* common conclusion *)
by rewrite add0n eqn_leq ltnNge count_size /= andbC.
Qed.

References for this lesson:

SSReflect manual
documentation of the library
- in particular seq

Demo (time permitting, or as an exercise)

you should be now able to read this proof


Lemma dvdn_fact m n : 0 < m <= n -> m %| n`!.
Proof.
case: m => //= m; elim: n => //= n IHn; rewrite ltnS leq_eqVlt.
by move=> /orP[ /eqP-> | /IHn]; [apply: dvdn_mulr | apply: dvdn_mull].
Qed.

Lemma prime_above m : {p | m < p & prime p}.
Proof.
(* Check pdivP. *)
have /pdivP[p pr_p p_dv_m1]: 1 < m`! + 1 by rewrite addn1 ltnS fact_gt0.
exists p => //; rewrite ltnNge; apply: contraL p_dv_m1 => p_le_m.
(* Check dvdn_addr. *)
by rewrite dvdn_addr ?dvdn_fact ?prime_gt0 // gtnNdvd ?prime_gt1.
Qed.

(notes)

This proof is also explained in the Math Comp Book

Recap of lesson 1

Today

Bookkeeping 101

Induction

Views are just lemmas (plus some automatic adaptors)

rewrite, one command to rule them all

rewrite and subterm selection

The reflect predicate

Proving the reflection lemma for eqn

Spec lemmas

Let's try out leqP on an ugly goal

Another commodity: ifP

Forward reasoning

References for this lesson:

Demo (time permitting, or as an exercise)

`rewrite`, one command to rule them all

`rewrite` and subterm selection

Proving the reflection lemma for `eqn`

Let's try out `leqP` on an ugly goal

Another commodity: `ifP`