# ProofObjectsThe Curry-Howard Correspondence

"

*Algorithms are the computational content of proofs*." --Robert Harper### Look again at the formal definition of the ev property.

Print ev.

(* ==>

Inductive ev : nat -> Prop :=

| ev_0 : ev 0

| ev_SS : forall n, ev n -> ev (S (S n)).

*)

Suppose we introduce an alternative pronunciation of ":".
Instead of "has type," we can say "is a proof of." For example,
the second line in the definition of ev declares that ev_0 : ev
0. Instead of "ev_0 has type ev 0," we can say that "ev_0
is a proof of ev 0."

This pun between types and propositions -- between : as "has type"
and : as "is a proof of" or "is evidence for" -- is called the

*Curry-Howard correspondence*. It proposes a deep connection between the world of logic and the world of computation:propositions ~ types proofs ~ data valuesSee [Wadler 2015] for a brief history and up-to-date exposition.

### Many useful insights follow from this connection. To begin with, it gives us a natural interpretation of the type of the ev_SS constructor:

Check ev_SS

: ∀ n,

ev n →

ev (S (S n)).

This can be read "ev_SS is a constructor that takes two
arguments -- a number n and evidence for the proposition ev
n -- and yields evidence for the proposition ev (S (S n))."

### Now let's look again at a previous proof involving ev.

Theorem ev_4 : ev 4.

Proof.

apply ev_SS. apply ev_SS. apply ev_0. Qed.

As with ordinary data values and functions, we can use the Print
command to see the

*proof object*that results from this proof script.Print ev_4.

(* ===> ev_4 = ev_SS 2 (ev_SS 0 ev_0)

: ev 4 *)

### Indeed, we can also write down this proof object

*directly*, without the need for a separate proof script:

Check (ev_SS 2 (ev_SS 0 ev_0))

: ev 4.

Similarly, recall that we can apply theorems to arguments
in proof scripts:

Theorem ev_4': ev 4.

Proof.

apply (ev_SS 2 (ev_SS 0 ev_0)).

Qed.

# Proof Scripts

Theorem ev_4'' : ev 4.

Proof.

Show Proof.

apply ev_SS.

Show Proof.

apply ev_SS.

Show Proof.

apply ev_0.

Show Proof.

Qed.

### Tactic proofs are useful and convenient, but they are not essential: in principle, we can always construct the required evidence by hand, as shown above. Then we can use Definition (rather than Theorem) to give a global name directly to this evidence.

Definition ev_4''' : ev 4 :=

ev_SS 2 (ev_SS 0 ev_0).

### All these different ways of building the proof lead to exactly the same evidence being saved in the global environment.

Print ev_4.

(* ===> ev_4 = ev_SS 2 (ev_SS 0 ev_0) : ev 4 *)

Print ev_4'.

(* ===> ev_4' = ev_SS 2 (ev_SS 0 ev_0) : ev 4 *)

Print ev_4''.

(* ===> ev_4'' = ev_SS 2 (ev_SS 0 ev_0) : ev 4 *)

Print ev_4'''.

