IndProp: Inductively Defined Propositions
Set Warnings "notationoverridden,parsing".
From LF Require Export Logic.
Require Coq.omega.Omega.
Inductively Defined Propositions
(ev_0) even 0
(ev_SS) even (S (S n))
(ev_0) even 0
(ev_SS) even 2
(ev_SS) even 4
Inductive Definition of Evenness
This definition is different in one crucial respect from previous
uses of Inductive: the thing we are defining is not a Type,
but rather a function from nat to Prop  that is, a property
of numbers. We've already seen other inductive definitions that
result in functions  for example, list, whose type is Type >
Type. What is really new here is that, because the nat
argument of even appears 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 even, we would have seen an
error:
Fail Inductive wrong_ev (n : nat) : Prop :=
 wrong_ev_0 : wrong_ev 0
 wrong_ev_SS : wrong_ev n > wrong_ev (S (S n)).
In an Inductive definition, an argument to the type
constructor on the left of the colon is called a "parameter",
whereas an argument on the right is called an "index".
For example, in Inductive list (X : Type) := ..., X is a
parameter; in Inductive even : nat > Prop := ..., the
unnamed nat argument is an index.
We can think of the definition of even as defining a Coq
property even : nat > Prop, together with primitive theorems
ev_0 : even 0 and ev_SS : forall n, even n > even (S (S n)).
That definition can also be written as follows...
Inductive even : nat > Prop :=
 ev_0 : even 0
 ev_SS : forall n, even n > even (S (S n)).
... making explicit the type of the rule ev_SS.
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 even for particular numbers...
... or we can use function application syntax:
We can also prove theorems that have hypotheses involving even.
Theorem ev_plus4 : forall n, even n > even (4 + n).
Proof.
intros n. simpl. intros Hn.
apply ev_SS. apply ev_SS. apply Hn.
Qed.
☐
Using Evidence in Proofs
Inversion on Evidence
Theorem ev_inversion :
forall (n : nat), even n >
(n = 0) \/ (exists n', n = S (S n') /\ even n').
Proof.
intros n E.
destruct E as [  n' E'].

left. reflexivity.

right. exists n'. split. reflexivity. apply E'.
Qed.
The following theorem can easily be proved using destruct on
evidence.
Theorem ev_minus2 : forall n,
even n > even (pred (pred n)).
Proof.
intros n E.
destruct E as [ n' E'].
 simpl. apply ev_0.
 simpl. apply E'.
