(** * PropRelInd: Properties, Relations and Induction *) Require Export Logic. (* ####################################################### *) (** * Relations *) (** A proposition parameterized by a number (such as [ev] or [beautiful]) can be thought of as a _property_ -- i.e., it defines a subset of [nat], namely those numbers for which the proposition is provable. In the same way, a two-argument proposition can be thought of as a _relation_ -- i.e., it defines a set of pairs for which the proposition is provable. *) (** Now with the full apparatus of logic connectives available, we can define a few more iteresting properties and relations--- and even sometimes prove things about them. **) (** For a warm-up, define an inductive binary relation [total_relation] that holds between every pair of natural numbers and an inductive binary relation [empty_relation] that never holds. *) (** [[ Inductive total_relation : nat -> nat -> Prop := ?? Inductive empty_relation : nat -> nat -> Prop := ?? ]] **) (** A list is _maximal_ with property [P] if it has the property, and every other list with the property is at most as long as it is: [[ Definition maximal {X:Type} (lmax : list X) (P : list X -> Prop) := ?? ]] *) (** Recall the definition of subsequence from the Bonusaufgabe in Blatt 4: **) Inductive subseq' {X:Type} : list X -> list X -> Prop := | sub_nil : forall l, subseq' [] l | sub_take : forall x l1 l2, subseq' l1 l2 -> subseq' (x :: l1) (x :: l2) | sub_skip : forall x l1 l2, subseq' l1 l2 -> subseq' l1 (x :: l2). (** Recall also the function [forallb] from one of more challenging exercises on polymorphism: *) Fixpoint forallb {X : Type} (test : X -> bool) (l : list X) : bool := match l with | [] => true | x :: l' => andb (test x) (forallb test l') end. (** A "good subsequence" for a given list [l] and a [test] is a subsequence of [l] all of whose members evaluate to [true] under the [test] : [[ Definition good_subseq {X:Type} (test : X -> bool) (l lsub : list X) := ]] **) (** Good subsequences can be extended with good elements: [[ Lemma good_subseq_extend : forall (X:Type) (test : X -> bool) (l lsub : list X) (x : X), ... ]] *) (** If [lmax] is a maximal good subsequence of [x :: l] and [x] is not good, then [lmax] is also a maximal good subsequence of [l] : [[ Lemma maximal_strengthening : forall (X:Type) (x:X) (lmax l : list X) (test : X -> bool), ... ]] **) (* ##################################################### *) (** * Induction Principles *) (** This is a good point to pause and take a deeper look at induction principles. Every time we declare a new [Inductive] datatype, Coq automatically generates an _induction principle_ for this type. The induction principle for a type [t] is called [t_ind]. Here is the one for natural numbers: *) Check nat_ind. (* ===> nat_ind : forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n *) (** The [induction] tactic is a straightforward wrapper that, at its core, simply performs [apply t_ind]. To see this more clearly, let's experiment a little with using [apply nat_ind] directly, instead of the [induction] tactic, to carry out some proofs. Here, for example, is an alternate proof of a theorem that we saw in the [Basics] chapter. *) Theorem mult_0_r' : forall n:nat, n * 0 = 0. Proof. apply nat_ind. Case "O". reflexivity. Case "S". simpl. intros n IHn. rewrite -> IHn. reflexivity. Qed. (** Why the [induction] tactic is nicer to use in practice: - In the second step of the proof we have to do a little manual bookkeeping (the [intros]). - We do not introduce [n] into the context before applying [nat_ind]. - The [apply] tactic automatically chooses variable names for us (in the second subgoal, here), whereas [induction] gives us a way to specify what names should be used. The automatic choice can be confusing---but note we always have [intros] afterwards. *) (** **** Exercise: (plus_one_r') *) (** Complete this proof as we did [mult_0_r'] above, without using the [induction] tactic. *) Theorem plus_one_r' : forall n:nat, n + 1 = S n. Proof. Admitted. (** The induction principles that Coq generates for other datatypes defined with [Inductive] follow a similar pattern. If we define a type [t] with constructors [c1] ... [cn], Coq generates a theorem with this shape: [[ t_ind : forall P : t -> Prop, ... case for c1 ... -> ... case for c2 ... -> ... ... case for cn ... -> forall n : t, P n ]] The specific shape of each case depends on the arguments to the corresponding constructor. Before trying to write down a general rule, let's look at some more examples. First, an example where the constructors take no arguments: *) Inductive yesno : Type := | yes : yesno | no : yesno. Check yesno_ind. (* ===> yesno_ind : forall P : yesno -> Prop, P yes -> P no -> forall y : yesno, P y *) (** Here's another example, this time with one of the constructors taking some arguments. *) Inductive natlist : Type := | nnil : natlist | ncons : nat -> natlist -> natlist. Check natlist_ind. (* ===> (modulo a little tidying) natlist_ind : forall P : natlist -> Prop, P nnil -> (forall (n : nat) (l : natlist), P l -> P (ncons n l)) -> forall n : natlist, P n *) (** From these examples, we can extract this general rule: - The type declaration gives several constructors; each corresponds to one clause of the induction principle. - Each constructor [c] takes argument types [a1]...[an]. - Each [ai] can be either [t] (the datatype we are defining) or some other type [s]. - The corresponding case of the induction principle says (in English): - "for all values [x1]...[xn] of types [a1]...[an], if [P] holds for each of the inductive arguments (each [xi] of type [t]), then [P] holds for [c x1 ... xn]". *) (** **** Exercise: (mytype) *) (** Find an inductive definition that gives rise to the following induction principle: [[ mytype_ind : forall (X : Type) (P : mytype X -> Prop), (forall x : X, P (constr1 X x)) -> (forall n : nat, P (constr2 X n)) -> (forall m : mytype X, P m -> forall n : nat, P (constr3 X m n)) -> forall m : mytype X, P m ]] *) (** [] *) (** **** Exercise: (foo) *) (** Find an inductive definition that gives rise to the following induction principle: [[ foo_ind : forall (X Y : Type) (P : foo X Y -> Prop), (forall x : X, P (bar X Y x)) -> (forall y : Y, P (baz X Y y)) -> (forall f1 : nat -> foo X Y, (forall n : nat, P (f1 n)) -> P (quux X Y f1)) -> forall f2 : foo X Y, P f2 ]] *) (** [] *) (* ####################### *) (** * Induction and Relations **) (** Induction is a particularly interesting subject when discussed in conjunction with _relations_ *) Module BadEquality. (** First, recall that even Coq's equality relation is not built in; the one we we've been using so far comes from the tandard library. We can perfectly well define it as: **) Inductive eq (X:Type) : X -> X -> Prop := refl_equal : forall x, eq X x x. (** Standard infix notation: *) Notation "x = y" := (eq _ x y) (at level 70, no associativity) : type_scope. (** The way to think about this definition is that, given a set [X], it defines a _family_ of propositions "[x] is equal to [y]," indexed by pairs of values ([x] and [y]) from [X]. There is just one way of constructing evidence for members of this family: applying the constructor [refl_equal] to a type [X] and a value [x : X] yields evidence that [x] is equal to [x]. *) (** **** Exercise: 2 stars (leibniz_equality) *) (** The inductive definitions of equality corresponds to _Leibniz equality_: what we mean when we say "[x] and [y] are equal" is that every property on [P] that is true of [x] is also true of [y]. *) Lemma leibniz_equality : forall (X : Type) (x y: X), x = y -> forall P : X -> Prop, P x -> P y. Proof. Admitted. (** But the induction principle for this equality is somewhat unsatisfying... *) Check eq_ind. End BadEquality. (** In the Coq standard library, the definition of equality is slightly different: *) Inductive eq' (X:Type) (x:X) : X -> Prop := refl_equal' : eq' X x x. (** The advantage of this definition is that the induction principle that Coq derives for it is precisely the familiar principle of _Leibniz equality_: what we mean when we say "[x] and [y] are equal" is that every property on [P] that is true of [x] is also true of [y]. *) Check eq'_ind. (* ===> forall (X : Type) (x : X) (P : X -> Prop), P x -> forall y : X, x =' y -> P y ===> (i.e., after a little reorganization) forall (X : Type) (x : X) forall y : X, x =' y -> forall P : X -> Prop, P x -> P y *) (** Keep in mind that the name of the standard library equality constructor is [[eq_refl]]. *) Module BadLeModule. (** Similarly, we can think of a perfectly natural definition of inequality. *) Inductive le : nat -> nat -> Prop := | le_n : forall n, le n n | le_S : forall n m, (le n m) -> (le n (S m)). Notation "m <= n" := (le m n). (** Proofs of facts about [<=] defined this way would use the constructors [le_n] and [le_S] and follow the same patterns as proofs about properties, like [ev] in chapter [Prop]. We can [apply] the constructors to prove [<=] goals (e.g., to show that [3<=3] or [3<=6]), and we can use tactics like [inversion] to extract information from [<=] hypotheses in the context (e.g., to prove that [~(2 <= 1)].) *) (** Here are some sanity checks on the definition. (Notice that, although these are the same kind of simple "unit tests" as we gave for the testing functions we wrote in the first few lectures, we must construct their proofs explicitly -- [simpl] and [reflexivity] don't do the job, because the proofs aren't just a matter of simplifying computations.) *) Theorem test_le1 : 3 <= 3. Proof. (* WORKED IN CLASS *) Admitted. Theorem test_le2 : 3 <= 6. Proof. (* WORKED IN CLASS *) Admitted. (** However, just look how the induction principle for this thing would look like ... *) Check le_ind. (* le_ind : forall P : nat -> nat -> Prop, (forall n : nat, P n n) -> (forall n m : nat, le n m -> P n m -> P n (S m)) -> forall n n0 : nat, le n n0 -> P n n0 *) End BadLeModule. (** But note that the left-hand argument [n] to [le] is the same everywhere in the definition, so we can actually make it a "general parameter" to the whole definition, rather than an argument to each constructor. *) Inductive le (n:nat) : nat -> Prop := | le_n : le n n | le_S : forall m, (le n m) -> (le n (S m)). Notation "m <= n" := (le m n). (** The second one is better, even though it looks less symmetric. Why? Because it gives us a simpler induction principle. (The same was true of our second version of [eq].) *) Check le_ind. (* ===> forall (n : nat) (P : nat -> Prop), P n -> (forall m : nat, n <= m -> P m -> P (S m)) -> forall n0 : nat, n <= n0 -> P n0 *) (* ##################################################### *) (** ** Induction Principles in [Prop] *) (** Earlier, we looked in detail at the induction principles that Coq generates for inductively defined _sets_. The induction principles for inductively defined _propositions_ like [gorgeous] are a tiny bit more complicated. As with all induction principles, we want to use the induction principle on [gorgeous] to prove things by inductively considering the possible shapes that something in [gorgeous] can have -- either it is evidence that [0] is gorgeous, or it is evidence that, for some [n], [3+n] is gorgeous, or it is evidence that, for some [n], [5+n] is gorgeous and it includes evidence that [n] itself is. Intuitively speaking, however, what we want to prove are not statements about _evidence_ but statements about _numbers_. So we want an induction principle that lets us prove properties of numbers by induction on evidence. For example, from what we've said so far, you might expect the inductive definition of [gorgeous]... [[ Inductive gorgeous : nat -> Prop := g_0 : gorgeous 0 | g_plus3 : forall n, gorgeous n -> gorgeous (3+m) | g_plus5 : forall n, gorgeous n -> gorgeous (5+m). ]] ...to give rise to an induction principle that looks like this... [[ gorgeous_ind_max : forall P : (forall n : nat, gorgeous n -> Prop), P O g_0 -> (forall (m : nat) (e : gorgeous m), P m e -> P (3+m) (g_plus3 m e) -> (forall (m : nat) (e : gorgeous m), P m e -> P (5+m) (g_plus5 m e) -> forall (n : nat) (e : gorgeous n), P n e ]] ... because: - Since [gorgeous] is indexed by a number [n] (every [gorgeous] object [e] is a piece of evidence that some particular number [n] is gorgeous), the proposition [P] is parameterized by both [n] and [e] -- that is, the induction principle can be used to prove assertions involving both a gorgeous number and the evidence that it is gorgeous. - Since there are three ways of giving evidence of gorgeousness ([gorgeous] has three constructors), applying the induction principle generates three subgoals: - We must prove that [P] holds for [O] and [b_0]. - We must prove that, whenever [n] is a gorgeous number and [e] is an evidence of its gorgeousness, if [P] holds of [n] and [e], then it also holds of [3+m] and [g_plus3 n e]. - We must prove that, whenever [n] is a gorgeous number and [e] is an evidence of its gorgeousness, if [P] holds of [n] and [e], then it also holds of [5+m] and [g_plus5 n e]. - If these subgoals can be proved, then the induction principle tells us that [P] is true for _all_ gorgeous numbers [n] and evidence [e] of their gorgeousness. But this is a little more flexibility than we actually need or want: it is giving us a way to prove logical assertions where the assertion involves properties of some piece of _evidence_ of gorgeousness, while all we really care about is proving properties of _numbers_ that are gorgeous -- we are interested in assertions about numbers, not about evidence. It would therefore be more convenient to have an induction principle for proving propositions [P] that are parameterized just by [n] and whose conclusion establishes [P] for all gorgeous numbers [n]: [[ forall P : nat -> Prop, ... -> forall n : nat, gorgeous n -> P n ]] For this reason, Coq actually generates the following simplified induction principle for [gorgeous]: *) Check gorgeous_ind. (* ===> gorgeous_ind : forall P : nat -> Prop, P 0 -> (forall n : nat, gorgeous n -> P n -> P (3 + n)) -> (forall n : nat, gorgeous n -> P n -> P (5 + n)) -> forall n : nat, gorgeous n -> P n *) (** In particular, Coq has dropped the evidence term [e] as a parameter of the the proposition [P], and consequently has rewritten the assumption [forall (n : nat) (e: gorgeous n), ...] to be [forall (n : nat), gorgeous n -> ...]; i.e., we no longer require explicit evidence of the provability of [gorgeous n]. *) (** In English, [gorgeous_ind] says: - Suppose, [P] is a property of natural numbers (that is, [P n] is a [Prop] for every [n]). To show that [P n] holds whenever [n] is gorgeous, it suffices to show: - [P] holds for [0], - for any [n], if [n] is gorgeous and [P] holds for [n], then [P] holds for [3+n], - for any [n], if [n] is gorgeous and [P] holds for [n], then [P] holds for [5+n]. *) (** We can apply [gorgeous_ind] directly instead of using [induction]. *) Theorem gorgeous__beautiful' : forall n, gorgeous n -> beautiful n. Proof. intros. apply gorgeous_ind. Case "g_0". apply b_0. Case "g_plus3". intros. apply b_sum. apply b_3. apply H1. Case "g_plus5". intros. apply b_sum. apply b_5. apply H1. apply H. Qed. (* ##################################################### *) (** ** More on the [induction] Tactic *) (** The [induction] tactic actually does even more low-level bookkeeping for us than we discussed above. Recall the informal statement of the induction principle for natural numbers: - If [P n] is some proposition involving a natural number n, and we want to show that P holds for _all_ numbers n, we can reason like this: - show that [P O] holds - show that, if [P n'] holds, then so does [P (S n')] - conclude that [P n] holds for all n. So, when we begin a proof with [intros n] and then [induction n], we are first telling Coq to consider a _particular_ [n] (by introducing it into the context) and then telling it to prove something about _all_ numbers (by using induction). What Coq actually does in this situation, internally, is to "re-generalize" the variable we perform induction on. For example, in the proof above that [plus] is associative... *) Theorem plus_assoc' : forall n m p : nat, n + (m + p) = (n + m) + p. Proof. (* ...we first introduce all 3 variables into the context, which amounts to saying "Consider an arbitrary [n], [m], and [p]..." *) intros n m p. (* ...We now use the [induction] tactic to prove [P n] (that is, [n + (m + p) = (n + m) + p]) for _all_ [n], and hence also for the particular [n] that is in the context at the moment. *) induction n as [| n']. Case "n = O". reflexivity. Case "n = S n'". (* In the second subgoal generated by [induction] -- the "inductive step" -- we must prove that [P n'] implies [P (S n')] for all [n']. The [induction] tactic automatically introduces [n'] and [P n'] into the context for us, leaving just [P (S n')] as the goal. *) simpl. rewrite -> IHn'. reflexivity. Qed. (** It also works to apply [induction] to a variable that is quantified in the goal. *) Theorem plus_comm' : forall n m : nat, n + m = m + n. Proof. induction n as [| n']. Case "n = O". intros m. rewrite -> plus_0_r. reflexivity. Case "n = S n'". intros m. simpl. rewrite -> IHn'. rewrite <- plus_n_Sm. reflexivity. Qed. (** Note that [induction n] leaves [m] still bound in the goal -- i.e., what we are proving inductively is a statement beginning with [forall m]. If we do [induction] on a variable that is quantified in the goal _after_ some other quantifiers, the [induction] tactic will automatically introduce the variables bound by these quantifiers into the context. *) Theorem plus_comm'' : forall n m : nat, n + m = m + n. Proof. (* Let's do induction on [m] this time, instead of [n]... *) induction m as [| m']. Case "m = O". simpl. rewrite -> plus_0_r. reflexivity. Case "m = S m'". simpl. rewrite <- IHm'. rewrite <- plus_n_Sm. reflexivity. Qed. (** [] *)