To play this document inside your browser use ALT-N and ALT-P.
You can save your edits inside your browser and load them back (edits are also saved when you close the window). Finally you can download the file for offline editing.
We link typed programs to statements with a proof.
Let's play a game in which we use inductive types as our satements.
We learn that 0 is a term of type nat, but Coq also accepts it as a proof of nat.
Now let's look at the function space.
The function space -> can represent implication. An inhabitant of A -> B is a function turning a proof of A into a proof of B (a program taking in input a term of type A and returning a term of type B).
The function space of type theory is *dependent*.
We managed to build (introduce) an arrow and a forall using fun. Let's see how we can use (eliminate) an arrow or a forall.
Following the Curry Howard correspondence *application* lets one call a function f : A -> B on a : A to obtain a term of type B. If the type of f is a dependent arrow (forall) f : forall x : A, B x then the argument a appears in the type of term we obtain, that is f a has type B a.
In other words application instantiates universally quantified lemmas and implements modus ponens.
Lemmas can be seen as views to transform assumptions.
So far we used nat (and P) as a predicate and -> for implication.
Can we use inductive types to model other predicates or connectives?
This slide corresponds to section 4.x of the Mathematical Components book
Let's start with $$ \top $$
Note: here the label Prop could be a synonym of Type.
Now let's look at $$ \bot $$
Connectives: $$ \land $$ and $$\lor $$
Quantifier $$ \exists $$
This slide corresponds to section 4.x of the Mathematical Components book
We want to prove theorems by induction, right? Hence there must be a term that corresponds to the induction principle. This term is a recursive function.
Note: Fixpoint is just sugar for Definition followed by fix.
This slide corresponds to section 4.x of the Mathematical Components book
We give here the intuition why some terms that are in principle well typed are rejected by Coq and why Coq is consistent.
What does it mean that t : T and T is not False?
Constructors are not the only terms that can inhabit a type. Hence we cannot simply look at terms, but we could look at their normal form.
Subject reduction: t : T and t ~> t1 then t1 : T. We claim there is not such t1 (normal form) that inhabits False.
We have to reject t that don't have a normal form.
Exaustiveness of pattern matching:
According to Curry Howard this means that in a case split we did not forget to consider a branch!
Termination of recursion:
According to Curry Howard this means that we did not do any circular argument.
Non termination is subtle since a recursive call could be hidden in a box.
This condition of inductive types is called positivity: The type of Hide would be (hidden -> False) -> hidden, where the first occurrence of hidden is on the left (negative) of the arrow.
This slide corresponds to section 3.2.3 of the Mathematical Components book
... and their elimination.
The intuition, operationally.
Inductive types can express tricky invariants:
Take home:
speclemmas, argument of the next lecture
This slide corresponds to section 4.x of the Mathematical Components book