Lab: Proofs are Programs

# Proofs are Programs This lab focuses on the Curry-Howard correspondence: propositions as types, proofs as programs, and simplification as evaluation. ## Propositions as types In lecture we developed the following correspondence between propositions and types: <table> <tr><th>Proposition</th><th>Symbol</th><th>OCaml</th><th>Coq</th></tr> <tr><td>Implication</td><td>\\(\rightarrow\\)</td><td>`->`</td><td>`->`</td></tr> <tr><td>Conjunction</td><td>\\(\wedge\\)</td><td>`*`</td><td>`and` or `/\`</td></tr> <tr><td>Disjunction</td><td>\\(\vee\\)</td><td>`('a,'b) or'`</td> <td>`or` or `\/`</td></tr> <tr><td>Truth</td><td>\\(\top\\)</td><td>`unit`</td><td>`True`</td></tr> <tr><td>Atomic proposition</td><td>\\(p, q, r, \ldots\\)</td><td>`'p, 'q, 'r, ...`</td> <td>`P, Q, R, ... : Prop`</td></tr> </table> Recall that we defined ``` type ('a,'b) or' = Left of 'a | Right of 'b ``` If we wanted a little closer parallel between conjunction and disjunction we could define an OCaml type constructor for pairs: ``` type ('a,'b) and' = 'a * 'b ``` ##### Exercise: props to types [✭✭] For each of the following propositions, write its corresponding type in both OCaml and Coq. * \\(\top \rightarrow p\\) * \\(p \wedge (q \wedge r)\\) * \\((p \vee q) \vee r)\\) &square; It is also possible to develop a correspondence for falsehood and negation. <table> <tr><th>Proposition</th><th>Symbol</th><th>OCaml</th><th>Coq</th></tr> <tr><td>False</td><td>\\(\bot\\)</td><td>`void`</td><td>`False`</td></tr> <tr><td>Negation</td><td>\\(\neg\\)</td><td>`'a neg`</td><td>`not` or `~`</td></tr> </table> The OCaml definitions used above are: ``` type void = {nope : 'a . 'a} type 'a neg = 'a -> void ``` The definition of `void` uses a syntax for types that we haven't seen before (and probably will never see again). It is an [explicit polymorphic type annotation][explicit]. In general, `'a . t` is a type in which `'a` is a type variable that may appear in `t`. Here, `nope :'a . 'a` specifically says that the field named `nope` must be able to be given any type `'a` whatsoever. That includes, e.g., both `int` and `string`. There is no value in OCaml that has type both `int` and `string`, so there is no value we could ever use to successfully create a record of type `void`. [explicit]: http://caml.inria.fr/pub/docs/manual-ocaml-4.04/extn.html#sec227 ##### Exercise: void [✭] The reason we chose `void` as the name for the type representing falsehood is that it is impossible to construct a value of this type: the set of values of type `void` is *devoid* of any members. Try entering the following code into utop: ``` type void = {nope : 'a . 'a};; {nope = 0};; ``` You'll get an type-checking error from trying to create the record: ``` Error: This field value has type int which is less general than 'a. 'a ``` The only way to get past the type checker here is with something that doesn't terminate normally, like an infinite loop. Try entering this code: ``` let rec inf_loop x = inf_loop x;; let ff1 = {nope = inf_loop ()};; ``` Note that `ff1` type checks (because we don't get a type error), but then construction of it never terminates. Type Control-C to break the infinite loop. Also try entering the following code: ``` let ff2 = {nope = failwith "nope"} ``` Again, that typechecks, but we never succeed in constructing `ff2` because the exception gets raised first.  &square; ##### Exercise: neg props to types [✭✭] For each of the following propositions, write its corresponding type in both OCaml and Coq. * \\(\bot \rightarrow p\\) * \\(p \vee \neg p\\) &square; ## Proofs as programs In lecture we developed the idea that the proof of a proposition corresponds to a program, where the type of the program corresponds to the proposition. For example, given the proposition \\(p \rightarrow p\\), we have the following correspondences: * In OCaml: the type corresponding to it is `'p -> 'p`. A program of that type is `fun x:'p -> x`. We could use a let definition like `let p_implies_p x:'p = x` to give that program a name. * In Coq: the type corresponding to it is `P -> P`, where `P : Prop`. A program of that type is `fun x:P => x`, assuming `P` is in scope. We could use a let definition like `Let p_implies_p (P:Prop) (x:P) := x.` to give that program a name and to make `P` an explicit argument. Note that Coq's type system requires us to make `P` an explicit type argument to the function, whereas OCaml's type system doesn't permit us to pass explicit type arguments at all. ##### Exercise: program proofs [✭✭✭] For each of the following propositions, determine its corresponding type in both OCaml and Coq, then write an OCaml and a Coq let definition to give a program of that type, as we did above. Your program proves that the type is *inhabited*, which means there is a value of that type. It also proves the proposition holds. * \\((p \wedge q) \rightarrow (q \wedge p)\\) * \\((p \vee q) \rightarrow (q \vee p)\\) &square; ##### Exercise: program proofs with not [✭✭✭✭] Do the same as the previous exercise for this proposition: * \\((p \vee \neg q) \rightarrow (q \rightarrow p)\\) *Hint:* in Coq, make use of `False_rect : forall P, False -> P` (discussed in the notes from the previous lecture); in OCaml, make use of `explode : void -> 'p` (in this lecture's slides). &square; ## Simplification as evaluation In lecture we mentioned that proof simplification corresponds to program evaluation. ##### Exercise: simplify [✭✭✭] Consider the following OCaml program: ``` let f x = snd ((fun x -> x,x) (fst x)) ``` * What is the type of that program? * What is the proposition corresponding to that type? * How would `f (1,2)` evaluate in the small-step semantics? * What simplified implementation of `f` does that evaluation suggest? (or perhaps there are several, though one is probably the simplest?) * Does your simplified `f` still have the same type as the original? (It should.) Your simplified `f` and the original `f` are both proofs of the same proposition, but evaluation has helped you to produce a simpler proof. &square;