# IndPropInductively Defined Propositions

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

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.
Fail Fixpoint reaches_1_in (n : nat) :=

if n =? 1 then 0

else 1 + reaches_1_in (f n).

if n =? 1 then 0

else 1 + reaches_1_in (f n).

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:
Conjecture collatz : ∀ n, reaches_1 n.

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.

Module LePlayground.

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.

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.

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.

## Permutations

*permutation*also has an elegant formulation as an inductive relation. For simplicity, let's focus on permutations of lists with exactly three elements.

Inductive Perm3 {X : Type} : list X → list X → Prop :=

| perm3_swap12 (a b c : X) :

Perm3 [a;b;c] [b;a;c]

| perm3_swap23 (a b c : X) :

Perm3 [a;b;c] [a;c;b]

| perm3_trans (l

Perm3 l

| perm3_swap12 (a b c : X) :

Perm3 [a;b;c] [b;a;c]

| perm3_swap23 (a b c : X) :

Perm3 [a;b;c] [a;c;b]

| perm3_trans (l

_{1}l_{2}l_{3}: list X) :Perm3 l

_{1}l_{2}→ Perm3 l_{2}l_{3}→ Perm3 l_{1}l_{3}.
This definition says:

- If l
_{2}can be obtained from l_{1}by swapping the first and second elements, then l_{2}is a permutation of l_{1}. - If l
_{2}can be obtained from l_{1}by swapping the second and third elements, then l_{2}is a permutation of l_{1}. - If l
_{2}is a permutation of l_{1}and l_{3}is a permutation of l_{2}, then l_{3}is a permutation of l_{1}.

## Evenness (yet again)

### We've already seen two ways of stating a proposition that a number n is even: We can say

*establish*its evenness from the following rules:

- The number 0 is even.
- If n is even, then S (S n) is even.

Inductive ev : nat → Prop :=

| ev_0 : ev 0

| ev_SS (n : nat) (H : ev n) : ev (S (S n)).

| ev_0 : ev 0

| ev_SS (n : nat) (H : ev n) : ev (S (S n)).

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

Theorem ev_4 : ev 4.

Proof. apply ev_SS. apply ev_SS. apply ev_0. Qed.

Proof. apply ev_SS. apply ev_SS. apply ev_0. Qed.

... or we can use function application syntax to combine several
constructors:

Theorem ev_4' : ev 4.

Proof. apply (ev_SS 2 (ev_SS 0 ev_0)). Qed.

Proof. apply (ev_SS 2 (ev_SS 0 ev_0)). Qed.

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.

### In other words, if someone gives us evidence E for the assertion ev n, then we know that E must be one of two things:

- 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*and even

*induction*on evidence of evenness...

## Inversion on Evidence

Theorem ev_inversion : ∀ (n : nat),

ev n →

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

Proof.

intros n E. destruct E as [ | n' E'] eqn:EE.

- (* E = ev_0 : ev 0 *)

left. reflexivity.

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

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

Qed.

ev n →

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

Proof.

intros n E. destruct E as [ | n' E'] eqn:EE.

- (* E = ev_0 : ev 0 *)

left. reflexivity.

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

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

Qed.

Facts like this are often called "inversion lemmas" because they
allow us to "invert" some given information to reason about all
the different ways it could have been derived.
Here, there are two ways to prove ev n, and the inversion lemma
makes this explicit.

Which tactics are needed to prove this goal?

n : nat

E : ev n

F : n = 1

======================

true = false
(1) destruct
(2) discriminate
(3) both destruct and discriminate
(4) These tactics are not sufficient to solve the goal.

n : nat

E : ev n

F : n = 1

======================

true = false

Lemma quiz_1_not_ev : ∀ n, ev n → n = 1 → true = false.

Proof.

intros n E F. destruct E as [| n' E'] eqn:EE.

- discriminate F.

- discriminate F.

Qed.

Proof.

intros n E F. destruct E as [| n' E'] eqn:EE.

- discriminate F.

- discriminate F.

Qed.

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.

### Coq provides a handy tactic called inversion that does the work of our inversion lemma and more besides.

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.

### We can use inversion to re-prove some theorems from Tactics.v. (Note that inversion also works on equality propositions.)

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.

### The tactic inversion actually works on any H : P where P is defined Inductively:

- For each constructor of P, make a subgoal where H is
constrained by the form of this constructor.
- Discard contradictory subgoals (such as ev_0 above).
- Generate auxiliary equalities (as with ev_SS above).

Which tactics are needed to prove this goal, in addition to
simpl and apply?

n : nat

E : ev (n + 2)

=====================

ev n
(1) inversion
(2) inversion, discriminate
(3) inversion, rewrite add_comm
(4) inversion, rewrite add_comm, discriminate
(5) These tactics are not sufficient to prove the goal.

n : nat

E : ev (n + 2)

=====================

ev n

Lemma quiz_ev_plus_2 : ∀ n, ev (n + 2) → ev n.

Proof.

intros n E. rewrite add_comm in E. inversion E. apply H

Qed.

Proof.

intros n E. rewrite add_comm in E. inversion E. apply H

_{0}.Qed.

Lemma ev_Even_firsttry : ∀ n,

ev n → Even n.

Proof.

(* WORK IN CLASS *) Admitted.

ev n → Even n.

Proof.

(* WORK IN CLASS *) Admitted.

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

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.

# Inductive Relations

*property*, a two-argument proposition defines a

*relation*.

Module Playground.

Just like properties, relations can be defined inductively. One
useful example is the "less than or equal to" relation on numbers
that we briefly saw above.

Inductive le : nat → nat → Prop :=

| le_n (n : nat) : le n n

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

Notation "n <= m" := (le n m).

| le_n (n : nat) : le n n

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

Notation "n <= m" := (le n m).

Theorem test_le

3 ≤ 3.

Proof.

(* WORK IN CLASS *) Admitted.

Theorem test_le

3 ≤ 6.

Proof.

(* WORK IN CLASS *) Admitted.

Theorem test_le

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

Proof.

(* WORK IN CLASS *) Admitted.

_{1}:3 ≤ 3.

Proof.

(* WORK IN CLASS *) Admitted.

Theorem test_le

_{2}:3 ≤ 6.

Proof.

(* WORK IN CLASS *) Admitted.

Theorem test_le

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

Proof.

(* WORK IN CLASS *) Admitted.

Definition lt (n m : nat) := le (S n) m.

Notation "m < n" := (lt m n).

Notation "m < n" := (lt m n).

End Playground.

# A Digression on Notation

Module bin1.

Inductive bin : Type :=

| Z

| B

| B

End bin1.

Inductive bin : Type :=

| Z

| B

_{0}(n : bin)| B

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

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

Module bin3.

Inductive bin : Type :=

| Z : bin

| B

| B

End bin3.

Inductive bin : Type :=

| Z : bin

| B

_{0}: bin → bin| B

_{1}: bin → bin.End bin3.

... where we put everything on the right of the colon.
For inductively defined

*propositions*, we need to explicitly give the result type for each constructor (because they are not all the same), so the first style doesn't make sense, but we can use either the second or the third interchangeably.# Case Study: Regular Expressions

Inductive reg_exp (T : Type) : Type :=

| EmptySet

| EmptyStr

| Char (t : T)

| App (r

| Union (r

| Star (r : reg_exp 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} _.

Arguments EmptyStr {T}.

Arguments Char {T} _.

Arguments App {T} _ _.

Arguments Union {T} _ _.

Arguments Star {T} _.

### We connect regular expressions and strings via the following rules, which define when a regular expression

*matches*some string:

- The expression EmptySet does not match any string.
- The expression EmptyStr matches the empty string [].
- The expression Char x matches the one-character string [x].
- If 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.

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

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 this clause in our informal definition...
... is not explicitly reflected in the above definition. Do we
need to add something?
(1) Yes, we should add a rule for this.
(2) No, one of the other rules already covers this case.
(3) No, the

- "The expression EmptySet does not match any string."

*lack*of a rule actually gives us the behavior we want.
Example reg_exp_ex

Example reg_exp_ex

Example reg_exp_ex

_{1}: [1] =~ Char 1.
Proof.

apply MChar.

Qed.

apply MChar.

Qed.

Example reg_exp_ex

_{2}: [1; 2] =~ App (Char 1) (Char 2).
Proof.

apply (MApp [1]).

- apply MChar.

- apply MChar.

Qed.

apply (MApp [1]).

- apply MChar.

- apply MChar.

Qed.

Example reg_exp_ex

_{3}: ¬([1; 2] =~ Char 1).
Proof.

intros H. inversion H.

Qed.

intros H. inversion H.

Qed.

Lemma MStar1 :

∀ T s (re : reg_exp T) ,

s =~ re →

s =~ Star re.

(* WORK IN CLASS *) Admitted.

∀ T s (re : reg_exp T) ,

s =~ re →

s =~ Star re.

(* WORK IN CLASS *) 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}.
A naive first attempt at setting up the induction. (Note
that we are performing induction on evidence!) (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}].
- (* 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.

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

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

The first subcase (where n =? m = true) is awkward
because we have to explicitly "switch worlds."
It would be annoying to have to do this kind of thing all the
time.
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

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

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

Notice that the only way to produce evidence for reflect P
true is by showing P and then using the ReflectT constructor.
If we play this reasoning backwards, it says we can extract
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:

*evidence*for P from evidence for reflect P true.
Theorem iff_reflect : ∀ P b, (P ↔ b = true) → reflect P b.

Proof.

(* WORK IN CLASS *) Admitted.

Proof.

(* WORK IN CLASS *) Admitted.

(The right-to-left implication is left as an exercise.)
We begin by recasting the eqb_eq lemma in terms of reflect:

### We can think of reflect as a kind of variant of the usual "if and only if" connective; the advantage of reflect is that, by destructing a hypothesis or lemma of the form reflect P b, we can perform case analysis on b while

*at the same time*generating appropriate hypothesis in the two branches (P in the first subgoal and ¬ P in the second).### Let's use reflect to produce a smoother proof of filter_not_empty_In.

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.

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.

### This small example shows reflection giving us a small gain in convenience; in larger developments, using reflect consistently can often lead to noticeably shorter and clearer proof scripts. We'll see many more examples in later chapters and in

*Programming Language Foundations*.

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