IndPropInductively Defined Propositions
Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
From LF Require Export Logic.
From LF Require Export Logic.
Inductively Defined Propositions
Example: The Collatz Conjecture
Fixpoint div2 (n : nat) :=
match n with
0 ⇒ 0
| 1 ⇒ 0
| S (S n) ⇒ S (div2 n)
end.
Definition f (n : nat) :=
if even n then div2 n
else (3 × n) + 1.
match n with
0 ⇒ 0
| 1 ⇒ 0
| S (S n) ⇒ S (div2 n)
end.
Definition f (n : nat) :=
if even n then div2 n
else (3 × n) + 1.
Next, we look at what happens when we repeatedly apply f to
some given starting number. For example, f 12 is 6, and f
6 is 3, so by repeatedly applying f we get the sequence
12, 6, 3, 10, 5, 16, 8, 4, 2, 1.
Similarly, if we start with 19, we get the longer sequence
19, 58, 29, 88, 44, 22, 11, 34, 17, 52, 26, 13, 40, 20, 10, 5,
16, 8, 4, 2, 1.
Both of these sequences eventually reach 1. The question
posed by Collatz was: Is the sequence starting from any
natural number guaranteed to reach 1 eventually?
To formalize this question in Coq, we might try to define a
recursive function that calculates the total number of steps
that it takes for such a sequence to reach 1.
This definition is rejected by Coq's termination checker, since
the argument to the recursive call, f n, is not "obviously
smaller" than n.
Indeed, this isn't just a pointless limitation: functions in Coq
are required to be total, to ensure logical consistency.
Moreover, we can't fix it by devising a more clever termination
checker: deciding whether this particular function is total
would be equivalent to settling the Collatz conjecture!
Fortunately, there is another way to do it: We can express the
concept "reaches 1 eventually" as an inductively defined
property of numbers:
Inductive Collatz_holds_for : nat → Prop :=
| Chf_done : Collatz_holds_for 1
| Chf_more (n : nat) : Collatz_holds_for (f n) → Collatz_holds_for n.
| Chf_done : Collatz_holds_for 1
| Chf_more (n : nat) : Collatz_holds_for (f n) → Collatz_holds_for n.
What we've done here is to use Coq's Inductive definition
mechanism to characterize the property "Collatz holds for..." by
stating two different ways in which it can hold: (1) Collatz holds
for 1 and (2) if Collatz holds for f n then it holds for
n.
For particular numbers, we can now argue that the Collatz sequence
reaches 1 like this (again, we'll go through the details of how
it works a bit later in the chapter):
Example Collatz_holds_for_12 : Collatz_holds_for 12.
Proof.
apply Chf_more. unfold f. simpl.
apply Chf_more. unfold f. simpl.
apply Chf_more. unfold f. simpl.
apply Chf_more. unfold f. simpl.
apply Chf_more. unfold f. simpl.
apply Chf_more. unfold f. simpl.
apply Chf_more. unfold f. simpl.
apply Chf_more. unfold f. simpl.
apply Chf_more. unfold f. simpl.
apply Chf_done. Qed.
Proof.
apply Chf_more. unfold f. simpl.
apply Chf_more. unfold f. simpl.
apply Chf_more. unfold f. simpl.
apply Chf_more. unfold f. simpl.
apply Chf_more. unfold f. simpl.
apply Chf_more. unfold f. simpl.
apply Chf_more. unfold f. simpl.
apply Chf_more. unfold f. simpl.
apply Chf_more. unfold f. simpl.
apply Chf_done. Qed.
The Collatz conjecture then states that the sequence beginning
from any number reaches 1:
If you succeed in proving this conjecture, you've got a bright
future as a number theorist! But don't spend too long on it --
it's been open since 1937.
Example: Ordering
The following definition says that there are two ways to
show that one number is less than or equal to another: either
observe that they are the same number, or, if the second has the
form S m, give evidence that the first is less than or equal to
m.
Inductive le : nat → nat → Prop :=
| le_n (n : nat) : le n n
| le_S (n m : nat) : le n m → le n (S m).
Notation "n <= m" := (le n m) (at level 70).
Example le_3_5 : 3 ≤ 5.
Proof.
apply le_S. apply le_S. apply le_n. Qed.
| le_n (n : nat) : le n n
| le_S (n m : nat) : le n m → le n (S m).
Notation "n <= m" := (le n m) (at level 70).
Example le_3_5 : 3 ≤ 5.
Proof.
apply le_S. apply le_S. apply le_n. Qed.
(By "reserving" the notation before defining the Inductive, we
can use it in the definition.)
Reserved Notation "n <= m" (at level 70).
Inductive le : nat → nat → Prop :=
| le_n (n : nat) : n ≤ n
| le_S (n m : nat) : n ≤ m → n ≤ (S m)
where "n <= m" := (le n m).
Inductive le : nat → nat → Prop :=
| le_n (n : nat) : n ≤ n
| le_S (n m : nat) : n ≤ m → n ≤ (S m)
where "n <= m" := (le n m).
Example: Transitive Closure
Inductive clos_trans {X: Type} (R: X→X→Prop) : X→X→Prop :=
| t_step (x y : X) :
R x y →
clos_trans R x y
| t_trans (x y z : X) :
clos_trans R x y →
clos_trans R y z →
clos_trans R x z.
| t_step (x y : X) :
R x y →
clos_trans R x y
| t_trans (x y z : X) :
clos_trans R x y →
clos_trans R y z →
clos_trans R x z.
For example, suppose we define a "parent of" relation on a group
of people...
Inductive Person : Type := Sage | Cleo | Ridley | Moss.
Inductive parent_of : Person → Person → Prop :=
po_SC : parent_of Sage Cleo
| po_SR : parent_of Sage Ridley
| po_CM : parent_of Cleo Moss.
Inductive parent_of : Person → Person → Prop :=
po_SC : parent_of Sage Cleo
| po_SR : parent_of Sage Ridley
| po_CM : parent_of Cleo Moss.
Then we can define "ancestor of" as its transitive closure:
Definition ancestor_of : Person → Person → Prop :=
clos_trans parent_of.
Example ancestor_of1 : ancestor_of Sage Moss.
Proof.
unfold ancestor_of. apply t_trans with Cleo.
- apply t_step. apply po_SC.
- apply t_step. apply po_CM. Qed.
clos_trans parent_of.
Example ancestor_of1 : ancestor_of Sage Moss.
Proof.
unfold ancestor_of. apply t_trans with Cleo.
- apply t_step. apply po_SC.
- apply t_step. apply po_CM. Qed.
Exercise: 1 star, standard, optional (close_refl_trans)
How would you modify this definition so that it defines reflexive and transitive closure? How about reflexive, symmetric, and transitive closure?
(* FILL IN HERE *)
☐
☐
Example: Permutations
Inductive Perm3 {X : Type} : list X → list X → Prop :=
| perm3_swap12 (a b c : X) :
Perm3 [a;b;c] [b;a;c]
| perm3_swap23 (a b c : X) :
Perm3 [a;b;c] [a;c;b]
| perm3_trans (l1 l2 l3 : list X) :
Perm3 l1 l2 → Perm3 l2 l3 → Perm3 l1 l3.
| perm3_swap12 (a b c : X) :
Perm3 [a;b;c] [b;a;c]
| perm3_swap23 (a b c : X) :
Perm3 [a;b;c] [a;c;b]
| perm3_trans (l1 l2 l3 : list X) :
Perm3 l1 l2 → Perm3 l2 l3 → Perm3 l1 l3.
This definition says:
- If l2 can be obtained from l1 by swapping the first and second elements, then l2 is a permutation of l1.
- If l2 can be obtained from l1 by swapping the second and third elements, then l2 is a permutation of l1.
- If l2 is a permutation of l1 and l3 is a permutation of l2, then l3 is a permutation of l1.
Exercise: 1 star, standard, optional (perm)
According to this definition, is [1;2;3] a permutation of [3;2;1]? Is [1;2;3] a permutation of itself?
(* FILL IN HERE *)
☐
☐
Example Perm3_example1 : Perm3 [1;2;3] [2;3;1].
Proof.
apply perm3_trans with [2;1;3].
- apply perm3_swap12.
- apply perm3_swap23. Qed.
Proof.
apply perm3_trans with [2;1;3].
- apply perm3_swap12.
- apply perm3_swap23. Qed.
Example: Evenness (yet again)
- The number 0 is even.
- If n is even, then S (S n) is even.
- Rule ev_0: The number 0 is even.
- Rule ev_SS: If n is even, then S (S n) is even.
This definition is interestingly different from previous uses of
Inductive. For one thing, we are defining not a Type (like
nat) or a function yielding a Type (like list), but rather a
function from nat to Prop -- that is, a property of numbers.
But what is really new is that, because the nat argument of ev
appears to the right of the colon on the first line, 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. Accordingly, the type of each constructor must be
specified explicitly (after a colon), and each constructor's type
must have the form ev n for some natural number n.
In contrast, recall the definition of list:
Inductive list (X:Type) : Type :=
| nil
| cons (x : X) (l : list X). or equivalently:
Inductive list (X:Type) : Type :=
| nil : list X
| cons (x : X) (l : list X) : list X. This definition introduces the X parameter globally, to the left of the colon, forcing the result of nil and cons to be the same type (i.e., list X). But if we had tried to bring nat to the left of the colon in defining ev, we would have seen an error:
Inductive list (X:Type) : Type :=
| nil
| cons (x : X) (l : list X). or equivalently:
Inductive list (X:Type) : Type :=
| nil : list X
| cons (x : X) (l : list X) : list X. This definition introduces the X parameter globally, to the left of the colon, forcing the result of nil and cons to be the same type (i.e., list X). But if we had tried to bring nat to the left of the colon in defining ev, we would have seen an error:
Fail Inductive wrong_ev (n : nat) : Prop :=
| wrong_ev_0 : wrong_ev 0
| wrong_ev_SS (H: wrong_ev n) : wrong_ev (S (S n)).
(* ===> Error: Last occurrence of "wrong_ev" must have "n" as 1st
argument in "wrong_ev 0". *)
| wrong_ev_0 : wrong_ev 0
| wrong_ev_SS (H: wrong_ev n) : wrong_ev (S (S n)).
(* ===> Error: Last occurrence of "wrong_ev" must have "n" as 1st
argument in "wrong_ev 0". *)
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" or "annotation."
For example, in Inductive list (X : Type) := ..., the X is a
parameter, while in Inductive ev : nat → Prop := ..., the
unnamed nat argument is an index.
We can think of this as defining a Coq property ev : nat →
Prop, together with "evidence constructors" ev_0 : ev 0 and
ev_SS : ∀ n, ev n → ev (S (S n)).
These evidence constructors can be thought of as "primitive
evidence of evenness", and they can be used just like proven
theorems. In particular, we can use Coq's apply tactic with the
constructor names to obtain evidence for ev of particular
numbers...
... or we can use function application syntax to combine several
constructors:
In this way, we can also prove theorems that have hypotheses
involving ev.
Theorem ev_plus4 : ∀ n, ev n → ev (4 + n).
Proof.
intros n. simpl. intros Hn. apply ev_SS. apply ev_SS. apply Hn.
Qed.
Proof.
intros n. simpl. intros Hn. apply ev_SS. apply ev_SS. apply Hn.
Qed.
Using Evidence in Proofs
- 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').
Inversion on Evidence
Theorem ev_inversion : ∀ (n : nat),
ev n →
(n = 0) ∨ (∃ n', n = S (S n') ∧ ev n').
Proof.
intros n E. destruct E as [ | n' E'] eqn:EE.
- (* E = ev_0 : ev 0 *)
left. reflexivity.
- (* E = ev_SS n' E' : ev (S (S n')) *)
right. ∃ n'. split. reflexivity. apply E'.
Qed.
ev n →
(n = 0) ∨ (∃ n', n = S (S n') ∧ ev n').
Proof.
intros n E. destruct E as [ | n' E'] eqn:EE.
- (* E = ev_0 : ev 0 *)
left. reflexivity.
- (* E = ev_SS n' E' : ev (S (S n')) *)
right. ∃ n'. split. reflexivity. apply E'.
Qed.
Facts like this are often called "inversion lemmas" because they
allow us to "invert" some given information to reason about all
the different ways it could have been derived.
Here, there are two ways to prove ev n, and the inversion lemma
makes this explicit.
We can use the inversion lemma that we proved above to help
structure proofs:
Theorem evSS_ev : ∀ n, ev (S (S n)) → ev n.
Proof.
intros n H. apply ev_inversion in H. destruct H as [H0|H1].
- discriminate H0.
- destruct H1 as [n' [Hnm Hev]]. injection Hnm as Heq.
rewrite Heq. apply Hev.
Qed.
Proof.
intros n H. apply ev_inversion in H. destruct H as [H0|H1].
- discriminate H0.
- destruct H1 as [n' [Hnm Hev]]. injection Hnm as Heq.
rewrite Heq. apply Hev.
Qed.
Note how the inversion lemma produces two subgoals, which
correspond to the two ways of proving ev. The first subgoal is
a contradiction that is discharged with discriminate. The
second subgoal makes use of injection and rewrite.
Coq provides a handy tactic called inversion that factors out
this common pattern, saving us the trouble of explicitly stating
and proving an inversion lemma for every Inductive definition we
make.
Here, the inversion tactic can detect (1) that the first case,
where n = 0, does not apply and (2) that the n' that appears
in the ev_SS case must be the same as n. It includes an
"as" annotation similar to destruct, allowing us to assign
names rather than have Coq choose them.
Theorem evSS_ev' : ∀ n,
ev (S (S n)) → ev n.
Proof.
intros n E. inversion E as [| n' E' Heq].
(* We are in the E = ev_SS n' E' case now. *)
apply E'.
Qed.
ev (S (S n)) → ev n.
Proof.
intros n E. inversion E as [| n' E' Heq].
(* We are in the E = ev_SS n' E' case now. *)
apply E'.
Qed.
The inversion tactic can apply the principle of explosion to
"obviously contradictory" hypotheses involving inductively defined
properties, something that takes a bit more work using our
inversion lemma. Compare:
Theorem one_not_even : ¬ ev 1.
Proof.
intros H. apply ev_inversion in H. destruct H as [ | [m [Hm _]]].
- discriminate H.
- discriminate Hm.
Qed.
Theorem one_not_even' : ¬ ev 1.
Proof.
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' : ¬ ev 1.
Proof.
intros H. inversion H. Qed.
Exercise: 1 star, standard (inversion_practice)
Prove the following result using inversion. (For extra practice, you can also prove it using the inversion lemma.)
Theorem inversion_ex1 : ∀ (n m o : nat),
[n; m] = [o; o] → [n] = [m].
Proof.
intros n m o H. inversion H. reflexivity. Qed.
Theorem inversion_ex2 : ∀ (n : nat),
S n = O → 2 + 2 = 5.
Proof.
intros n contra. inversion contra. Qed.
[n; m] = [o; o] → [n] = [m].
Proof.
intros n m o H. inversion H. reflexivity. Qed.
Theorem inversion_ex2 : ∀ (n : nat),
S n = O → 2 + 2 = 5.
Proof.
intros n contra. inversion contra. Qed.
Here's how inversion works in general.
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.
- 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 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 to the proof context all equations that must hold of the arguments given to P -- e.g., n' = n in the proof of evSS_ev).
We could try to proceed by case analysis or induction on n. But
since ev is mentioned in a premise, this strategy seems
unpromising, because (as we've noted before) the induction
hypothesis will talk about n-1 (which is not even!). Thus, it
seems better to first try inversion on the evidence for ev.
Indeed, the first case can be solved trivially. And we can
seemingly make progress on the second case with a helper lemma.
intros n E. inversion E as [EQ' | n' E' EQ'].
- (* E = ev_0 *) ∃ 0. reflexivity.
- (* E = ev_SS n' E' *)
- (* E = ev_0 *) ∃ 0. reflexivity.
- (* E = ev_SS n' E' *)
Unfortunately, the second case is harder. We need to show ∃
n0, S (S n') = double n0, 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 a similar
one that involves a different piece of evidence for ev: namely
E'. More formally, we could finish our proof if we could show
that
∃ 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 would suffice.
∃ 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 would suffice.
assert (H: (∃ k', n' = double k')
→ (∃ n0, S (S n') = double n0)).
{ intros [k' EQ'']. ∃ (S k'). simpl.
rewrite <- EQ''. reflexivity. }
apply H.
→ (∃ n0, S (S n') = double n0)).
{ intros [k' EQ'']. ∃ (S k'). simpl.
rewrite <- EQ''. reflexivity. }
apply H.
Unfortunately, now we are stuck. To see this clearly, let's
move E' back into the goal from the hypotheses.
generalize dependent E'.
Now it is obvious that we are trying to prove another instance
of the same theorem we set out to prove -- only here we are
talking about n' instead of n.
Abort.
Induction on Evidence
Lemma ev_Even : ∀ n,
ev n → Even n.
Proof.
intros n E.
induction E as [|n' E' IH].
- (* E = ev_0 *)
unfold Even. ∃ 0. reflexivity.
- (* E = ev_SS n' E'
with IH : Even n' *)
unfold Even in IH.
destruct IH as [k Hk].
rewrite Hk.
unfold Even. ∃ (S k). simpl. reflexivity.
Qed.
ev n → Even n.
Proof.
intros n E.
induction E as [|n' E' IH].
- (* E = ev_0 *)
unfold Even. ∃ 0. reflexivity.
- (* E = ev_SS n' E'
with IH : Even n' *)
unfold Even in IH.
destruct IH as [k Hk].
rewrite Hk.
unfold Even. ∃ (S k). simpl. 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.
Theorem ev_Even_iff : ∀ n,
ev n ↔ Even n.
Proof.
intros n. split.
- (* -> *) apply ev_Even.
- (* <- *) unfold Even. intros [k Hk]. rewrite Hk. apply ev_double.
Qed.
ev n ↔ Even n.
Proof.
intros n. split.
- (* -> *) apply ev_Even.
- (* <- *) unfold 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 -- in particular for
formalizing the semantics of programming languages.
The following exercises provide simple examples of this
technique, to help you familiarize yourself with it.
Exercise: 2 stars, standard (ev_sum)
Exercise: 4 stars, advanced, optional (ev'_ev)
In general, there may be multiple ways of defining a property inductively. For example, here's a (slightly contrived) alternative definition for ev:
Inductive ev' : nat → Prop :=
| ev'_0 : ev' 0
| ev'_2 : ev' 2
| ev'_sum n m (Hn : ev' n) (Hm : ev' m) : ev' (n + m).
| ev'_0 : ev' 0
| ev'_2 : ev' 2
| ev'_sum n m (Hn : ev' n) (Hm : ev' m) : ev' (n + m).
Prove that this definition is logically equivalent to the old one.
To streamline the proof, use the technique (from the Logic
chapter) of applying theorems to arguments, and note that the same
technique works with constructors of inductively defined
propositions.
Theorem ev_ev__ev : ∀ n m,
ev (n+m) → ev n → ev m.
(* Hint: There are two pieces of evidence you could attempt to induct upon
here. If one doesn't work, try the other. *)
Proof.
(* FILL IN HERE *) Admitted.
☐
ev (n+m) → ev n → ev m.
(* Hint: There are two pieces of evidence you could attempt to induct upon
here. If one doesn't work, try the other. *)
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 3 stars, standard, optional (ev_plus_plus)
This exercise can be completed without induction or case analysis. But, you will need a clever assertion and some tedious rewriting. Hint: Is (n+m) + (n+p) even?
Theorem ev_plus_plus : ∀ n m p,
ev (n+m) → ev (n+p) → ev (m+p).
Proof.
(* FILL IN HERE *) Admitted.
☐
ev (n+m) → ev (n+p) → ev (m+p).
Proof.
(* FILL IN HERE *) Admitted.
☐
Inductive Relations
Just like properties, relations can be defined inductively. One
useful example is the "less than or equal to" relation on numbers
that we briefly saw above.
Inductive le : nat → nat → Prop :=
| le_n (n : nat) : le n n
| le_S (n m : nat) (H : le n m) : le n (S m).
Notation "n <= m" := (le n m).
| le_n (n : nat) : le n n
| le_S (n m : nat) (H : le n m) : le n (S m).
Notation "n <= m" := (le n m).
(We've written the definition a bit differently this time,
giving explicit names to the arguments to the constructors and
moving them to the left of the colons.)
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.
(* WORKED IN CLASS *)
apply le_n. Qed.
Theorem test_le2 :
3 ≤ 6.
Proof.
(* WORKED IN CLASS *)
apply le_S. apply le_S. apply le_S. apply le_n. Qed.
Theorem test_le3 :
(2 ≤ 1) → 2 + 2 = 5.
Proof.
(* WORKED IN CLASS *)
intros H. inversion H. inversion H2. Qed.
3 ≤ 3.
Proof.
(* WORKED IN CLASS *)
apply le_n. Qed.
Theorem test_le2 :
3 ≤ 6.
Proof.
(* WORKED IN CLASS *)
apply le_S. apply le_S. apply le_S. apply le_n. Qed.
Theorem test_le3 :
(2 ≤ 1) → 2 + 2 = 5.
Proof.
(* WORKED IN CLASS *)
intros H. inversion H. inversion H2. Qed.
The "strictly less than" relation n < m can now be defined
in terms of le.
Exercise: 2 stars, standard, optional (total_relation)
Define an inductive binary relation total_relation that holds between every pair of natural numbers.
Inductive total_relation : nat → nat → Prop :=
(* FILL IN HERE *)
.
Theorem total_relation_is_total : ∀ n m, total_relation n m.
Proof.
(* FILL IN HERE *) Admitted.
☐
(* FILL IN HERE *)
.
Theorem total_relation_is_total : ∀ n m, total_relation n m.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 2 stars, standard, optional (empty_relation)
Define an inductive binary relation empty_relation (on numbers) that never holds.
Inductive empty_relation : nat → nat → Prop :=
(* FILL IN HERE *)
.
Theorem empty_relation_is_empty : ∀ n m, ¬ empty_relation n m.
Proof.
(* FILL IN HERE *) Admitted.
☐
(* FILL IN HERE *)
.
Theorem empty_relation_is_empty : ∀ n m, ¬ empty_relation n m.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 5 stars, standard, optional (le_and_lt_facts)
Lemma le_trans : ∀ m n o, m ≤ n → n ≤ o → m ≤ o.
Proof.
(* FILL IN HERE *) Admitted.
Theorem O_le_n : ∀ n,
0 ≤ n.
Proof.
(* FILL IN HERE *) Admitted.
Theorem n_le_m__Sn_le_Sm : ∀ n m,
n ≤ m → S n ≤ S m.
Proof.
(* FILL IN HERE *) Admitted.
Theorem Sn_le_Sm__n_le_m : ∀ n m,
S n ≤ S m → n ≤ m.
Proof.
(* FILL IN HERE *) Admitted.
Theorem lt_ge_cases : ∀ n m,
n < m ∨ n ≥ m.
Proof.
(* FILL IN HERE *) Admitted.
Theorem le_plus_l : ∀ a b,
a ≤ a + b.
Proof.
(* FILL IN HERE *) Admitted.
Theorem plus_le : ∀ n1 n2 m,
n1 + n2 ≤ m →
n1 ≤ m ∧ n2 ≤ m.
Proof.
(* FILL IN HERE *) Admitted.
Theorem add_le_cases : ∀ n m p q,
n + m ≤ p + q → n ≤ p ∨ m ≤ q.
Proof.
(* FILL IN HERE *) Admitted.
Theorem O_le_n : ∀ n,
0 ≤ n.
Proof.
(* FILL IN HERE *) Admitted.
Theorem n_le_m__Sn_le_Sm : ∀ n m,
n ≤ m → S n ≤ S m.
Proof.
(* FILL IN HERE *) Admitted.
Theorem Sn_le_Sm__n_le_m : ∀ n m,
S n ≤ S m → n ≤ m.
Proof.
(* FILL IN HERE *) Admitted.
Theorem lt_ge_cases : ∀ n m,
n < m ∨ n ≥ m.
Proof.
(* FILL IN HERE *) Admitted.
Theorem le_plus_l : ∀ a b,
a ≤ a + b.
Proof.
(* FILL IN HERE *) Admitted.
Theorem plus_le : ∀ n1 n2 m,
n1 + n2 ≤ m →
n1 ≤ m ∧ n2 ≤ m.
Proof.
(* FILL IN HERE *) Admitted.
Theorem add_le_cases : ∀ n m p q,
n + m ≤ p + q → n ≤ p ∨ m ≤ q.
Hint: May be easiest to prove by induction on n.
Proof.
(* FILL IN HERE *) Admitted.
Theorem plus_le_compat_l : ∀ n m p,
n ≤ m →
p + n ≤ p + m.
Proof.
(* FILL IN HERE *) Admitted.
Theorem plus_le_compat_r : ∀ n m p,
n ≤ m →
n + p ≤ m + p.
Proof.
(* FILL IN HERE *) Admitted.
Theorem le_plus_trans : ∀ n m p,
n ≤ m →
n ≤ m + p.
Proof.
(* FILL IN HERE *) Admitted.
Theorem n_lt_m__n_le_m : ∀ n m,
n < m →
n ≤ m.
Proof.
(* FILL IN HERE *) Admitted.
Theorem plus_lt : ∀ n1 n2 m,
n1 + n2 < m →
n1 < m ∧ n2 < m.
Proof.
(* FILL IN HERE *) Admitted.
☐
(* FILL IN HERE *) Admitted.
Theorem plus_le_compat_l : ∀ n m p,
n ≤ m →
p + n ≤ p + m.
Proof.
(* FILL IN HERE *) Admitted.
Theorem plus_le_compat_r : ∀ n m p,
n ≤ m →
n + p ≤ m + p.
Proof.
(* FILL IN HERE *) Admitted.
Theorem le_plus_trans : ∀ n m p,
n ≤ m →
n ≤ m + p.
Proof.
(* FILL IN HERE *) Admitted.
Theorem n_lt_m__n_le_m : ∀ n m,
n < m →
n ≤ m.
Proof.
(* FILL IN HERE *) Admitted.
Theorem plus_lt : ∀ n1 n2 m,
n1 + n2 < m →
n1 < m ∧ n2 < m.
Proof.
(* FILL IN HERE *) Admitted.
☐
Theorem leb_complete : ∀ n m,
n <=? m = true → n ≤ m.
Proof.
(* FILL IN HERE *) Admitted.
Theorem leb_correct : ∀ n m,
n ≤ m →
n <=? m = true.
n <=? m = true → n ≤ m.
Proof.
(* FILL IN HERE *) Admitted.
Theorem leb_correct : ∀ n m,
n ≤ m →
n <=? m = true.
Hint: May be easiest to prove by induction on m.
Proof.
(* FILL IN HERE *) Admitted.
(* FILL IN HERE *) Admitted.
Hint: The next two can easily be proved without using induction.
Theorem leb_iff : ∀ n m,
n <=? m = true ↔ n ≤ m.
Proof.
(* FILL IN HERE *) Admitted.
Theorem leb_true_trans : ∀ n m o,
n <=? m = true → m <=? o = true → n <=? o = true.
Proof.
(* FILL IN HERE *) Admitted.
☐
n <=? m = true ↔ n ≤ m.
Proof.
(* FILL IN HERE *) Admitted.
Theorem leb_true_trans : ∀ n m o,
n <=? m = true → m <=? o = true → n <=? o = true.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 3 stars, standard, especially useful (R_provability)
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:
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
.
| 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?
- R 1 1 2
- R 2 2 6
- 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.
(* FILL IN HERE *)
(* Do not modify the following line: *)
Definition manual_grade_for_R_provability : option (nat×string) := None.
☐
(* Do not modify the following line: *)
Definition manual_grade_for_R_provability : option (nat×string) := None.
☐
Exercise: 3 stars, standard, optional (R_fact)
The relation R above actually encodes a familiar function. Figure out which function; then state and prove this equivalence in Coq.
Definition fR : nat → nat → nat
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Theorem R_equiv_fR : ∀ m n o, R m n o ↔ fR m n = o.
Proof.
(* FILL IN HERE *) Admitted.
☐
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Theorem R_equiv_fR : ∀ m n o, R m n o ↔ fR m n = o.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 3 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;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.
- (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.
Inductive subseq : list nat → list nat → Prop :=
(* FILL IN HERE *)
.
Theorem subseq_refl : ∀ (l : list nat), subseq l l.
Proof.
(* FILL IN HERE *) Admitted.
Theorem subseq_app : ∀ (l1 l2 l3 : list nat),
subseq l1 l2 →
subseq l1 (l2 ++ l3).
Proof.
(* FILL IN HERE *) Admitted.
Theorem subseq_trans : ∀ (l1 l2 l3 : list nat),
subseq l1 l2 →
subseq l2 l3 →
subseq l1 l3.
Proof.
(* Hint: be careful about what you are doing induction on and which
other things need to be generalized... *)
(* FILL IN HERE *) Admitted.
☐
(* FILL IN HERE *)
.
Theorem subseq_refl : ∀ (l : list nat), subseq l l.
Proof.
(* FILL IN HERE *) Admitted.
Theorem subseq_app : ∀ (l1 l2 l3 : list nat),
subseq l1 l2 →
subseq l1 (l2 ++ l3).
Proof.
(* FILL IN HERE *) Admitted.
Theorem subseq_trans : ∀ (l1 l2 l3 : list nat),
subseq l1 l2 →
subseq l2 l3 →
subseq l1 l3.
Proof.
(* Hint: be careful about what you are doing induction on and which
other things need to be generalized... *)
(* FILL IN HERE *) Admitted.
☐
Exercise: 2 stars, standard, optional (R_provability2)
Suppose we give Coq the following definition:Inductive R : nat → list nat → Prop :=
| c1 : R 0 []
| c2 n l (H: R n l) : R (S n) (n :: l)
| c3 n l (H: 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]
(* FILL IN HERE *)
☐
☐
A Digression on Notation
... which omits the result types because they are all the same (i.e., bin).
It is completely equivalent to this...
... where we fill them in, and this...
... where we put everything on the right of the colon.
For inductively defined propositions, we need to explicitly give
the result type for each constructor (because they are not all the
same), so the first style doesn't make sense, but we can use
either the second or the third interchangeably.
Case Study: Regular Expressions
Inductive reg_exp (T : Type) : Type :=
| EmptySet
| EmptyStr
| Char (t : T)
| App (r1 r2 : reg_exp T)
| Union (r1 r2 : reg_exp T)
| Star (r : reg_exp T).
Arguments EmptySet {T}.
Arguments EmptyStr {T}.
Arguments Char {T} _.
Arguments App {T} _ _.
Arguments Union {T} _ _.
Arguments Star {T} _.
| EmptySet
| EmptyStr
| Char (t : T)
| App (r1 r2 : reg_exp T)
| Union (r1 r2 : reg_exp T)
| Star (r : reg_exp T).
Arguments EmptySet {T}.
Arguments EmptyStr {T}.
Arguments Char {T} _.
Arguments App {T} _ _.
Arguments Union {T} _ _.
Arguments Star {T} _.
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.
(Technical aside: 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 present 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. We use the notation s =~ re in
place of exp_match s re.
- 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.
Reserved Notation "s =~ re" (at level 80).
Inductive exp_match {T} : list T → reg_exp T → Prop :=
| MEmpty : [] =~ EmptyStr
| MChar x : [x] =~ (Char x)
| MApp s1 re1 s2 re2
(H1 : s1 =~ re1)
(H2 : s2 =~ re2)
: (s1 ++ s2) =~ (App re1 re2)
| MUnionL s1 re1 re2
(H1 : s1 =~ re1)
: s1 =~ (Union re1 re2)
| MUnionR re1 s2 re2
(H2 : s2 =~ re2)
: s2 =~ (Union re1 re2)
| MStar0 re : [] =~ (Star re)
| MStarApp s1 s2 re
(H1 : s1 =~ re)
(H2 : s2 =~ (Star re))
: (s1 ++ s2) =~ (Star re)
where "s =~ re" := (exp_match s re).
Inductive exp_match {T} : list T → reg_exp T → Prop :=
| MEmpty : [] =~ EmptyStr
| MChar x : [x] =~ (Char x)
| MApp s1 re1 s2 re2
(H1 : s1 =~ re1)
(H2 : s2 =~ re2)
: (s1 ++ s2) =~ (App re1 re2)
| MUnionL s1 re1 re2
(H1 : s1 =~ re1)
: s1 =~ (Union re1 re2)
| MUnionR re1 s2 re2
(H2 : s2 =~ re2)
: s2 =~ (Union re1 re2)
| MStar0 re : [] =~ (Star re)
| MStarApp s1 s2 re
(H1 : s1 =~ re)
(H2 : s2 =~ (Star re))
: (s1 ++ s2) =~ (Star re)
where "s =~ re" := (exp_match s 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.")
Second, 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 string
[1] 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].
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].
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 shape expected by MStarApp.)
Exercise: 3 stars, standard (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.
Lemma empty_is_empty : ∀ T (s : list T),
¬ (s =~ EmptySet).
Proof.
(* FILL IN HERE *) Admitted.
Lemma MUnion' : ∀ T (s : list T) (re1 re2 : reg_exp T),
s =~ re1 ∨ s =~ re2 →
s =~ Union re1 re2.
Proof.
(* FILL IN HERE *) Admitted.
¬ (s =~ EmptySet).
Proof.
(* FILL IN HERE *) Admitted.
Lemma MUnion' : ∀ T (s : list T) (re1 re2 : reg_exp T),
s =~ re1 ∨ s =~ re2 →
s =~ Union re1 re2.
Proof.
(* FILL IN HERE *) 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' : ∀ T (ss : list (list T)) (re : reg_exp T),
(∀ s, In s ss → s =~ re) →
fold app ss [] =~ Star re.
Proof.
(* FILL IN HERE *) Admitted.
☐
(∀ s, In s ss → s =~ re) →
fold app ss [] =~ Star re.
Proof.
(* FILL IN HERE *) Admitted.
☐
Fixpoint re_chars {T} (re : reg_exp T) : 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.
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.
The main theorem:
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].
(* WORKED IN CLASS *)
- (* MEmpty *)
simpl in Hin. destruct Hin.
- (* MChar *)
simpl. simpl in Hin.
apply Hin.
- (* MApp *)
simpl.
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].
(* WORKED IN CLASS *)
- (* MEmpty *)
simpl in Hin. destruct Hin.
- (* MChar *)
simpl. simpl in Hin.
apply Hin.
- (* MApp *)
simpl.
Something interesting happens in the MApp case. We obtain
two induction hypotheses: One that applies when x occurs in
s1 (which matches re1), and a second one that applies when x
occurs in s2 (which matches re2).
rewrite In_app_iff in ×.
destruct Hin as [Hin | Hin].
+ (* In x s1 *)
left. apply (IH1 Hin).
+ (* In x s2 *)
right. apply (IH2 Hin).
- (* MUnionL *)
simpl. rewrite In_app_iff.
left. apply (IH Hin).
- (* MUnionR *)
simpl. rewrite In_app_iff.
right. apply (IH Hin).
- (* MStar0 *)
destruct Hin.
- (* MStarApp *)
simpl.
destruct Hin as [Hin | Hin].
+ (* In x s1 *)
left. apply (IH1 Hin).
+ (* In x s2 *)
right. apply (IH2 Hin).
- (* MUnionL *)
simpl. rewrite In_app_iff.
left. apply (IH Hin).
- (* MUnionR *)
simpl. rewrite In_app_iff.
right. apply (IH Hin).
- (* MStar0 *)
destruct Hin.
- (* MStarApp *)
simpl.
Here again we get two induction hypotheses, and they illustrate
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.
rewrite In_app_iff in Hin.
destruct Hin as [Hin | Hin].
+ (* In x s1 *)
apply (IH1 Hin).
+ (* In x s2 *)
apply (IH2 Hin).
Qed.
destruct Hin as [Hin | Hin].
+ (* In x s1 *)
apply (IH1 Hin).
+ (* In x s2 *)
apply (IH2 Hin).
Qed.
Exercise: 4 stars, standard (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.
Fixpoint re_not_empty {T : Type} (re : reg_exp T) : bool
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Lemma re_not_empty_correct : ∀ T (re : reg_exp T),
(∃ s, s =~ re) ↔ re_not_empty re = true.
Proof.
(* FILL IN HERE *) Admitted.
☐
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Lemma re_not_empty_correct : ∀ T (re : reg_exp T),
(∃ s, s =~ re) ↔ re_not_empty re = true.
Proof.
(* FILL IN HERE *) Admitted.
☐
The remember Tactic
Lemma star_app: ∀ 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.
s1 =~ Star re →
s2 =~ Star re →
s1 ++ s2 =~ Star re.
Proof.
intros T s1 s2 re H1.
Now, 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 IH|re1 s2' re2 Hmatch IH
|re''|s1 s2' re'' Hmatch1 IH1 Hmatch2 IH2].
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 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...
- (* MEmpty *)
simpl. intros H. apply H.
simpl. intros H. apply H.
... but most cases get stuck. For MChar, for instance, we
must show
s2 =~ Char x' →
x'::s2 =~ Char x' which is clearly impossible.
s2 =~ Char x' →
x'::s2 =~ Char x' which is clearly impossible.
- (* MChar. *) intros H. simpl. (* Stuck... *)
Abort.
Abort.
The problem here 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 like Star re.
(In this respect, induction on evidence behaves more like
destruct-without-eqn: than like inversion.)
A possible, but awkward, way to solve this problem is "manually
generalizing" over the problematic expressions by adding
explicit equality hypotheses to the lemma:
Lemma star_app: ∀ T (s1 s2 : list T) (re re' : reg_exp T),
re' = Star re →
s1 =~ re' →
s2 =~ Star re →
s1 ++ s2 =~ Star re.
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 works, but it makes the statement of the lemma a bit ugly.
Fortunately, there is a better way...
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: ∀ 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.
remember (Star re) as re'.
s1 =~ Star re →
s2 =~ Star re →
s1 ++ s2 =~ Star re.
Proof.
intros T s1 s2 re H1.
remember (Star re) as re'.
We now have Heqre' : re' = Star re.
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].
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, allowing us to
conclude immediately.
- (* MEmpty *) discriminate.
- (* MChar *) discriminate.
- (* MApp *) discriminate.
- (* MUnionL *) discriminate.
- (* MUnionR *) discriminate.
- (* MChar *) discriminate.
- (* MApp *) discriminate.
- (* MUnionL *) discriminate.
- (* MUnionR *) 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.
- (* MStar0 *)
intros H. apply H.
- (* MStarApp *)
intros H1. rewrite <- app_assoc.
apply MStarApp.
+ apply Hmatch1.
+ apply IH2.
× apply Heqre'.
× apply H1.
Qed.
intros H. apply H.
- (* MStarApp *)
intros H1. rewrite <- app_assoc.
apply MStarApp.
+ apply Hmatch1.
+ apply IH2.
× apply Heqre'.
× apply H1.
Qed.
Exercise: 4 stars, standard, optional (exp_match_ex2)
Lemma MStar'' : ∀ T (s : list T) (re : reg_exp T),
s =~ Star re →
∃ ss : list (list T),
s = fold app ss []
∧ ∀ s', In s' ss → s' =~ re.
Proof.
(* FILL IN HERE *) Admitted.
☐
s =~ Star re →
∃ ss : list (list T),
s = fold app ss []
∧ ∀ s', In s' ss → s' =~ re.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 5 stars, advanced (weak_pumping)
One of the first really 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. (For the sake of simplicity in this exercise, we consider a slightly weaker theorem than is usually stated in courses on automata theory -- hence the name weak_pumping.)
Module Pumping.
Fixpoint pumping_constant {T} (re : reg_exp T) : nat :=
match re with
| EmptySet ⇒ 1
| EmptyStr ⇒ 1
| Char _ ⇒ 2
| App re1 re2 ⇒
pumping_constant re1 + pumping_constant re2
| Union re1 re2 ⇒
pumping_constant re1 + pumping_constant re2
| Star r ⇒ pumping_constant r
end.
Fixpoint pumping_constant {T} (re : reg_exp T) : nat :=
match re with
| EmptySet ⇒ 1
| EmptyStr ⇒ 1
| Char _ ⇒ 2
| App re1 re2 ⇒
pumping_constant re1 + pumping_constant re2
| Union re1 re2 ⇒
pumping_constant re1 + pumping_constant re2
| Star r ⇒ pumping_constant r
end.
You may find these lemmas about the pumping constant useful when
proving the pumping lemma below.
Lemma pumping_constant_ge_1 :
∀ T (re : reg_exp T),
pumping_constant re ≥ 1.
Lemma pumping_constant_0_false :
∀ T (re : reg_exp T),
pumping_constant re = 0 → False.
∀ T (re : reg_exp T),
pumping_constant re ≥ 1.
Proof.
intros T re. induction re.
- (* EmptySet *)
apply le_n.
- (* EmptyStr *)
apply le_n.
- (* Char *)
apply le_S. apply le_n.
- (* App *)
simpl.
apply le_trans with (n:=pumping_constant re1).
apply IHre1. apply le_plus_l.
- (* Union *)
simpl.
apply le_trans with (n:=pumping_constant re1).
apply IHre1. apply le_plus_l.
- (* Star *)
simpl. apply IHre.
Qed.
intros T re. induction re.
- (* EmptySet *)
apply le_n.
- (* EmptyStr *)
apply le_n.
- (* Char *)
apply le_S. apply le_n.
- (* App *)
simpl.
apply le_trans with (n:=pumping_constant re1).
apply IHre1. apply le_plus_l.
- (* Union *)
simpl.
apply le_trans with (n:=pumping_constant re1).
apply IHre1. apply le_plus_l.
- (* Star *)
simpl. apply IHre.
Qed.
Lemma pumping_constant_0_false :
∀ T (re : reg_exp T),
pumping_constant re = 0 → False.
Proof.
intros T re H.
assert (Hp1 : pumping_constant re ≥ 1).
{ apply pumping_constant_ge_1. }
rewrite H in Hp1. inversion Hp1.
Qed.
intros T re H.
assert (Hp1 : pumping_constant re ≥ 1).
{ apply pumping_constant_ge_1. }
rewrite H in Hp1. inversion Hp1.
Qed.
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.
match n with
| 0 ⇒ []
| S n' ⇒ l ++ napp n' l
end.
This auxiliary lemma might also be useful in your proof of the
pumping lemma.
Lemma napp_plus: ∀ T (n m : nat) (l : list T),
napp (n + m) l = napp n l ++ napp m l.
Lemma napp_star :
∀ T m s1 s2 (re : reg_exp T),
s1 =~ re → s2 =~ Star re →
napp m s1 ++ s2 =~ Star re.
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.
intros T n m l.
induction n as [|n IHn].
- reflexivity.
- simpl. rewrite IHn, app_assoc. reflexivity.
Qed.
Lemma napp_star :
∀ T m s1 s2 (re : reg_exp T),
s1 =~ re → s2 =~ Star re →
napp m s1 ++ s2 =~ Star re.
The (weak) 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 weak_pumping : ∀ T (re : reg_exp T) s,
s =~ re →
pumping_constant re ≤ length s →
∃ s1 s2 s3,
s = s1 ++ s2 ++ s3 ∧
s2 ≠ [] ∧
∀ m, s1 ++ napp m s2 ++ s3 =~ re.
s =~ re →
pumping_constant re ≤ length s →
∃ s1 s2 s3,
s = s1 ++ s2 ++ s3 ∧
s2 ≠ [] ∧
∀ m, s1 ++ napp m s2 ++ s3 =~ re.
Complete the proof below. Several of the lemmas about le that
were in an optional exercise earlier in this chapter may also be
useful.
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 ].
- (* MEmpty *)
simpl. intros contra. inversion contra.
(* FILL IN HERE *) Admitted.
☐
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 ].
- (* MEmpty *)
simpl. intros contra. inversion contra.
(* FILL IN HERE *) Admitted.
☐
Exercise: 5 stars, advanced, optional (pumping)
Now here is the usual version of the pumping lemma. In addition to requiring that s2 ≠ [], it also requires that length s1 + length s2 ≤ pumping_constant re.
Lemma pumping : ∀ T (re : reg_exp T) s,
s =~ re →
pumping_constant re ≤ length s →
∃ s1 s2 s3,
s = s1 ++ s2 ++ s3 ∧
s2 ≠ [] ∧
length s1 + length s2 ≤ pumping_constant re ∧
∀ m, s1 ++ napp m s2 ++ s3 =~ re.
s =~ re →
pumping_constant re ≤ length s →
∃ s1 s2 s3,
s = s1 ++ s2 ++ s3 ∧
s2 ≠ [] ∧
length s1 + length s2 ≤ pumping_constant re ∧
∀ m, s1 ++ napp m s2 ++ s3 =~ re.
You may want to copy your proof of weak_pumping below.
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 ].
- (* MEmpty *)
simpl. intros contra. inversion contra.
(* FILL IN HERE *) Admitted.
End Pumping.
☐
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 ].
- (* MEmpty *)
simpl. intros contra. inversion contra.
(* FILL IN HERE *) Admitted.
End Pumping.
☐
Case Study: Improving Reflection
Theorem filter_not_empty_In : ∀ n l,
filter (fun x ⇒ n =? x) l ≠ [] →
In n l.
Proof.
intros n l. induction l as [|m l' IHl'].
- (* l = *)
simpl. intros H. apply H. reflexivity.
- (* l = m :: l' *)
simpl. destruct (n =? m) eqn:H.
+ (* n =? m = true *)
intros _. rewrite eqb_eq in H. rewrite H.
left. reflexivity.
+ (* n =? m = false *)
intros H'. right. apply IHl'. apply H'.
Qed.
filter (fun x ⇒ n =? x) l ≠ [] →
In n l.
Proof.
intros n l. induction l as [|m l' IHl'].
- (* l = *)
simpl. intros H. apply H. reflexivity.
- (* l = m :: l' *)
simpl. destruct (n =? m) eqn:H.
+ (* n =? m = true *)
intros _. rewrite eqb_eq in H. rewrite H.
left. reflexivity.
+ (* n =? m = false *)
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 sort of reasoning by defining an inductive
proposition that yields a better case-analysis principle for n =?
m. Instead of generating the assumption (n =? m) = true, which
usually requires some massaging before we can use it, this
principle gives us right away the assumption we really need: n =
m.
Following the terminology introduced in Logic, we call this
the "reflection principle for equality on numbers," and we say
that the boolean n =? m is reflected in the proposition n =
m.
Inductive reflect (P : Prop) : bool → Prop :=
| ReflectT (H : P) : reflect P true
| ReflectF (H : ¬ P) : reflect P false.
| 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. It states that the property P
reflects (intuitively, is 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 we can extract evidence for P from a proof of
reflect P true.
Similarly, the only way to show reflect P false is by tagging
evidence for ¬ P with the ReflectF constructor.
To put this observation to work, we first prove that the
statements P ↔ b = true and reflect P b are indeed
equivalent. First, the left-to-right implication:
Theorem iff_reflect : ∀ P b, (P ↔ b = true) → reflect P b.
Proof.
(* WORKED IN CLASS *)
intros P b H. destruct b eqn:Eb.
- apply ReflectT. rewrite H. reflexivity.
- apply ReflectF. rewrite H. intros H'. discriminate.
Qed.
Proof.
(* WORKED IN CLASS *)
intros P b H. destruct b eqn:Eb.
- apply ReflectT. rewrite H. reflexivity.
- apply ReflectF. rewrite H. intros H'. discriminate.
Qed.
Now you prove the right-to-left implication:
Exercise: 2 stars, standard, especially useful (reflect_iff)
Lemma eqbP : ∀ n m, reflect (n = m) (n =? m).
Proof.
intros n m. apply iff_reflect. rewrite eqb_eq. reflexivity.
Qed.
Proof.
intros n m. apply iff_reflect. rewrite eqb_eq. reflexivity.
Qed.
The proof of filter_not_empty_In now goes as follows. Notice
how the calls to destruct and rewrite in the earlier proof of
this theorem are combined here into a single call to
destruct.
(To see this clearly, execute 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' : ∀ n l,
filter (fun x ⇒ n =? x) l ≠ [] →
In n l.
Proof.
intros n l. induction l as [|m l' IHl'].
- (* l = *)
simpl. intros H. apply H. reflexivity.
- (* l = m :: l' *)
simpl. destruct (eqbP n m) as [H | H].
+ (* n = m *)
intros _. rewrite H. left. reflexivity.
+ (* n <> m *)
intros H'. right. apply IHl'. apply H'.
Qed.
filter (fun x ⇒ n =? x) l ≠ [] →
In n l.
Proof.
intros n l. induction l as [|m l' IHl'].
- (* l = *)
simpl. intros H. apply H. reflexivity.
- (* l = m :: l' *)
simpl. destruct (eqbP n m) as [H | H].
+ (* n = m *)
intros _. rewrite H. left. reflexivity.
+ (* n <> m *)
intros H'. right. apply IHl'. apply H'.
Qed.
Exercise: 3 stars, standard, especially useful (eqbP_practice)
Use eqbP as above to prove the following:
Fixpoint count n l :=
match l with
| [] ⇒ 0
| m :: l' ⇒ (if n =? m then 1 else 0) + count n l'
end.
Theorem eqbP_practice : ∀ n l,
count n l = 0 → ~(In n l).
Proof.
intros n l Hcount. induction l as [| m l' IHl'].
(* FILL IN HERE *) Admitted.
☐
match l with
| [] ⇒ 0
| m :: l' ⇒ (if n =? m then 1 else 0) + count n l'
end.
Theorem eqbP_practice : ∀ n l,
count n l = 0 → ~(In n l).
Proof.
intros n l Hcount. induction l as [| m l' IHl'].
(* FILL IN HERE *) Admitted.
☐
Additional Exercises
Exercise: 3 stars, standard, especially useful (nostutter_defn)
Formulating inductive definitions of properties is an important skill you'll need in this course. Try to solve this exercise without any help.
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.)
Example test_nostutter_1: nostutter [3;1;4;1;5;6].
(* FILL IN HERE *) Admitted.
(*
Proof. repeat constructor; apply eqb_neq; auto.
Qed.
*)
Example test_nostutter_2: nostutter (@nil nat).
(* FILL IN HERE *) Admitted.
(*
Proof. repeat constructor; apply eqb_neq; auto.
Qed.
*)
Example test_nostutter_3: nostutter [5].
(* FILL IN HERE *) Admitted.
(*
Proof. repeat constructor; auto. Qed.
*)
Example test_nostutter_4: not (nostutter [3;1;1;4]).
(* FILL IN HERE *) Admitted.
(*
Proof. intro.
repeat match goal with
h: nostutter _ ⊢ _ => inversion h; clear h; subst
end.
contradiction; auto. Qed.
*)
(* Do not modify the following line: *)
Definition manual_grade_for_nostutter : option (nat×string) := None.
☐
(* FILL IN HERE *) Admitted.
(*
Proof. repeat constructor; apply eqb_neq; auto.
Qed.
*)
Example test_nostutter_2: nostutter (@nil nat).
(* FILL IN HERE *) Admitted.
(*
Proof. repeat constructor; apply eqb_neq; auto.
Qed.
*)
Example test_nostutter_3: nostutter [5].
(* FILL IN HERE *) Admitted.
(*
Proof. repeat constructor; auto. Qed.
*)
Example test_nostutter_4: not (nostutter [3;1;1;4]).
(* FILL IN HERE *) Admitted.
(*
Proof. intro.
repeat match goal with
h: nostutter _ ⊢ _ => inversion h; clear h; subst
end.
contradiction; auto. Qed.
*)
(* Do not modify the following line: *)
Definition manual_grade_for_nostutter : option (nat×string) := None.
☐
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:[1;4;6;2;3] is an in-order 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 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.
Inductive merge {X:Type} : list X → list X → list X → Prop :=
(* FILL IN HERE *)
.
Theorem merge_filter : ∀ (X : Set) (test: X→bool) (l l1 l2 : list X),
merge l1 l2 l →
All (fun n ⇒ test n = true) l1 →
All (fun n ⇒ test n = false) l2 →
filter test l = l1.
Proof.
(* FILL IN HERE *) Admitted.
(* FILL IN HERE *)
☐
(* FILL IN HERE *)
.
Theorem merge_filter : ∀ (X : Set) (test: X→bool) (l l1 l2 : list X),
merge l1 l2 l →
All (fun n ⇒ test n = true) l1 →
All (fun n ⇒ test n = false) l2 →
filter test l = l1.
Proof.
(* FILL IN HERE *) Admitted.
(* FILL IN HERE *)
☐
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.
(* FILL IN HERE *)
☐
☐
Exercise: 4 stars, standard, optional (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 like
c : ∀ l, l = rev l → pal l may seem obvious, but will not work very well.) - Prove (pal_app_rev) that
∀ l, pal (l ++ rev l). - Prove (pal_rev that)
∀ l, pal l → l = rev l.
Inductive pal {X:Type} : list X → Prop :=
(* FILL IN HERE *)
.
Theorem pal_app_rev : ∀ (X:Type) (l : list X),
pal (l ++ (rev l)).
Proof.
(* FILL IN HERE *) Admitted.
Theorem pal_rev : ∀ (X:Type) (l: list X) , pal l → l = rev l.
Proof.
(* FILL IN HERE *) Admitted.
☐
(* FILL IN HERE *)
.
Theorem pal_app_rev : ∀ (X:Type) (l : list X),
pal (l ++ (rev l)).
Proof.
(* FILL IN HERE *) Admitted.
Theorem pal_rev : ∀ (X:Type) (l: list X) , pal l → l = rev l.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 5 stars, standard, 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∀ l, l = rev l → pal l.
Theorem palindrome_converse: ∀ {X: Type} (l: list X),
l = rev l → pal l.
Proof.
(* FILL IN HERE *) Admitted.
☐
l = rev l → pal l.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 4 stars, advanced, optional (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:
(* Fixpoint In (A : Type) (x : A) (l : list A) : Prop :=
match l with
| => False
| x' :: l' => x' = x \/ In A x l'
end *)
match l with
| => False
| x' :: l' => x' = x \/ In A x l'
end *)
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.
(* FILL IN HERE *)
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.
(* FILL IN HERE *)
Finally, state and prove one or more interesting theorems relating
disjoint, NoDup and ++ (list append).
(* FILL IN HERE *)
(* Do not modify the following line: *)
Definition manual_grade_for_NoDup_disjoint_etc : option (nat×string) := None.
☐
(* Do not modify the following line: *)
Definition manual_grade_for_NoDup_disjoint_etc : option (nat×string) := None.
☐
Exercise: 4 stars, advanced, optional (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...
Lemma in_split : ∀ (X:Type) (x:X) (l:list X),
In x l →
∃ l1 l2, l = l1 ++ x :: l2.
Proof.
(* FILL IN HERE *) Admitted.
In x l →
∃ l1 l2, l = l1 ++ x :: l2.
Proof.
(* FILL IN HERE *) Admitted.
Now define a property repeats such that repeats X l asserts
that l contains at least one repeated element (of type X).
Inductive repeats {X:Type} : list X → Prop :=
(* FILL IN HERE *)
.
(* Do not modify the following line: *)
Definition manual_grade_for_check_repeats : option (nat×string) := None.
(* FILL IN HERE *)
.
(* Do not modify the following line: *)
Definition manual_grade_for_check_repeats : option (nat×string) := None.
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.
Theorem pigeonhole_principle: excluded_middle →
∀ (X:Type) (l1 l2:list X),
(∀ x, In x l1 → In x l2) →
length l2 < length l1 →
repeats l1.
Proof.
intros EM X l1. induction l1 as [|x l1' IHl1'].
(* FILL IN HERE *) Admitted.
☐
∀ (X:Type) (l1 l2:list X),
(∀ x, In x l1 → In x l2) →
length l2 < length l1 →
repeats l1.
Proof.
intros EM X l1. induction l1 as [|x l1' IHl1'].
(* FILL IN HERE *) Admitted.
☐
Extended Exercise: A Verified Regular-Expression 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 equality-testing
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 regex-matching 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 : ∀ (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 : ∀ (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 : ∀ (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 : ∀ (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 non-empty string.
Lemma empty_nomatch_ne : ∀ (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.
Char a matches no string that starts with a non-a character.
Lemma char_nomatch_char :
∀ (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.
∀ (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.
If Char a matches a non-empty string, then the string's tail is empty.
Lemma char_eps_suffix : ∀ (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.
App re0 re1 matches string s iff s = s0 ++ s1, where s0
matches re0 and s1 matches re1.
Lemma app_exists : ∀ (s : string) re0 re1,
s =~ App re0 re1 ↔
∃ s0 s1, s = s0 ++ s1 ∧ s0 =~ re0 ∧ s1 =~ re1.
Proof.
intros.
split.
- intros. inversion H. ∃ 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 ↔
∃ s0 s1, s = s0 ++ s1 ∧ s0 =~ re0 ∧ s1 =~ re1.
Proof.
intros.
split.
- intros. inversion H. ∃ 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)
App re0 re1 matches a::s iff re0 matches the empty string and a::s matches re1 or s=s0++s1, where a::s0 matches re0 and s1 matches re1.
Lemma app_ne : ∀ (a : ascii) s re0 re1,
a :: s =~ (App re0 re1) ↔
([ ] =~ re0 ∧ a :: s =~ re1) ∨
∃ s0 s1, s = s0 ++ s1 ∧ a :: s0 =~ re0 ∧ s1 =~ re1.
Proof.
(* FILL IN HERE *) Admitted.
☐
a :: s =~ (App re0 re1) ↔
([ ] =~ re0 ∧ a :: s =~ re1) ∨
∃ s0 s1, s = s0 ++ s1 ∧ a :: s0 =~ re0 ∧ s1 =~ re1.
Proof.
(* FILL IN HERE *) Admitted.
☐
Lemma union_disj : ∀ (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)
a::s matches Star re iff s = s0 ++ s1, where a::s0 matches re and s1 matches Star re. Like app_ne, this observation is critical, so understand it, prove it, and keep it in mind.
Lemma star_ne : ∀ (a : ascii) s re,
a :: s =~ Star re ↔
∃ s0 s1, s = s0 ++ s1 ∧ a :: s0 =~ re ∧ s1 =~ Star re.
Proof.
(* FILL IN HERE *) Admitted.
☐
a :: s =~ Star re ↔
∃ s0 s1, s = s0 ++ s1 ∧ a :: s0 =~ re ∧ s1 =~ Star re.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 2 stars, standard, optional (match_eps)
Complete the definition of match_eps so that it tests if a given regex matches the empty string:
Fixpoint match_eps (re: reg_exp ascii) : bool
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
☐
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
☐
Exercise: 3 stars, standard, optional (match_eps_refl)
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.)
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)
Define derive so that it derives strings. One natural implementation uses match_eps in some cases to determine if key regex's match the empty string.
Fixpoint derive (a : ascii) (re : reg_exp ascii) : reg_exp ascii
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
☐
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
☐
"c" =~ EmptySet:
"c" =~ Char c:
"c" =~ Char d:
"c" =~ App (Char c) EmptyStr:
Example test_der3 : match_eps (derive c (App (Char c) EmptyStr)) = true.
Proof.
(* FILL IN HERE *) Admitted.
Proof.
(* FILL IN HERE *) Admitted.
"c" =~ App EmptyStr (Char c):
Example test_der4 : match_eps (derive c (App EmptyStr (Char c))) = true.
Proof.
(* FILL IN HERE *) Admitted.
Proof.
(* FILL IN HERE *) Admitted.
"c" =~ Star c:
Example test_der5 : match_eps (derive c (Star (Char c))) = true.
Proof.
(* FILL IN HERE *) Admitted.
Proof.
(* FILL IN HERE *) Admitted.
"cd" =~ App (Char c) (Char d):
Example test_der6 :
match_eps (derive d (derive c (App (Char c) (Char d)))) = true.
Proof.
(* FILL IN HERE *) Admitted.
match_eps (derive d (derive c (App (Char c) (Char d)))) = true.
Proof.
(* FILL IN HERE *) Admitted.
"cd" =~ App (Char d) (Char c):
Example test_der7 :
match_eps (derive d (derive c (App (Char d) (Char c)))) = false.
Proof.
(* FILL IN HERE *) Admitted.
match_eps (derive d (derive c (App (Char d) (Char c)))) = false.
Proof.
(* FILL IN HERE *) Admitted.
Exercise: 4 stars, standard, optional (derive_corr)
Prove that derive in fact always derives strings.
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)
Complete the definition of regex_match so that it matches regexes.
Fixpoint regex_match (s : string) (re : reg_exp ascii) : bool
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
☐
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
☐
Exercise: 3 stars, standard, optional (regex_match_correct)
Finally, prove that regex_match in fact matches regexes.
(* 2024-10-04 13:52 *)