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.



Lesson 4: summary

  • Curry Howard: the big picture + dependent function space
  • Predicates and connectives + introduction + elimination
  • Induction
  • Consistency
  • Dependent elimination

Curry Howard

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.

In type theory: p is a proof of T means that p inhabits the type T.

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?


(notes)

This slide corresponds to section 4.x of the Mathematical Components book


Predicates and connectives

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


(notes)

This slide corresponds to section 4.x of the Mathematical Components book


Induction

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.


(notes)

This slide corresponds to section 4.x of the Mathematical Components book


Consistency

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.


(notes)

This slide corresponds to section 3.2.3 of the Mathematical Components book


Inductive types with indexes (casse-tĂȘte)

... and their elimination.

The intuition, operationally.

Inductive types can express tricky invariants:

Take home:

  • the elimination of an inductive data type with indexes expresses equations between the value of the indexes in the type of the eliminated term and the value of the indexes prescribed in the declatation of the inductive data
  • the implicit equations are substituted automatically at elimination time
  • working with indexed data is hard, too hard :-/
  • we can still make good use of indexes when we define spec lemmas, argument of the next lecture


(notes)

This slide corresponds to section 4.x of the Mathematical Components book


Lesson 4: sum up

  • In Coq terms/types play a double role: + programs and their types + statements and their proofs
  • Inductives can be used to model predicates and connectives
  • Pattern machind and recursion can model induction
  • The empty type is, well, empty, hence Coq is consistent
  • Inductives with indexes