ProofObjects: The Curry-Howard Correspondence

“Algorithms are the computational content of proofs.” —Robert Harper

In Coq we have seen machanisms for

• Programming: using inductive data types and functions over them.
• Proving: using inductive propositions, implication, universal quantification.

Not separate, but related.

Types and propositions

between [:] as “has type” and [:] as “is a proof of” or “is evidence for” — is called the “Curry-Howard correspondence“.

propositions ~ types

proofs ~ data values

E.g. the definition of ev and proof of (ev 4).

Proof Scripts

Gradually constructing a proof object — a term whose type is the proposition being proved!!

The tactics between [Proof] and [Qed] tell it how to build up a term of the required type.

Let’s see what happens with the help of [Show Proof command].

• A proof script is to fill the hole(?Goal).
• Tactic proofs are useful and convenient but not essential. We can use [Definition] rather than [Theorem] to give a global name directly to the evidence.

Quantifiers, Implications, Functions

Proof of propositions including implications map to construct function(hypotheses as params and conclusion as results)

The equivalent proof/def of ex_plus4.

Programmig with Tactics

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]. And terminate the proof with [Defined] rather than [Qed].

End with [Defined] rather than [Qed] make the definition “transparent”. NEED BETTER UNDERSTANDING.

Logical Connectives as Inductive Types

Here we know what conjunction [/] actually means.

This clarify why [destruct] and [intros] patterns can be used on a conjunctive hypothesis. Case analysis allow us to consider all possible ways in which [P /\ Q] was proved. Her just one (from the [conj] constructor).

Exercise: construct a proof object for the following proposition.

Disjunction

The inductive definition.

Existential Quantification

Construct the witness of such a Prop

[True] and [False]

Both simple

[False] is an inductive type with no constructors. NO WAY TO BUILD AN EVIDENCE OR MAKE A DEFINITION!!

Equality

Inductive definition

The Inductive definition is equivalent to Leibniz equality.

From inductive definition, the only way to construct a equal pair is applying the constructor [eq_refl] to a type [X] and value [x : X].