Qed.
However, this variation cannot easily be handled with destruct.
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.
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.
We could patch this proof by replacing the goal even n,
which does not mention the replaced term S (S n), by the
equivalent goal even (pred (pred (S (S n)))), which does mention
this term, after which destruct can make progress. But it is
more straightforward to use our inversion lemma.
Theorem evSS_ev : forall n, even (S (S n)) > even n.
Proof. intros n H. apply ev_inversion in H. destruct H.
 discriminate H.
 destruct H as [n' [Hnm Hev]]. injection Hnm.
intro Heq. rewrite Heq. apply Hev.
Qed.
Coq provides a tactic called inversion, which does the work of
our inversion lemma and more besides.
The inversion tactic can detect (1) that the first case
(n = 0) does not apply and (2) that the n' that appears in the
ev_SS case must be the same as n. It has an "as" variant
similar to destruct, allowing us to assign names rather than
have Coq choose them.
Theorem evSS_ev' : forall n,
even (S (S n)) > even n.
Proof.
intros n E.
inversion E as [ n' E'].
apply E'.
Qed.
The inversion tactic can apply the principle of explosion to
"obviously contradictory" hypotheses involving inductive
properties, something that takes a bit more work using our
inversion lemma. For example:
Theorem one_not_even : ~ even 1.
Proof.
intros H. apply ev_inversion in H.
destruct H as [  [m [Hm _]]].
 discriminate H.
 discriminate Hm.
Qed.
Theorem one_not_even' : ~ even 1.
intros H. inversion H. Qed.
Proof.
intros H. apply ev_inversion in H.
destruct H as [  [m [Hm _]]].
 discriminate H.
 discriminate Hm.
Qed.
Theorem one_not_even' : ~ even 1.
intros H. inversion H. Qed.
Exercise: 1 star, standard (inversion_practice)
☐
The inversion tactic does quite a bit of work. When
applied to equalities, as a special case, it does the work of both
discriminate and injection. In addition, it carries out the
intros and rewrites that are typically necessary in the case
of injection. It can also be applied, more generally, to analyze
evidence for inductively defined propositions. As examples, we'll
use it to reprove some theorems from Tactics.v.
Theorem inversion_ex1 : forall (n m o : nat),
[n; m] = [o; o] >
[n] = [m].
Proof.
intros n m o H. inversion H. reflexivity. Qed.
Theorem inversion_ex2 : forall (n : nat),
S n = O >
2 + 2 = 5.
Proof.
intros n contra. inversion contra. Qed.
Here's how inversion works in general. Suppose the name
H 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 H generates a subgoal in which
H 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 selfcontradictory; 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).
The ev_double exercise above shows that our new notion of
evenness is implied by the two earlier ones (since, by
even_bool_prop in chapter Logic, 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 even 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 even.
Indeed, the first case can be solved trivially.
intros n E. inversion E as [ n' E'].

exists 0. reflexivity.
 simpl.
Unfortunately, the second case is harder. We need to show exists
k, S (S n') = double k, but the only available assumption is
E', which states that even 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 a similar
one that involves a different piece of evidence for even:
namely E'. More formally, we can finish our proof by showing
that
exists k', n' = double k',
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 : (exists k', n' = double k') >
(exists k, S (S n') = double k)).
{ intros [k' Hk']. rewrite Hk'. exists (S k'). reflexivity. }
apply I.
Abort.
Induction on Evidence
Lemma ev_even : forall n,
even n > exists k, n = double k.
Proof.
intros n E.
induction E as [n' E' IH].

exists 0. reflexivity.

destruct IH as [k' Hk'].
rewrite Hk'. exists (S k'). reflexivity.
Qed.
Here, we can see that Coq produced an IH that corresponds
to E', the single recursive occurrence of even 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.
Theorem ev_even_iff : forall n,
even n <> exists k, n = double k.
Proof.
intros n. split.
 apply ev_even.
 intros [k Hk]. rewrite Hk. apply ev_double.
Qed.
As we will see in later chapters, induction on evidence is a
recurring technique across many areas, and in particular when
formalizing 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, standard (ev_sum)
☐
In general, there may be multiple ways of defining a
property inductively. For example, here's a (slightly contrived)
alternative definition for even:
Exercise: 4 stars, advanced, optional (even'_ev)
Inductive even' : nat > Prop :=
 even'_0 : even' 0
 even'_2 : even' 2
 even'_sum n m (Hn : even' n) (Hm : even' m) : even' (n + m).
Prove that this definition is logically equivalent to the old
one. (You may want to look at the previous theorem when you get
to the induction step.)
☐
Finding the appropriate thing to do induction on is a
bit tricky here:
Exercise: 3 stars, advanced, recommended (ev_ev__ev)
☐
This exercise just requires applying existing lemmas. No
induction or even case analysis is needed, though some of the
rewriting may be tedious.
Exercise: 3 stars, standard, optional (ev_plus_plus)
☐
Inductive Relations
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.
Inductive le : nat > nat > Prop :=
 le_n n : le n n
 le_S n m (H : le n m) : le n (S m).
Notation "m <= n" := (le m n).
Proofs of facts about <= using the constructors le_n and
le_S follow the same patterns as proofs about properties, like
even 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.
Here are a few more simple relations on numbers:
Inductive square_of : nat > nat > Prop :=
 sq n : square_of n (n * n).
Inductive next_nat : nat > nat > Prop :=
 nn n : next_nat n (S n).
Inductive next_even : nat > nat > Prop :=
 ne_1 n : even (S n) > next_even n (S n)
 ne_2 n (H : even (S (S n))) : next_even n (S (S n)).
Exercise: 2 stars, standard, optional (total_relation)
Exercise: 2 stars, standard, optional (empty_relation)
From the definition of le, we can sketch the behaviors of
destruct, inversion, and induction on a hypothesis H
providing evidence of the form le e1 e2. Doing destruct H
will generate two cases. In the first case, e1 = e2, and it
will replace instances of e2 with e1 in the goal and context.
In the second case, e2 = S n' for some n' for which le e1 n'
holds, and it will replace instances of e2 with S n'.
Doing inversion H will remove impossible cases and add generated
equalities to the context for further use. Doing induction H
will, in the second case, add the induction hypothesis that the
goal holds when e2 is replaced with n'.
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.
Exercise: 3 stars, standard, optional (le_exercises)
Lemma le_trans : forall m n o, m <= n > n <= o > m <= o.
Proof.
Admitted.
Theorem O_le_n : forall n,
0 <= n.
Proof.
Admitted.
Theorem n_le_m__Sn_le_Sm : forall n m,
n <= m > S n <= S m.
Proof.
Admitted.
Theorem Sn_le_Sm__n_le_m : forall n m,
S n <= S m > n <= m.
Proof.
Admitted.
Theorem le_plus_l : forall a b,
a <= a + b.
Proof.
Admitted.
Theorem plus_lt : forall n1 n2 m,
n1 + n2 < m >
n1 < m /\ n2 < m.
Proof.
unfold lt.
Admitted.
Theorem lt_S : forall n m,
n < m >
n < S m.
Proof.
Admitted.
Theorem leb_complete : forall n m,
n <=? m = true > n <= m.
Proof.
Admitted.
Hint: The next one may be easiest to prove by induction on m.
Hint: This one can easily be proved without using induction.
Theorem leb_true_trans : forall n m o,
n <=? m = true > m <=? o = true > n <=? o = true.
Proof.
Admitted.
☐
Exercise: 3 stars, standard, recommended (R_provability)
Inductive R : nat > nat > nat > Prop :=
 c1 : R 0 0 0
 c2 m n o (H : R m n o) : R (S m) n (S o)
 c3 m n o (H : R m n o) : R m (S n) (S o)
 c4 m n o (H : R (S m) (S n) (S (S o))) : R m n o
 c5 m n o (H : R m n o) : R n m o.
 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.
☐
The relation R above actually encodes a familiar function.
Figure out which function; then state and prove this equivalence
in Coq?
Exercise: 3 stars, standard, optional (R_fact)
Definition fR : nat > nat > nat
. Admitted.
Theorem R_equiv_fR : forall m n o, R m n o <> fR m n = o.
Proof.
Admitted.
☐
Exercise: 2 stars, advanced (subsequence)
 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!
Inductive subseq : list nat > list nat > Prop :=
.
Theorem subseq_refl : forall (l : list nat), subseq l l.
Proof.
Admitted.
Theorem subseq_app : forall (l1 l2 l3 : list nat),
subseq l1 l2 >
subseq l1 (l2 ++ l3).
Proof.
Admitted.
Theorem subseq_trans : forall (l1 l2 l3 : list nat),
subseq l1 l2 >
subseq l2 l3 >
subseq l1 l3.
Proof.
Admitted.
☐
Suppose we give Coq the following definition:
Inductive R : nat > list nat > Prop :=
 c1 : R 0 ☐
 c2 : forall n l, R n l > R (S n) (n :: l)
 c3 : forall n l, R (S n) l > R n l.
Which of the following propositions are provable?
Exercise: 2 stars, standard, optional (R_provability2)
Case Study: Regular Expressions
Inductive reg_exp {T : Type} : Type :=
 EmptySet
 EmptyStr
 Char (t : T)
 App (r1 r2 : reg_exp)
 Union (r1 r2 : reg_exp)
 Star (r : reg_exp).
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:
We can easily translate this informal definition into an
Inductive one as follows:
 The expression EmptySet does not match any string.
 The expression EmptyStr matches the empty string [].
 The expression Char x matches the onecharacter 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.
Inductive exp_match {T} : list T > reg_exp > Prop :=
 MEmpty : exp_match [] EmptyStr
 MChar x : exp_match [x] (Char x)
 MApp s1 re1 s2 re2
(H1 : exp_match s1 re1)
(H2 : exp_match s2 re2) :
exp_match (s1 ++ s2) (App re1 re2)
 MUnionL s1 re1 re2
(H1 : exp_match s1 re1) :
exp_match s1 (Union re1 re2)
 MUnionR re1 s2 re2
(H2 : exp_match s2 re2) :
exp_match s2 (Union re1 re2)
 MStar0 re : exp_match [] (Star re)
 MStarApp s1 s2 re
(H1 : exp_match s1 re)
(H2 : exp_match s2 (Star re)) :
exp_match (s1 ++ s2) (Star re).
Again, for readability, we can also display this definition using
inferencerule notation. At the same time, let's introduce a more
readable infix notation.
(MEmpty) ☐ =~ EmptyStr
(MChar) x =~ Char x
(MApp) s1 ++ s2 =~ App re1 re2
(MUnionL) s1 =~ Union re1 re2
(MUnionR) s2 =~ Union re1 re2
(MStar0) ☐ =~ Star re
(MStarApp) s1 ++ s2 =~ Star re
Example reg_exp_ex1 : [1] =~ Char 1.
Proof.
apply MChar.
Qed.
Example reg_exp_ex2 : [1; 2] =~ App (Char 1) (Char 2).
Proof.
apply (MApp [1] _ [2]).
 apply MChar.
 apply MChar.
Qed.
(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:
We can define helper functions for writing down regular
expressions. The reg_exp_of_list function constructs a regular
expression that matches exactly the list that it receives as an
argument:
Fixpoint reg_exp_of_list {T} (l : list T) :=
match l with
 [] => EmptyStr
 x :: l' => App (Char x) (reg_exp_of_list l')
end.
Example reg_exp_ex4 : [1; 2; 3] =~ reg_exp_of_list [1; 2; 3].
Proof.
simpl. apply (MApp [1]).
{ apply MChar. }
apply (MApp [2]).
{ apply MChar. }
apply (MApp [3]).
{ apply MChar. }
apply MEmpty.
Qed.
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.
Lemma MStar1 :
forall T s (re : @reg_exp T) ,
s =~ re >
s =~ Star re.
Proof.
intros T s re H.
rewrite < (app_nil_r _ s).
apply (MStarApp s [] re).
 apply H.
 apply MStar0.
Qed.
(Note the use of app_nil_r to change the goal of the theorem to
exactly the same shape expected by MStarApp.)
The following lemmas show that the informal matching rules given
at the beginning of the chapter can be obtained from the formal
inductive definition.
Exercise: 3 stars, standard (exp_match_ex1)
Lemma empty_is_empty : forall T (s : list T),
~ (s =~ EmptySet).
Proof.
Admitted.
Lemma MUnion' : forall T (s : list T) (re1 re2 : @reg_exp T),
s =~ re1 \/ s =~ re2 >
s =~ Union re1 re2.
Proof.
Admitted.
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.
Lemma MStar' : forall T (ss : list (list T)) (re : reg_exp),
(forall s, In s ss > s =~ re) >
fold app ss [] =~ Star re.
Proof.
Admitted.
☐
Prove that reg_exp_of_list satisfies the following
specification:
Exercise: 4 stars, standard, optional (reg_exp_of_list_spec)
Lemma reg_exp_of_list_spec : forall T (s1 s2 : list T),
s1 =~ reg_exp_of_list s2 <> s1 = s2.
Proof.
Admitted.
☐
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 as character literals
somewhere in re.
To state this theorem, we first define a function re_chars that
lists all characters that occur in a regular expression:
Fixpoint re_chars {T} (re : reg_exp) : list T :=
match re with
 EmptySet => []
 EmptyStr => []
 Char x => [x]
 App re1 re2 => re_chars re1 ++ re_chars re2
 Union re1 re2 => re_chars re1 ++ re_chars re2
 Star re => re_chars re
end.
We can then phrase our theorem as follows:
Theorem in_re_match : forall T (s : list T) (re : reg_exp) (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,
rather than induction on the regular expression 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, standard (re_not_empty)
Fixpoint re_not_empty {T : Type} (re : @reg_exp T) : bool
. Admitted.
Lemma re_not_empty_correct : forall T (re : @reg_exp T),
(exists s, s =~ re) <> re_not_empty re = true.
Proof.
Admitted.
☐
The remember Tactic
Lemma star_app: forall T (s1 s2 : list T) (re : @reg_exp T),
s1 =~ Star re >
s2 =~ Star re >
s1 ++ s2 =~ Star re.
Proof.
intros T s1 s2 re H1.
Just doing an inversion on H1 won't get us very far in
the recursive cases. (Try it!). So we need induction (on
evidence!). Here is a naive first attempt:
induction H1
as [x's1 re1 s2' re2 Hmatch1 IH1 Hmatch2 IH2
s1 re1 re2 Hmatch IHre1 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 have 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 cases 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, induction on evidence behaves more like
destructwithouteqn: than like inversion.)
An awkward way to solve this problem is "manually generalizing"
over the problematic expressions by adding explicit equality
hypotheses to the lemma:
Lemma star_app: forall T (s1 s2 : list T) (re re' : reg_exp),
re' = Star re >
s1 =~ re' >
s2 =~ Star re >
s1 ++ s2 =~ Star re.
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.
Abort.
The tactic 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:
Lemma star_app: forall T (s1 s2 : list T) (re : reg_exp),
s1 =~ Star re >
s2 =~ Star re >
s1 ++ s2 =~ Star re.
Proof.
intros T s1 s2 re H1.
remember (Star re) as re'.
generalize dependent s2.
induction H1
as [x's1 re1 s2' re2 Hmatch1 IH1 Hmatch2 IH2
s1 re1 re2 Hmatch IHre1 s2' re2 Hmatch IH
re''s1 s2' re'' Hmatch1 IH1 Hmatch2 IH2].
The Heqre' is contradictory in most cases, allowing us to
conclude immediately.
 discriminate.
 discriminate.
 discriminate.
 discriminate.
 discriminate.
The interesting cases are those that correspond to Star. 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.

injection Heqre'. intros Heqre'' s H. apply H.

injection Heqre'. intros H0.
intros s2 H1. rewrite < app_assoc.
apply MStarApp.
+ apply Hmatch1.
+ apply IH2.
* rewrite H0. reflexivity.
* apply H1.
Qed.
Exercise: 4 stars, standard, optional (exp_match_ex2)
Lemma MStar'' : forall T (s : list T) (re : reg_exp),
s =~ Star re >
exists ss : list (list T),
s = fold app ss []
/\ forall s', In s' ss > s' =~ re.
Proof.
Admitted.
☐
One of the first really interesting theorems in the theory of
regular expressions is the socalled 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."
Exercise: 5 stars, advanced (pumping)
Module Pumping.
Fixpoint pumping_constant {T} (re : @reg_exp T) : nat :=
match re with
 EmptySet => 0
 EmptyStr => 1
 Char _ => 2
 App re1 re2 =>
pumping_constant re1 + pumping_constant re2
 Union re1 re2 =>
pumping_constant re1 + pumping_constant re2
 Star _ => 1
end.
Next, it is useful to define an auxiliary function that repeats a
string (appends it to itself) some number of times.
Fixpoint napp {T} (n : nat) (l : list T) : list T :=
match n with
 0 => []
 S n' => l ++ napp n' l
end.
Lemma napp_plus: forall T (n m : nat) (l : list T),
napp (n + m) l = napp n l ++ napp m l.
Proof.
intros T n m l.
induction n as [n IHn].
 reflexivity.
 simpl. rewrite IHn, app_assoc. reflexivity.
Qed.
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.
Lemma pumping : forall T (re : @reg_exp T) s,
s =~ re >
pumping_constant re <= length s >
exists s1 s2 s3,
s = s1 ++ s2 ++ s3 /\
s2 <> [] /\
forall m, s1 ++ napp m s2 ++ s3 =~ re.
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 lowlevel
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.
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.
☐
Case Study: Improving Reflection
Theorem filter_not_empty_In : forall n l,
filter (fun x => n =? x) l <> [] >
In n l.
Proof.
intros n l. induction l as [m l' IHl'].

simpl. intros H. apply H. reflexivity.

simpl. destruct (n =? m) eqn:H.
+
intros _. rewrite eqb_eq in H. rewrite H.
left. reflexivity.
+
intros H'. right. apply IHl'. apply H'.
Qed.
In the first branch after destruct, we explicitly apply
the eqb_eq lemma to the equation generated by
destructing n =? m, to convert the assumption n =? m
= true into the assumption n = m; then we had to rewrite
using this assumption to complete the case.
We can streamline this by defining an inductive proposition that
yields a better caseanalysis principle for n =? m.
Instead of generating an equation such as (n =? m) = true,
which is generally not directly useful, this principle gives us
right away the assumption we really need: n = m.
Inductive reflect (P : Prop) : bool > Prop :=
 ReflectT (H : P) : reflect P true
 ReflectF (H : ~ P) : reflect P false.
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: that
is, P holds if and only if b = true. To see this, notice
that, by definition, the only way we can produce evidence for
reflect P true is by showing P and then 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. Similarly, 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
statements P <> b = true and reflect P b are indeed
equivalent. First, the lefttoright implication:
Theorem iff_reflect : forall P b, (P <> b = true) > reflect P b.
Proof.
intros P b H. destruct b.
 apply ReflectT. rewrite H. reflexivity.
 apply ReflectF. rewrite H. intros H'. discriminate.
Qed.
☐
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).
Lemma eqbP : forall n m, reflect (n = m) (n =? m).
Proof.
intros n m. apply iff_reflect. rewrite eqb_eq. reflexivity.
Qed.
A smoother 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 with Coq and observe the differences in
proof state at the beginning of the first case of the
destruct.)
Theorem filter_not_empty_In' : forall n l,
filter (fun x => n =? x) l <> [] >
In n l.
Proof.
intros n l. induction l as [m l' IHl'].

simpl. intros H. apply H. reflexivity.

simpl. destruct (eqbP n m) as [H  H].
+
intros _. rewrite H. left. reflexivity.
+
intros H'. right. apply IHl'. apply H'.
Qed.
Fixpoint count n l :=
match l with
 [] => 0
 m :: l' => (if n =? m then 1 else 0) + count n l'
end.
Theorem eqbP_practice : forall n l,
count n l = 0 > ~(In n l).
Proof.
Admitted.
☐
This small example shows how reflection gives us a small gain in
convenience; in larger developments, using reflect consistently
can often lead to noticeably shorter and clearer proof scripts.
We'll see many more examples in later chapters and in Programming
Language Foundations.
The use of the reflect property has been popularized by
SSReflect, a Coq library that has been used to formalize
important results in mathematics, including as the 4color theorem
and the FeitThompson theorem. The name SSReflect stands for
smallscale reflection, i.e., the pervasive use of reflection to
simplify small proof steps with boolean computations.
Additional Exercises
Exercise: 3 stars, standard, recommended (nostutter_defn)
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 asis, but you can also prove each
example with more basic tactics.)
Example test_nostutter_1: nostutter [3;1;4;1;5;6].
Admitted.
Example test_nostutter_2: nostutter (@nil nat).
Admitted.
Example test_nostutter_3: nostutter [5].
Admitted.
Example test_nostutter_4: not (nostutter [3;1;1;4]).
Admitted.
Definition manual_grade_for_nostutter : option (nat*string) := None.
☐
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 "inorder 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,
1;4;6;2;3
is an inorder merge of
1;6;2
and
4;3.
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
inorder 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: 4 stars, advanced (filter_challenge)
☐
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: 5 stars, advanced, optional (filter_challenge_2)
Exercise: 4 stars, standard, optional (palindromes)
 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 like
 Prove (pal_app_rev) that
 Prove (pal_rev that)
☐
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
forall l, l = rev l > pal l.
Exercise: 5 stars, standard, optional (palindrome_converse)
Exercise: 4 stars, advanced, optional (NoDup)
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).
☐
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 nontrivial
machinery to prove, but we now have enough...
First prove an easy useful lemma.
Exercise: 4 stars, advanced, optional (pigeonhole_principle)
Lemma in_split : forall (X:Type) (x:X) (l:list X),
In x l >
exists l1 l2, l = l1 ++ x :: l2.
Proof.
Admitted.
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., forall 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.
Theorem pigeonhole_principle: forall (X:Type) (l1 l2:list X),
excluded_middle >
(forall x, In x l1 > In x l2) >
length l2 < length l1 >
repeats l1.
Proof.
intros X l1. induction l1 as [x l1' IHl1'].
Admitted.
Definition manual_grade_for_check_repeats : option (nat*string) := None.
☐
Extended Exercise: A Verified RegularExpression Matcher
The Coq standard library contains a distinct inductive definition
of strings of ASCII characters. However, we will use the above
definition of strings as lists as ASCII characters in order to apply
the existing definition of the match relation.
We could also define a regex matcher over polymorphic lists, not lists
of ASCII characters specifically. The matching algorithm that we will
implement needs to be able to test equality of elements in a given
list, and thus needs to be given an equalitytesting
function. Generalizing the definitions, theorems, and proofs that we
define for such a setting is a bit tedious, but workable.
The proof of correctness of the regex matcher will combine
properties of the regexmatching function with properties of the
match relation that do not depend on the matching function. We'll go
ahead and prove the latter class of properties now. Most of them have
straightforward proofs, which have been given to you, although there
are a few key lemmas that are left for you to prove.
Each provable Prop is equivalent to True.
Lemma provable_equiv_true : forall (P : Prop), P > (P <> True).
Proof.
intros.
split.
 intros. constructor.
 intros _. apply H.
Qed.
Proof.
intros.
split.
 intros. constructor.
 intros _. apply H.
Qed.
Each Prop whose negation is provable is equivalent to False.
Lemma not_equiv_false : forall (P : Prop), ~P > (P <> False).
Proof.
intros.
split.
 apply H.
 intros. destruct H0.
Qed.
Proof.
intros.
split.
 apply H.
 intros. destruct H0.
Qed.
EmptySet matches no string.
Lemma null_matches_none : forall (s : string), (s =~ EmptySet) <> False.
Proof.
intros.
apply not_equiv_false.
unfold not. intros. inversion H.
Qed.
Proof.
intros.
apply not_equiv_false.
unfold not. intros. inversion H.
Qed.
EmptyStr only matches the empty string.
Lemma empty_matches_eps : forall (s : string), s =~ EmptyStr <> s = [ ].
Proof.
split.
 intros. inversion H. reflexivity.
 intros. rewrite H. apply MEmpty.
Qed.
Proof.
split.
 intros. inversion H. reflexivity.
 intros. rewrite H. apply MEmpty.
Qed.
EmptyStr matches no nonempty string.
Lemma empty_nomatch_ne : forall (a : ascii) s, (a :: s =~ EmptyStr) <> False.
Proof.
intros.
apply not_equiv_false.
unfold not. intros. inversion H.
Qed.
Proof.
intros.
apply not_equiv_false.
unfold not. intros. inversion H.
Qed.
Lemma char_nomatch_char :
forall (a b : ascii) s, b <> a > (b :: s =~ Char a <> False).
Proof.
intros.
apply not_equiv_false.
unfold not.
intros.
apply H.
inversion H0.
reflexivity.
Qed.
forall (a b : ascii) s, b <> a > (b :: s =~ Char a <> False).
Proof.
intros.
apply not_equiv_false.
unfold not.
intros.
apply H.
inversion H0.
reflexivity.
Qed.
Lemma char_eps_suffix : forall (a : ascii) s, a :: s =~ Char a <> s = [ ].
Proof.
split.
 intros. inversion H. reflexivity.
 intros. rewrite H. apply MChar.
Qed.
Proof.
split.
 intros. inversion H. reflexivity.
 intros. rewrite H. apply MChar.
Qed.
Lemma app_exists : forall (s : string) re0 re1,
s =~ App re0 re1 <>
exists s0 s1, s = s0 ++ s1 /\ s0 =~ re0 /\ s1 =~ re1.
Proof.
intros.
split.
 intros. inversion H. exists s1, s2. split.
* reflexivity.
* split. apply H3. apply H4.
 intros [ s0 [ s1 [ Happ [ Hmat0 Hmat1 ] ] ] ].
rewrite Happ. apply (MApp s0 _ s1 _ Hmat0 Hmat1).
Qed.
s =~ App re0 re1 <>
exists s0 s1, s = s0 ++ s1 /\ s0 =~ re0 /\ s1 =~ re1.
Proof.
intros.
split.
 intros. inversion H. exists s1, s2. split.
* reflexivity.
* split. apply H3. apply H4.
 intros [ s0 [ s1 [ Happ [ Hmat0 Hmat1 ] ] ] ].
rewrite Happ. apply (MApp s0 _ s1 _ Hmat0 Hmat1).
Qed.
Exercise: 3 stars, standard, optional (app_ne)
Lemma app_ne : forall (a : ascii) s re0 re1,
a :: s =~ (App re0 re1) <>
([ ] =~ re0 /\ a :: s =~ re1) \/
exists s0 s1, s = s0 ++ s1 /\ a :: s0 =~ re0 /\ s1 =~ re1.
Proof.
Admitted.
a :: s =~ (App re0 re1) <>
([ ] =~ re0 /\ a :: s =~ re1) \/
exists s0 s1, s = s0 ++ s1 /\ a :: s0 =~ re0 /\ s1 =~ re1.
Proof.
Admitted.
Lemma union_disj : forall (s : string) re0 re1,
s =~ Union re0 re1 <> s =~ re0 \/ s =~ re1.
Proof.
intros. split.
 intros. inversion H.
+ left. apply H2.
+ right. apply H1.
 intros [ H  H ].
+ apply MUnionL. apply H.
+ apply MUnionR. apply H.
Qed.
s =~ Union re0 re1 <> s =~ re0 \/ s =~ re1.
Proof.
intros. split.
 intros. inversion H.
+ left. apply H2.
+ right. apply H1.
 intros [ H  H ].
+ apply MUnionL. apply H.
+ apply MUnionR. apply H.
Qed.
Exercise: 3 stars, standard, optional (star_ne)
Lemma star_ne : forall (a : ascii) s re,
a :: s =~ Star re <>
exists s0 s1, s = s0 ++ s1 /\ a :: s0 =~ re /\ s1 =~ Star re.
Proof.
Admitted.
☐
The definition of our regex matcher will include two fixpoint
functions. The first function, given regex re, will evaluate to a
value that reflects whether re matches the empty string. The
function will satisfy the following property:
Exercise: 2 stars, standard, optional (match_eps)
☐
Now, prove that match_eps indeed tests if a given regex matches
the empty string. (Hint: You'll want to use the reflection lemmas
ReflectT and ReflectF.)
Exercise: 3 stars, standard, optional (match_eps_refl)
☐
We'll define other functions that use match_eps. However, the
only property of match_eps that you'll need to use in all proofs
over these functions is match_eps_refl.
The key operation that will be performed by our regex matcher will
be to iteratively construct a sequence of regex derivatives. For each
character a and regex re, the derivative of re on a is a regex
that matches all suffixes of strings matched by re that start with
a. I.e., re' is a derivative of re on a if they satisfy the
following relation:
A function d derives strings if, given character a and regex
re, it evaluates to the derivative of re on a. I.e., d
satisfies the following property:
Exercise: 3 stars, standard, optional (derive)
☐
The derive function should pass the following tests. Each test
establishes an equality between an expression that will be
evaluated by our regex matcher and the final value that must be
returned by the regex matcher. Each test is annotated with the
match fact that it reflects.
"c" =~ EmptySet:
"c" =~ Char c:
"c" =~ Char d:
"c" =~ App (Char c) EmptyStr:
"c" =~ App EmptyStr (Char c):
"c" =~ Star c:
"cd" =~ App (Char c) (Char d):
Example test_der6 :
match_eps (derive d (derive c (App (Char c) (Char d)))) = true.
Proof.
Admitted.
match_eps (derive d (derive c (App (Char c) (Char d)))) = true.
Proof.
Admitted.
"cd" =~ App (Char d) (Char c):
Example test_der7 :
match_eps (derive d (derive c (App (Char d) (Char c)))) = false.
Proof.
Admitted.
match_eps (derive d (derive c (App (Char d) (Char c)))) = false.
Proof.
Admitted.
Exercise: 4 stars, standard, optional (derive_corr)
☐
We'll define the regex matcher using derive. However, the only
property of derive that you'll need to use in all proofs of
properties of the matcher is derive_corr.
A function m matches regexes if, given string s and regex re,
it evaluates to a value that reflects whether s is matched by
re. I.e., m holds the following property:
Exercise: 2 stars, standard, optional (regex_match)
☐
Finally, prove that regex_match in fact matches regexes.
Hint: if your definition of regex_match applies match_eps to
regex re, then a natural proof applies match_eps_refl to re
and destructs the result to generate cases in which you may assume
that re does or does not match the empty string.
Hint: if your definition of regex_match applies derive to
character x and regex re, then a natural proof applies
derive_corr to x and re to prove that x :: s =~ re given
s =~ derive x re, and vice versa.
Exercise: 3 stars, standard, optional (regex_refl)
☐