(** * Lab: Induction in Coq *) Require Import List Arith. (**********************************************************************) (* Exercise: app_assoc coq [1 star]. In Coq, the list append operator is written [++]. Complete the following proof by induction, which shows that application is associative. Hint: the solution is in the lecture slides. *) Theorem app_assoc : forall (A:Type) (l1 l2 l3 : list A), l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3. Proof. intros A l1 l2 l3. induction l1 as [ | h t IH]. (* FILL IN, and change [Abort] to [Qed]. *) Abort. (**********************************************************************) (* Exercise: app_assoc math [2 star]. Prove that the OCaml [@] operator is also associative. Your answer should be a mathematical proof, not a Coq proof. We have supplied part of the proof for you. Theorem: for all lists lst1, lst2, and lst3, lst1 @ (lst2 @ lst3) = (lst1 @ lst2) @ lst3. Proof: by induction on lst1. The property being proved is: P(l) = FILL IN Case: lst1 = [] Show: FILL IN Case: lst1 = h::t IH: FILL IN Show: FILL IN QED *) (**********************************************************************) (* Exercise: rev_append math [3 star]. Prove the following theorem, which shows how list reversal distributes over list append. Theorem: for all lists lst1 and lst2, rev (lst1 @ lst2) = rev lst2 @ rev lst1. Recall that [rev] is defined as follows: << let rec rev = function | [] -> [] | h::t -> rev t @ [h] >> Your answer should be a mathematical proof, not a Coq proof. In the inductive case, you will need the lemma proved above saying that append is associative. In the base case, you will need this lemma: Lemma: for all lists lst, lst @ [] = lst. Proof: given in lecture. Here, again, is the theorem you should prove: Theorem: for all lists lst1 and lst2, rev (lst1 @ lst2) = rev lst2 @ rev lst1. Proof: FILL IN *) (**********************************************************************) (* Exercise: rev_append coq [3 star]. Now prove the same theorem as the previous exercise, but in Coq. The Coq list reversal function [rev] is defined in the standard library for you. Use the mathematical proof you gave above as a guide. For the base case, you will need the lemma [app_nil] that we proved in lecture; we've inserted the code for it below. You can use that lemma in your own proof with the [rewrite] tactic. *) Lemma app_nil : forall (A:Type) (lst : list A), lst ++ nil = lst. Proof. intros A lst. induction lst as [ | h t IH]. - trivial. - simpl. rewrite -> IH. trivial. Qed. Theorem rev_append : forall (A:Type) (lst1 lst2 : list A), rev (lst1 ++ lst2) = rev lst2 ++ rev lst1. Proof. (* FILL IN, and change [Abort] to [Qed] *) Abort. (**********************************************************************) (* Exercise: rev involutive [3 star]. Prove that [rev] is _involutive_, meaning that it is its own inverse. That is, [rev (rev lst) = lst]. Hint: for the inductive case, there is a lemma that has already been proved in this lab that you will find very helpful. Part of this exercise is figuring out which lemmma that is. *) Theorem rev_involutive : forall (A:Type) (lst : list A), rev (rev lst) = lst. Proof. (* FILL IN, and change [Abort] to [Qed] *) Abort. (**********************************************************************) (* Exercise: app_length [3 star, optional]. Prove the following theorem in Coq. *) Theorem app_length : forall (A:Type) (l1 l2 : list A), length (l1 ++ l2) = length l1 + length l2. Proof. (* FILL IN, and change [Abort] to [Qed] *) Abort. (**********************************************************************) (* Exercise: rev_length [3 star, optional]. Prove the following theorem in Coq. Hint: previous exercise(s) as lemma, and the [ring] tactic. *) Theorem app_rev : forall (A:Type) (lst : list A), length (rev lst) = length lst. Proof. (* FILL IN, and change [Abort] to [Qed] *) Abort. (**********************************************************************) (* INDUCTION ON BINARY TREES *) (* Here is a Coq type for binary trees: *) Inductive tree (A : Type) : Type := | Leaf : tree A | Node : tree A -> A -> tree A -> tree A. (* The following commands cause the [A] argument to be implicit to the [Leaf] and [Node] constructors. *) Arguments Leaf [A]. Arguments Node [A] _ _ _. (* The equivalent OCaml type would be: << type 'a tree = | Leaf | Node of 'a tree * 'a * 'a tree >> *) (* The _reflection_ operation swaps the left and right subtrees at every node. *) Fixpoint reflect {A : Type} (t : tree A) := match t with | Leaf => Leaf | Node l v r => Node (reflect r) v (reflect l) end. (* The equivalent OCaml function would be: << let rec reflect = function | Leaf -> Leaf | Node (l,v,r) -> Node (reflect r, v, reflect l) >> *) (* A proof by induction on a binary tree has the following structure: Theorem: For all binary trees t, P(t). Proof: by induction on t. Case: t = Leaf Show: P(Leaf) Case: t = Node(l,v,r) IH1: P(l) IH2: P(r) Show: P(Node(l,v,r)) QED Note that we get _two_ inductive hypotheses in the inductive case, one for each subtree. *) (**********************************************************************) (* Exercise: tree_ind [2 star]. Explain the output of the following command in your own words, relating it to the proof structure given above for induction on binary trees. Hint: read the notes on induction principles. *) Check tree_ind. (**********************************************************************) (* Exercise: reflect_involutive math [3 star]. Prove the following theorem mathematically (not in Coq). Theorem: for all trees t, reflect (reflect t) = t Proof: by induction on t. P(t) = reflect (reflect t) = t Case: t = Leaf Show: FILL IN Case: t = Node(l,v,r) IH1: P(l) = reflect(reflect l) = l IH2: P(r) = reflect(reflect r) = r Show: FILL IN QED *) (**********************************************************************) (* Exercise: reflect_involutive coq [3 star]. State and prove a theorem in Coq that shows reflect is involutive. Use your mathematical proof from the previous exercise as a guide. Hint: the [induction] tactic expects the arguments for the inductive case in the following order: the left subtree, the IH for the left subtree, the value at the node, the right subtree, and the IH for the right subtree. *) (* UNCOMMENT AND COMPLETE Theorem reflect_involutive : ... *) (**********************************************************************) (* Exercise: height [4 star]. 1. Write a Coq function [height] that computes the height of a binary tree. Recall that the height of a leaf is 0, and the height of a node is 1 more than the maximum of the heights of its two subtrees. The standard library does contain a [max] function that will be helpful. 2. Prove that [reflect] preserves the height of a tree. Hint: [Nat.max_comm]. 3. Write a Coq function [perfect : nat -> tree nat], such that [perfect h] constructs the perfect binary tree of height [h], and the value at the root is [1], and if the value at a node is [v], then the values of its left and right subnodes are [2*v] and [2*v+1]. For example, [perfect 3] is << Node (Node (Node Leaf 4 Leaf)  2  (Node Leaf 5 Leaf))  1 (Node (Node Leaf 6 Leaf)  3  (Node Leaf 7 Leaf)) >> 4. Prove that the height of [perfect h] is in fact [h]. Hint 1: induct on [h]. Hint 2: don't introduce all the variables. Hint 3: [Nat.max_idempotent]. *)