Acknowledgements
This material is taken verbatim from Software Foundations V4.0
Copyright (c) 2016
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in
all copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
THE SOFTWARE.
Assumed Knowledge:
* Understands how to construct propositions in Coq
Learning Outcomes:
* TODO
Inductively Defined Propositions
In the
Logic chapter we looked at several ways of writing
propositions, including conjunction, disjunction, and quantifiers.
In this chapter, we bring a new tool into the mix:
inductive
definitions.
Recall that we have seen two ways of stating that a number
n is
even: We can say (1)
evenb n = true, or (2)
∃ k, n =
double k. Yet another possibility is to say that
n is even if
we can establish its evenness from the following rules:
- Rule ev_0: The number 0 is even.
- Rule ev_SS: If n is even, then S (S n) is even.
To illustrate how this new definition of evenness works, let's use
its rules to show that
4 is even. By rule
ev_SS, it suffices
to show that
2 is even. This, in turn, is again guaranteed by
rule
ev_SS, as long as we can show that
0 is even. But this
last fact follows directly from the
ev_0 rule.
We will see many definitions like this one during the rest
of the course. For purposes of informal discussions, it is
helpful to have a lightweight notation that makes them easy to
read and write.
Inference rules are one such notation:
ev n |
(ev_SS)
|
|
ev (S (S n)) |
|
Each of the textual rules above is reformatted here as an
inference rule; the intended reading is that, if the
premises
above the line all hold, then the
conclusion below the line
follows. For example, the rule
ev_SS says that, if
n
satisfies
ev, then
S (S n) also does. If a rule has no
premises above the line, then its conclusion holds
unconditionally.
We can represent a proof using these rules by combining rule
applications into a
proof tree. Here's how we might transcribe
the above proof that
4 is even:
------ (
ev_0)
ev 0
------ (
ev_SS)
ev 2
------ (
ev_SS)
ev 4
Why call this a "tree" (rather than a "stack", for example)?
Because, in general, inference rules can have multiple premises.
We will see examples of this below.
Putting all of this together, we can translate the definition of
evenness into a formal Coq definition using an
Inductive
declaration, where each constructor corresponds to an inference
rule:
This definition is different in one crucial respect from
previous uses of
Inductive: its result is not a
Type, but
rather a function from
nat to
Prop — that is, a property of
numbers. Note that we've already seen other inductive definitions
that result in functions, such as
list, whose type is
Type →
Type. What is new here is that, because the
nat argument of
ev appears
unnamed, to the
right of the colon, it is allowed
to take different values in the types of different constructors:
0 in the type of
ev_0 and
S (S n) in the type of
ev_SS.
In contrast, the definition of
list names the
X parameter
globally, to the
left of the colon, forcing the result of
nil and
cons to be the same (
list X). Had we tried to bring
nat to the left in defining
ev, we would have seen an error:
("Parameter" here is Coq jargon for an argument on the left of the
colon in an
Inductive definition; "index" is used to refer to
arguments on the right of the colon.)
We can think of the definition of
ev as defining a Coq property
ev : nat → Prop, together with theorems
ev_0 : ev 0 and
ev_SS : ∀ n, ev n → ev (S (S n)). Such "constructor
theorems" have the same status as proven theorems. In particular,
we can use Coq's
apply tactic with the rule names to prove
ev
for particular numbers...
... or we can use function application syntax:
We can also prove theorems that have hypotheses involving ev.
More generally, we can show that any number multiplied by 2 is even:
Exercise: 1 star (ev_double)
☐
Using Evidence in Proofs
Besides
constructing evidence that numbers are even, we can also
reason about such evidence.
Introducing
ev with an
Inductive declaration tells Coq not
only that the constructors
ev_0 and
ev_SS are valid ways to
build evidence that some number is even, but also that these two
constructors are the
only ways to build evidence that numbers
are even (in the sense of
ev).
In other words, if someone gives us evidence
E for the assertion
ev n, then we know that
E must have one of two shapes:
- E is ev_0 (and n is O), or
- E is ev_SS n' E' (and n is S (S n'), where E' is
evidence for ev n').
This suggests that it should be possible to analyze a hypothesis
of the form
ev n much as we do inductively defined data
structures; in particular, it should be possible to argue by
induction and
case analysis on such evidence. Let's look at a
few examples to see what this means in practice.
Inversion on Evidence
Subtracting two from an even number yields another even number.
We can easily prove this claim with the techniques that we've
already seen, provided that we phrase it in the right way. If we
state it in terms of
evenb, for instance, we can proceed by a
simple case analysis on
n:
We can state the same claim in terms of ev, but this quickly
leads us to an obstacle: Since ev is defined inductively —
rather than as a function — Coq doesn't know how to simplify a
goal involving ev n after case analysis on n. As a
consequence, the same proof strategy fails:
The solution is to perform case analysis on the evidence that
ev
n directly. By the definition of
ev, there are two cases to
consider:
- If that evidence is of the form ev_0, we know that n = 0.
Therefore, it suffices to show that ev (pred (pred 0)) holds.
By the definition of pred, this is equivalent to showing that
ev 0 holds, which directly follows from ev_0.
- Otherwise, that evidence must have the form ev_SS n' E', where
n = S (S n') and E' is evidence for ev n'. We must then
show that ev (pred (pred (S (S n')))) holds, which, after
simplification, follows directly from E'.
We can invoke this kind of argument in Coq using the
inversion
tactic. Besides allowing us to reason about equalities involving
constructors,
inversion provides a case-analysis principle for
inductively defined propositions. When used in this way, its
syntax is similar to
destruct: We pass it a list of identifiers
separated by
| characters to name the arguments to each of the
possible constructors. For instance:
Theorem ev_minus2 :
∀n,
ev n → ev (
pred (
pred n)).
Proof.
intros n E.
inversion E as [|
n' E'].
-
simpl.
apply ev_0.
-
simpl.
apply E'.
Qed.
Note that, in this particular case, it is also possible to replace
inversion by destruct:
Theorem ev_minus2' :
∀n,
ev n → ev (
pred (
pred n)).
Proof.
intros n E.
destruct E as [|
n' E'].
-
simpl.
apply ev_0.
-
simpl.
apply E'.
Qed.
The difference between the two forms is that inversion is more
convenient when used on a hypothesis that consists of an inductive
property applied to a complex expression (as opposed to a single
variable). Here's is a concrete example. Suppose that we wanted
to prove the following variation of ev_minus2:
Intuitively, we know that evidence for the hypothesis cannot
consist just of the ev_0 constructor, since O and S are
different constructors of the type nat; hence, ev_SS is the
only case that applies. Unfortunately, destruct is not smart
enough to realize this, and it still generates two subgoals. Even
worse, in doing so, it keeps the final goal unchanged, failing to
provide any useful information for completing the proof.
Proof.
intros n E.
destruct E as [| n' E'].
-
Abort.
What happened, exactly? Calling
destruct has the effect of
replacing all occurrences of the property argument by the values
that correspond to each constructor. This is enough in the case
of
ev_minus2' because that argument,
n, is mentioned directly
in the final goal. However, it doesn't help in the case of
evSS_ev since the term that gets replaced (
S (S n)) is not
mentioned anywhere.
The
inversion tactic, on the other hand, can detect (1) that the
first case does not apply, and (2) that the
n' that appears on
the
ev_SS case must be the same as
n. This allows us to
complete the proof:
Theorem evSS_ev :
∀n,
ev (
S (
S n))
→ ev n.
Proof.
intros n E.
inversion E as [|
n' E'].
apply E'.
Qed.
By using inversion, we can also apply the principle of explosion
to "obviously contradictory" hypotheses involving inductive
properties. For example:
Exercise: 1 star (inversion_practice)
Prove the following results using
inversion.
☐
The way we've used
inversion here 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.
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. For those,
inversion
adds all equations into the proof context that must hold of the
arguments given to
P (e.g.,
S (S n') = n in the proof of
evSS_ev).
Induction on Evidence
The
ev_double exercise above shows that our new notion of
evenness is implied by the two earlier ones (since, by
even_bool_prop, we already know that those are equivalent to
each other). To show that all three coincide, we just need the
following lemma:
We could try to proceed by case analysis or induction on n. But
since ev is mentioned in a premise, this strategy would probably
lead to a dead end, as in the previous section. Thus, it seems
better to first try inversion on the evidence for ev. Indeed,
the first case can be solved trivially.
intros n E. inversion E as [| n' E'].
-
∃0. reflexivity.
- simpl.
Unfortunately, the second case is harder. We need to show
∃
k, S (S n') = double k, but the only available assumption is
E', which states that
ev n' holds. Since this isn't directly
useful, it seems that we are stuck and that performing case
analysis on
E was a waste of time.
If we look more closely at our second goal, however, we can see
that something interesting happened: By performing case analysis
on
E, we were able to reduce the original result to an similar
one that involves a
different piece of evidence for
ev:
E'.
More formally, we can finish our proof by showing that
which is the same as the original statement, but with
n' instead
of
n. Indeed, it is not difficult to convince Coq that this
intermediate result suffices.
assert (
I : (
∃k',
n' =
double k')
→
(
∃k,
S (
S n') =
double k)).
{
intros [
k' Hk'].
rewrite Hk'.
∃(
S k').
reflexivity. }
apply I.
If this looks familiar, it is no coincidence: We've encountered
similar problems in the
Induction chapter, when trying to use
case analysis to prove results that required induction. And once
again the solution is... induction!
The behavior of
induction on evidence is the same as its
behavior on data: It causes Coq to generate one subgoal for each
constructor that could have used to build that evidence, while
providing an induction hypotheses for each recursive occurrence of
the property in question.
Let's try our current lemma again:
Abort.
Lemma ev_even :
∀n,
ev n → ∃k,
n =
double k.
Proof.
intros n E.
induction E as [|
n' E' IH].
-
∃0.
reflexivity.
-
destruct IH as [
k' Hk'].
rewrite Hk'.
∃(
S k').
reflexivity.
Qed.
Here, we can see that Coq produced an
IH that corresponds to
E', the single recursive occurrence of
ev in its own
definition. Since
E' mentions
n', the induction hypothesis
talks about
n', as opposed to
n or some other number.
The equivalence between the second and third definitions of
evenness now follows.
As we will see in later chapters, induction on evidence is a
recurring technique when studying the semantics of programming
languages, where many properties of interest are defined
inductively. The following exercises provide simple examples of
this technique, to help you familiarize yourself with it.
Exercise: 2 stars (ev_sum)
☐
Exercise: 4 stars, advanced (ev_alternate)
In general, there may be multiple ways of defining a
property inductively. For example, here's a (slightly contrived)
alternative definition for
ev:
Prove that this definition is logically equivalent to
the old one.
☐
Exercise: 3 stars, advanced, recommended (ev_ev__ev)
Finding the appropriate thing to do induction on is a
bit tricky here:
☐
Exercise: 3 stars, optional (ev_plus_plus)
This exercise just requires applying existing lemmas. No
induction or even case analysis is needed, though some of the
rewriting may be tedious.
☐
Inductive Relations
A proposition parameterized by a number (such as
ev)
can be thought of as a
property — i.e., it defines
a subset of
nat, namely those numbers for which the proposition
is provable. In the same way, a two-argument proposition can be
thought of as a
relation — i.e., it defines a set of pairs for
which the proposition is provable.
One useful example is the "less than or equal to"
relation on numbers.
The following definition should be fairly intuitive. It
says that there are two ways to give evidence that one number is
less than or equal to another: either observe that they are the
same number, or give evidence that the first is less than or equal
to the predecessor of the second.
Proofs of facts about
≤ using the constructors
le_n and
le_S follow the same patterns as proofs about properties, like
ev above. We can
apply the constructors to prove
≤
goals (e.g., to show that
3≤3 or
3≤6), and we can use
tactics like
inversion to extract information from
≤
hypotheses in the context (e.g., to prove that
(2 ≤ 1) →
2+2=5.)
Here are some sanity checks on the definition. (Notice that,
although these are the same kind of simple "unit tests" as we gave
for the testing functions we wrote in the first few lectures, we
must construct their proofs explicitly —
simpl and
reflexivity don't do the job, because the proofs aren't just a
matter of simplifying computations.)
Theorem test_le1 :
3 ≤ 3.
Proof.
apply le_n.
Qed.
Theorem test_le2 :
3 ≤ 6.
Proof.
apply le_S.
apply le_S.
apply le_S.
apply le_n.
Qed.
Theorem test_le3 :
(2 ≤ 1)
→ 2 + 2 = 5.
Proof.
intros H.
inversion H.
inversion H2.
Qed.
The "strictly less than" relation n < m can now be defined
in terms of le.
Here are a few more simple relations on numbers:
Exercise: 2 stars, recommended (total_relation)
Define an inductive binary relation
total_relation that holds
between every pair of natural numbers.
☐
Exercise: 2 stars (empty_relation)
Define an inductive binary relation
empty_relation (on numbers)
that never holds.
☐
Exercise: 3 stars, optional (le_exercises)
Here are a number of facts about the
≤ and
< relations that
we are going to need later in the course. The proofs make good
practice exercises.
Hint: The next one may be easiest to prove by induction on m.
Hint: This theorem can easily be proved without using induction.
Exercise: 2 stars, optional (leb_iff)
☐
Exercise: 3 stars, recommended (R_provability2)
We can define three-place relations, four-place relations,
etc., in just the same way as binary relations. For example,
consider the following three-place relation on numbers:
- Which of the following propositions are provable?
- If we dropped constructor c5 from the definition of R,
would the set of provable propositions change? Briefly (1
sentence) explain your answer.
- If we dropped constructor c4 from the definition of R,
would the set of provable propositions change? Briefly (1
sentence) explain your answer.
☐
Exercise: 3 stars, optional (R_fact)
The relation
R above actually encodes a familiar function.
Figure out which function; then state and prove this equivalence
in Coq?
☐
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,
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;2]
[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 subseq_refl that subsequence is reflexive, that is,
any list is a subsequence of itself.
- Prove subseq_app 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 subseq_trans 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!
☐
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?
- R 2 [1;0]
- R 1 [1;2;1;0]
- R 6 [3;2;1;0]
☐
Case Study: Regular Expressions
The
ev property provides a simple example for illustrating
inductive definitions and the basic techniques for reasoning about
them, but it is not terribly exciting — after all, it is
equivalent to the two non-inductive of evenness that we had
already seen, and does not seem to offer any concrete benefit over
them. To give a better sense of the power of inductive
definitions, we now show how to use them to model a classic
concept in computer science:
regular expressions.
Regular expressions are a simple language for describing strings,
defined as elements of the following inductive type. (The names
of the constructors should become clear once we explain their
meaning below.)
Note that this definition is
polymorphic: Regular expressions in
reg_exp T describe strings with characters drawn from
T —
that is, lists of elements of
T. (We depart slightly from
standard practice in that we do not require the type
T to be
finite. This results in a somewhat different theory of regular
expressions, but the difference is not significant for our
purposes.)
We connect regular expressions and strings via the following
rules, which define when a regular expression
matches some
string:
- The expression EmptySet does not match any string.
- The expression EmptyStr matches the empty string [].
- The expression Char x matches the one-character string [x].
- If re1 matches s1, and re2 matches s2, then App re1
re2 matches s1 ++ s2.
- If at least one of re1 and re2 matches s, then Union re1
re2 matches s.
- Finally, if we can write some string s as the concatenation of
a sequence of strings s = s_1 ++ ... ++ s_k, and the
expression re matches each one of the strings s_i, then
Star re matches s. (As a special case, the sequence of
strings may be empty, so Star re always matches the empty
string [] no matter what re is.)
We can easily translate this informal definition into an
Inductive one as follows:
Once again, for readability, we can also display this definition
using inference-rule notation. At the same time, let's introduce
a more readable infix notation.
Notation "s =~ re" := (
exp_match s re) (
at level 80).
s1 =~ re1 s2 =~ re2 |
(MApp)
|
|
s1 ++ s2 =~ App re1 re2 |
|
s1 =~ re1 |
(MUnionL)
|
|
s1 =~ Union re1 re2 |
|
s2 =~ re2 |
(MUnionR)
|
|
s2 =~ Union re1 re2 |
|
s1 =~ re s2 =~ Star re |
(MStarApp)
|
|
s1 ++ s2 =~ Star re |
|
Notice that these rules are not
quite the same as the informal
ones that we gave at the beginning of the section. First, we
don't need to include a rule explicitly stating that no string
matches
EmptySet; we just don't happen to include any rule that
would have the effect of some string matching
EmptySet. (Indeed, the syntax of inductive definitions doesn't
even
allow us to give such a "negative rule.")
Furthermore, the informal rules for
Union and
Star correspond
to two constructors each:
MUnionL /
MUnionR, and
MStar0 /
MStarApp. The result is logically equivalent to the original
rules, but more convenient to use in Coq, since the recursive
occurrences of
exp_match are given as direct arguments to the
constructors, making it easier to perform induction on evidence.
(The
exp_match_ex1 and
exp_match_ex2 exercises below ask you
to prove that the constructors given in the inductive declaration
and the ones that would arise from a more literal transcription of
the informal rules are indeed equivalent.)
Let's illustrate these rules with a few examples.
(Notice how the last example applies
MApp to the strings
[1]
and
[2] directly. Since the goal mentions
[1; 2] instead of
[1] ++ [2], Coq wouldn't be able to figure out how to split the
string on its own.)
Using
inversion, we can also show that certain strings do
not
match a regular expression:
Example reg_exp_ex3 : ¬ ([1; 2] =~
Char 1).
Proof.
intros H.
inversion H.
Qed.
We can define helper functions to help write down regular
expressions. The reg_exp_of_list function constructs a regular
expression that matches exactly the list that it receives as an
argument:
We can also prove general facts about exp_match. For instance,
the following lemma shows that every string s that matches re
also matches Star re.
(Note the use of
app_nil_r to change the goal of the theorem to
exactly the same shape expected by
MStarApp.)
Exercise: 3 stars (exp_match_ex1)
The following lemmas show that the informal matching rules given
at the beginning of the chapter can be obtained from the formal
inductive definition.
The next lemma is stated in terms of the
fold function from the
Poly chapter: If
ss : list (list T) represents a sequence of
strings
s1, ..., sn, then
fold app ss [] is the result of
concatenating them all together.
☐
Exercise: 4 stars (reg_exp_of_list)
Prove that
reg_exp_of_list satisfies the following
specification:
☐
Since the definition of
exp_match has a recursive
structure, we might expect that proofs involving regular
expressions will often require induction on evidence. For
example, suppose that we wanted to prove the following intuitive
result: If a regular expression
re matches some string
s, then
all elements of
s must occur somewhere in
re. To state this
theorem, we first define a function
re_chars that lists all
characters that occur in a regular expression:
We can then phrase our theorem as follows:
Theorem in_re_match :
∀T (
s :
list T) (
re :
reg_exp T) (
x :
T),
s =~
re →
In x s →
In x (
re_chars re).
Proof.
intros T s re x Hmatch Hin.
induction Hmatch
as [
|
x'
|
s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2
|
s1 re1 re2 Hmatch IH|
re1 s2 re2 Hmatch IH
|
re|
s1 s2 re Hmatch1 IH1 Hmatch2 IH2].
-
apply Hin.
-
apply Hin.
-
simpl.
rewrite in_app_iff in *.
destruct Hin as [
Hin |
Hin].
+
left.
apply (
IH1 Hin).
+
right.
apply (
IH2 Hin).
-
simpl.
rewrite in_app_iff.
left.
apply (
IH Hin).
-
simpl.
rewrite in_app_iff.
right.
apply (
IH Hin).
-
destruct Hin.
Something interesting happens in the MStarApp case. We obtain
two induction hypotheses: One that applies when x occurs in
s1 (which matches re), and a second one that applies when x
occurs in s2 (which matches Star re). This is a good
illustration of why we need induction on evidence for exp_match,
as opposed to re: The latter would only provide an induction
hypothesis for strings that match re, which would not allow us
to reason about the case In x s2.
-
simpl.
rewrite in_app_iff in Hin.
destruct Hin as [
Hin |
Hin].
+
apply (
IH1 Hin).
+
apply (
IH2 Hin).
Qed.
Exercise: 4 stars (re_not_empty)
Write a recursive function
re_not_empty that tests whether a
regular expression matches some string. Prove that your function
is correct.
☐
The remember Tactic
One potentially confusing feature of the
induction tactic is
that it happily lets you try to set up an induction over a term
that isn't sufficiently general. The net effect of this will be
to lose information (much as
destruct can do), and leave you
unable to complete the proof. Here's an example:
Just doing an inversion on H1 won't get us very far in the
recursive cases. (Try it!). So we need induction. Here is a naive
first attempt:
induction H1
as [|x'|s1 re1 s2' re2 Hmatch1 IH1 Hmatch2 IH2
|s1 re1 re2 Hmatch IH|re1 s2' re2 Hmatch IH
|re''|s1 s2' re'' Hmatch1 IH1 Hmatch2 IH2].
But now, although we get seven cases (as we would expect from the
definition of exp_match), we lost a very important bit of
information from H1: the fact that s1 matched something of the
form Star re. This means that we have to give proofs for all
seven constructors of this definition, even though all but two of
them (MStar0 and MStarApp) are contradictory. We can still
get the proof to go through for a few constructors, such as
MEmpty...
-
simpl. intros H. apply H.
... but most of them get stuck. For
MChar, for instance, we
must show that
s2 =~
Char x' → x' ::
s2 =~
Char x',
which is clearly impossible.
-
Abort.
The problem is that
induction over a Prop hypothesis only works
properly with hypotheses that are completely general, i.e., ones
in which all the arguments are variables, as opposed to more
complex expressions, such as
Star re. In this respect it
behaves more like
destruct than like
inversion.
We can solve this problem by generalizing over the problematic
expressions with an explicit equality:
We can now proceed by performing induction over evidence directly,
because the argument to the first hypothesis is sufficiently
general, which means that we can discharge most cases by inverting
the
re' = Star re equality in the context.
This idiom is so common that Coq provides a tactic to
automatically generate such equations for us, avoiding thus the
need for changing the statements of our theorems. Calling
remember e as x causes Coq to (1) replace all occurrences of the
expression
e by the variable
x, and (2) add an equation
x =
e to the context. Here's how we can use it to show the above
result:
We now have Heqre' : re' = Star re.
generalize dependent s2.
induction H1
as [|x'|s1 re1 s2' re2 Hmatch1 IH1 Hmatch2 IH2
|s1 re1 re2 Hmatch IH|re1 s2' re2 Hmatch IH
|re''|s1 s2' re'' Hmatch1 IH1 Hmatch2 IH2].
The Heqre' is contradictory in most cases, which allows us to
conclude immediately.
- inversion Heqre'.
- inversion Heqre'.
- inversion Heqre'.
- inversion Heqre'.
- inversion Heqre'.
In the interesting cases (those that correspond to Star), we can
proceed as usual. Note that the induction hypothesis IH2 on the
MStarApp case mentions an additional premise Star re'' = Star
re', which results from the equality generated by remember.
-
inversion Heqre'.
intros s H.
apply H.
-
inversion Heqre'.
rewrite H0 in IH2,
Hmatch1.
intros s2 H1.
rewrite ← app_assoc.
apply MStarApp.
+
apply Hmatch1.
+
apply IH2.
*
reflexivity.
*
apply H1.
Qed.
Exercise: 4 stars (exp_match_ex2)
The
MStar'' lemma below (combined with its converse, the
MStar' exercise above), shows that our definition of
exp_match
for
Star is equivalent to the informal one given previously.
☐
Exercise: 5 stars, advanced (pumping)
One of the first interesting theorems in the theory of regular
expressions is the so-called
pumping lemma, which states,
informally, that any sufficiently long string
s matching a
regular expression
re can be "pumped" by repeating some middle
section of
s an arbitrary number of times to produce a new
string also matching
re.
To begin, we need to define "sufficiently long." Since we are
working in a constructive logic, we actually need to be able to
calculate, for each regular expression
re, the minimum length
for strings
s to guarantee "pumpability."
Next, it is useful to define an auxiliary function that repeats a
string (appends it to itself) some number of times.
Now, the pumping lemma itself says that, if s =~ re and if the
length of s is at least the pumping constant of re, then s
can be split into three substrings s1 ++ s2 ++ s3 in such a way
that s2 can be repeated any number of times and the result, when
combined with s1 and s3 will still match re. Since s2 is
also guaranteed not to be the empty string, this gives us
a (constructive!) way to generate strings matching re that are
as long as we like.
To streamline the proof (which you are to fill in), the omega
tactic, which is enabled by the following Require, is helpful in
several places for automatically completing tedious low-level
arguments involving equalities or inequalities over natural
numbers. We'll return to omega in a later chapter, but feel
free to experiment with it now if you like. The first case of the
induction gives an example of how it is used.
Require Import Coq.omega.Omega.
Proof.
intros T re s Hmatch.
induction Hmatch
as [ |
x |
s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2
|
s1 re1 re2 Hmatch IH |
re1 s2 re2 Hmatch IH
|
re |
s1 s2 re Hmatch1 IH1 Hmatch2 IH2 ].
-
simpl.
omega.
Admitted.
End Pumping.
☐
Improving Reflection
We've seen in the
Logic chapter that we often need to
relate boolean computations to statements in
Prop.
Unfortunately, performing this conversion by hand can result in
tedious proof scripts. Consider the proof of the following
theorem:
Theorem filter_not_empty_In :
∀n l,
filter (
beq_nat n)
l ≠ []
→
In n l.
Proof.
intros n l.
induction l as [|
m l' IHl'].
-
simpl.
intros H.
apply H.
reflexivity.
-
simpl.
destruct (
beq_nat n m)
eqn:
H.
+
intros _.
rewrite beq_nat_true_iff in H.
rewrite H.
left.
reflexivity.
+
intros H'.
right.
apply IHl'.
apply H'.
Qed.
In the first branch after
destruct, we explicitly
apply the
beq_nat_true_iff lemma to the equation generated by
destructing
beq_nat n m, to convert the assumption
beq_nat n m
= true into the assumption
n = m, which is what we need to
complete this case.
We can streamline this proof by defining an inductive proposition
that yields a better case-analysis principle for
beq_nat n
m. Instead of generating an equation such as
beq_nat n m =
true, which is not directly useful, this principle gives us right
away the assumption we need:
n = m. We'll actually define
something a bit more general, which can be used with arbitrary
properties (and not just equalities):
The
reflect property takes two arguments: a proposition
P and a boolean
b. Intuitively, it states that the property
P is
reflected in (i.e., equivalent to) the boolean
b:
P
holds if and only if
b = true. To see this, notice that, by
definition, the only way we can produce evidence that
reflect P
true holds is by showing that
P is true and using the
ReflectT constructor. If we invert this statement, this means
that it should be possible to extract evidence for
P from a
proof of
reflect P true. Conversely, the only way to show
reflect P false is by combining evidence for
¬ P with the
ReflectF constructor.
It is easy to formalize this intuition and show that the two
statements are indeed equivalent:
Exercise: 2 stars, recommended (reflect_iff)
☐
The advantage of
reflect over the normal "if and only if"
connective is that, by destructing a hypothesis or lemma of the
form
reflect P b, we can perform case analysis on
b while at
the same time generating appropriate hypothesis in the two
branches (
P in the first subgoal and
¬ P in the second).
To use
reflect to produce a better proof of
filter_not_empty_In, we begin by recasting the
beq_nat_iff_true lemma into a more convenient form in terms of
reflect:
The new proof of filter_not_empty_In now goes as follows.
Notice how the calls to destruct and apply are combined into a
single call to destruct. (To see this clearly, look at the two
proofs of filter_not_empty_In in your Coq browser and observe
the differences in proof state at the beginning of the first case
of the destruct.)
Theorem filter_not_empty_In' :
∀n l,
filter (
beq_nat n)
l ≠ []
→
In n l.
Proof.
intros n l.
induction l as [|
m l' IHl'].
-
simpl.
intros H.
apply H.
reflexivity.
-
simpl.
destruct (
beq_natP n m)
as [
H |
H].
+
intros _.
rewrite H.
left.
reflexivity.
+
intros H'.
right.
apply IHl'.
apply H'.
Qed.
Although this technique arguably gives us only a small gain
in convenience for this particular proof, using
reflect
consistently often leads to shorter and clearer proofs. We'll see
many more examples where
reflect comes in handy in later
chapters.
The use of the
reflect property was popularized by
SSReflect,
a Coq library that has been used to formalize important results in
mathematics, including as the 4-color theorem and the
Feit-Thompson theorem. The name SSReflect stands for
small-scale
reflection, i.e., the pervasive use of reflection to simplify
small proof steps with boolean computations.
Additional Exercises
Exercise: 4 stars, recommended (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 l
may seem obvious, but will not work very well.)
- Prove (pal_app_rev) that
- Prove (pal_rev that)
☐
Exercise: 5 stars, optional (palindrome_converse)
Again, the converse direction is significantly more difficult, due
to the lack of evidence. Using your definition of
pal from the
previous exercise, prove that
☐
Exercise: 4 stars, advanced (filter_challenge)
Let's prove that our definition of
filter from the
Poly
chapter matches an abstract specification. Here is the
specification, written out informally in English:
A list
l is an "in-order merge" of
l1 and
l2 if it contains
all the same elements as
l1 and
l2, in the same order as
l1
and
l2, but possibly interleaved. For example,
is an in-order merge of
and
Now, suppose we have a set
X, a function
test: X→bool, and a
list
l of type
list X. Suppose further that
l is an
in-order merge of two lists,
l1 and
l2, such that every item
in
l1 satisfies
test and no item in
l2 satisfies test. Then
filter test l = l1.
Translate this specification into a Coq theorem and prove
it. (You'll need to begin by defining what it means for one list
to be a merge of two others. Do this with an inductive relation,
not a
Fixpoint.)
☐
Exercise: 5 stars, advanced, optional (filter_challenge_2)
A different way to characterize the behavior of
filter goes like
this: Among all subsequences of
l with the property that
test
evaluates to
true on all their members,
filter test l is the
longest. Formalize this claim and prove it.
☐
Exercise: 4 stars, advanced (NoDup)
Recall the definition of the
In property from the
Logic
chapter, which asserts that a value
x appears at least once in a
list
l:
Your first task is to use In to define a proposition disjoint X
l1 l2, which should be provable exactly when l1 and l2 are
lists (with elements of type X) that have no elements in
common.
Next, use In to define an inductive proposition NoDup X
l, which should be provable exactly when l is a list (with
elements of type X) where every member is different from every
other. For example, NoDup nat [1;2;3;4] and NoDup
bool [] should be provable, while NoDup nat [1;2;1] and
NoDup bool [true;true] should not be.
Finally, state and prove one or more interesting theorems relating
disjoint, NoDup and ++ (list append).
☐
Exercise: 3 stars, recommended (nostutter)
Formulating inductive definitions of properties is an important
skill you'll need in this course. Try to solve this exercise
without any help at all.
We say that a list "stutters" if it repeats the same element
consecutively. The property "
nostutter mylist" means that
mylist does not stutter. Formulate an inductive definition for
nostutter. (This is different from the
NoDup property in the
exercise above; the sequence
1;4;1 repeats but does not
stutter.)
Make sure each of these tests succeeds, but feel free to change
the suggested proof (in comments) if the given one doesn't work
for you. Your definition might be different from ours and still
be correct, in which case the examples might need a different
proof. (You'll notice that the suggested proofs use a number of
tactics we haven't talked about, to make them more robust to
different possible ways of defining nostutter. You can probably
just uncomment and use them as-is, but you can also prove each
example with more basic tactics.)
☐
Exercise: 4 stars, advanced (pigeonhole principle)
The
pigeonhole principle states a basic fact about counting: if
we distribute more than
n items into
n pigeonholes, some
pigeonhole must contain at least two items. As often happens, this
apparently trivial fact about numbers requires non-trivial
machinery to prove, but we now have enough...
First prove an easy useful lemma.
Now define a property repeats such that repeats X l asserts
that l contains at least one repeated element (of type X).
Now, here's a way to formalize the pigeonhole principle. Suppose
list
l2 represents a list of pigeonhole labels, and list
l1
represents the labels assigned to a list of items. If there are
more items than labels, at least two items must have the same
label — i.e., list
l1 must contain repeats.
This proof is much easier if you use the
excluded_middle
hypothesis to show that
In is decidable, i.e.,
∀ x l, (In x
l) ∨ ¬ (In x l). However, it is also possible to make the proof
go through
without assuming that
In is decidable; if you
manage to do this, you will not need the
excluded_middle
hypothesis.