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.

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:

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.

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.


  • structures your proof as a tree,
  • provides a more expressive logic (closed under forall, exists…).


  • provide computation.

We want the best of the two worlds, and a way to link them: views.

This slide corresponds to section 3.x of the Mathematical Components book

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.

This slide corresponds to sections 4.1.1 and 4.1.2 of the Mathematical Components book

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.

This slide corresponds to sections 4.1.3 and 4.1.4 of the Mathematical Components book

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.

This slide corresponds to section 4.2 of the Mathematical Components book

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.


  • -[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


Equality modulo

The notation m = n %[mod d] is an abbreviation for m %% d = n %% d.

GCD, relative primality and primality