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.

##
Reflection in the large

###
In this lecture

- Play with the syntax of our goals
- Develop some automation thanks to computation

###
Conversion rule

The conversion rule (for the machine):

$$
\frac{\Gamma \vdash t : (\forall x:A, B) \qquad
\Gamma \vdash u : A' \qquad
\Gamma \vdash A \equiv A'}{\Gamma \vdash t~u : B[x \gets u]}
$$

The conversion rule (from a human):

types are *quotiented* by *computation*

Remark: `erefl true` works as a proof for `e = true`
no matter how many reduction steps it takes to normalize
`e` to `true`.

##
Recap: computation and variables

- Why is the first goal trivial by computation?
- Why the second is not?

We used the lemma `muln0` before. Can't we explain Coq
to use it for us?

Yes!

###
Idea

- we could write a program that simplifies expressions
- we could prove it correct
- we could have Coq run it for us

The `expr` data type is the *syntax* of expressions.
It is a data type like `nat` or `bool` are we know how to
write programs on this data.

Let's write a program that deals with `Zero`, i.e. that implements
the simplication rule $$n * 0 = 0$$ and $$0 * n = 0$$.

We have to link these expressions and our goals.
Each expression in `expr` represents an expression in our goal.
Let's make this map explicit.

What would it mean for `simplify` to be correct?

Now let's take advantage of our program

###
Let's add more simplification rules!

The rule we want is $$n - n = 0$$ when n is a number.

We have to link these expressions and out goals.
Each expression in `expr` represents an expression in out goal.
Let's make this map explicit.

What would it mean for `simplify` to be correct?

Now let's try to take advantage of it

What went wrong is that we did not completely move variables
away from the syntax we manipulate. But it is easy to fix.

###
Let's give a syntax to variables.

Interpretation now takes a map `c` from the ids of variables
to arbitrary terms in out target type.

##
To sum up

- computation is well defined on any term, including terms with variables
- computation is
*complete* on closed terms (you reach a normal form
that is made of constructors)
- computation happens
*inside* the logic (terms are quotiented wrt computation)
- computation can be very fast (decades of research in CS)
- applications of this technique
+ simplification in a ring
+ 4 color theorem
+ Pocklington primality test