(** * IndProp: Inductively Defined Propositions *) Set Warnings "-notation-overridden". 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 [csf] on numbers, as follows (where [csf] stands for "Collatz step function"): *) Fixpoint div2 (n : nat) : nat := match n with 0 => 0 | 1 => 0 | S (S n) => S (div2 n) end. Definition csf (n : nat) : nat := if even n then div2 n else (3 * n) + 1. (** Next, we look at what happens when we repeatedly apply [csf] to some given starting number. For example, [csf 12] is [6], and [csf 6] is [3], so by repeatedly applying [csf] 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_ positive 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 reaches1_in (n : nat) : nat := if n =? 1 then 0 else 1 + reaches1_in (csf n). (** You can write this definition in a standard programming language. This definition is, however, rejected by Coq's termination checker, since the argument to the recursive call, [csf 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! *) (** Another idea could be to express the concept of "eventually reaches [1] in the Collatz sequence" as an _recursively defined property_ of numbers [Collatz_holds_for : nat -> Prop]. *) Fail Fixpoint Collatz_holds_for (n : nat) : Prop := match n with | 0 => False | 1 => True | _ => if even n then Collatz_holds_for (div2 n) else Collatz_holds_for ((3 * n) + 1) end. (** This recursive function is also rejected by the termination checker, since while we can in principle convince Coq that [div2 n] is smaller than [n], we can't convince it that [(3 * n) + 1] is smaller than [n]. Since it's definitely not! *) (** Fortunately, there is another way to do it: We can express the concept "reaches [1] eventually in the Collatz sequence" as an _inductively defined property_ of numbers. Intuitively, this property is defined by a set of rules: ------------------- (Chf_one) Collatz_holds_for 1 even n = true Collatz_holds_for (div2 n) --------------------------------------------- (Chf_even) Collatz_holds_for n even n = false Collatz_holds_for ((3 * n) + 1) ------------------------------------------------- (Chf_odd) Collatz_holds_for n So there are three ways to prove that a number [n] eventually reaches 1 in the Collatz sequence: - [n] is 1; - [n] is even and [div2 n] reaches 1; - [n] is odd and [(3 * n) + 1] reaches 1. *) (** We can prove that a number reaches 1 by constructing a (finite) derivation using these rules. For instance, here is the derivation proving that 12 reaches 1 (where we left out the evenness/oddness premises): ———————————————————— (Chf_one) Collatz_holds_for 1 ———————————————————— (Chf_even) Collatz_holds_for 2 ———————————————————— (Chf_even) Collatz_holds_for 4 ———————————————————— (Chf_even) Collatz_holds_for 8 ———————————————————— (Chf_even) Collatz_holds_for 16 ———————————————————— (Chf_odd) Collatz_holds_for 5 ———————————————————— (Chf_even) Collatz_holds_for 10 ———————————————————— (Chf_odd) Collatz_holds_for 3 ———————————————————— (Chf_even) Collatz_holds_for 6 ———————————————————— (Chf_even) Collatz_holds_for 12 *) (** Formally in Coq, the [Collatz_holds_for] property is _inductively defined_: *) Inductive Collatz_holds_for : nat -> Prop := | Chf_one : Collatz_holds_for 1 | Chf_even (n : nat) : even n = true -> Collatz_holds_for (div2 n) -> Collatz_holds_for n | Chf_odd (n : nat) : even n = false -> Collatz_holds_for ((3 * n) + 1) -> Collatz_holds_for n. (** For particular numbers, we can now prove that the Collatz sequence reaches [1] (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_even. reflexivity. simpl. apply Chf_even. reflexivity. simpl. apply Chf_odd. reflexivity. simpl. apply Chf_even. reflexivity. simpl. apply Chf_odd. reflexivity. simpl. apply Chf_even. reflexivity. simpl. apply Chf_even. reflexivity. simpl. apply Chf_even. reflexivity. simpl. apply Chf_even. reflexivity. simpl. apply Chf_one. Qed. (** The Collatz conjecture then states that the sequence beginning from _any_ positive number reaches [1]: *) Conjecture collatz : forall n, n <> 0 -> 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: Binary relation for comparing numbers *) (** A binary _relation_ on a set [X] has Coq type [X -> X -> Prop]. This 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 : nat -> nat -> Prop], the less-than-or-equal-to relation, which can be inductively defined by the following two rules: *) (** ------ (le_n) le n n le n m ---------- (le_S) le n (S m) *) (** This corresponds to the following inductive definition in Coq: *) 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). End LePlayground. (* ================================================================= *) (** ** Example: Transitive Closure *) (** As another example, the _transitive closure_ of a relation [R] is the smallest relation that contains [R] and that is transitive. This can be defined by the following two rules: R x y ---------------- (t_step) clos_trans R x y clos_trans R x y clos_trans R y z ------------------------------------ (t_trans) clos_trans R x z In Coq this looks as follows: *) 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. (** The [parent_of] relation is not transitive, but we can define an "ancestor of" relation as its transitive closure: *) Definition ancestor_of : Person -> Person -> Prop := clos_trans parent_of. (** Here is a derivation showing that Sage is an ancestor of Moss: ———————————————————(po_SC) ———————————————————(po_CM) parent_of Sage Cleo parent_of Cleo Moss —————————————————————(t_step) —————————————————————(t_step) ancestor_of Sage Cleo ancestor_of Cleo Moss ————————————————————————————————————————————————————(t_trans) ancestor_of Sage Moss *) Example ancestor_of_ex : 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: Reflexive and Transitive Closure *) (** As another example, the _reflexive and transitive closure_ of a relation [R] is the smallest relation that contains [R] and that is reflexive and transitive. This can be defined by the following three rules (where we added a reflexivity rule to [clos_trans]): R x y --------------------- (rt_step) clos_refl_trans R x y --------------------- (rt_refl) clos_refl_trans R x x clos_refl_trans R x y clos_refl_trans R y z ---------------------------------------------- (rt_trans) clos_refl_trans R x z *) Inductive clos_refl_trans {X: Type} (R: X->X->Prop) : X->X->Prop := | rt_step (x y : X) : R x y -> clos_refl_trans R x y | rt_refl (x : X) : clos_refl_trans R x x | rt_trans (x y z : X) : clos_refl_trans R x y -> clos_refl_trans R y z -> clos_refl_trans R x z. (** For instance, this enables an equivalent definition of the Collatz conjecture. First we define the binary relation corresponding to the Collatz step function [csf]: *) Definition cs (n m : nat) : Prop := csf n = m. (** This Collatz step relation can be used in conjunction with the reflexive and transitive closure operation to define a Collatz multi-step ([cms]) relation, expressing that a number [n] reaches another number [m] in zero or more Collatz steps: *) Definition cms n m := clos_refl_trans cs n m. Conjecture collatz' : forall n, n <> 0 -> cms n 1. (* ================================================================= *) (** ** 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. We can define them by the following rules: --------------------- (perm3_swap12) Perm3 [a;b;c] [b;a;c] --------------------- (perm3_swap23) Perm3 [a;b;c] [a;c;b] Perm3 l1 l2 Perm3 l2 l3 ----------------------------- (perm3_trans) Perm3 l1 l3 For instance we can derive [Perm3 [1;2;3] [3;2;1]] as follows: ————————(perm_swap12) —————————————————————(perm_swap23) Perm3 [1;2;3] [2;1;3] Perm3 [2;1;3] [2;3;1] ——————————————————————————————(perm_trans) ————————————(perm_swap12) Perm3 [1;2;3] [2;3;1] Perm [2;3;1] [3;2;1] —————————————————————————————————————————————————————(perm_trans) Perm3 [1;2;3] [3;2;1] *) (** In Coq [Perm3] is given the following inductive definition: *) 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. (* ================================================================= *) (** ** 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] (using the recursive boolean function [even]), or (2) [exists k, n = double k] (using an existential quantifier). *) (** A third possibility, which we'll use as a simple running example here, is to say that a number is even if we can _establish_ its evenness from the following two rules: ---- (ev_0) ev 0 ev n ------------ (ev_SS) ev (S (S n)) *) (** To illustrate how this new definition of evenness works, let's imagine using it to show that [4] is even: ———— (ev_0) ev 0 ———————————— (ev_SS) ev (S (S 0)) ———————————————————— (ev_SS) ev (S (S (S (S 0)))) *) (** 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 put off discussing syntax so far, but there are both similarities and a few differences between inductive properties like [ev] and inductive types like [nat] or [list]: Inductive list (X:Type) : Type := | nil : list X | cons (x : X) (l : list X) : list X. *) (** Beyond this syntactic distinction, we can think of the inductive definition of [ev] as defining a Coq property [ev : nat -> Prop], together with two "evidence constructors": *) Check ev_0 : ev 0. Check ev_SS : forall (n : nat), ev n -> ev (S (S n)). (** In fact, Coq also accepts the following equivalent definition of [ev]: *) Module EvPlayground. Inductive ev : nat -> Prop := | ev_0 : ev 0 | ev_SS : forall (n : nat), ev n -> ev (S (S n)). End EvPlayground. (** 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. (* ================================================================= *) (** ** Constructing Evidence for Permutations *) (** Similarly we can apply the evidence constructors to obtain evidence of [Perm3 [1;2;3] [3;2;1]]: *) Lemma Perm3_rev : Perm3 [1;2;3] [3;2;1]. Proof. apply perm3_trans with (l2:=[2;3;1]). - apply perm3_trans with (l2:=[2;1;3]). + apply perm3_swap12. + apply perm3_swap23. - apply perm3_swap12. Qed. (** And again we can equivalently use function application syntax to combine several constructors. Note that the Coq type checker can infer not only types, but also nats and lists. *) Lemma Perm3_rev' : Perm3 [1;2;3] [3;2;1]. Proof. apply (perm3_trans _ [2;3;1] _ (perm3_trans _ [2;1;3] _ (perm3_swap12 _ _ _) (perm3_swap23 _ _ _)) (perm3_swap12 _ _ _)). Qed. (** So the informal derivation trees we drew above are not too far from what's happening formally. Formally we're using the evidence constructors to build _evidence trees_, similar to the finite trees we built using the constructors of data types such as nat, list, binary trees, etc. *) (* ################################################################# *) (** * 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 proposition [ev n], then we know that [E] must be one of two things: - [E = ev_0] and [n = O], or - [E = ev_SS n' E'], where [n = S (S n')] and [E'] is evidence for [ev n']. *) (** This suggests that it should be possible to do _case analysis_ and even _induction_ on evidence of evenness... *) (* ================================================================= *) (** ** Destructing and Inverting 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. *) (** 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 E. apply ev_inversion in E. destruct E as [H0|H1]. - discriminate H0. - destruct H1 as [n' [Hnn' E']]. injection Hnn' as Hnn'. rewrite Hnn'. apply E'. 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' Hnn']. (* 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. unfold Even. intros n E. induction E as [|n' E' IH]. - (* E = ev_0 *) exists 0. reflexivity. - (* E = ev_SS n' E', with IH : Even n' *) destruct IH as [k Hk]. rewrite Hk. exists (S k). simpl. reflexivity. Qed. (* ################################################################# *) (** * Case Study: Regular Expressions *) (** Regular expressions are a natural 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} _. (** Note that this definition is _polymorphic_: Regular expressions in [reg_exp T] describe strings with characters drawn from [T] -- which in this exercise we represent as _lists_ with elements from [T]. *) (** We connect regular expressions and strings by defining when a regular expression _matches_ some string. Informally this looks as follows: - 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 intuition into a set of rules, where we write [s =~ re] to say that [s] matches [re]: -------------- (MEmpty) [] =~ EmptyStr --------------- (MChar) [x] =~ (Char x) s1 =~ re1 s2 =~ re2 --------------------------- (MApp) (s1 ++ s2) =~ (App re1 re2) s1 =~ re1 --------------------- (MUnionL) s1 =~ (Union re1 re2) s2 =~ re2 --------------------- (MUnionR) s2 =~ (Union re1 re2) --------------- (MStar0) [] =~ (Star re) s1 =~ re s2 =~ (Star re) ----------------------- (MStarApp) (s1 ++ s2) =~ (Star re) *) (** This directly corresponds to the following [Inductive] definition. 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 s2 re1 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? (A) Yes, we should add a rule for this. (B) No, one of the other rules already covers this case. (C) 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 string [s] matches a regular expression [re], 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 | s2 re1 re2 Hmatch IH | re | s1 s2 re Hmatch1 IH1 Hmatch2 IH2]. (* WORK IN CLASS *) Admitted. (* ================================================================= *) (** ** The [remember] Tactic *) (** Since the definition of [exp_match] has a recursive structure, we might expect that proofs involving regular expressions will often require induction on evidence. *) (** 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 eqn:Eq] causes Coq to (1) replace all occurrences of the expression [e] by the variable [x], and (2) add an equation [Eq : 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' eqn:Eq. (** We now have [Eq : 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 [Eq] 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]. *) - (* MStar0 *) intros H. apply H. - (* MStarApp *) intros H1. rewrite <- app_assoc. apply MStarApp. + apply Hmatch1. + apply IH2. * apply Eq. * apply H1. (** 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]. *) 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 *) (** We've seen that we often need to relate boolean computations to statements in [Prop]: *) Check eqb_eq : forall n1 n2, (n1 =? n2) = true <-> n1 = n2. (** However, this 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 = nil *) 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 [EQnm | NEQnm]. + (* n = m *) intros _. rewrite EQnm. 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. *)