# IndPropInductively Defined Propositions

Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".

From LF Require Export Logic.

From Coq Require Import Lia.

From LF Require Export Logic.

From Coq Require Import Lia.

# Inductively Defined Propositions

*inductively defined propositions*.

## The Collatz Conjecture

*Collatz Conjecture*is a famous open problem in number theory.

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: Does the sequence starting from
To formalize this question in Coq, we might try to define a
recursive

*any*natural number eventually reach 1?*function*that computes 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 silly limitation of the termination
checker. Functions in Coq are required to be total, and checking
that 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 reaches_1 : nat → Prop :=

| term_done : reaches_1 1

| term_more (n : nat) : reaches_1 (f n) → reaches_1 n.

| term_done : reaches_1 1

| term_more (n : nat) : reaches_1 (f n) → reaches_1 n.

The details of such definitions are written will be explained
below; for the moment, the way to read this one is: "The number
1 reaches 1, and any number n reaches 1 if f n does."
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!

## Transitive Closure

*relation*on a set X is a family of propositions parameterized by two elements of X -- i.e., a proposition about pairs of elements of X.

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

End LePlayground.

| le_n (n : nat) : le n n

| le_S (n m : nat) : le n m → le n (S m).

End LePlayground.

The

*transitive closure*of a relation R is the smallest relation that contains R and that is transitive.
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.

## Evenness (yet again)

*establish*its evenness from the following rules:

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

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

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

*destruct*such evidence, reasoning about how it could have been built.

*only*ways to build evidence that numbers are ev.

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

*case analysis*or by

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

## Inversion on Evidence

*directly*.

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

- discriminate H

- destruct H

rewrite Heq. apply Hev.

Qed.

Proof.

intros n H. apply ev_inversion in H. destruct H as [H

_{0}|H_{1}].- discriminate H

_{0}.- destruct H

_{1}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_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.
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., S (S 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 ∃
n
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

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

_{0}, S (S n') = double n_{0}, 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.*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.

assert (H: (∃ k', n' = double k')

→ (∃ n

{ intros [k' EQ'']. ∃ (S k'). simpl.

rewrite <- EQ''. reflexivity. }

apply H.

→ (∃ n

_{0}, S (S n') = double n_{0})).{ 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 E' *)

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 E' *)

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)

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.

☐

_{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: 5 stars, standard (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 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 : ∀ n

n

n

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

_{1}n_{2}m,n

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

_{1}≤ m ∧ n_{2}≤ 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 : ∀ n

n

n

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

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.

☐

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

Inductive subseq : list nat → list nat → Prop :=

| sub_nil l : subseq [] l

| sub_take x l

| sub_skip x l

.

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.

(* Hint: be careful about what you are doing induction on and which

other things need to be generalized... *)

(* FILL IN HERE *) Admitted.

| sub_nil l : subseq [] l

| sub_take x l

_{1}l_{2}(H : subseq l_{1}l_{2}) : subseq (x :: l_{1}) (x :: l_{2})| sub_skip x l

_{1}l_{2}(H : subseq l_{1}l_{2}) : subseq l_{1}(x :: l_{2}).

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.

(* Hint: be careful about what you are doing induction on and which

other things need to be generalized... *)

(* FILL IN HERE *) Admitted.

# A Digression on Notation

... which omits the result types because they are all bin.
It is completely equivalent to this...

Module bin2.

Inductive bin : Type :=

| Z : bin

| B

| B

End bin2.

Inductive bin : Type :=

| Z : bin

| B

_{0}(n : bin) : bin| B

_{1}(n : bin) : bin.End bin2.

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

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

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.

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

☐

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.

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.

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'

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

Fixpoint re_not_empty {T : Type} (re : reg_exp T) : bool :=

match re with

| EmptySet ⇒ false

| EmptyStr ⇒ true

| Char _ ⇒ true

| App re

| Union re

| Star re ⇒ true

end.

Lemma re_not_empty_correct : ∀ T (re : reg_exp T),

(∃ s, s =~ re) ↔ re_not_empty re = true.

Proof.

(* FILL IN HERE *) Admitted.

☐

match re with

| EmptySet ⇒ false

| EmptyStr ⇒ true

| Char _ ⇒ true

| App re

_{1}re_{2}⇒ (re_not_empty re_{1}) && (re_not_empty re_{2})| Union re

_{1}re_{2}⇒ (re_not_empty re_{1}) || (re_not_empty re_{2})| Star re ⇒ true

end.

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}.
Now, 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. (We can begin by generalizing s_{2}, since it's pretty clear that we are going to have to walk over both s_{1}and s_{2}in parallel.)
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

s

x'::s

s

_{2}=~ Char x' →x'::s

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

Abort.

_{2}H. simpl. (* Stuck... *)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 (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 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 (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' as Heqre''. intros s H. apply H.

- (* MStarApp *)

injection Heqre' as Heqre''.

intros s

apply MStarApp.

+ apply Hmatch1.

+ apply IH

× rewrite Heqre''. reflexivity.

× apply H

Qed.

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

- (* MStarApp *)

injection Heqre' as Heqre''.

intros s

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

+ apply Hmatch1.

+ apply IH

_{2}.× rewrite Heqre''. reflexivity.

× apply H

_{1}.Qed.

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

pumping_constant re

| Union re

pumping_constant re

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

apply IHre1. apply le_plus_l.

- (* Union *)

simpl.

apply le_trans with (n:=pumping_constant re

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 re

_{1}).apply IHre1. apply le_plus_l.

- (* Union *)

simpl.

apply le_trans with (n:=pumping_constant re

_{1}).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 (Hp

{ apply pumping_constant_ge_1. }

inversion Hp

- rewrite H in Hp

- rewrite H in Hp

Qed.

intros T re H.

assert (Hp

_{1}: pumping_constant re ≥ 1).{ apply pumping_constant_ge_1. }

inversion Hp

_{1}as [Hp_{1}'| p Hp_{1}' Hp_{1}''].- rewrite H in Hp

_{1}'. discriminate Hp_{1}'.- rewrite H in Hp

_{1}''. discriminate Hp_{1}''.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 s

s

napp m s

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 s

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

_{1}=~ re → s_{2}=~ Star re →napp m s

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

| s

| re | s

- (* MEmpty *)

simpl. intros contra. inversion contra.

(* FILL IN HERE *) Admitted.

☐

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.

☐

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

*reflects*(intuitively, is equivalent to) the boolean b: that is, P holds if and only if b = true.
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)

*at the same time*generating appropriate hypothesis in the two branches (P in the first subgoal and ¬ P in the second).

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.

☐

*Programming Language Foundations*.

*SSReflect*, a Coq library that has been used to formalize important results in mathematics, including 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 by turning them into boolean computations.

(* 2022-08-22 10:32 *)