(** * IndProp: Inductively Defined Propositions *) Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality". From LF Require Export Logic. (* ################################################################# *) (** * Inductively Defined Propositions *) (** In the [Logic] chapter, we looked at several ways of writing propositions, including conjunction, disjunction, and existential quantification. In this chapter, we bring yet another new tool into the mix: _inductively defined propositions_. To begin, some examples... *) (* ================================================================= *) (** ** Example: The Collatz Conjecture *) (** The _Collatz Conjecture_ is a famous open problem in number theory. Its statement is quite simple. First, we define a function [f] on numbers, as follows: *) 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. (** Next, we look at what happens when we repeatedly apply [f] to some given starting number. For example, [f 12] is [6], and [f 6] is [3], so by repeatedly applying [f] we get the sequence [12, 6, 3, 10, 5, 16, 8, 4, 2, 1]. Similarly, if we start with [19], we get the longer sequence [19, 58, 29, 88, 44, 22, 11, 34, 17, 52, 26, 13, 40, 20, 10, 5, 16, 8, 4, 2, 1]. Both of these sequences eventually reach [1]. The question posed by Collatz was: Is the sequence starting from _any_ natural number guaranteed to reach [1] eventually? *) (** To formalize this question in Coq, we might try to define a recursive _function_ that calculates the total number of steps that it takes for such a sequence to reach [1]. *) Fail Fixpoint reaches_1_in (n : nat) := 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 pointless limitation: functions in Coq are required to be total, to ensure logical consistency. Moreover, we can't fix it by devising a more clever termination checker: deciding whether this particular function is total would be equivalent to settling the Collatz conjecture! *) (** Fortunately, there is another way to do it: We can express the concept "reaches [1] eventually" as an _inductively defined property_ of numbers: *) Inductive Collatz_holds_for : nat -> Prop := | Chf_done : Collatz_holds_for 1 | Chf_more (n : nat) : Collatz_holds_for (f n) -> Collatz_holds_for n. (** What we've done here is to use Coq's [Inductive] definition mechanism to characterize the property "Collatz holds for..." by stating two different ways in which it can hold: (1) Collatz holds for [1] and (2) if Collatz holds for [f n] then it holds for [n]. *) (** For particular numbers, we can now argue that the Collatz sequence reaches [1] like this (again, we'll go through the details of how it works a bit later in the chapter): *) Example Collatz_holds_for_12 : Collatz_holds_for 12. Proof. apply Chf_more. unfold f. simpl. apply Chf_more. unfold f. simpl. apply Chf_more. unfold f. simpl. apply Chf_more. unfold f. simpl. apply Chf_more. unfold f. simpl. apply Chf_more. unfold f. simpl. apply Chf_more. unfold f. simpl. apply Chf_more. unfold f. simpl. apply Chf_more. unfold f. simpl. apply Chf_done. Qed. (** The Collatz conjecture then states that the sequence beginning from _any_ number reaches [1]: *) Conjecture collatz : forall n, Collatz_holds_for 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. *) (* ================================================================= *) (** ** Example: Ordering *) (** A binary _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]. *) (** For example, one familiar binary relation on [nat] is [le], the less-than-or-equal-to relation. We've already seen how to define it as a boolean computation. Here is a "direct" propositional definition. *) 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). Notation "n <= m" := (le n m) (at level 70). Example le_3_5 : 3 <= 5. Proof. apply le_S. apply le_S. apply le_n. Qed. End LePlayground. Module LePlayground1. (** (By "reserving" the notation before defining the [Inductive], we can use it in the definition.) *) Reserved Notation "n <= m" (at level 70). Inductive le : nat -> nat -> Prop := | le_n (n : nat) : n <= n | le_S (n m : nat) : n <= m -> n <= (S m) where "n <= m" := (le n m). End LePlayground1. (* ================================================================= *) (** ** Example: Transitive Closure *) (** As another example, 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. (** For example, suppose we define a "parent of" relation on a group of people... *) Inductive Person : Type := Sage | Cleo | Ridley | Moss. Inductive parent_of : Person -> Person -> Prop := po_SC : parent_of Sage Cleo | po_SR : parent_of Sage Ridley | po_CM : parent_of Cleo Moss. (** Then we can define "ancestor of" as its transitive closure: *) Definition ancestor_of : Person -> Person -> Prop := clos_trans parent_of. Example ancestor_of1 : ancestor_of Sage Moss. Proof. unfold ancestor_of. apply t_trans with Cleo. - apply t_step. apply po_SC. - apply t_step. apply po_CM. Qed. (* ================================================================= *) (** ** Example: Permutations *) (** The familiar mathematical concept of _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 (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]. *) Example Perm3_example1 : Perm3 [1;2;3] [2;3;1]. Proof. apply perm3_trans with [2;1;3]. - apply perm3_swap12. - apply perm3_swap23. Qed. (* ================================================================= *) (** ** Example: Evenness (yet again) *) (** We've already seen two ways of stating a proposition that a number [n] is even: We can say (1) [even n = true], or (2) [exists k, n = double k]. A third possibility, which we'll use as a running example for the rest of this chapter, is to say that [n] is even if we can _establish_ its evenness from the following rules: - The number [0] is even. - If [n] is even, then [S (S n)] is even. *) (** We can translate the informal definition of evenness from above into a formal [Inductive] declaration, where each "way that a number can be even" corresponds to a separate constructor: *) Inductive ev : nat -> Prop := | 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 : forall 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. (** ... 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. (** In this way, we can also prove theorems that have hypotheses involving [ev]. *) Theorem ev_plus4 : forall n, ev n -> ev (4 + n). Proof. intros n. simpl. intros Hn. apply ev_SS. apply ev_SS. apply Hn. Qed. (* ################################################################# *) (** * Using Evidence in Proofs *) (** Besides _constructing_ evidence that numbers are even, we can also _destruct_ such evidence, reasoning about how it could have been built. Defining [ev] with an [Inductive] declaration tells Coq not only that the constructors [ev_0] and [ev_SS] are valid ways to build evidence that some number is [ev], but also that these two constructors are the _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']). *) (** This suggests that it should be possible to do _case analysis_ and even _induction_ on evidence of evenness... *) (* ================================================================= *) (** ** Inversion on Evidence *) (** We can prove our characterization of evidence for [ev n], using [destruct]. *) Theorem ev_inversion : forall (n : nat), ev n -> (n = 0) \/ (exists 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. exists 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 : forall 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. (** Coq provides a handy tactic called [inversion] that does the work of our inversion lemma and more besides. *) Theorem evSS_ev' : forall 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. (** We can use [inversion] to re-prove some theorems from [Tactics.v]. Note that [inversion] also works on equality propositions. *) Theorem inversion_ex1 : forall (n m o : nat), [n; m] = [o; o] -> [n] = [m]. Proof. intros n m o H. inversion H. reflexivity. Qed. Theorem inversion_ex2 : forall (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 [Inductive]ly: - 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). *) (** Let's try to show that our new notion of evenness implies our earlier notion (the one based on [double]). *) Lemma ev_Even_firsttry : forall n, ev n -> Even n. Proof. (* WORK IN CLASS *) Admitted. (* ================================================================= *) (** ** Induction on Evidence *) (** If this story feels familiar, it is no coincidence: We encountered similar problems in the [Induction] chapter, when trying to use case analysis to prove results that required induction. And once again the solution is... induction! *) (** Let's try proving that lemma again: *) Lemma ev_Even : forall n, ev n -> Even n. Proof. intros n E. induction E as [|n' E' IH]. - (* E = ev_0 *) unfold Even. exists 0. reflexivity. - (* E = ev_SS n' E' with IH : Even n' *) unfold Even in IH. destruct IH as [k Hk]. rewrite Hk. unfold Even. exists (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 *) (** Just as a single-argument proposition defines a _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). (** Some sanity checks... *) 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. (** The "strictly less than" relation [n < m] can now be defined in terms of [le]. *) Definition lt (n m : nat) := le (S n) m. Notation "n < m" := (lt n m). End Playground. (* ################################################################# *) (** * A Digression on Notation *) (** There are several equivalent ways of writing inductive types.  We've mostly seen this style... *) Module bin1. Inductive bin : Type := | Z | B0 (n : bin) | B1 (n : bin). End bin1. (** ... which omits the result types because they are all the same (i.e., [bin]). *) (** It is completely equivalent to this... *) Module 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. (** ... 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 are a simple language for describing sets of strings. Their syntax is defined as follows: *) Inductive reg_exp (T : Type) : Type := | EmptySet | EmptyStr | Char (t : T) | App (r1 r2 : reg_exp T) | Union (r1 r2 : reg_exp T) | Star (r : reg_exp T). Arguments EmptySet {T}. Arguments EmptyStr {T}. Arguments Char {T} _. Arguments App {T} _ _. Arguments Union {T} _ _. Arguments Star {T} _. (** 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]. In particular, the sequence of strings may be empty, so [Star re] always matches the empty string [[]] no matter what [re] is. *) (** 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]. *) 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). (* QUIZ Notice that this clause in our informal definition... - "The expression [EmptySet] does not match any string." ... 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. *) Example reg_exp_ex1 : [1] =~ Char 1. Proof. apply MChar. Qed. Example reg_exp_ex2 : [1; 2] =~ App (Char 1) (Char 2). Proof. apply (MApp [1]). - apply MChar. - apply MChar. Qed. Example reg_exp_ex3 : ~ ([1; 2] =~ Char 1). Proof. intros H. inversion H. Qed. (** Something more interesting: *) Lemma MStar1 : forall T s (re : reg_exp T) , s =~ re -> s =~ Star re. (* WORK IN CLASS *) Admitted. (** Naturally, proofs about [exp_match] often require induction (on evidence!). *) (** For example, suppose we want to prove the following intuitive result: If a regular expression [re] matches some string [s], then all elements of [s] must occur as character literals somewhere in [re]. To state this as a theorem, we first define a function [re_chars] that lists all characters that occur in a regular expression: *) Fixpoint re_chars {T} (re : reg_exp T) : list T := match re with | EmptySet => [] | EmptyStr => [] | Char x => [x] | App re1 re2 => re_chars re1 ++ re_chars re2 | Union re1 re2 => re_chars re1 ++ re_chars re2 | Star re => re_chars re end. (** This lemma from chapter [Logic] will be useful in the proof of the theorem just below it. *) Lemma In_app_iff : forall A l l' (a:A), In a (l++l') <-> In a l \/ In a l'. Proof. intros A l. induction l as [|a' l' IH]. - intros l' a. simpl. split. + intros H. right. apply H. + intros [[]|H]. apply H. - intros l'' a. simpl. rewrite IH. rewrite or_assoc. reflexivity. Qed. Theorem in_re_match : forall T (s : list T) (re : reg_exp T) (x : T), s =~ re -> In x s -> In x (re_chars re). Proof. intros T s re x Hmatch Hin. induction Hmatch as [| x' | s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2 | s1 re1 re2 Hmatch IH | re1 s2 re2 Hmatch IH | re | s1 s2 re Hmatch1 IH1 Hmatch2 IH2]. (* WORK IN CLASS *) Admitted. (* ================================================================= *) (** ** The [remember] Tactic *) (** One potentially confusing feature of the [induction] tactic is that it will let you try to perform an induction over a term that isn't sufficiently general. The effect of this is to lose information (much as [destruct] without an [eqn:] clause can do), and leave you unable to complete the proof. Here's an example: *) Lemma star_app: forall 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. (** Here is a naive first attempt at setting up the induction. (Note that we are performing induction on evidence!) *) 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]. (** We can get through the first case... *) - (* MEmpty *) simpl. intros H. apply H. (** ... but most cases get stuck. For [MChar], for instance, we must show s2 =~ Char x' -> x'::s2 =~ Char x' which is clearly impossible. *) - (* MChar. *) intros 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]. 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: forall T (s1 s2 : list T) (re re' : reg_exp T), 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: forall 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'. (** We now have [Heqre' : re' = Star re]. *) induction H1 as [|x'|s1 re1 s2' re2 Hmatch1 IH1 Hmatch2 IH2 |s1 re1 re2 Hmatch IH|re1 s2' re2 Hmatch IH |re''|s1 s2' re'' Hmatch1 IH1 Hmatch2 IH2]. (** The [Heqre'] is contradictory in most cases, allowing us to conclude immediately. *) - (* MEmpty *) discriminate. - (* MChar *) discriminate. - (* MApp *) discriminate. - (* MUnionL *) discriminate. - (* MUnionR *) discriminate. (** The interesting cases are those that correspond to [Star]. Note that the induction hypothesis [IH2] on the [MStarApp] case mentions an additional premise [Star re'' = Star re], which results from the equality generated by [remember]. *) - (* MStar0 *) intros H. apply H. - (* MStarApp *) intros H1. rewrite <- app_assoc. apply MStarApp. + apply Hmatch1. + apply IH2. * apply Heqre'. * apply H1. Qed. (** The remainder of this section in the full version of the chapter develops an extended exercise on regular expressions, leading up to a proof of the well-known "pumping lemma." Informally, this lemma states 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]. *) (* ################################################################# *) (** * Case Study: Improving Reflection *) (** Relating boolean computations to statements in [Prop] can result in some tedium in proof scripts. Consider: *) Theorem filter_not_empty_In : forall 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. (** 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. *) (** 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. (** 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 : forall P b, (P <-> b = true) -> reflect P b. Proof. (* WORK IN CLASS *) Admitted. (** (The right-to-left implication is left as an exercise.) *) (** We can think of [reflect] as a 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]. We begin by recasting the [eqb_eq] lemma in terms of [reflect]: *) Lemma eqbP : forall n m, reflect (n = m) (n =? m). 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' : forall 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. (** 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_. This way of using [reflect] was popularized by _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 streamline small proof steps by turning them into boolean computations. *)