# IndPropInductively Defined Propositions

Set Warnings "-notation-overridden,-parsing".

From LF Require Export Logic.

Require Coq.omega.Omega.

From LF Require Export Logic.

Require Coq.omega.Omega.

# Inductively Defined Propositions

*inductive definitions*.

- Rule ev_0: The number 0 is even.
- Rule ev_SS: If n is even, then S (S n) is even.

*Inference rules*are one such notation:

(ev_0) | |

even 0 |

even n | (ev_SS) |

even (S (S n)) |

*premises*above the line all hold, then the

*conclusion*below the line follows. For example, the rule ev_SS says that, if n satisfies even, then S (S n) also does. If a rule has no premises above the line, then its conclusion holds unconditionally.

*proof tree*. Here's how we might transcribe the above proof that 4 is even:

-------- (ev_0)

even 0

-------- (ev_SS)

even 2

-------- (ev_SS)

even 4

even 0

-------- (ev_SS)

even 2

-------- (ev_SS)

even 4

## Inductive Definition of Evenness

This definition is different in several crucial respects 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
In contrast, recall the definition of list:
This definition names the X parameter

*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. The overall type of each constructor must be specified after a colon; each constructor type must have the form even n for some natural number n.
Inductive list (X:Type) : Type :=

| nil

| cons (x : X) (l : list X).

| nil

| cons (x : X) (l : list X).

*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 (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) := ..., 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 : ∀ n, even n → even (S (S n)).
That definition can equivalently be written as follows...
... 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...

Inductive even : nat → Prop :=

| ev_0 : even 0

| ev_SS : ∀n, even n → even (S (S n)).

| ev_0 : even 0

| ev_SS : ∀n, even n → even (S (S n)).

... or we can use function application syntax:

We can also prove theorems that have hypotheses involving even.

