Use ALT-(up-arrow) and ALT-(down-arrow) to process this document inside your browser, line-by-line.
Use ALT-(right-arrow) to go to the cursor.
You can
save your edits
inside your browser and
load them back.
Finally, you can
download
your working copy of the file, e.g., for sending it to teachers.
what follows is a slide, it creates an index item next to the scroll bar,
just move the mouse there.
Induction and proof management
Outline:
Goal management ↑
- naming everything can become bothersome
- but, we should not let the system give random names
- we adopt some sort of
stack & heap
model
(cf Cheat sheet: Management of the goal)
The stack model of a goal
(* begining of heap *)
ci : Ti
…
dj := ej : Tj
…
Fk : Pk ci
…
(* end of heap *)
=================
forall (xl : Tl) (* top of the stack *)
…,
Pn xl -> (* nth element of the stack *)
… ->
Conclusion (* bottom of the stack = no more elements *)
We simulate the previous stack with the following commands:
(notes)
This slide corresponds to section
Bookkeeping of the online documentation of the ssreflect proof language.
Managing the stack with tacticials => and :
- tactic=> names executes tactic, and introduces with a names.
- tactic: names puts the named objects on top of the stack, then execute tactic.
- move is the tactic that does nothing (no-op, idtac) and is just a support for the two tacticial described above.
intro-pattern and discharge patterns
You can write
- tactic=> i_items where i_items is a list of
intro items
, where each i_item can be either,
- x a name, or
- _ to remove the top of the stack (if possible), or
- // close trivial subgoals, or
- /= perform simplifications, or
- //= do both the previous, or
- -> rewrite using the top of the stack, left to right, or
- <- same but right to left, or
- [i_items|…|i_items] introductions on various sub-goals
when tactic is case or elim,
- …
cf ssreflect documentation on introduction to the context
- tactic: d_items where d_items is a list of
discharge
items d_item_1 … d_item_n, and is equivalent to move: d_item_n; …; move: d_item_1, and
- tactic must be move, case, elim, apply, exact or congr,
- move: name clears the name from the context,
- move: pattern generalize a sub-term of the goal that match the pattern,
- move: (name) forces name to be a pattern, hence not clearing it.
cf ssreflect documentation on discharge
Proof by induction: generalizing the induction hypothesis ↑
Tactics elim work on the top of the stack
Indeed, elim: x y z => [t| u v w] is the same as
- move: x y z.
- elim.
- move=> t. in one sub-goal, move=> u v w. in the other.
Examples:
Generalizing the induction hypothesis.
Sometimes, we have to generalize the induction hypothesis, and in such cases, we may use the tacticial : to generalize just before performing elim. This can even be done in the same line.
This script can be abbreviated
Proof. by elim: s1 z0 => [//|x xs IH] acc /=; rewrite IH. Qed.
Using views. ↑
There are two types of connectives.
- connectives in Prop: P /\ Q, P \/ Q, ~ P, P -> Q, forall x, P x, exists x, Q x, which denote statements.
- connectives in bool: P && Q, P || Q, ~~ P, P ==> Q, [forall x, P x] and [exists x, Q x], which can be computed (thus, the boolean universal and existential can only work on finite types, which are out of the scope of this lecture).
Let's play a little with and and andb, or and orb in order to understand the difference.
Propositions:
- structures your proof as a tree,
- provides a more expressive logic (closed under forall, exists…).
Booleans:
We want the best of the two worlds, and a way to link them: views.
Stating and proving a reflection view
To link a concept in bool and one in Prop we typically
use the reflect P b predicate, which is a specialisation
of equivalence P <-> b,
where one side is in Prop and the other in bool.
To prove reflect we use the tactic prove_reflect.
Using views in forward chaining
The syntax /view can be put in intro patterns
to modify the top assumption using view
Using view in backward chaining
The apply: tactic accepts a /view flag
to modify the goal using view.
Using views with other lemmas
- By processing an assumption through a lemma.
- The leading / makes the lemma work as a function.
- If the lemma states A -> B, we can use it as a function to get a proof of B from a proof of A.
Views summary
- reflect and prove_reflect
- move=> /v H forward chaining with a view (new i_item)
- apply/v backward chaining with a view
Organizing your proofs ↑
With have: and suff:
- have i_items : statement. asks you to prove statement first.
- suff i_items : statement. asks you to prove statement last.
- have i_items := term. generalizes term and puts in on the top of the stack.
This last one is very useful as an alternative of
Check, since you can play with
the result which is on the top of the stack.
cf
ssreflect documentation on rewrite
With set and pose, naming expressions
- pose name := pattern, generalizes every hole in the pattern,
and puts a definition name in the context for it.
It does NOT change the conclusion.
- set name := pattern, finds the pattern in the conclusion,
and puts a definition name in the context.
Finally, it substitutes the pattern for name in the conclusion.
Variants of the rewrite tactic.
Use rewrite -equation to rewrite right to left.
Use rewrite [pattern]equation to select what you want to rewrite.
Use -[pattern]/term to replace a term by a convertible one.
e.g.
- -[2]/(1 + 1) replaces 2 by 1 + 1,
- -[2 ^ 2]/4 replaces 2 ^ 2 by 4,
- -[m]/(0 * d + m) replaces m by 0 * d + m.
A few steps into the arithmetic library. ↑
The main functions symbols (besides addn, muln, subn, ...)
Large and Strict comparison.
Euclidean division edivn and its quotient divn and remainder modn
Divisibility
Equality modulo
The notation m = n %[mod d] is an abbreviation for m %% d = n %% d.
GCD, relative primality and primality