(* ===> ev_4''' = ev_SS 2 (ev_SS 0 ev_0) : ev 4 *)

# Quantifiers, Implications, Functions

*constructors*introduced by Inductively defined data types, and

*functions*.

### For example, consider this statement:

Theorem ev_plus4 : ∀ n, ev n → ev (4 + n).

Proof.

intros n H. simpl.

apply ev_SS.

apply ev_SS.

apply H.

Qed.

### What is the proof object corresponding to ev_plus4?

*type*is ∀ n, ev n → ev (4 + n) -- that is, a

*function*that takes two arguments (one number and a piece of evidence) and returns a piece of evidence!

Definition ev_plus4' : ∀ n, ev n → ev (4 + n) :=

fun (n : nat) ⇒ fun (H : ev n) ⇒

ev_SS (S (S n)) (ev_SS n H).

Or equivalently:

Definition ev_plus4'' (n : nat) (H : ev n)

: ev (4 + n) :=

ev_SS (S (S n)) (ev_SS n H).

Check ev_plus4''

: ∀ n : nat,

ev n →

ev (4 + n).

### When we view the proposition being proved by ev_plus4 as a function type, one interesting point becomes apparent: The second argument's type, ev n, mentions the

*value*of the first argument, n.

*dependent types*are not found in conventional programming languages, they can be useful in programming too, as the recent flurry of activity in the functional programming community demonstrates.

### Notice that both implication (→) and quantification (∀) correspond to functions on evidence. In fact, they are really the same thing: → is just a shorthand for a degenerate use of ∀ where there is no dependency, i.e., no need to give a name to the type on the left-hand side of the arrow:

∀ (x:nat), nat

= ∀ (_:nat), nat

= nat → nat

Recall the definition of ev:

Inductive ev : nat → Prop :=

| ev_0 : ev 0

| ev_SS : ∀ n, ev n → ev (S (S n)).
What is the type of this expression?

fun (n : nat) ⇒

fun (H : ev n) ⇒

ev_SS (2 + n) (ev_SS n H)
(1) ∀ n, ev n
(2) ∀ n, ev (2 + n)
(3) ∀ n, ev n → ev n
(4) ∀ n, ev n → ev (2 + n)
(5) ∀ n, ev n → ev (4 + n)
(6) Not typeable

Inductive ev : nat → Prop :=

| ev_0 : ev 0

| ev_SS : ∀ n, ev n → ev (S (S n)).

fun (n : nat) ⇒

fun (H : ev n) ⇒

ev_SS (2 + n) (ev_SS n H)

# Programming with Tactics

*programs*using

*tactics*rather than explicit terms. Naturally, the answer is yes!

Definition add1 : nat → nat.

intro n.

Show Proof.

apply S.

Show Proof.

apply n. Defined.

Print add1.

(* ==>

add1 = fun n : nat => S n

: nat -> nat

*)

Compute add1 2.

(* ==> 3 : nat *)

### Notice that we terminate the Definition with a . rather than with := followed by a term. This tells Coq to enter

*proof scripting mode*to build an object of type nat → nat. Also, we terminate the proof with Defined rather than Qed; this makes the definition

*transparent*so that it can be used in computation like a normally-defined function. (Qed-defined objects are opaque during computation.)

# Logical Connectives as Inductive Types

## Conjunction

Inductive and (P Q : Prop) : Prop :=

| conj : P → Q → and P Q.

Arguments conj [P] [Q].

Notation "P /\ Q" := (and P Q) : type_scope.

Notice the similarity with the definition of the prod type,
given in chapter Poly; the only difference is that prod takes
Type arguments, whereas and takes Prop arguments.

Print prod.

(* ===>

Inductive prod (X Y : Type) : Type :=

| pair : X -> Y -> X * Y. *)

### This similarity should clarify why destruct and intros patterns can be used on a conjunctive hypothesis. Case analysis allows us to consider all possible ways in which P ∧ Q was proved -- here just one (the conj constructor).

Theorem proj1' : ∀ P Q,

P ∧ Q → P.

Proof.

intros P Q HPQ. destruct HPQ as [HP HQ]. apply HP.

Show Proof.

Qed.

Similarly, the split tactic actually works for any inductively
defined proposition with exactly one constructor. In particular,
it works for and:

Lemma and_comm : ∀ P Q : Prop, P ∧ Q ↔ Q ∧ P.

Proof.

intros P Q. split.

- intros [HP HQ]. split.

+ apply HQ.

+ apply HP.

- intros [HQ HP]. split.

+ apply HP.

+ apply HQ.

Qed.

### This shows why the inductive definition of and can be manipulated by tactics as we've been doing. We can also use it to build proofs directly, using pattern-matching. For instance:

Definition and_comm'_aux P Q (H : P ∧ Q) : Q ∧ P :=

match H with

| conj HP HQ ⇒ conj HQ HP

end.

Definition and_comm' P Q : P ∧ Q ↔ Q ∧ P :=

conj (and_comm'_aux P Q) (and_comm'_aux Q P).

What is the type of this expression?

fun P Q R (H

match (H

| (conj _ _ HP _, conj _ _ _ HR) ⇒ conj P R HP HR

end.
(1) ∀ P Q R, P ∧ Q → Q ∧ R → P ∧ R
(2) ∀ P Q R, Q ∧ P → R ∧ Q → P ∧ R
(3) ∀ P Q R, P ∧ R
(4) ∀ P Q R, P ∨ Q → Q ∨ R → P ∨ R
(5) Not typeable

fun P Q R (H

_{1}: and P Q) (H_{2}: and Q R) ⇒match (H

_{1},H_{2}) with| (conj _ _ HP _, conj _ _ _ HR) ⇒ conj P R HP HR

end.

## Disjunction

Inductive or (P Q : Prop) : Prop :=

| or_introl : P → or P Q

| or_intror : Q → or P Q.

Arguments or_introl [P] [Q].

Arguments or_intror [P] [Q].

Notation "P \/ Q" := (or P Q) : type_scope.

This declaration explains the behavior of the destruct tactic on
a disjunctive hypothesis, since the generated subgoals match the
shape of the or_introl and or_intror constructors.
Once again, we can also directly write proof objects for theorems
involving or, without resorting to tactics.

Definition inj_l : ∀ (P Q : Prop), P → P ∨ Q :=

fun P Q HP ⇒ or_introl HP.

Theorem inj_l' : ∀ (P Q : Prop), P → P ∨ Q.

Proof.

intros P Q HP. left. apply HP.

Qed.

Definition or_elim : ∀ (P Q R : Prop), (P ∨ Q) → (P → R) → (Q → R) → R :=

fun P Q R HPQ HPR HQR ⇒

match HPQ with

| or_introl HP ⇒ HPR HP

| or_intror HQ ⇒ HQR HQ

end.

Theorem or_elim' : ∀ (P Q R : Prop), (P ∨ Q) → (P → R) → (Q → R) → R.

Proof.

intros P Q R HPQ HPR HQR.

destruct HPQ as [HP | HQ].

- apply HPR. apply HP.

- apply HQR. apply HQ.

Qed.

What is the type of this expression?

fun P Q H ⇒

match H with

| or_introl HP ⇒ or_intror Q P HP

| or_intror HQ ⇒ or_introl Q P HQ

end.
(1) ∀ P Q H, Q ∨ P ∨ H
(2) ∀ P Q, P ∨ Q → P ∨ Q
(3) ∀ P Q H, P ∨ Q → Q ∨ P → H
(4) ∀ P Q, P ∨ Q → Q ∨ P
(5) Not typeable

fun P Q H ⇒

match H with

| or_introl HP ⇒ or_intror Q P HP

| or_intror HQ ⇒ or_introl Q P HQ

end.

## Existential Quantification

Inductive ex {A : Type} (P : A → Prop) : Prop :=

| ex_intro : ∀ x : A, P x → ex P.

Notation "'exists' x , p" :=

(ex (fun x ⇒ p))

(at level 200, right associativity) : type_scope.

This may benefit from a little unpacking. The core definition is
for a type former ex that can be used to build propositions of
the form ex P, where P itself is a
The notation in the standard library is a slight variant of
the above, enabling syntactic forms such as ∃ x y, P x y.

*function*from witness values in the type A to propositions. The ex_intro constructor then offers a way of constructing evidence for ex P, given a witness x and a proof of P x.### The more familiar form ∃ x, P x desugars to an expression involving ex:

Check ex (fun n ⇒ ev n) : Prop.

Here's how to define an explicit proof object involving ex:

Definition some_nat_is_even : ∃ n, ev n :=

ex_intro ev 4 (ev_SS 2 (ev_SS 0 ev_0)).

Inductive True : Prop :=

| I : True.

It has one constructor (so every proof of True is the same, so
being given a proof of True is not informative.)
False is equally simple -- indeed, so simple it may look
syntactically wrong at first glance!

Inductive False : Prop := .

That is, False is an inductive type with

*no*constructors -- i.e., no way to build evidence for it. For example, there is no way to complete the following definition such that it succeeds (rather than fails).Fail Definition contra : False :=

0 = 1.

But it is possible to destruct False by pattern matching. There can
be no patterns that match it, since it has no constructors. So
the pattern match also is so simple it may look syntactically
wrong at first glance.

Definition false_implies_zero_eq_one : False → 0 = 1 :=

fun contra ⇒ match contra with end.

Since there are no branches to evaluate, the match expression
can be considered to have any type we want, including 0 = 1.
Indeed, it's impossible to ever cause the match to be evaluated,
because we can never construct a value of type False to pass to
the function.

Inductive eq {X:Type} : X → X → Prop :=

| eq_refl : ∀ x, eq x x.

Notation "x == y" := (eq x y)

(at level 70, no associativity)

: type_scope.

*convertible*according to computation rules: function application, inlining of definitions, and simplification of matches.

Lemma four: 2 + 2 == 1 + 3.

Proof.

apply eq_refl.

Qed.

Definition four' : 2 + 2 == 1 + 3 :=

eq_refl 4.

Definition singleton : ∀ (X:Type) (x:X), []++[x] == x::[] :=

fun (X:Type) (x:X) ⇒ eq_refl [x].

Which of the following is a correct proof object for the proposition

∃ x, x + 3 = 4
?
(1) eq_refl 4
(2) ex_intro nat (fun z ⇒ (z + 3 = 4)) 1 eq_refl
(3) ex_intro nat (z + 3 = 4) 1 (eq_refl 4)
(4) ex_intro nat (fun z ⇒ (z + 3 = 4)) 1 (eq_refl 4)
(5) ex_intro nat (fun z ⇒ (z + 3 = 4)) 1 (eq_refl 1)
(6) none of the above

∃ x, x + 3 = 4

Which of the following propositions is proved by
providing an explicit witness w using exist w?
(1) ∀ x: nat, (∃ n, x = S n) → (x<>0)
(2) ∀ x: nat, (x<>0) → (∃ n, x = S n)
(3) ∀ x: nat, (x=0) → ~(∃ n, x = S n)
(4) ∀ x: nat, x = 4 → (x<>0)
(5) none of the above

# The Coq Trusted Computing Base

Fail Definition or_bogus : ∀ P Q, P ∨ Q → P :=

fun (P Q : Prop) (A : P ∨ Q) ⇒

match A with

| or_introl H ⇒ H

end.

And this one:

Fail Fixpoint infinite_loop {X : Type} (n : nat) {struct n} : X :=

infinite_loop n.

Fail Definition falso : False := infinite_loop 0.

User-written tactics could produce invalid proof objects.
Qed runs the type checker to detect that.