Theorem ev_plus4 : ∀n, even n → even (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

*constructing*evidence that numbers are even, we can also

*reason about*such evidence.

*only*ways to build evidence that numbers are even (in the sense of even).

- 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 even n').

*induction*and

*case analysis*on such evidence. Let's look at a few examples to see what this means in practice.

## Inversion on Evidence

*directly*. As a tool, we can prove our characterization of evidence for even n, using destruct.

Theorem ev_inversion :

∀(n : nat), even n →

(n = 0) ∨ (∃n', n = S (S n') ∧ even n').

Proof.

intros n E.

destruct E as [ | n' E'].

- (* E = ev_0 : even 0 *)

left. reflexivity.

- (* E = ev_SS n' E' : even (S (S n')) *)

right. ∃n'. split. reflexivity. apply E'.

Qed.

∀(n : nat), even n →

(n = 0) ∨ (∃n', n = S (S n') ∧ even n').

Proof.

intros n E.

destruct E as [ | n' E'].

- (* E = ev_0 : even 0 *)

left. reflexivity.

- (* E = ev_SS n' E' : even (S (S n')) *)

right. ∃n'. split. reflexivity. apply E'.

Qed.

The following theorem can easily be proved using destruct on
evidence.

Theorem ev_minus2 : ∀n,

even n → even (pred (pred n)).

Proof.

intros n E.

destruct E as [| n' E'].

- (* E = ev_0 *) simpl. apply ev_0.

- (* E = ev_SS n' E' *) simpl. apply E'.

Qed.

even n → even (pred (pred n)).

Proof.

intros n E.

destruct E as [| n' E'].

- (* E = ev_0 *) simpl. apply ev_0.

- (* E = ev_SS n' E' *) 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'].

- (* E = ev_0. *)

(* We must prove that n is even from no assumptions! *)

Abort.

intros n E.

destruct E as [| n' E'].

- (* E = ev_0. *)

(* We must prove that n is even from no assumptions! *)

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 : ∀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.

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' : ∀n,

even (S (S n)) → even n.

Proof.

intros n E.

inversion E as [| n' E' EQ].

(* We are in the E = ev_SS n' E' case now. *)

apply E'.

Qed.

even (S (S n)) → even n.

Proof.

intros n E.

inversion E as [| n' E' EQ].

(* 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 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)

Prove the following result using inversion. For extra practice, also prove it using the inversion lemma.
Theorem inversion_ex

[n; m] = [o; o] →

[n] = [m].

Proof.

intros n m o H. inversion H. reflexivity. Qed.

Theorem inversion_ex

S n = O →

2 + 2 = 5.

Proof.

intros n contra. inversion contra. Qed.

_{1}: ∀(n m o : nat),[n; m] = [o; o] →

[n] = [m].

Proof.

intros n m o H. inversion H. reflexivity. Qed.

Theorem inversion_ex

_{2}: ∀(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 self-contradictory; inversion throws
these away. The ones that are left represent the cases that must
be proved to establish the original goal. For those, inversion
adds all equations into the proof context that must hold of the
arguments given to P (e.g., S (S n') = n in the proof of
evSS_ev).
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, 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 even. Indeed, the first case can be solved trivially.
intros n E. inversion E as [EQ' | n' E' EQ'].

- (* E = ev_0 *)

∃0. reflexivity.

- (* E = ev_SS n' E' *) simpl.

- (* E = ev_0 *)

∃0. reflexivity.

- (* E = ev_SS n' E' *) simpl.

Unfortunately, the second case is harder. We need to show ∃
k, S (S n') = double k, but the only available assumption is
E', which states that 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
∃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 : (∃k', n' = double k') →

(∃k, S (S n') = double k)).

{ intros [k' Hk']. rewrite Hk'. ∃(S k'). reflexivity. }

apply I. (* reduce the original goal to the new one *)

Abort.

(∃k, S (S n') = double k)).

{ intros [k' Hk']. rewrite Hk'. ∃(S k'). reflexivity. }

apply I. (* reduce the original goal to the new one *)

Abort.

## Induction on Evidence

Lemma ev_even : ∀n,

even n → ∃k, n = double k.

Proof.

intros n E.

induction E as [|n' E' IH].

- (* E = ev_0 *)

∃0. reflexivity.

- (* E = ev_SS n' E'

with IH : exists k', n' = double k' *)

destruct IH as [k' Hk'].

rewrite Hk'. ∃(S k'). reflexivity.

Qed.

even n → ∃k, n = double k.

Proof.

intros n E.

induction E as [|n' E' IH].

- (* E = ev_0 *)

∃0. reflexivity.

- (* E = ev_SS n' E'

with IH : exists k', n' = double k' *)

destruct IH as [k' Hk'].

rewrite Hk'. ∃(S k'). reflexivity.

Qed.

Here, we can see that Coq produced an IH that corresponds
to E', the single recursive occurrence of 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 : ∀n,

even n ↔ ∃k, n = double k.

Proof.

intros n. split.

- (* -> *) apply ev_even.

- (* <- *) intros [k Hk]. rewrite Hk. apply ev_double.

Qed.

even n ↔ ∃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)

#### Exercise: 4 stars, advanced, optional (even'_ev)

In general, there may be multiple ways of defining a property inductively. For example, here's a (slightly contrived) alternative definition for even:
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).

| 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.
To streamline the proof, use the technique (from Logic) of
applying theorems to arguments, and note that the same technique
works with constructors of inductively defined propositions.

☐
#### Exercise: 3 stars, advanced, recommended (ev_ev__ev)

There are two pieces of evidence you could attempt to induct upon here. If one doesn't work, try the other.#### Exercise: 3 stars, standard, optional (ev_plus_plus)

This exercise just requires applying existing lemmas. No induction or even case analysis is needed, though some of the rewriting may be tedious.
Theorem ev_plus_plus : ∀n m p,

even (n+m) → even (n+p) → even (m+p).

Proof.

(* FILL IN HERE *) Admitted.

☐
even (n+m) → even (n+p) → even (m+p).

Proof.

(* FILL IN HERE *) Admitted.

# Inductive Relations

*property*— i.e., it defines a subset of nat, namely those numbers for which the proposition is provable. In the same way, a two-argument proposition can be thought of as a

*relation*— i.e., it defines a set of pairs for which the proposition is provable.

One useful example is the "less than or equal to" relation on
numbers.
The following definition should be fairly intuitive. It
says that there are two ways to give evidence that one number is
less than or equal to another: either observe that they are the
same number, or give evidence that the first is less than or equal
to the predecessor of the second.

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).

| 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_le

3 ≤ 3.

Proof.

(* WORKED IN CLASS *)

apply le_n. Qed.

Theorem test_le

3 ≤ 6.

Proof.

(* WORKED IN CLASS *)

apply le_S. apply le_S. apply le_S. apply le_n. Qed.

Theorem test_le

(2 ≤ 1) → 2 + 2 = 5.

Proof.

(* WORKED IN CLASS *)

intros H. inversion H. inversion H

_{1}:3 ≤ 3.

Proof.

(* WORKED IN CLASS *)

apply le_n. Qed.

Theorem test_le

_{2}:3 ≤ 6.

Proof.

(* WORKED IN CLASS *)

apply le_S. apply le_S. apply le_S. apply le_n. Qed.

Theorem test_le

_{3}:(2 ≤ 1) → 2 + 2 = 5.

Proof.

(* WORKED IN CLASS *)

intros H. inversion H. inversion H

_{2}. Qed.
The "strictly less than" relation n < m can now be defined
in terms of le.

Here are a few more simple relations on numbers:

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 (H: even (S n)) : next_even n (S n)

| ne_2 n (H:even (S (S n))) : next_even n (S (S n)).

| 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 (H: 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)

Define an inductive binary relation total_relation that holds between every pair of natural numbers.
(* FILL IN HERE *)

☐
#### Exercise: 2 stars, standard, optional (empty_relation)

Define an inductive binary relation empty_relation (on numbers) that never holds.
(* FILL IN HERE *)

☐
_{1}e

_{2}. Doing destruct H will generate two cases. In the first case, e

_{1}= e

_{2}, and it will replace instances of e

_{2}with e

_{1}in the goal and context. In the second case, e

_{2}= S n' for some n' for which le e

_{1}n' holds, and it will replace instances of e

_{2}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 e

_{2}is replaced with n'.

#### Exercise: 3 stars, standard, optional (le_exercises)

Here are a number of facts about the ≤ and < relations that we are going to need later in the course. The proofs make good practice exercises.
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 le_plus_l : ∀a b,

a ≤ a + b.

Proof.

(* FILL IN HERE *) Admitted.

Theorem plus_le : ∀n

n

n

Proof.

(* FILL IN HERE *) Admitted.

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 le_plus_l : ∀a b,

a ≤ a + b.

Proof.

(* FILL IN HERE *) Admitted.

Theorem plus_le : ∀n

_{1}n_{2}m,n

_{1}+ n_{2}≤ m →n

_{1}≤ m ∧ n_{2}≤ m.Proof.

(* FILL IN HERE *) Admitted.

Hint: the next one may be easiest to prove by induction on n.

Theorem add_le_cases : ∀n m p q,

n + m ≤ p + q → n ≤ p ∨ m ≤ q.

Proof.

(* FILL IN HERE *) Admitted.

Theorem lt_S : ∀n m,

n < m →

n < S m.

Proof.

(* FILL IN HERE *) Admitted.

Theorem plus_lt : ∀n

n

n

Proof.

(* FILL IN HERE *) Admitted.

Theorem leb_complete : ∀n m,

n <=? m = true → n ≤ m.

Proof.

(* FILL IN HERE *) Admitted.

n + m ≤ p + q → n ≤ p ∨ m ≤ q.

Proof.

(* FILL IN HERE *) Admitted.

Theorem lt_S : ∀n m,

n < m →

n < S m.

Proof.

(* FILL IN HERE *) Admitted.

Theorem plus_lt : ∀n

_{1}n_{2}m,n

_{1}+ n_{2}< m →n

_{1}< m ∧ n_{2}< m.Proof.

(* FILL IN HERE *) Admitted.

Theorem leb_complete : ∀n m,

n <=? m = true → n ≤ m.

Proof.

(* FILL IN HERE *) Admitted.

Hint: The next one may be easiest to prove by induction on m.

Hint: The next one can easily be proved without using induction.

Theorem leb_true_trans : ∀n m o,

n <=? m = true → m <=? o = true → n <=? o = true.

Proof.

(* FILL IN HERE *) Admitted.

☐
☐
n <=? m = true → m <=? o = true → n <=? o = true.

Proof.

(* FILL IN HERE *) Admitted.

#### Exercise: 3 stars, standard, recommended (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 :=

| c

| c

| c

| c

| c

| c

_{1}: R 0 0 0| c

_{2}m n o (H : R m n o) : R (S m) n (S o)| c

_{3}m n o (H : R m n o) : R m (S n) (S o)| c

_{4}m n o (H : R (S m) (S n) (S (S o))) : R m n o| c

_{5}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 c
_{5}from the definition of R, would the set of provable propositions change? Briefly (1 sentence) explain your answer. - If we dropped constructor c
_{4}from the definition of R, would the set of provable propositions change? Briefly (1 sentence) explain your answer.

(* Do not modify the following line: *)

Definition manual_grade_for_R_provability : option (nat*string) := None.

☐
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: 2 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 [1;1;1;2;2;3]

[1;2;7;3]

[5;6;1;9;9;2;7;3;8]

*not*a subsequence of any of the lists

[1;2]

[1;3]

[5;6;2;1;7;3;8].

[1;3]

[5;6;2;1;7;3;8].

- Define an inductive proposition subseq on list nat that
captures what it means to be a subsequence. (Hint: You'll need
three cases.)
- Prove subseq_refl that subsequence is reflexive, that is,
any list is a subsequence of itself.
- Prove subseq_app that for any lists l
_{1}, l_{2}, and l_{3}, if l_{1}is a subsequence of l_{2}, then l_{1}is also a subsequence of l_{2}++ l_{3}. - (Optional, harder) Prove subseq_trans that subsequence is
transitive — that is, if l
_{1}is a subsequence of l_{2}and l_{2}is a subsequence of l_{3}, then l_{1}is a subsequence of l_{3}. Hint: choose your induction carefully!

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 : ∀(l

subseq l

subseq l

Proof.

(* FILL IN HERE *) Admitted.

Theorem subseq_trans : ∀(l

subseq l

subseq l

subseq l

Proof.

(* FILL IN HERE *) Admitted.

☐
(* FILL IN HERE *)

.

Theorem subseq_refl : ∀(l : list nat), subseq l l.

Proof.

(* FILL IN HERE *) Admitted.

Theorem subseq_app : ∀(l

_{1}l_{2}l_{3}: list nat),subseq l

_{1}l_{2}→subseq l

_{1}(l_{2}++ l_{3}).Proof.

(* FILL IN HERE *) Admitted.

Theorem subseq_trans : ∀(l

_{1}l_{2}l_{3}: list nat),subseq l

_{1}l_{2}→subseq l

_{2}l_{3}→subseq l

_{1}l_{3}.Proof.

(* FILL IN HERE *) Admitted.

#### Exercise: 2 stars, standard, optional (R_provability2)

Suppose we give Coq the following definition:
Inductive R : nat → list nat → Prop :=

| c

| c

| c

Which of the following propositions are provable?
| c

_{1}: R 0 []| c

_{2}n l (H: R n l) : R (S n) (n :: l)| c

_{3}n l (H: R (S n) l) : R n l.- R 2 [1;0]
- R 1 [1;2;1;0]
- R 6 [3;2;1;0]

(* FILL IN HERE *)

☐
# Case Study: Regular Expressions

*regular expressions*.

Inductive reg_exp (T : Type) : Type :=

| EmptySet

| EmptyStr

| Char (t : T)

| App (r

| Union (r

| 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 (r

_{1}r_{2}: reg_exp T)| Union (r

_{1}r_{2}: 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
(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
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; by "reserving" the notation before
defining the Inductive, we can use it in the definition!

*polymorphic*: Regular expressions in reg_exp T describe strings with characters drawn from T — that is, lists of elements of T.*matches*some string:- The expression EmptySet does not match any string.
- The expression EmptyStr matches the empty string [].
- The expression Char x matches the one-character string [x].
- If re
_{1}matches s_{1}, and re_{2}matches s_{2}, then App re_{1}re_{2}matches s_{1}++ s_{2}. - If at least one of re
_{1}and re_{2}matches s, then Union re_{1}re_{2}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 s

(H

(H

(s

| MUnionL s

(H

s

| MUnionR re

(H

s

| MStar0 re : [] =~ (Star re)

| MStarApp s

(H

(H

(s

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 s

_{1}re_{1}s_{2}re_{2}(H

_{1}: s_{1}=~ re_{1})(H

_{2}: s_{2}=~ re_{2}) :(s

_{1}++ s_{2}) =~ (App re_{1}re_{2})| MUnionL s

_{1}re_{1}re_{2}(H

_{1}: s_{1}=~ re_{1}) :s

_{1}=~ (Union re_{1}re_{2})| MUnionR re

_{1}s_{2}re_{2}(H

_{2}: s_{2}=~ re_{2}) :s

_{2}=~ (Union re_{1}re_{2})| MStar0 re : [] =~ (Star re)

| MStarApp s

_{1}s_{2}re(H

_{1}: s_{1}=~ re)(H

_{2}: s_{2}=~ (Star re)) :(s

_{1}++ s_{2}) =~ (Star re)where "s =~ re" := (exp_match s re).

Again, for readability, we can also display this definition using
inference-rule notation.

Notice that these rules are not
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_ex
Let's illustrate these rules with a few examples.

(MEmpty) | |

[] =~ EmptyStr |

(MChar) | |

[x] =~ Char x |

s_{1} =~ re_{1} s_{2} =~ re_{2} |
(MApp) |

s_{1} ++ s_{2} =~ App re_{1} re_{2} |

s_{1} =~ re_{1} |
(MUnionL) |

s_{1} =~ Union re_{1} re_{2} |

s_{2} =~ re_{2} |
(MUnionR) |

s_{2} =~ Union re_{1} re_{2} |

(MStar0) | |

[] =~ Star re |

s_{1} =~ re s_{2} =~ Star re |
(MStarApp) |

s_{1} ++ s_{2} =~ Star re |

*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.")_{1}and exp_match_ex_{2}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.)
(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_ex

match l with

| [] ⇒ EmptyStr

| x :: l' ⇒ App (Char x) (reg_exp_of_list l')

end.

Example reg_exp_ex

_{4}: [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 same shape expected by MStarApp.)
#### Exercise: 3 stars, standard (exp_match_ex

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_ex_{1})

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) (re

s =~ re

s =~ Union re

Proof.

(* FILL IN HERE *) Admitted.

¬(s =~ EmptySet).

Proof.

(* FILL IN HERE *) Admitted.

Lemma MUnion' : ∀T (s : list T) (re

_{1}re_{2}: reg_exp T),s =~ re

_{1}∨ s =~ re_{2}→s =~ Union re

_{1}re_{2}.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 s

_{1}, ..., 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.

#### Exercise: 4 stars, standard, optional (reg_exp_of_list_spec)

Prove that reg_exp_of_list satisfies the following specification:
Lemma reg_exp_of_list_spec : ∀T (s

s

Proof.

(* FILL IN HERE *) Admitted.

☐
_{1}s_{2}: list T),s

_{1}=~ reg_exp_of_list s_{2}↔ s_{1}= s_{2}.Proof.

(* FILL IN HERE *) Admitted.

Fixpoint re_chars {T} (re : reg_exp T) : list T :=

match re with

| EmptySet ⇒ []

| EmptyStr ⇒ []

| Char x ⇒ [x]

| App re

| Union re

| Star re ⇒ re_chars re

end.

(* Sooner: BCP: Recheck the HIDEFROMHTML stuff around here... *)

match re with

| EmptySet ⇒ []

| EmptyStr ⇒ []

| Char x ⇒ [x]

| App re

_{1}re_{2}⇒ re_chars re_{1}++ re_chars re_{2}| Union re

_{1}re_{2}⇒ re_chars re_{1}++ re_chars re_{2}| Star re ⇒ re_chars re

end.

(* Sooner: BCP: Recheck the HIDEFROMHTML stuff around here... *)

We can then phrase our theorem as follows:

Theorem in_re_match : ∀T (s : list T) (re : reg_exp T) (x : T),

s =~ re →

In x s →

In x (re_chars re).

Proof.

intros T s re x Hmatch Hin.

induction Hmatch

as [| x'

| s

| s

| re | s

(* 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'

| s

_{1}re_{1}s_{2}re_{2}Hmatch1 IH_{1}Hmatch2 IH_{2}| s

_{1}re_{1}re_{2}Hmatch IH | re_{1}s_{2}re_{2}Hmatch IH| re | s

_{1}s_{2}re Hmatch1 IH_{1}Hmatch2 IH_{2}].(* 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 s_{1}(which matches re_{1}), and a second one that applies when x occurs in s_{2}(which matches re_{2}).
simpl. rewrite In_app_iff in *.

destruct Hin as [Hin | Hin].

+ (* In x s

left. apply (IH

+ (* In x s

right. apply (IH

- (* 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 s

_{1}*)left. apply (IH

_{1}Hin).+ (* In x s

_{2}*)right. apply (IH

_{2}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 s

_{2}.
rewrite In_app_iff in Hin.

destruct Hin as [Hin | Hin].

+ (* In x s

apply (IH

+ (* In x s

apply (IH

Qed.

destruct Hin as [Hin | Hin].

+ (* In x s

_{1}*)apply (IH

_{1}Hin).+ (* In x s

_{2}*)apply (IH

_{2}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 (s

s

s

s

Proof.

intros T s

_{1}s_{2}: list T) (re : reg_exp T),s

_{1}=~ Star re →s

_{2}=~ Star re →s

_{1}++ s_{2}=~ Star re.Proof.

intros T s

_{1}s_{2}re H_{1}.
Just doing an inversion on H

_{1}won't get us very far in the recursive cases. (Try it!). So we need induction (on evidence!). Here is a naive first attempt:
generalize dependent s

induction H

as [|x'|s

|s

|re''|s

_{2}.induction H

_{1}as [|x'|s

_{1}re_{1}s_{2}' re_{2}Hmatch1 IH_{1}Hmatch2 IH_{2}|s

_{1}re_{1}re_{2}Hmatch IH|re_{1}s_{2}' re_{2}Hmatch IH|re''|s

_{1}s_{2}' re'' Hmatch1 IH_{1}Hmatch2 IH_{2}].
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 H

_{1}: the fact that s_{1}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 s

simpl. intros s

_{2}H. apply H.
... but most cases get stuck. For MChar, for instance, we
must show that

s

which is clearly impossible.
_{2}=~ Char x' → x' :: s_{2}=~ Char x',
- (* MChar. *) intros s

Abort.

_{2}H. simpl. (* Stuck... *)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
destruct-without-eqn: 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: ∀T (s

re' = Star re →

s

s

s

_{1}s_{2}: list T) (re re' : reg_exp T),re' = Star re →

s

_{1}=~ re' →s

_{2}=~ Star re →s

_{1}++ s_{2}=~ 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: ∀T (s

s

s

s

Proof.

intros T s

remember (Star re) as re'.

_{1}s_{2}: list T) (re : reg_exp T),s

_{1}=~ Star re →s

_{2}=~ Star re →s

_{1}++ s_{2}=~ Star re.Proof.

intros T s

_{1}s_{2}re H_{1}.remember (Star re) as re'.

We now have Heqre' : re' = Star re.

generalize dependent s

induction H

as [|x'|s

|s

|re''|s

_{2}.induction H

_{1}as [|x'|s

_{1}re_{1}s_{2}' re_{2}Hmatch1 IH_{1}Hmatch2 IH_{2}|s

_{1}re_{1}re_{2}Hmatch IH|re_{1}s_{2}' re_{2}Hmatch IH|re''|s

_{1}s_{2}' re'' Hmatch1 IH_{1}Hmatch2 IH_{2}].
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 IH

_{2}on the MStarApp case mentions an additional premise Star re'' = Star re, which results from the equality generated by remember.
- (* MStar0 *)

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

- (* MStarApp *)

injection Heqre'. intros H

intros s

apply MStarApp.

+ apply Hmatch1.

+ apply IH

* rewrite H

* apply H

Qed.

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

- (* MStarApp *)

injection Heqre'. intros H

_{0}.intros s

_{2}H_{1}. rewrite <- app_assoc.apply MStarApp.

+ apply Hmatch1.

+ apply IH

_{2}.* rewrite H

_{0}. reflexivity.* apply H

_{1}.Qed.

#### Exercise: 4 stars, standard, optional (exp_match_ex_{2})

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 (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.

Module Pumping.

Fixpoint pumping_constant {T} (re : reg_exp T) : nat :=

match re with

| EmptySet ⇒ 0

| EmptyStr ⇒ 1

| Char _ ⇒ 2

| App re

pumping_constant re

| Union re

pumping_constant re

| Star _ ⇒ 1

end.

Fixpoint pumping_constant {T} (re : reg_exp T) : nat :=

match re with

| EmptySet ⇒ 0

| EmptyStr ⇒ 1

| Char _ ⇒ 2

| App re

_{1}re_{2}⇒pumping_constant re

_{1}+ pumping_constant re_{2}| Union re

_{1}re_{2}⇒pumping_constant re

_{1}+ pumping_constant re_{2}| 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: ∀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.

match n with

| 0 ⇒ []

| S n' ⇒ l ++ napp n' l

end.

Lemma napp_plus: ∀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 s

_{1}++ s_{2}++ s_{3}in such a way that s_{2}can be repeated any number of times and the result, when combined with s_{1}and s_{3}will still match re. Since s_{2}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 : ∀T (re : reg_exp T) s,

s =~ re →

pumping_constant re ≤ length s →

∃s

s = s

s

∀m, s

s =~ re →

pumping_constant re ≤ length s →

∃s

_{1}s_{2}s_{3},s = s

_{1}++ s_{2}++ s_{3}∧s

_{2}≠ [] ∧∀m, s

_{1}++ napp m s_{2}++ s_{3}=~ re.
You are to fill in the proof. Several of the lemmas about
le that were in an optional exercise earlier in this chapter
may be useful.

Proof.

intros T re s Hmatch.

induction Hmatch

as [ | x | s

| s

| re | s

- (* MEmpty *)

simpl. intros contra. inversion contra.

(* FILL IN HERE *) Admitted.

End Pumping.

☐
intros T re s Hmatch.

induction Hmatch

as [ | x | s

_{1}re_{1}s_{2}re_{2}Hmatch1 IH_{1}Hmatch2 IH_{2}| s

_{1}re_{1}re_{2}Hmatch IH | re_{1}s_{2}re_{2}Hmatch IH| re | s

_{1}s_{2}re Hmatch1 IH_{1}Hmatch2 IH_{2}].- (* 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 by defining an inductive proposition that
yields a better case-analysis 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.

| 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
It is easy to formalize this intuition and show that the
statements P ↔ b = true and reflect P b are indeed
equivalent. First, the left-to-right implication:

*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.
Theorem iff_reflect : ∀P b, (P ↔ b = true) → reflect P b.

Proof.

(* WORKED IN CLASS *)

intros P b H. destruct b.

- apply ReflectT. rewrite H. reflexivity.

- apply ReflectF. rewrite H. intros H'. discriminate.

Qed.

☐
Proof.

(* WORKED IN CLASS *)

intros P b H. destruct b.

- apply ReflectT. rewrite H. reflexivity.

- apply ReflectF. rewrite H. intros H'. discriminate.

Qed.

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.

A smoother proof of filter_not_empty_In now goes as follows.
Notice how the calls to destruct and rewrite 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' : ∀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.

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.

(* 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.

(* FILL IN HERE *) Admitted.

*Programming Language Foundations*.

*SSReflect*, a Coq library that has been used to formalize important results in mathematics, including as the 4-color theorem and the Feit-Thompson theorem. The name SSReflect stands for

*small-scale reflection*, i.e., the pervasive use of reflection to simplify small proof steps with boolean computations.

# Additional Exercises

#### Exercise: 3 stars, standard, recommended (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 at all.
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; apply eqb_false; 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; apply eqb_false; 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}and l

_{2}if it contains all the same elements as l

_{1}and l

_{2}, in the same order as l

_{1}and l

_{2}, but possibly interleaved. For example,

[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, l_{1}and l

_{2}, such that every item in l

_{1}satisfies test and no item in l

_{2}satisfies test. Then filter test l = l

_{1}.

(* FILL IN HERE *)

(* Do not modify the following line: *)

Definition manual_grade_for_filter_challenge : option (nat*string) := None.

☐
(* Do not modify the following line: *)

Definition manual_grade_for_filter_challenge : option (nat*string) := None.

#### 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 lmay 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.

(* FILL IN HERE *)

(* Do not modify the following line: *)

Definition manual_grade_for_pal_pal_app_rev_pal_rev : option (nat*string) := None.

☐
(* Do not modify the following line: *)

Definition manual_grade_for_pal_pal_app_rev_pal_rev : option (nat*string) := None.

#### 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.

(* FILL IN HERE *)

☐
#### 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
l

_{1}l_{2}, which should be provable exactly when l_{1}and l_{2}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 →

∃l

Proof.

(* FILL IN HERE *) Admitted.

In x l →

∃l

_{1}l_{2}, l = l_{1}++ x :: l_{2}.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).

Now, here's a way to formalize the pigeonhole principle. Suppose
list l
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

_{2}represents a list of pigeonhole labels, and list l_{1}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 l_{1}must contain repeats.*without*assuming that In is decidable; if you manage to do this, you will not need the excluded_middle hypothesis.
Theorem pigeonhole_principle: ∀(X:Type) (l

excluded_middle →

(∀x, In x l

length l

repeats l

Proof.

intros X l

(* FILL IN HERE *) Admitted.

(* Do not modify the following line: *)

Definition manual_grade_for_check_repeats : option (nat*string) := None.

☐
_{1}l_{2}:list X),excluded_middle →

(∀x, In x l

_{1}→ In x l_{2}) →length l

_{2}< length l_{1}→repeats l

_{1}.Proof.

intros X l

_{1}. induction l_{1}as [|x l_{1}' IHl1'].(* FILL IN HERE *) Admitted.

(* Do not modify the following line: *)

Definition manual_grade_for_check_repeats : option (nat*string) := None.

## 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 H

Qed.

Proof.

intros.

split.

- apply H.

- intros. destruct H

_{0}.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 H

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 H

_{0}.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 re

_{0}re_{1}matches string s iff s = s_{0}++ s_{1}, where s_{0}matches re_{0}and s_{1}matches re_{1}.
Lemma app_exists : ∀(s : string) re

s =~ App re

∃s

Proof.

intros.

split.

- intros. inversion H. ∃s

* reflexivity.

* split. apply H

- intros [ s

rewrite Happ. apply (MApp s

Qed.

_{0}re_{1},s =~ App re

_{0}re_{1}↔∃s

_{0}s_{1}, s = s_{0}++ s_{1}∧ s_{0}=~ re_{0}∧ s_{1}=~ re_{1}.Proof.

intros.

split.

- intros. inversion H. ∃s

_{1}, s_{2}. split.* reflexivity.

* split. apply H

_{3}. apply H_{4}.- intros [ s

_{0}[ s_{1}[ Happ [ Hmat0 Hmat1 ] ] ] ].rewrite Happ. apply (MApp s

_{0}_ s_{1}_ Hmat0 Hmat1).Qed.

#### Exercise: 3 stars, standard, optional (app_ne)

App re_{0}re

_{1}matches a::s iff re

_{0}matches the empty string and a::s matches re

_{1}or s=s

_{0}++s

_{1}, where a::s

_{0}matches re

_{0}and s

_{1}matches re

_{1}.

Lemma app_ne : ∀(a : ascii) s re

a :: s =~ (App re

([ ] =~ re

∃s

Proof.

(* FILL IN HERE *) Admitted.

☐
_{0}re_{1},a :: s =~ (App re

_{0}re_{1}) ↔([ ] =~ re

_{0}∧ a :: s =~ re_{1}) ∨∃s

_{0}s_{1}, s = s_{0}++ s_{1}∧ a :: s_{0}=~ re_{0}∧ s_{1}=~ re_{1}.Proof.

(* FILL IN HERE *) Admitted.

_{0}re

_{1}iff s matches re

_{0}or s matches re

_{1}.

Lemma union_disj : ∀(s : string) re

s =~ Union re

Proof.

intros. split.

- intros. inversion H.

+ left. apply H

+ right. apply H

- intros [ H | H ].

+ apply MUnionL. apply H.

+ apply MUnionR. apply H.

Qed.

_{0}re_{1},s =~ Union re

_{0}re_{1}↔ s =~ re_{0}∨ s =~ re_{1}.Proof.

intros. split.

- intros. inversion H.

+ left. apply H

_{2}.+ right. apply H

_{1}.- 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 = s_{0}++ s

_{1}, where a::s

_{0}matches re and s

_{1}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 ↔

∃s

Proof.

(* FILL IN HERE *) Admitted.

☐
a :: s =~ Star re ↔

∃s

_{0}s_{1}, s = s_{0}++ s_{1}∧ a :: s_{0}=~ re ∧ s_{1}=~ 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._{0}re

_{1}) to a Boolean combination of Prop's over simple regex's (e.g., s =~ re

_{0}∨ s =~ re

_{1}) using lemmas given above that are logical equivalences. You can then reason about these Prop's naturally using intro and destruct.

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_refl)

Finally, prove that regex_match in fact matches regexes.
(* Fri 30 Aug 2019 02:44:46 PM CEST *)