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