# 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 [&#10029;&#10029;] 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 [&#10029;] 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. <!-- Another way that does actually type check, but trying to use the value crashes...  let f : 'a . 'a = Obj.magic ();; let ff = {nope = f};; ff.nope 0;; Segmentation fault  --> &square; ##### Exercise: neg props to types [&#10029;&#10029;] 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 [&#10029;&#10029;&#10029;] 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 [&#10029;&#10029;&#10029;&#10029;] 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 [&#10029;&#10029;&#10029;] 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;