ProofObjectsWorking with Explicit Evidence in Coq
Require Export Logic.
Programming and proving in Coq are two sides of the same coin.
Proving manipulates evidence, much as programs manipuate data.
Q. If evidence is data, what are propositions themselves?
A. They are types!
Look again at the formal definition of the beautiful property.
Print beautiful.
(* ==>
Inductive beautiful : nat -> Prop :=
b_0 : beautiful 0
| b_3 : beautiful 3
| b_5 : beautiful 5
| b_sum : forall n m : nat, beautiful n -> beautiful m -> beautiful (n + m)
*)
The trick is to introduce an alternative pronunciation of ":".
Instead of "has type," we can also say "is a proof of." For
example, the second line in the definition of beautiful declares
that b_0 : beautiful 0. Instead of "b_0 has type
beautiful 0," we can say that "b_0 is a proof of beautiful 0."
Similarly for b_3 and b_5.
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 valuesMany useful insights follow from this connection. To begin with, it gives us a natural interpretation of the type of b_sum constructor:
Check b_sum.
(* ===> b_sum : forall n m,
beautiful n ->
beautiful m ->
beautiful (n+m) *)
This can be read "b_sum is a constructor that takes four
arguments — two numbers, n and m, and two pieces of evidence,
for the propositions beautiful n and beautiful m, respectively —
and yields evidence for the proposition beautiful (n+m)."
Now let's look again at a previous proof involving beautiful.
Theorem eight_is_beautiful: beautiful 8.
Proof.
apply b_sum with (n := 3) (m := 5).
apply b_3.
apply b_5. Qed.
Just 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 eight_is_beautiful.
(* ===> eight_is_beautiful = b_sum 3 5 b_3 b_5
: beautiful 8 *)
We can use b_sum to build a proof directly, by applying
it to appropriate arguments:
Check (b_sum 3 5 b_3 b_5).
(* ===> beautiful (3 + 5) *)
This gives us an alternative way to write the proof that 8 is
beautiful:
Theorem eight_is_beautiful': beautiful 8.
Proof.
apply (b_sum 3 5 b_3 b_5).
Qed.
Notice that we're using apply here in a new way: instead of just
supplying the name of a hypothesis or previously proved theorem
whose type matches the current goal, we are supplying an
expression that directly builds evidence with the required
type.
Proof Scripts and Proof Objects
Theorem eight_is_beautiful'': beautiful 8.
Proof.
Show Proof.
apply b_sum with (n:=3) (m:=5).
Show Proof.
apply b_3.
Show Proof.
apply b_5.
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 a
piece of evidence.
Definition eight_is_beautiful''' : beautiful 8 :=
b_sum 3 5 b_3 b_5.
All these different ways of building the proof lead to exactly the
same evidence being saved in the global environment.
Print eight_is_beautiful.
(* ===> eight_is_beautiful = b_sum 3 5 b_3 b_5 : beautiful 8 *)
Print eight_is_beautiful'.
(* ===> eight_is_beautiful' = b_sum 3 5 b_3 b_5 : beautiful 8 *)
Print eight_is_beautiful''.
(* ===> eight_is_beautiful'' = b_sum 3 5 b_3 b_5 : beautiful 8 *)
Print eight_is_beautiful'''.
(* ===> eight_is_beautiful''' = b_sum 3 5 b_3 b_5 : beautiful 8 *)
Recall the type of b_sum:
(2) beautiful 6
(3) beautiful (beautiful (3 + 3))
(4) beautiful 3
(5) No type can be assigned
∀n m,
beautiful n →
beautiful m →
beautiful (n+m)
What is the type of the following expression?
beautiful n →
beautiful m →
beautiful (n+m)
b_sum 3 0 b_3 b_0
(1) beautiful (n + m)
What about this one?
(2) beautiful 6
(3) beautiful (beautiful (3 + 3))
(4) beautiful 3
(5) No type can be assigned
b_sum 3 3 b_3 (b_sum 0 3 b_0 b_3))
(1) beautiful (n + m)
What about this one?
(2) beautiful 5
(3) beautiful 3
(4) No type can be assigned
b_sum 5 3 b_3 b_5
(1) beautiful 8
What about this one?
(2) beautiful 3 → beautiful 6
(3) beautiful 6
(4) beautiful 3
(5) No type can be assigned.
b_sum 3 3 b_3
(1) beautiful 3 → beautiful 3
Quantification, Implications and Functions
Theorem b_plus3: ∀n, beautiful n → beautiful (3+n).
Proof.
intros n H.
apply b_sum.
apply b_3.
apply H.
Qed.
What is the proof object corresponding to b_plus3?
We're looking for an expression whose type is ∀ n,
beautiful n → beautiful (3+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 b_plus3' : ∀n, beautiful n → beautiful (3+n) :=
fun (n : nat) ⇒ fun (H : beautiful n) ⇒
b_sum 3 n b_3 H.
Check b_plus3'.
(* ===> b_plus3' : forall n : nat, beautiful n -> beautiful (3+n) *)
Recall that fun n ⇒ blah means "the function that, given n,
yields blah." Another equivalent way to write this definition is:
Definition b_plus3'' (n : nat) (H : beautiful n) : beautiful (3+n) :=
b_sum 3 n b_3 H.
Check b_plus3''.
(* ===> b_plus3'' : forall n, beautiful n -> beautiful (3+n) *)
When we view the proposition being proved by b_plus3 as a function type,
one aspect of it may seem a little unusual. The second argument's
type, beautiful n, mentions the value of the first argument, n.
While such dependent types are not commonly found in programming
languages, even functional ones like ML or Haskell, they can
be useful there too.
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 LHS of the arrow.
Definition beautiful_plus3 : Prop :=
∀n, ∀(E : beautiful n), beautiful (n+3).
Definition beautiful_plus3' : Prop :=
∀n, ∀(_ : beautiful n), beautiful (n+3).
Definition beatiful_plus3'' : Prop :=
∀n, beautiful n → beautiful (n+3).
In general, "P → Q" is just syntactic sugar for
"∀ (_:P), Q".
What is the type of this expression?
(2) ∀ x y : nat, beautiful (3 + x)
(3) beautiful (3 + x)
(4) ∀ x : nat, beautiful x → beautiful (3 + x)
(5) No type can be assigned.
fun x y ⇒ b_sum 3 x b_3 y
(1) nat → nat → beautiful (3 + x)
It is particularly revealing to look at proof objects involving the
logical connectives that we defined with inductive propositions in Logic.v.
Theorem and_example :
(beautiful 0) ∧ (beautiful 3).
Proof.
apply conj.
(* Case "left". *) apply b_0.
(* Case "right". *) apply b_3. Qed.
Print and_example.
(* ===> conj (beautiful 0) (beautiful 3) b_0 b_3
: beautiful 0 /λ beautiful 3 *)
Theorem and_commut : ∀P Q : Prop,
P ∧ Q → Q ∧ P.
Proof.
intros P Q H.
inversion H as [HP HQ].
split.
(* Case "left". *) apply HQ.
(* Case "right". *) apply HP. Qed.
Print and_commut.
(* ===>
and_commut =
fun (P Q : Prop) (H : P /λ Q) =>
(fun H0 : Q /λ P => H0)
match H with
| conj HP HQ => (fun (HP0 : P) (HQ0 : Q) => conj Q P HQ0 HP0) HP HQ
end
: forall P Q : Prop, P /λ Q -> Q /λ P *)
After simplifying some direct application of fun expressions to arguments,
we get:
(* ===>
and_commut =
fun (P Q : Prop) (H : P /λ Q) =>
match H with
| conj HP HQ => conj Q P HQ HP
end
: forall P Q : Prop, P /λ Q -> Q /λ P *)
Giving Explicit Arguments to Lemmas and Hypotheses
Check plus_comm.
(* ==>
plus_comm
: forall n m : nat, n + m = m + n *)
Lemma plus_comm_r : ∀a b c, c + (b + a) = c + (a + b).
Proof.
intros a b c.
(* rewrite plus_comm. *)
(* rewrites in the first possible spot; not what we want *)
rewrite (plus_comm b a). (* directs rewriting to the right spot *)
reflexivity. Qed.
In this case, giving just one argument would be sufficient.
Lemma plus_comm_r' : ∀a b c, c + (b + a) = c + (a + b).
Proof.
intros a b c.
rewrite (plus_comm b).
reflexivity. Qed.
Arguments must be given in order, but wildcards (_)
may be used to skip arguments that Coq can infer.
Lemma plus_comm_r'' : ∀a b c, c + (b + a) = c + (a + b).
Proof.
intros a b c.
rewrite (plus_comm _ a).
reflexivity. Qed.
The author of a lemma can choose to declare easily inferable arguments
to be implicit, just as with functions and constructors.
The with clauses we've already seen is really just a way of
specifying selected arguments by name rather than position:
Lemma plus_comm_r''' : ∀a b c, c + (b + a) = c + (a + b).
Proof.
intros a b c.
rewrite plus_comm with (n := b).
reflexivity. Qed.
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
*)
Eval compute in 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.
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.