# 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:
Proposition | Symbol | OCaml | Coq |
Implication | \\(\rightarrow\\) | `->` | `->` |
Conjunction | \\(\wedge\\) | `*` | `and` or `/\` |
Disjunction | \\(\vee\\) | `('a,'b) or'` |
`or` or `\/` |
Truth | \\(\top\\) | `unit` | `True` |
Atomic proposition | \\(p, q, r, \ldots\\) | `'p, 'q, 'r, ...` |
`P, Q, R, ... : Prop` |
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)\\)
□
It is also possible to develop a correspondence for falsehood
and negation.
Proposition | Symbol | OCaml | Coq |
False | \\(\bot\\) | `void` | `False` |
Negation | \\(\neg\\) | `'a neg` | `not` or `~` |
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.
□
##### 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\\)
□
## 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)\\)
□
##### 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).
□
## 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.
□