Require Import List. Import ListNotations. Require Import PeanoNat. Import Nat. (* Question 1: a) Define a recursive function replace so that replace n m l replaces every occurrence of the natural number n by the number m in the list l. Example: Eval compute in replace 2 3 [1;2;3;2;1]. yields [1; 3; 3; 3; 1]. Hint: - Use x =? y two compare two natural numbers (returns bool). *) Fixpoint replace (n m : nat) (l : list nat) : list nat := match l with | [] => [] | a :: l' => if a =? n then m :: replace n m l' else a :: replace n m l' end. (* b) Prove the lemma below. Hints: - Use induction on l. - Use the tactic contradiction if your assumptions are contradictory. - *) Lemma L1 : forall (n m : nat) (l : list nat), In n (replace n m l) -> m=n. Proof. intros. induction l; simpl in H. contradiction. case_eq (a =? n); intro; rewrite H0 in H; simpl in H; destruct H. trivial. apply IHl in H; trivial. apply eqb_neq in H0; contradiction. apply IHl in H; trivial. Qed. (* c) Prove the lemma below. Hints: - Use induction on l. - You might find the lemmas useful: + eqb_eq : forall n m : nat, (n =? m) = true <-> n = m + eqb_neq : forall x y : nat, (x =? y) = false <-> x <> y + f_equal : forall (A B : Type) (f : A -> B) (x y : A), x = y -> f x = f y *) Definition Injective {A B :Type} (f : A -> B) : Prop := forall (x y : A), x <> y -> f x <> f y . Lemma L2 : forall (f : nat -> nat) (n m : nat) (l : list nat), Injective f -> map f (replace n m l) = replace (f n) (f m) (map f l). Proof. intros. induction l; simpl. trivial. case_eq (a =? n); intro; simpl. apply eqb_eq in H0; apply (f_equal f) in H0; apply eqb_eq in H0. rewrite H0. rewrite IHl; trivial. apply eqb_neq in H0; apply H in H0; apply eqb_neq in H0. rewrite H0. rewrite IHl; trivial. Qed. (* Question 2: a) Define the data type tree A of binary trees that store elements of an arbitrary type A in the leaves and in the inner nodes. An example of a tree of type tree nat is visualized below. Note that this is not the actual implementation, of course. 2 / \ 3 1 / \ 1 4 *) Inductive tree (A : Type) : Type := | leaf : A -> tree A | node : A -> tree A -> tree A -> tree A. (* b) Implement a recursive function mapTree that applies a function f : A -> B to all elements in a tree of type tree A returning a tree of type tree B. Example: map S "tree from a)" yields the tree 3 / \ 4 2 / \ 2 5 *) Fixpoint mapTree {A B : Type} (f : A -> B) (t : tree A) : tree B := match t with | leaf _ x => leaf _ (f x) | node _ x tl tr => node _ (f x) (mapTree f tl) (mapTree f tr) end. (* c) Implement a recursive function collapse that collects all elements in a tree of type tree A in a list of type list A. Collect the elements in a infix manner, i.e., first the elements of the left subtree, then the element at the current node followed by the elements in the right subtree. Example: collapse "tree from a)" yields [1;3;4;2;1]. Hint: Use the append function ++. *) Fixpoint collapse {A : Type} (t : tree A) : list A := match t with | leaf _ x => [x] | node _ x tl tr => collapse tl ++ [x] ++ collapse tr end. (* d) Prove the lemma below. Hints: - Use induction on the tree t. - You might find the lemma map_app : forall (A B : Type) (f : A -> B) (l l' : list A), map f (l ++ l') = map f l ++ map f l' useful. *) Lemma L3 {A B : Type} : forall (f : A -> B) (t : tree A), collapse (mapTree f t) = map f (collapse t). Proof. intros. induction t0; simpl. trivial. rewrite IHt0_1, IHt0_2. rewrite map_app; simpl; trivial. Qed.