(*| ====================================================== Week 4: Inductive Propositions and Inductive Reasoning ====================================================== :status: hidden Author `Aurèle Barrière `__, `Adam Chlipala `__, `Benjamin C. Pierce `__ License No redistribution allowed (usage by permission in CS-428). .. contents:: .. coq:: none |*) From Coq Require Import Arith Lia String. Open Scope string_scope. Import Nat. Require Import List. Import ListNotations. (*| Introduction ============ So far, we've seen how to define Coq functions, and how to define simple propositions. Examples of propositions included equality (for instance, proving that the result of a function call is equal to something). But we've also been constructing propositions with quantifiers (`exists`, `forall`), conjunction, disjunction, implication... In this lecture, we look at yet another way to define propositions: the inductive ones. - We'll see how to define these inductive propositions. - We'll see how these can be particularly convenient to express propositions that were not so easy to define using our previous tools. - We'll see how to reason about them, by case analysis, inversion or induction, generalizing the induction principles we've been using before. Revisiting Eval =============== Remember the simple language of arithmetic expressions with variables defined in Week 1. |*) Notation var := string. Inductive arith : Set := | Const (n : nat) | Var (x : var) | Plus (e1 e2 : arith) | Times (e1 e2 : arith). Example ex1 := Const 42. Example ex2 := Plus (Const 1) (Times (Var "x") (Var "y")). (*| It was pretty easy to define natural semantics for these expressions with a simple function. Of course, to evaluate variables, we needed a "valuation", a function defining the value of each variable. The result is a function. Coq can compute it. |*) Notation val := (var -> nat). Fixpoint eval (vn: val) (e: arith) : nat := match e with | Const n => n | Var v => vn v | Plus e1 e2 => eval vn e1 + eval vn e2 | Times e1 e2 => eval vn e1 * eval vn e2 end. Example eval_example: nat := (eval (fun _ => 0) (Plus (Const 58) (Const 12))). Compute eval_example. (* .unfold *) (*| If you have some experience in defining programming language semantics, you might be used to another style of definition, with horizontal bars. (Blackboard example). Let's try to write the same thing in Coq: |*) Inductive ieval: val -> arith -> nat -> Prop := | i_const: forall (vn:val) (n:nat), ieval vn (Const n) n | i_var: forall (vn:val) (v:var) (n:nat) (EVAL_VAR: vn v = n), ieval vn (Var v) n | i_plus: forall (vn:val) (e1 e2:arith) (n1 n2:nat) (EVAL_LEFT: ieval vn e1 n1) (EVAL_RIGHT: ieval vn e2 n2), ieval vn (Plus e1 e2) (n1 + n2) | i_times: forall (vn:val) (e1 e2:arith) (n1 n2:nat) (EVAL_LEFT: ieval vn e1 n1) (EVAL_RIGHT: ieval vn e2 n2), ieval vn (Times e1 e2) (n1 * n2). (*| The process of turning the blackboard rules into Coq rules has been straightforward: - rule names become constructor names - hypotheses above the bar become universally quantified - conclusions below the bar are conclusions of each constructor. Note that naming hypotheses is optional and could be replaced by an implication. But what does this represent in Coq? We have just defined an inductive proposition (note the `Inductive` and `Prop` keywords). Just like `a = b` was a proposition, now `ieval vn e n` is a proposition. What do we love to do with propositions? Prove them! |*) Lemma ieval_example: ieval (fun _ => 0) (Plus (Const 58) (Const 12)) 70. Proof. (* each constructor can be applied, like a blackboard rule *) Fail apply i_plus. (* the rule expects the Plus to evaluate to an addition, let's show that 70 is in fact an addition *) replace 70 with (58 + 12) by lia. apply i_plus. (* apply (i_plus _ _ _ 58 12). would have also worked *) (* our rule had two premises. we need to prove them both *) - apply i_const. - apply i_const. Qed. (*| This is a start. But we can prove more interesting properties. For instance, let's prove the following property: |*) Theorem eval_implies_ieval: forall (vn:val) (e:arith) (n:nat), eval vn e = n -> ieval vn e n. Proof. intros vn e. induction e; intros; simpl in H. - subst. apply i_const. - apply i_var. assumption. - rewrite <- H. apply i_plus. + apply IHe1. reflexivity. + apply IHe2. reflexivity. - rewrite <- H. apply i_times. + apply IHe1. reflexivity. + apply IHe2. reflexivity. Qed. (* let's make it a bit more automated *) Theorem eval_implies_ieval': forall (vn:val) (e:arith) (n:nat), eval vn e = n -> ieval vn e n. Proof. induction e; intros; subst; constructor; auto. (* constructor applies the first inductive rule it can apply! *) Qed. (*| We could expect doing the other implication... but we'll wait a bit for now. You might think this is a bit more painful than just writing the evaluation function, and for that particular case you may be right. But let's now consider some variations. What if some of my variables are undefined? In my valuation function, we'll represent this with an option. |*) Notation valop := (var -> option nat). Example vo:valop := (fun v => match v with | "x" => Some 17 | "y" => Some 3 | _ => None end). (*| What should be the behavior of arithmetic expressions containing such undefined variables? First, we could just say that the expression does not evaluate at all. In our functional version of eval, we could do this with an option (left as exercise). What about our inductive proposition? |*) Inductive ioeval: valop -> arith -> nat -> Prop := | io_const: forall (vn:valop) (n:nat), ioeval vn (Const n) n | io_var: forall (vn:valop) (v:var) (n:nat) (EVAL_VAR: vn v = Some n), (* here we change to a Some *) ioeval vn (Var v) n | io_plus: forall (vn:valop) (e1 e2:arith) (n1 n2:nat) (EVAL_LEFT: ioeval vn e1 n1) (EVAL_RIGHT: ioeval vn e2 n2), ioeval vn (Plus e1 e2) (n1 + n2) | io_times: forall (vn:valop) (e1 e2:arith) (n1 n2:nat) (EVAL_LEFT: ioeval vn e1 n1) (EVAL_RIGHT: ioeval vn e2 n2), ioeval vn (Times e1 e2) (n1 * n2). (*| No further changes are needed. We simply did not give a meaning to variables `v` when `vn v = None`. The arithmetic expression has "blocking semantics", there is no way to construct a proof tree evaluating this expression to any value using that valuation. In fact we can even prove it. |*) Lemma blocking_sem: forall ret, ~ (ioeval vo (Var "z") ret). Proof. unfold not. intros. inversion H. (* what happened here? we'll discuss it soon *) simpl in EVAL_VAR. inversion EVAL_VAR. Qed. (*| But now, consider another variation, non-determinism. Suppose that now, undefined variable may evaluate to any possible number! This would be difficult to define in the functional style of `eval`. But how would you adapt the blackboard rules? We can do the same thing in our Coq inductive proposition: |*) Inductive ineval: valop -> arith -> nat -> Prop := | in_const: forall (vn:valop) (n:nat), ineval vn (Const n) n | in_var: forall (vn:valop) (v:var) (n:nat) (EVAL_VAR: vn v = Some n), ineval vn (Var v) n | in_undef: forall (vn:valop) (v:var) (n:nat) (UNDEFINED: vn v = None), (* for any possible n! *) ineval vn (Var v) n | in_plus: forall (vn:valop) (e1 e2:arith) (n1 n2:nat) (EVAL_LEFT: ineval vn e1 n1) (EVAL_RIGHT: ineval vn e2 n2), ineval vn (Plus e1 e2) (n1 + n2) | in_times: forall (vn:valop) (e1 e2:arith) (n1 n2:nat) (EVAL_LEFT: ineval vn e1 n1) (EVAL_RIGHT: ineval vn e2 n2), ineval vn (Times e1 e2) (n1 * n2). (*| We can now prove that a non-deterministic expression like `(Var "z")` has several meanings. |*) Lemma z_meaning1: ineval vo (Var "z") 623. Proof. apply in_undef. simpl. reflexivity. Qed. Lemma z_meaning2: ineval vo (Var "z") 236236. Proof. apply in_undef. simpl. reflexivity. Qed. (*| Interestingly, we see that these inductive propositions are convenient to define - partial functions (instead of using an option type) - multi-valued functions (or non-deterministic) In both cases, the idea is that we see such functions as mathematical relations between their input and their output. While Coq functions are expected to be total (each input has an output) and deterministic (only one output), this notion of relation can accommodate broader definitions. Of course, this expressivity comes at the cost of having a function that can actually be computed within Coq. But this is still convenient for models, invariant, semantics, specifications... We also previously saw that Coq functions were expected to terminate. Is this also a restriction we can lift by using an inductive proposition? Let us now leave our arithmetic expressions and consider the famous Collatz or Syracuse conjecture. The Syracuse sequence computes the next natural number in the sequence as follows: - if k (the last number of the sequence) is equal to 1, the sequence is over - if k is even, divide it by 2 and call Syracuse recursively on the result - if k is odd, multiply it by 3, add 1 and call Syracuse recursively on the result. The sequence is then determined by the first number. Starting from 12, we get the sequence `12, 6, 3, 10, 5, 16, 8, 4, 2, 1`. Starting from 19, we get the sequence è19, 58, 29, 88, 44, 22, 11, 34, 17, 52, 26, 13, 40, 20, 10, 5, 16, 8, 4, 2, 1`. The Collatz conjecture states that this sequence is always finite, in other words that 1 is always reached, for any starting natural number. To formalize this conjecture 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. |*) (* next number in the Syracuse sequence *) Definition next_syracuse (k : nat) := if even k then div2 k else (3 * k) + 1. Fail Fixpoint reaches_1_in (n : nat) := if Nat.eqb n 1 then 1 else 1 + reaches_1_in (next_syracuse n). (* .unfold .fails .no-goals *) (*| .. massert:: .s(Fixpoint).msg(subterm) This definition is rejected by Coq's termination checker, since the argument to the recursive call, `next_syracuse 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 (next_syracuse 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 `next_syracuse n` then it holds for `n`. We can prove that indeed the Collatz conjecture holds for some numbers: |*) Example Collatz_holds_for_12 : Collatz_holds_for 12. Proof. apply Chf_more. unfold next_syracuse. simpl. apply Chf_more. unfold next_syracuse. simpl. apply Chf_more. unfold next_syracuse. simpl. apply Chf_more. unfold next_syracuse. simpl. apply Chf_more. unfold next_syracuse. simpl. apply Chf_more. unfold next_syracuse. simpl. apply Chf_more. unfold next_syracuse. simpl. apply Chf_more. unfold next_syracuse. simpl. apply Chf_more. unfold next_syracuse. simpl. apply Chf_done. Qed. (*| Of course if you manage to prove the theorem below, I would be very impressed. |*) Theorem Collatz_Conjecture: forall n, Collatz_holds_for n. Proof. Admitted. (*| Taking A Step Back: Defining Inductive Propositions =================================================== You now have a methodology to define any kind of relations as inductive propositions. As we translated blackboard rules into Coq, you may have noted that the syntax was strangely similar to defining inductive datatypes. This is an important observation, that we'll reuse soon when doing proofs about inductive propositions. If we think about the blackboard rules, whenever you use them to prove something, you build a "proof derivation" or a "proof tree". This proof tree itself looks like something we could describe with an inductive datatype! In some way, by defining the Coq inductive proposition, you defined the different ways to build the proof tree: it's as if you described the proof tree inductive type. Now, proving that some inductive proposition holds amounts to constructing a proof tree, or constructing an element of that inductive type you just defined. In Coq, we can show the proofs object being constructed. Let's look at these proof trees for an example. |*) Example Collatz_holds_for_12' : Collatz_holds_for 12. Proof. apply Chf_more; unfold next_syracuse; simpl. Show Proof. apply Chf_more; unfold next_syracuse; simpl. Show Proof. apply Chf_more; unfold next_syracuse; simpl. Show Proof. apply Chf_more; unfold next_syracuse; simpl. Show Proof. apply Chf_more; unfold next_syracuse; simpl. Show Proof. apply Chf_more; unfold next_syracuse; simpl. Show Proof. apply Chf_more; unfold next_syracuse; simpl. Show Proof. apply Chf_more; unfold next_syracuse; simpl. Show Proof. apply Chf_more; unfold next_syracuse; simpl. Show Proof. apply Chf_done. Qed. (*| Now, let's familiarize ourselves with some more inductive propositions. We can use them to represent sets! |*) Inductive my_favorite_numbers : nat -> Prop := | ILike17 : my_favorite_numbers 17 | ILike23 : my_favorite_numbers 23 | ILike28 : my_favorite_numbers 28. (*| Let's a pick a simple relation between natural numbers: being strictly less than another number. |*) Inductive lt: nat -> nat -> Prop := | lt_next: forall n, lt n (S n) | lt_skip: forall n m (LT: lt n m), lt n (S m). Lemma lt36: lt 3 6. Proof. apply lt_skip. apply lt_skip. apply lt_next. Qed. (*| In fact, this `lt` relation can be seen as the transitive closure of another relation, relating numbers that are off by one (for instance, 4 and 5). We can similarly define this notion of transitive closure as an inductive proposition. |*) (* TC : Transitive Closure *) Inductive tc {A} (R : A -> A -> Prop) : A -> A -> Prop := | TcBase : forall x y, R x y -> tc R x y | TcTrans : forall x y z, tc R x y -> tc R y z -> tc R x z. (*| Let's redefine `lt` now as a transitive closure. |*) Definition oneApart (n m : nat) : Prop := n + 1 = m. Definition lt' : nat -> nat -> Prop := tc oneApart. (*| Let's see another use of the transitive closure: parent relationships. Let's define a family with their parent relationships. |*) Inductive person : Type := | Hera | Ares | Hephaestus | Eros. Inductive parent_of: person -> person -> Prop := | he_ar: parent_of Hera Ares | he_he: parent_of Hera Hephaestus | ar_er: parent_of Ares Eros. Definition ancestor_of : person -> person -> Prop := tc parent_of. Example ancestor_of1 : ancestor_of Hera Eros. Proof. unfold ancestor_of. apply TcTrans with Ares. - apply TcBase. apply he_ar. - apply TcBase. apply ar_er. Qed. (*| Useless question: what do you think is the simplest way to define an inductive proposition that never holds? And an inductive relation that always hold? |*) Inductive useless: nat -> Prop := . Inductive total_relation : nat -> nat -> Prop := | tot n m : total_relation n m. (*| One last example: we can define what it means for natural numbers to be even. Of course there are many equivalent definitions. |*) Inductive ev : nat -> Prop := | ev_0: ev 0 | ev_SS (n : nat) (H : ev n) : ev (S (S n)). (*| Inductive Reasoning =================== By defining our inductive propositions with rules, we've not only a way to construct evidence that a property holds, using each rule as a theorem. We've also established that the only way for the property to hold is by having a proof tree using only these inductive constructors. This is a very strong observation when conducting proofs with inductive propositions! 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`. To go back to the inductive types comparison, similarly every list is either a nil list or the concatenation of some elements to some other list. This means that, just like on inductive types, we can destruct and do induction on the proof trees of inductive propositions! So we can for instance prove the following lemma! |*) 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. (*| But this such a common reasoning pattern that Coq provides a handy tactic called `inversion` that factors it out, saving us the trouble of explicitly stating and proving an inversion lemma for every `Inductive` definition we make. Here, the `inversion` tactic can detect (1) that the first case, where `n = 0`, does not apply and (2) that the `n'` that appears in the `ev_SS` case must be the same as `n`. It includes an `as` annotation similar to `destruct`, allowing us to assign names rather than have Coq choose them. |*) 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. (*| Some more examples proofs with inversion: |*) Theorem one_not_even' : ~ ev 1. Proof. intros H. inversion H. Qed. Theorem favorites_below_50 : forall n, my_favorite_numbers n -> n < 50. Proof. intros n H. inversion H. - lia. - lia. - lia. Qed. Theorem SSSSev__even : forall n, ev (S (S (S (S n)))) -> ev n. Proof. intros n E. inversion E as [| n' E' EQ']. inversion E' as [| n'' E'' EQ'']. apply E''. Qed. (*| The `inversion` tactic does quite a bit of work. For example, when applied to an equality assumption, it does the work of both `discriminate` and `injection`. In addition, it carries out the `intros` and `rewrite`s that are typically necessary in the case of `injection`. It can also be applied to analyze evidence for arbitrary inductively defined propositions, not just equality. 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). .. exercise:: Inverting with no cases How many goals would be generated by doing an inversion on a `useless` proposition? .. solution:: None. |*) Theorem empty_useless: forall n, ~ useless n. Proof. unfold not. intros n H. inversion H. Qed. (*| But let's go even further. Just like we've seen that we can define a principle of induction on any inductive datatype, without surprise we can do inductive reasoning on the proof trees of inductive propositions! The behavior of `induction` on evidence (or proof tree) is the same as its behavior on data: It causes Coq to generate one subgoal for each constructor that could have used to build that evidence, while providing an induction hypothesis for each recursive occurrence of the property in question. Let's revisit our two definitions of `eval` and their equivalence; |*) Theorem ieval_implies_eval: forall (vn:val) (e:arith) (n:nat), ieval vn e n -> eval vn e = n. Proof. intros vn e. induction e; intros; inversion H; subst; simpl; try reflexivity. - apply IHe1 in EVAL_LEFT. apply IHe2 in EVAL_RIGHT. rewrite EVAL_LEFT. rewrite EVAL_RIGHT. reflexivity. - apply IHe1 in EVAL_LEFT. apply IHe2 in EVAL_RIGHT. rewrite EVAL_LEFT. rewrite EVAL_RIGHT. reflexivity. Qed. (*| Now with an induction on `ieval`: |*) Theorem ieval_implies_eval': forall (vn:val) (e:arith) (n:nat), ieval vn e n -> eval vn e = n. Proof. intros vn e n H. induction H; simpl. - reflexivity. - assumption. - rewrite IHieval1. rewrite IHieval2. reflexivity. - rewrite IHieval1. rewrite IHieval2. reflexivity. Qed. (* a bit simpler: *) Theorem ieval_implies_eval'': forall (vn:val) (e:arith) (n:nat), ieval vn e n -> eval vn e = n. Proof. induction 1; simpl; auto. Qed. (*| Even though we got to the same result by doing either an induction on an element of an inductive type or an induction on the inductive proposition, it's important to understand that we are doing two entirely different proofs. Let's see an example with `ev`. |*) Theorem ev_ev__ev : forall n m, ev (n+m) -> ev n -> ev m. Proof. induction n; intros. - simpl in H. assumption. - (* .unfold *) apply IHn. (* .unfold *) (*| This induction hypothesis does not seem helpful at all. |*) Abort. Theorem ev_ev__ev : forall n m, ev (n+m) -> ev n -> ev m. Proof. intros n m. generalize dependent n. induction m; intros. - constructor. - (* .unfold *) (*| I don't have anything in my context to prove `ev (S m)`… |*) Abort. (* OK I get it, you want me to use induction on a prop: *) Theorem ev_ev__ev : forall n m, ev (n+m) -> ev n -> ev m. Proof. intros n m Hnm. Fail solve[induction Hnm]. (* it seems like we lose the information that n+m is 0... *) remember (n+m) as nm. (* otherwise it gets discarded *) induction Hnm; intros Hn. - destruct m. + constructor. + rewrite add_succ_r in Heqnm. inversion Heqnm. - (* .unfold *) apply IHHnm. (* .unfold *) (*| I'm still lost. |*) Abort. (*| Actually, not only do we have to be careful about induction on a value vs induction on a proposition but also, induction on different propositions are different proofs: choose the right one! |*) Theorem ev_ev__ev : forall n m, ev (n+m) -> ev n -> ev m. Proof. intros n m Enm En. induction En as [| n' En']. - (* En = ev_0 *) simpl in Enm. apply Enm. - (* En = ev_SS *) simpl in Enm. inversion Enm. apply IHEn'. apply H0. Qed. (*| Maybe there's a lesson here... Doing induction on random things may not be the best proof strategy. Every time we define an inductive proposition, Coq creates an induction principle: .. coq:: unfold |*) (* just like for inductive types: *) Check nat_ind. (* for inductive propositions: *) Check useless_ind. Check total_relation_ind. Check lt_ind. Check ieval_ind. Check parent_of_ind. (*| Exercises ========= .. exercise:: `lt` .. coq:: |*) Theorem lt'_lt : forall n m, lt' n m -> n < m. (*| .. solution:: .. coq:: |*) Proof. intros n m H. induction H. - unfold oneApart in H. lia. - (* .unfold *) (*| I got IHtc1 and IHtc2 by induction. |*) lia. Qed. (*| .. coq:: |*) Lemma lt'_O_S : forall m, lt' 0 (S m). (*| .. solution:: .. coq:: |*) Proof. intros m. induction m. - apply TcBase. unfold oneApart. lia. - apply TcTrans with (S m). assumption. apply TcBase. unfold oneApart. lia. Qed. (*| .. coq:: |*) Lemma lt_lt'' : forall n k, lt' n (S k + n). (*| .. solution:: .. coq:: |*) Proof. intros n k. induction k. - apply TcBase. unfold oneApart. lia. - apply TcTrans with (S (k + n)). assumption. apply TcBase. unfold oneApart. lia. Qed. (*| .. coq:: |*) Theorem lt_lt' : forall n m, n < m -> lt' n m. (*| .. solution:: .. coq:: |*) Proof. intros n m H. replace m with (S (m - n - 1) + n) by lia. apply lt_lt''. (* induction quickly make proofs complicated. try to use it only when necessary ! Similarly nested inductions should mostly be avoided. If needed, create intermediate lemmas. *) Qed. (*| .. exercise:: Transitive closure **Transitive closure is idempotent.** |*) Theorem tc_tc2 : forall A (R : A -> A -> Prop) x y, tc R x y -> tc (tc R) x y. (*| .. solution:: .. coq:: |*) Proof. intros A R x y H. induction H. - apply TcBase. apply TcBase. assumption. - apply TcTrans with y. assumption. assumption. Qed. (*| .. coq:: |*) Theorem tc2_tc : forall A (R : A -> A -> Prop) x y, tc (tc R) x y -> tc R x y. (*| .. solution:: .. coq:: |*) Proof. intros A R x y H. induction H. - assumption. - apply TcTrans with y. assumption. assumption. Qed. (*| .. exercise:: Permutations Let's define inductively list permutations. This example is directly taken from the Coq standard library. |*) Inductive Permutation {A} : list A -> list A -> Prop := | perm_nil : Permutation [] [] | perm_skip : forall x l l', Permutation l l' -> Permutation (x::l) (x::l') | perm_swap : forall x y l, Permutation (y::x::l) (x::y::l) | perm_trans : forall l l' l'', Permutation l l' -> Permutation l' l'' -> Permutation l l''. Lemma permut_test: Permutation [3;4;5] [5;4;3]. (*| .. solution:: .. coq:: |*) Proof. apply perm_trans with ([4;3;5]). { apply perm_swap. } apply perm_trans with [4;5;3]. 2: { apply perm_swap. } apply perm_skip. apply perm_swap. Qed. (*| .. coq:: |*) Lemma Permutation_to_front : forall A (a : A) (ls : list A), Permutation (a :: ls) (ls ++ [a]). (*| .. solution:: .. coq:: |*) Proof. induction ls. - apply perm_skip. apply perm_nil. - apply perm_trans with (a0 :: a :: ls). apply perm_swap. apply perm_skip. assumption. Qed. (*| .. coq:: |*) Theorem Permutation_rev : forall A (ls : list A), Permutation ls (rev ls). (*| .. solution:: .. coq:: |*) Proof. induction ls. - apply perm_nil. - apply perm_trans with (a :: rev ls). apply perm_skip. assumption. apply Permutation_to_front. Qed. (*| .. coq:: |*) Theorem Permutation_length : forall A (ls1 ls2 : list A), Permutation ls1 ls2 -> length ls1 = length ls2. (*| .. solution:: .. coq:: |*) Proof. intros A ls1 ls2 H. induction H; try reflexivity. - simpl. rewrite IHPermutation. reflexivity. - lia. Qed. (*| .. coq:: |*) Lemma Permutation_refl : forall A (ls : list A), Permutation ls ls. (*| .. solution:: .. coq:: |*) Proof. induction ls. - apply perm_nil. - apply perm_skip. assumption. Qed. (*| .. coq:: |*) Lemma Permutation_app1 : forall A (ls1 ls2 ls : list A), Permutation ls1 ls2 -> Permutation (ls1 ++ ls) (ls2 ++ ls). (*| .. solution:: .. coq:: |*) Proof. intros A ls1 ls2 ls H. induction H. - apply Permutation_refl. - apply perm_skip. apply IHPermutation. - apply perm_swap. - apply perm_trans with (l' ++ ls). apply IHPermutation1. apply IHPermutation2. Qed. (*| .. coq:: |*) Lemma Permutation_app2 : forall A (ls ls1 ls2 : list A), Permutation ls1 ls2 -> Permutation (ls ++ ls1) (ls ++ ls2). (*| .. solution:: .. coq:: |*) Proof. induction ls; intros. - simpl. assumption. - apply perm_skip. apply IHls. assumption. Qed. (*| .. coq:: |*) Theorem Permutation_app : forall A (ls1 ls1' ls2 ls2' : list A), Permutation ls1 ls1' -> Permutation ls2 ls2' -> Permutation (ls1 ++ ls2) (ls1' ++ ls2'). (*| .. solution:: .. coq:: |*) Proof. intros. apply perm_trans with (ls1' ++ ls2). { apply Permutation_app1. assumption. } apply Permutation_app2. assumption. Qed. (*| **Bonus exercise**: we could have defined Permutation with a function, for instance checking that both list are equal after being sorted. Do you think some of these lemmas would have been equally easy to prove? .. exercise:: Even .. coq:: |*) Theorem ev_minus2 : forall n, ev n -> ev (pred (pred n)). (*| .. solution:: .. coq:: |*) Proof. intros n E. destruct E as [| n' E'] eqn:EE. - (* E = ev_0 *) simpl. apply ev_0. - (* E = ev_SS n' E' *) simpl. apply E'. Qed. (*| .. coq:: |*) Theorem evSS_ev_remember : forall n, ev (S (S n)) -> ev n. (*| .. solution:: .. coq:: :name: evss |*) Proof. intros n E. remember (S (S n)) as k eqn:Hk. (* .unfold *) destruct E as [|n' E'] eqn:EE. - (* E = ev_0 *) (* .unfold *) (*| Now we do have an assumption, in which :mquote:`.io#evss.s(remember).h#Hk.type` has been rewritten as :mquote:`.s(-).h#Hk.type` (:mref:`.s(-).h#Hk`) by `destruct`. That assumption gives us a contradiction. |*) discriminate Hk. - (* E = ev_S n' E' *) (* .unfold *) (*| This time :mquote:`.io#evss.s(remember).h#Hk.type` has been rewritten as :mquote:`.s(-).h#Hk.type` (:mref:`.s(-).h#Hk`). |*) injection Hk as Heq. rewrite <- Heq. apply E'. Qed. (*| .. coq:: |*) Theorem inversion_ex1 : forall (n m o : nat), [n; m] = [o; o] -> [n] = [m]. (*| .. solution:: .. coq:: |*) Proof. intros n m o H. inversion H. reflexivity. Qed. (*| .. coq:: |*) Theorem inversion_ex2 : forall (n : nat), S n = O -> 2 + 2 = 5. (*| .. solution:: .. coq:: |*) Proof. intros n contra. inversion contra. Qed. (*| .. coq:: |*) Theorem ev_sum : forall n m, ev n -> ev m -> ev (n + m). (*| .. solution:: .. coq:: |*) Proof. intros n m Hn Hm. induction Hn as [|n' Hn IH]. - (* ev_0 *) simpl. apply Hm. - (* ev_SS *) simpl. apply ev_SS. apply IH. Qed. (*| Next question: define an inductive relation between two lists stating that one is a subsequence of the other. .. solution:: .. coq:: |*) Inductive subseq : list nat -> list nat -> Prop := | sub_nil l : subseq [] l | sub_take x l1 l2 (H : subseq l1 l2) : subseq (x :: l1) (x :: l2) | sub_skip x l1 l2 (H : subseq l1 l2) : subseq l1 (x :: l2) . (*| .. coq:: |*) Theorem subseq_refl : forall (l : list nat), subseq l l. (*| .. solution:: .. coq:: |*) Proof. induction l as [|x l']. - (* l = [] *) apply sub_nil. - (* l = x :: l' *) apply sub_take. apply IHl'. Qed. (*| .. coq:: |*) Theorem subseq_app : forall (l1 l2 l3 : list nat), subseq l1 l2 -> subseq l1 (l2 ++ l3). (*| .. solution:: .. coq:: |*) Proof. intros l1 l2 l3 H. induction H. - (* sub_nil *) apply sub_nil. - (* sub_take *) simpl. apply sub_take. apply IHsubseq. - (* sub_skip *) simpl. apply sub_skip. apply IHsubseq. Qed. (*| .. coq:: |*) Theorem subseq_trans : forall (l1 l2 l3 : list nat), subseq l1 l2 -> subseq l2 l3 -> subseq l1 l3. (*| .. solution:: .. coq:: |*) Proof. (* Hint: be careful about what you are doing induction on and which other things need to be generalized... *) intros l1 l2 l3 S12 S23. generalize dependent l1. induction S23 as [|x l2 l3 |x l2 l3]. - (* sub_nil *) intros l1 S12. inversion S12. apply sub_nil. - (* sub_take *) intros l1 S12. inversion S12. apply sub_nil. apply sub_take. apply IHS23. apply H1. apply sub_skip. apply IHS23. apply H1. - (* sub_skip *) intros l1 S12. apply sub_skip. apply IHS23. apply S12. Qed.