IndPropInductively Defined Propositions
Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
From LF Require Export Logic.
Inductively Defined Propositions
The Collatz Conjecture
Fixpoint div2 (n : nat) :=
match n with
0 ⇒ 0
| 1 ⇒ 0
| S (S n) ⇒ S (div2 n)
end.
Definition f (n : nat) :=
if even n then div2 n
else (3 × n) + 1.
match n with
0 ⇒ 0
| 1 ⇒ 0
| S (S n) ⇒ S (div2 n)
end.
Definition f (n : nat) :=
if even n then div2 n
else (3 × n) + 1.
Next, we look at what happens when we repeatedly apply f to some
given starting number. For example, f 12 is 6, and f 6 is
3, so by repeatedly applying f we get the sequence 12, 6, 3,
10, 5, 16, 8, 4, 2, 1.
Similarly, if we start with 19, we get the longer sequence 19,
58, 29, 88, 44, 22, 11, 34, 17, 52, 26, 13, 40, 20, 10, 5, 16, 8,
4, 2, 1.
Both of these sequences eventually reach 1. The question posed
by Collatz was: Does the sequence starting from any natural
number eventually reach 1?
To formalize this question in Coq, we might try to define a
recursive 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
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
Inductive Perm3 {X : Type} : list X → list X → Prop :=
| perm3_swap12 (a b c : X) :
Perm3 [a;b;c] [b;a;c]
| perm3_swap23 (a b c : X) :
Perm3 [a;b;c] [a;c;b]
| perm3_trans (l1 l2 l3 : list X) :
Perm3 l1 l2 → Perm3 l2 l3 → Perm3 l1 l3.
| perm3_swap12 (a b c : X) :
Perm3 [a;b;c] [b;a;c]
| perm3_swap23 (a b c : X) :
Perm3 [a;b;c] [a;c;b]
| perm3_trans (l1 l2 l3 : list X) :
Perm3 l1 l2 → Perm3 l2 l3 → Perm3 l1 l3.
This definition says:
- If l2 can be obtained from l1 by swapping the first and second elements, then l2 is a permutation of l1.
- If l2 can be obtained from l1 by swapping the second and third elements, then l2 is a permutation of l1.
- If l2 is a permutation of l1 and l3 is a permutation of l2, then l3 is a permutation of l1.
Evenness (yet again)
We've already seen two ways of stating a proposition that a number n is even: We can say
- 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
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').
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 [H0|H1].
- discriminate H0.
- destruct H1 as [n' [Hnm Hev]]. injection Hnm as Heq.
rewrite Heq. apply Hev.
Qed.
Proof.
intros n H. apply ev_inversion in H. destruct H as [H0|H1].
- discriminate H0.
- destruct H1 as [n' [Hnm Hev]]. injection Hnm as Heq.
rewrite Heq. apply Hev.
Qed.
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_ex1 : ∀ (n m o : nat),
[n; m] = [o; o] → [n] = [m].
Proof.
intros n m o H. inversion H. reflexivity. Qed.
Theorem inversion_ex2 : ∀ (n : nat),
S n = O → 2 + 2 = 5.
Proof.
intros n contra. inversion contra. Qed.
[n; m] = [o; o] → [n] = [m].
Proof.
intros n m o H. inversion H. reflexivity. Qed.
Theorem inversion_ex2 : ∀ (n : nat),
S n = O → 2 + 2 = 5.
Proof.
intros n contra. inversion contra. Qed.
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 H0.
Qed.
Proof.
intros n E. rewrite add_comm in E. inversion E. apply H0.
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 n' *)
unfold Even in IH.
destruct IH as [k Hk].
rewrite Hk.
unfold Even. ∃ (S k). simpl. reflexivity.
Qed.
ev n → Even n.
Proof.
intros n E.
induction E as [|n' E' IH].
- (* E = ev_0 *)
unfold Even. ∃ 0. reflexivity.
- (* E = ev_SS n' E'
with IH : Even n' *)
unfold Even in IH.
destruct IH as [k Hk].
rewrite Hk.
unfold Even. ∃ (S k). simpl. reflexivity.
Qed.
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
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_le1 :
3 ≤ 3.
Proof.
(* WORK IN CLASS *) Admitted.
Theorem test_le2 :
3 ≤ 6.
Proof.
(* WORK IN CLASS *) Admitted.
Theorem test_le3 :
(2 ≤ 1) → 2 + 2 = 5.
Proof.
(* WORK IN CLASS *) Admitted.
3 ≤ 3.
Proof.
(* WORK IN CLASS *) Admitted.
Theorem test_le2 :
3 ≤ 6.
Proof.
(* WORK IN CLASS *) Admitted.
Theorem test_le3 :
(2 ≤ 1) → 2 + 2 = 5.
Proof.
(* WORK IN CLASS *) Admitted.
Definition lt (n m : nat) := le (S n) m.
Notation "n < m" := (lt n m).
Notation "n < m" := (lt n m).
End Playground.
A Digression on Notation
Module bin1.
Inductive bin : Type :=
| Z
| B0 (n : bin)
| B1 (n : bin).
End bin1.
Inductive bin : Type :=
| Z
| B0 (n : bin)
| B1 (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
| B0 (n : bin) : bin
| B1 (n : bin) : bin.
End bin2.
Inductive bin : Type :=
| Z : bin
| B0 (n : bin) : bin
| B1 (n : bin) : bin.
End bin2.
... where we fill them in, and this...
Module bin3.
Inductive bin : Type :=
| Z : bin
| B0 : bin → bin
| B1 : bin → bin.
End bin3.
Inductive bin : Type :=
| Z : bin
| B0 : bin → bin
| B1 : 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 (r1 r2 : reg_exp T)
| Union (r1 r2 : reg_exp T)
| Star (r : reg_exp T).
| EmptySet
| EmptyStr
| Char (t : T)
| App (r1 r2 : reg_exp T)
| Union (r1 r2 : reg_exp T)
| Star (r : reg_exp T).
Arguments EmptySet {T}.
Arguments EmptyStr {T}.
Arguments Char {T} _.
Arguments App {T} _ _.
Arguments Union {T} _ _.
Arguments Star {T} _.
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 re1 matches s1, and re2 matches s2,
then App re1 re2 matches s1 ++ s2.
- If at least one of re1 and re2 matches s,
then Union re1 re2 matches s.
- Finally, if we can write some string s as the concatenation
of a sequence of strings s = s_1 ++ ... ++ s_k, and the
expression re matches each one of the strings s_i,
then Star re matches s.
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 s1 re1 s2 re2
(H1 : s1 =~ re1)
(H2 : s2 =~ re2)
: (s1 ++ s2) =~ (App re1 re2)
| MUnionL s1 re1 re2
(H1 : s1 =~ re1)
: s1 =~ (Union re1 re2)
| MUnionR re1 s2 re2
(H2 : s2 =~ re2)
: s2 =~ (Union re1 re2)
| MStar0 re : [] =~ (Star re)
| MStarApp s1 s2 re
(H1 : s1 =~ re)
(H2 : s2 =~ (Star re))
: (s1 ++ s2) =~ (Star re)
where "s =~ re" := (exp_match s re).
Inductive exp_match {T} : list T → reg_exp T → Prop :=
| MEmpty : [] =~ EmptyStr
| MChar x : [x] =~ (Char x)
| MApp s1 re1 s2 re2
(H1 : s1 =~ re1)
(H2 : s2 =~ re2)
: (s1 ++ s2) =~ (App re1 re2)
| MUnionL s1 re1 re2
(H1 : s1 =~ re1)
: s1 =~ (Union re1 re2)
| MUnionR re1 s2 re2
(H2 : s2 =~ re2)
: s2 =~ (Union re1 re2)
| MStar0 re : [] =~ (Star re)
| MStarApp s1 s2 re
(H1 : s1 =~ re)
(H2 : s2 =~ (Star re))
: (s1 ++ s2) =~ (Star re)
where "s =~ re" := (exp_match s re).
Notice that 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 lack of a rule actually gives us the behavior we
want.
- "The expression EmptySet does not match any string."
Example reg_exp_ex1 : [1] =~ Char 1.
Example reg_exp_ex2 : [1; 2] =~ App (Char 1) (Char 2).
Example reg_exp_ex3 : ¬([1; 2] =~ Char 1).
Proof.
apply MChar.
Qed.
apply MChar.
Qed.
Example reg_exp_ex2 : [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_ex3 : ¬([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 (s1 s2 : list T) (re : reg_exp T),
s1 =~ Star re →
s2 =~ Star re →
s1 ++ s2 =~ Star re.
Proof.
intros T s1 s2 re H1.
s1 =~ Star re →
s2 =~ Star re →
s1 ++ s2 =~ Star re.
Proof.
intros T s1 s2 re H1.
A naive first attempt at setting up the induction. (Note
that we are performing induction on evidence!) (We can begin by generalizing s2, since it's pretty clear that we
are going to have to walk over both s1 and s2 in parallel.)
generalize dependent s2.
induction H1
as [|x'|s1 re1 s2' re2 Hmatch1 IH1 Hmatch2 IH2
|s1 re1 re2 Hmatch IH|re1 s2' re2 Hmatch IH
|re''|s1 s2' re'' Hmatch1 IH1 Hmatch2 IH2].
induction H1
as [|x'|s1 re1 s2' re2 Hmatch1 IH1 Hmatch2 IH2
|s1 re1 re2 Hmatch IH|re1 s2' re2 Hmatch IH
|re''|s1 s2' re'' Hmatch1 IH1 Hmatch2 IH2].
- (* MEmpty *)
simpl. intros s2 H. apply H.
simpl. intros s2 H. apply H.
... but most cases get stuck. For MChar, for instance, we
must show
s2 =~ Char x' →
x'::s2 =~ Char x' which is clearly impossible.
s2 =~ Char x' →
x'::s2 =~ Char x' which is clearly impossible.
- (* MChar. *) intros s2 H. simpl. (* Stuck... *)
Abort.
Abort.
The problem here is that induction over a Prop hypothesis only works properly with hypotheses that are "completely general," i.e., ones in which all the arguments are variables, as opposed to more complex expressions like Star re.
Lemma star_app: ∀ T (s1 s2 : list T) (re re' : reg_exp T),
re' = Star re →
s1 =~ re' →
s2 =~ Star re →
s1 ++ s2 =~ Star re.
re' = Star re →
s1 =~ re' →
s2 =~ Star re →
s1 ++ s2 =~ Star re.
This works, but it makes the statement of the lemma a bit ugly.
Fortunately, there is a better way...
Abort.
The tactic remember e as x causes Coq to (1) replace all occurrences of the expression e by the variable x, and (2) add an equation x = e to the context. Here's how we can use it to show the above result:
Lemma star_app: ∀ T (s1 s2 : list T) (re : reg_exp T),
s1 =~ Star re →
s2 =~ Star re →
s1 ++ s2 =~ Star re.
Proof.
intros T s1 s2 re H1.
remember (Star re) as re'.
s1 =~ Star re →
s2 =~ Star re →
s1 ++ s2 =~ Star re.
Proof.
intros T s1 s2 re H1.
remember (Star re) as re'.
We now have Heqre' : re' = Star re.
generalize dependent s2.
induction H1
as [|x'|s1 re1 s2' re2 Hmatch1 IH1 Hmatch2 IH2
|s1 re1 re2 Hmatch IH|re1 s2' re2 Hmatch IH
|re''|s1 s2' re'' Hmatch1 IH1 Hmatch2 IH2].
induction H1
as [|x'|s1 re1 s2' re2 Hmatch1 IH1 Hmatch2 IH2
|s1 re1 re2 Hmatch IH|re1 s2' re2 Hmatch IH
|re''|s1 s2' re'' Hmatch1 IH1 Hmatch2 IH2].
- (* MEmpty *) discriminate.
- (* MChar *) discriminate.
- (* MApp *) discriminate.
- (* MUnionL *) discriminate.
- (* MUnionR *) discriminate.
- (* MChar *) discriminate.
- (* MApp *) discriminate.
- (* MUnionL *) discriminate.
- (* MUnionR *) discriminate.
The interesting cases are those that correspond to Star. Note
that the induction hypothesis IH2 on the MStarApp case
mentions an additional premise Star re'' = Star re, which
results from the equality generated by remember.
- (* MStar0 *)
intros s H. apply H.
- (* MStarApp *)
intros s2 H1. rewrite <- app_assoc.
apply MStarApp.
+ apply Hmatch1.
+ apply IH2.
× apply Heqre'.
× apply H1.
Qed.
intros s H. apply H.
- (* MStarApp *)
intros s2 H1. rewrite <- app_assoc.
apply MStarApp.
+ apply Hmatch1.
+ apply IH2.
× apply Heqre'.
× apply H1.
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 reflected in the proposition n =
m.
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.
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
evidence for P from evidence for reflect P true.
To put this observation to work, we first prove that the
statements P ↔ b = true and reflect P b are indeed
equivalent. First, the left-to-right implication:
Theorem iff_reflect : ∀ P b, (P ↔ b = true) → reflect P b.
Proof.
(* 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.