PropPropositions and Evidence
Require Export MoreCoq.
In previous chapters, we have seen many examples of factual
claims (propositions) and ways of presenting evidence of their
truth (proofs). In particular, we have worked extensively with
equality propositions of the form e1 = e2, with
implications (P → Q), and with quantified propositions
(∀ x, P).
This chapter will take us on a first tour of the
propositional (logical) side of Coq.
In particular, we will expand our repertoire of primitive
propositions to include user-defined propositions, not just
equality propositions (which are more-or-less "built in" to Coq).
Inductively Defined Propositions
- Rule b_0: The number 0 is beautiful.
- Rule b_3: The number 3 is beautiful.
- Rule b_5: The number 5 is beautiful.
- Rule b_sum: If n and m are both beautiful, then so is their sum.
(b_0) | |
beautiful 0 |
(b_3) | |
beautiful 3 |
(b_5) | |
beautiful 5 |
beautiful n beautiful m | (b_sum) |
beautiful (n+m) |
----------- (b_3) ----------- (b_5)
beautiful 3 beautiful 5
------------------------------- (b_sum)
beautiful 8
Of course, there are other ways of using these rules to argue that
8 is beautiful, for instance:
beautiful 3 beautiful 5
------------------------------- (b_sum)
beautiful 8
----------- (b_5) ----------- (b_3)
beautiful 5 beautiful 3
------------------------------- (b_sum)
beautiful 8
beautiful 5 beautiful 3
------------------------------- (b_sum)
beautiful 8
Exercise: 1 star (varieties_of_beauty)
How many different ways are there to show that 8 is beautiful?(* FILL IN HERE *)
☐
In Coq, we can express the definition of beautiful as
follows:
Inductive beautiful : nat → Prop :=
b_0 : beautiful 0
| b_3 : beautiful 3
| b_5 : beautiful 5
| b_sum : ∀n m, beautiful n → beautiful m → beautiful (n+m).
The first line declares that beautiful is a proposition — or,
more formally, a family of propositions "indexed by" natural
numbers. (That is, for each number n, the claim that "n is
beautiful" is a proposition.) Such a family of propositions is
often called a property of numbers. Each of the remaining lines
embodies one of the rules for beautiful numbers.
The rules introduced this way have the same status as proven
theorems; that is, they are true axiomatically.
So we can use Coq's apply tactic with the rule names to prove
that particular numbers are beautiful.
Theorem three_is_beautiful: beautiful 3.
Proof.
(* This simply follows from the rule b_3. *)
apply b_3.
Qed.
Theorem eight_is_beautiful: beautiful 8.
Proof.
(* First we use the rule b_sum, telling Coq how to
instantiate n and m. *)
apply b_sum with (n:=3) (m:=5).
(* To solve the subgoals generated by b_sum, we must provide
evidence of beautiful 3 and beautiful 5. Fortunately we
have rules for both. *)
apply b_3.
apply b_5.
Qed.
As you would expect, we can also prove theorems that have
hypotheses about beautiful.
Theorem beautiful_plus_eight: ∀n, beautiful n → beautiful (8+n).
Proof.
intros n B.
apply b_sum with (n:=8) (m:=n).
apply eight_is_beautiful.
apply B.
Qed.
Theorem b_timesm: ∀n m, beautiful n → beautiful (m*n).
Proof.
(* FILL IN HERE *) Admitted.
Proof.
(* FILL IN HERE *) Admitted.
☐
Induction Over Evidence
- E is b_0 (and n is O),
- E is b_3 (and n is 3),
- E is b_5 (and n is 5), or
- E is b_sum n1 n2 E1 E2 (and n is n1+n2, where E1 is evidence that n1 is beautiful and E2 is evidence that n2 is beautiful).
Inductive gorgeous : nat → Prop :=
g_0 : gorgeous 0
| g_plus3 : ∀n, gorgeous n → gorgeous (3+n)
| g_plus5 : ∀n, gorgeous n → gorgeous (5+n).
Exercise: 1 star (gorgeous_tree)
Write out the definition of gorgeous numbers using inference rule notation.☐
Exercise: 1 star (gorgeous_plus13)
Theorem gorgeous_plus13: ∀n,
gorgeous n → gorgeous (13+n).
Proof.
(* FILL IN HERE *) Admitted.
gorgeous n → gorgeous (13+n).
Proof.
(* FILL IN HERE *) Admitted.
☐
It seems intuitively obvious that, although gorgeous and
beautiful are presented using slightly different rules, they are
actually the same property in the sense that they are true of the
same numbers. Indeed, we can prove this.
Theorem gorgeous__beautiful : ∀n,
gorgeous n → beautiful n.
Proof.
intros n H.
induction H as [|n'|n'].
Case "g_0".
apply b_0.
Case "g_plus3".
apply b_sum. apply b_3.
apply IHgorgeous.
Case "g_plus5".
apply b_sum. apply b_5. apply IHgorgeous.
Qed.
Notice that the argument proceeds by induction on the evidence H!
Let's see what happens if we try to prove this by induction on n
instead of induction on the evidence H.
Theorem gorgeous__beautiful_FAILED : ∀n,
gorgeous n → beautiful n.
Proof.
intros. induction n as [| n'].
Case "n = 0". apply b_0.
Case "n = S n'". (* We are stuck! *)
Abort.
The problem here is that doing induction on n doesn't yield a
useful induction hypothesis. Knowing how the property we are
interested in behaves on the predecessor of n doesn't help us
prove that it holds for n. Instead, we would like to be able to
have induction hypotheses that mention other numbers, such as n -
3 and n - 5. This is given precisely by the shape of the
constructors for gorgeous.
Exercise: 2 stars (gorgeous_sum)
Theorem gorgeous_sum : ∀n m,
gorgeous n → gorgeous m → gorgeous (n + m).
Proof.
(* FILL IN HERE *) Admitted.
gorgeous n → gorgeous m → gorgeous (n + m).
Proof.
(* FILL IN HERE *) Admitted.
Theorem beautiful__gorgeous : ∀n, beautiful n → gorgeous n.
Proof.
(* FILL IN HERE *) Admitted.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 3 stars, optional (g_times2)
Prove the g_times2 theorem below without using gorgeous__beautiful. You might find the following helper lemma useful.Lemma helper_g_times2 : ∀x y z, x + (z + y)= z + x + y.
Proof.
(* FILL IN HERE *) Admitted.
Theorem g_times2: ∀n, gorgeous n → gorgeous (2*n).
Proof.
intros n H. simpl.
induction H.
(* FILL IN HERE *) Admitted.
☐
From Boolean Functions to Propositions
Definition even (n:nat) : Prop :=
evenb n = true.
That is, we can define "n is even" to mean "the function evenb
returns true when applied to n."
Note that here we have given a name
to a proposition using a Definition, just as we have
given names to expressions of other sorts. This isn't a fundamentally
new kind of proposition; it is still just an equality.
Another alternative is to define the concept of evenness
directly. Instead of going via the evenb function ("a number is
even if a certain computation yields true"), we can say what the
concept of evenness means by giving two different ways of
presenting evidence that a number is even.
Inductive ev : nat → Prop :=
| ev_0 : ev O
| ev_SS : ∀n:nat, ev n → ev (S (S n)).
This definition says that there are two ways to give
evidence that a number m is even. First, 0 is even, and
ev_0 is evidence for this. Second, if m = S (S n) for some
n and we can give evidence e that n is even, then m is
also even, and ev_SS n e is the evidence.
Exercise: 1 star (double_even)
Theorem double_even : ∀n,
ev (double n).
Proof.
(* FILL IN HERE *) Admitted.
☐
We have seen that the proposition "n is even" can be
phrased in two different ways — indirectly, via a boolean testing
function evenb, or directly, by inductively describing what
constitutes evidence for evenness. These two ways of defining
evenness are about equally easy to state and work with. Which we
choose is basically a question of taste.
However, for many other properties of interest, the direct
inductive definition is preferable, since writing a testing
function may be awkward or even impossible.
One such property is beautiful. This is a perfectly sensible
definition of a set of numbers, but we cannot translate its
definition directly into a Coq Fixpoint (or into a recursive
function in any other common programming language). We might be
able to find a clever way of testing this property using a
Fixpoint (indeed, it is not too hard to find one in this case),
but in general this could require arbitrarily deep thinking. In
fact, if the property we are interested in is uncomputable, then
we cannot define it as a Fixpoint no matter how hard we try,
because Coq requires that all Fixpoints correspond to
terminating computations.
On the other hand, writing an inductive definition of what it
means to give evidence for the property beautiful is
straightforward.
Discussion: Computational vs. Inductive Definitions
Exercise: 1 star (ev__even)
Here is a proof that the inductive definition of evenness implies the computational one.Theorem ev__even : ∀n,
ev n → even n.
Proof.
intros n E. induction E as [| n' E'].
Case "E = ev_0".
unfold even. reflexivity.
Case "E = ev_SS n' E'".
unfold even. apply IHE'.
Qed.
Could this proof also be carried out by induction on n instead
of E? If not, why not?
(* FILL IN HERE *)
☐
The induction principle for inductively defined propositions does
not follow quite the same form as that of inductively defined
sets. For now, you can take the intuitive view that induction on
evidence ev n is similar to induction on n, but restricts our
attention to only those numbers for which evidence ev n could be
generated. We'll look at the induction principle of ev in more
depth below, to explain what's really going on.
(* FILL IN HERE *)
☐
Exercise: 1 star (l_fails)
The following proof attempt will not succeed.
Theorem l : ∀n,
ev n.
Proof.
intros n. induction n.
Case "O". simpl. apply ev_0.
Case "S".
...
Intuitively, we expect the proof to fail because not every
number is even. However, what exactly causes the proof to fail?
ev n.
Proof.
intros n. induction n.
Case "O". simpl. apply ev_0.
Case "S".
...
☐
Exercise: 2 stars (ev_sum)
Here's another exercise requiring induction.Theorem ev_sum : ∀n m,
ev n → ev m → ev (n+m).
Proof.
(* FILL IN HERE *) Admitted.
☐
Inversion on Evidence
Theorem ev_minus2: ∀n,
ev n → ev (pred (pred n)).
Proof.
intros n E.
inversion E as [| n' E'].
Case "E = ev_0". simpl. apply ev_0.
Case "E = ev_SS n' E'". simpl. apply E'. Qed.
Exercise: 1 star, optional (ev_minus2_n)
What happens if we try to use destruct on n instead of inversion on E?(* FILL IN HERE *)
☐
Another example, in which inversion helps narrow down to
the relevant cases.
Theorem SSev__even : ∀n,
ev (S (S n)) → ev n.
Proof.
intros n E.
inversion E as [| n' E'].
apply E'. Qed.
These uses of inversion may seem a bit mysterious at first.
Until now, we've only used inversion on equality
propositions, to utilize injectivity of constructors or to
discriminate between different constructors. But we see here
that inversion can also be applied to analyzing evidence
for inductively defined propositions.
(You might also expect that destruct would be a more suitable
tactic to use here. Indeed, it is possible to use destruct, but
it often throws away useful information, and the eqn: qualifier
doesn't help much in this case.)
Here's how inversion works in general. Suppose the name
I refers to an assumption P in the current context, where
P has been defined by an Inductive declaration. Then,
for each of the constructors of P, inversion I generates
a subgoal in which I has been replaced by the exact,
specific conditions under which this constructor could have
been used to prove P. Some of these subgoals will be
self-contradictory; inversion throws these away. The ones
that are left represent the cases that must be proved to
establish the original goal.
In this particular case, the inversion analyzed the construction
ev (S (S n)), determined that this could only have been
constructed using ev_SS, and generated a new subgoal with the
arguments of that constructor as new hypotheses. (It also
produced an auxiliary equality, which happens to be useless here.)
We'll begin exploring this more general behavior of inversion in
what follows.
Exercise: 1 star (inversion_practice)
Theorem SSSSev__even : ∀n,
ev (S (S (S (S n)))) → ev n.
Proof.
(* FILL IN HERE *) Admitted.
ev (S (S (S (S n)))) → ev n.
Proof.
(* FILL IN HERE *) Admitted.
The inversion tactic can also be used to derive goals by showing
the absurdity of a hypothesis.
Theorem even5_nonsense :
ev 5 → 2 + 2 = 9.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 3 stars, advanced (ev_ev__ev)
Finding the appropriate thing to do induction on is a bit tricky here:Theorem ev_ev__ev : ∀n m,
ev (n+m) → ev n → ev m.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 3 stars, optional (ev_plus_plus)
Here's an exercise that just requires applying existing lemmas. No induction or even case analysis is needed, but some of the rewriting may be tedious.Theorem ev_plus_plus : ∀n m p,
ev (n+m) → ev (n+p) → ev (m+p).
Proof.
(* FILL IN HERE *) Admitted.
☐
Additional Exercises
Exercise: 4 stars (palindromes)
A palindrome is a sequence that reads the same backwards as forwards.- Define an inductive proposition pal on list X that
captures what it means to be a palindrome. (Hint: You'll need
three cases. Your definition should be based on the structure
of the list; just having a single constructor
c : ∀l, l = rev l → pal lmay seem obvious, but will not work very well.)
- Prove that
∀l, pal (l ++ rev l).
- Prove that
∀l, pal l → l = rev l.
(* FILL IN HERE *)
☐
Exercise: 5 stars, optional (palindrome_converse)
Using your definition of pal from the previous exercise, prove that
∀l, l = rev l → pal l.
(* FILL IN HERE *)
☐
Exercise: 4 stars, advanced (subsequence)
A list is a subsequence of another list if all of the elements in the first list occur in the same order in the second list, possibly with some extra elements in between. For example,
[1,2,3]
is a subsequence of each of the lists
[1,2,3]
[1,1,1,2,2,3]
[1,2,7,3]
[5,6,1,9,9,2,7,3,8]
but it is not a subsequence of any of the lists
[1,1,1,2,2,3]
[1,2,7,3]
[5,6,1,9,9,2,7,3,8]
[1,2]
[1,3]
[5,6,2,1,7,3,8]
[1,3]
[5,6,2,1,7,3,8]
- Define an inductive proposition subseq on list nat that
captures what it means to be a subsequence. (Hint: You'll need
three cases.)
- Prove that subsequence is reflexive, that is, any list is a
subsequence of itself.
- Prove that for any lists l1, l2, and l3, if l1 is a
subsequence of l2, then l1 is also a subsequence of l2 ++
l3.
- (Optional, harder) Prove that subsequence is transitive — that is, if l1 is a subsequence of l2 and l2 is a subsequence of l3, then l1 is a subsequence of l3. Hint: choose your induction carefully!
(* FILL IN HERE *)
☐
☐
Exercise: 2 stars, optional (R_provability)
Suppose we give Coq the following definition:
Inductive R : nat → list nat → Prop :=
| c1 : R 0 []
| c2 : ∀n l, R n l → R (S n) (n :: l)
| c3 : ∀n l, R (S n) l → R n l.
Which of the following propositions are provable?
| c1 : R 0 []
| c2 : ∀n l, R n l → R (S n) (n :: l)
| c3 : ∀n l, R (S n) l → R n l.
- R 2 [1,0]
- R 1 [1,2,1,0]
- R 6 [3,2,1,0]
(* $Date: 2013-07-01 18:48:47 -0400 (Mon, 01 Jul 2013) $ *)