ProofObjectsThe Curry-Howard Correspondence
Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
From LF Require Export IndProp.
"_Algorithms are the computational content of proofs."
Robert Harper
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:
Many useful insights follow from this connection. To begin with,
it gives us a natural interpretation of the type of the ev_SS
constructor:
propositions ~ types proofs ~ data valuesSee [Wadler 2015] for a brief history and up-to-date exposition.
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.
As with ordinary data values and functions, we can use the Print
command to see the proof object that results from this proof
script.
Indeed, we can also write down this proof object directly,
without the need for a separate proof script:
The expression ev_SS 2 (ev_SS 0 ev_0) can be thought of as
instantiating the parameterized constructor ev_SS with the
specific arguments 2 and 0 plus the corresponding proof
objects for its premises ev 2 and ev 0. Alternatively, we can
think of ev_SS as a primitive "evidence constructor" that, when
applied to a particular number, wants to be further applied to
evidence that this number is even; its type,
∀ n, ev n → ev (S (S n)),
expresses this functionality, in the same way that the polymorphic
type ∀ X, list X expresses the fact that the constructor
nil can be thought of as a function from types to empty lists
with elements of that type.
We saw in the Logic chapter that we can use function
application syntax to instantiate universally quantified variables
in lemmas, as well as to supply evidence for assumptions that
these lemmas impose. For instance:
∀ n, ev n → ev (S (S n)),
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.
At any given moment, Coq has constructed a term with a
"hole" (indicated by ?Goal here, and so on), and it knows what
type of evidence is needed to fill this hole.
Each hole corresponds to a subgoal, and the proof is
finished when there are no more subgoals. At this point, the
evidence we've built is stored in the global context under the name
given in the Theorem command.
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.
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 *)
Exercise: 2 stars, standard (eight_is_even)
Give a tactic proof and a proof object showing that ev 8.Theorem ev_8 : ev 8.
Proof.
(* FILL IN HERE *) Admitted.
Definition ev_8' : ev 8
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
☐
Quantifiers, Implications, Functions
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?
We're looking for an expression whose 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!
Here it is:
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).
Recall that fun n ⇒ blah means "the function that, given n,
yields blah," and that Coq treats 4 + n and S (S (S (S n)))
as synonyms. Another equivalent way to write this definition is:
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.
While such 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
For example, consider this proposition:
∀ (x:nat), nat
= ∀ (_:nat), nat
= nat → nat
A proof term inhabiting this proposition would be a function
with two arguments: a number n and some evidence E that n is
even. But the name E for this evidence is not used in the rest
of the statement of ev_plus2, so it's a bit silly to bother
making up a name for it. We could write it like this instead,
using the dummy identifier _ in place of a real name:
Or, equivalently, we can write it in a more familiar way:
In general, "P → Q" is just syntactic sugar for
"∀ (_:P), Q".
Programming with Tactics
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.)
This feature is mainly useful for writing functions with dependent
types, which we won't explore much further in this book. But it
does illustrate the uniformity and orthogonality of the basic
ideas in Coq.
Logical Connectives as Inductive Types
Conjunction
Module And.
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.
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.
End And.
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).
Definition conj_fact : ∀ P Q R, P ∧ Q → Q ∧ R → P ∧ R
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
☐
Disjunction
Module Or.
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.
End Or.
Definition or_commut' : ∀ P Q, P ∨ Q → Q ∨ P
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
☐
Existential Quantification
Module Ex.
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.
End Ex.
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 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 notation in the standard library is a slight variant of
the above, enabling syntactic forms such as ∃ x y, P x y.
The more familiar form ∃ x, P x desugars to an expression
involving ex:
Here's how to define an explicit proof object involving ex:
Definition ex_ev_Sn : ex (fun n ⇒ ev (S n))
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
☐
It has one constructor (so every proof of True is the same, so
being given a proof of True is not informative.)
Exercise: 1 star, standard (p_implies_true)
Construct a proof object for the following proposition.Definition p_implies_true : ∀ P, P → True
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
☐
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).
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.
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.
Exercise: 1 star, standard (ex_falso_quodlibet')
Construct a proof object for the following proposition.Definition ex_falso_quodlibet' : ∀ P, False → P
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
☐
Module MyEquality.
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.
The way to think about this definition (which is just a slight
variant of the standard library's) is that, given a set X, it
defines a family of propositions "x is equal to y," indexed
by pairs of values (x and y) from X. There is just one way
of constructing evidence for members of this family: applying the
constructor eq_refl to a type X and a single value x : X,
which yields evidence that x is equal to x.
Other types of the form eq x y where x and y are not the
same are thus uninhabited.
We can use eq_refl to construct evidence that, for example, 2 =
2. Can we also use it to construct evidence that 1 + 1 = 2?
Yes, we can. Indeed, it is the very same piece of evidence!
The reason is that Coq treats as "the same" any two terms that are
convertible according to a simple set of computation rules.
These rules, which are similar to those used by Compute, include
evaluation of function application, inlining of definitions, and
simplification of matches.
The reflexivity tactic that we have used to prove
equalities up to now is essentially just shorthand for apply
eq_refl.
In tactic-based proofs of equality, the conversion rules are
normally hidden in uses of simpl (either explicit or implicit in
other tactics such as reflexivity).
But you can see them directly at work in the following explicit
proof objects:
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].
Exercise: 2 stars, standard (equality__leibniz_equality)
The inductive definition of equality implies Leibniz equality: what we mean when we say "x and y are equal" is that every property on P that is true of x is also true of y.Lemma equality__leibniz_equality : ∀ (X : Type) (x y: X),
x == y → ∀ P:X→Prop, P x → P y.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 3 stars, standard, optional (leibniz_equality__equality)
Show that, in fact, the inductive definition of equality is equivalent to Leibniz equality. Hint: the proof is quite short; about all you need to do is to invent a clever property P to instantiate the antecedent.Lemma leibniz_equality__equality : ∀ (X : Type) (x y: X),
(∀ P:X→Prop, P x → P y) → x == y.
Proof.
(* FILL IN HERE *) Admitted.
☐
Inversion, Again
- takes a hypothesis H whose type P is inductively defined,
and
- for each constructor C in P's definition,
- generates a new subgoal in which we assume H was
built with C,
- adds the arguments (premises) of C to the context of
the subgoal as extra hypotheses,
- matches the conclusion (result type) of C against the
current goal and calculates a set of equalities that must
hold in order for C to be applicable,
- adds these equalities to the context (and, for convenience,
rewrites them in the goal), and
- if the equalities are not satisfiable (e.g., they involve things like S n = O), immediately solves the subgoal.
- generates a new subgoal in which we assume H was
built with C,
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.
All the types here match correctly, but the match only
considers one of the possible constructors for or. Coq's
exhaustiveness check will reject this definition.
Third, the checker must make sure that each recursive function
terminates. It does this using a syntactic check to make sure
that each recursive call is on a subexpression of the original
argument. To see why this is essential, consider this alleged
proof:
Fail Fixpoint infinite_loop {X : Type} (n : nat) {struct n} : X :=
infinite_loop n.
Fail Definition falso : False := infinite_loop 0.
Recursive function infinite_loop purports to return a
value of any type X that you would like. (The struct
annotation on the function tells Coq that it recurses on argument
n, not X.) Were Coq to allow infinite_loop, then falso
would be definable, thus giving evidence for False. So Coq rejects
infinite_loop.
Note that the soundness of Coq depends only on the
correctness of this typechecking engine, not on the tactic
machinery. If there is a bug in a tactic implementation (and this
certainly does happen!), that tactic might construct an invalid
proof term. But when you type Qed, Coq checks the term for
validity from scratch. Only theorems whose proofs pass the
type-checker can be used in further proof developments.
(* 2021-03-18 17:23 *)