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 inside your browser and . Finally, you can 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.

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

### 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.

(notes)

### 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).

#### Propositions:

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

#### Booleans:

• provide computation.

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

(notes)
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.

(notes)
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.

(notes)
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.

(notes)
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

### 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 -[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, ...)

### Equality modulo

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