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.

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