(* Homework 01 *)
(* include some library code *)
Require Import List.
Require Import NPeano.
(* decide if two nats are equal *)
Fixpoint nat_eq (m n: nat) : bool :=
match m, n with
| O, O => true
| S mp, S np => nat_eq mp np
| _, _ => false
end.
(* [PROBLEM 1]
Define nat_le to decide if one nat is less than or equal to another.
Hint: You do not need to use any form of disjunction.
*)
Fixpoint nat_le (m n: nat) : bool :=
(* TODO *)
false.
Eval cbv in (nat_le 5 5). (* true *)
Eval cbv in (nat_le 3 5). (* true *)
Eval cbv in (nat_le 5 3). (* false *)
(* [PROBLEM 2]
Uset nat_le to define nat_lt which should decide if one nat is less than another.
For full credit, do not use other boolean functions.
*)
Definition nat_lt (m n: nat) : bool :=
(* TODO *)
false.
Eval cbv in (nat_lt 5 5). (* false *)
Eval cbv in (nat_lt 3 5). (* true *)
Eval cbv in (nat_lt 5 3). (* false *)
(* binary trees of nats *)
Inductive nat_tree : Set :=
| Leaf : nat_tree
| Branch : nat -> nat_tree -> nat_tree -> nat_tree.
(* ordered insertion *)
Fixpoint insert (n: nat) (nt: nat_tree) : nat_tree :=
match nt with
| Leaf => Branch n Leaf Leaf
| Branch m tl tr =>
if nat_lt n m then
Branch m (insert n tl) tr
else
Branch m tl (insert n tr)
end.
(* [PROBLEM 3]
Define of_list to produce an ordered tree containing all elements from the list.
Use insert to help with sorting. Do not worry about duplicates in the list.
*)
Fixpoint of_list (ns: list nat) : nat_tree :=
(* TODO *)
Leaf.
(* [PROBLEM 4]
Define to_list, which provides a list of elements generated by an in-order traversal of the tree nt.
For the difference between in-order, post-order, and pre-order traversals, see:
http://en.wikipedia.org/wiki/Tree_traversal
Recall from lecture that we can append with the ++ operator.
*)
Fixpoint to_list (nt: nat_tree) : list nat :=
(* TODO *)
nil.
(* [PROBLEM 5]
Define sum to add up all the nats in a nat_tree.
*)
Fixpoint sum (nt: nat_tree) : nat :=
(* TODO *)
0.
(* [PROBLEM 6]
Define prod to multiply up all the nats in a nat_tree.
*)
Fixpoint prod (nt: nat_tree) : nat :=
(* TODO *)
1.
(* [PROBLEM 7]
Define size to produce the number of nats in a nat_tree.
Note that Leaf should have size 0.
*)
Fixpoint size (nt: nat_tree) : nat :=
(* TODO *)
0.
(* [PROBLEM 8]
Define avg to compute the arithmetic mean of all the nats in a nat_tree.
Notes: Infix / is nat division. The average of an empty tree will be 0.
*)
Definition avg (nt: nat_tree) : nat :=
(* TODO *)
0.
(* [PROBLEM 9]
Define map to apply a function of type nat -> nat to every nat in a nat_tree.
The resulting tree should have exactly the same structure as the initial tree.
*)
Fixpoint map (f: nat -> nat) (nt: nat_tree) : nat_tree :=
(* TODO *)
Leaf.
(* [PROBLEM 10]
Define increment_all to add one to all the nats in a nat_tree.
For full credit, do not use recursion (keep the Definition, don't change to Fixpoint).
*)
Definition increment_all (nt: nat_tree) : nat_tree :=
(* TODO *)
Leaf.
(* fold over nat_trees *)
Fixpoint fold {T: Type} (base: T) (f: T -> nat -> T) (nt: nat_tree) : T :=
match nt with
| Leaf => base
| Branch n l r => f (fold (fold base f l) f r) n
end.
(* [PROBLEM 11]
Define sum' to add up all the nats in a nat_tree.
For full credit, do not use recursion (keep the Definition, don't change to Fixpoint).
*)
Definition sum' := (* TODO *) 0.
(* [PROBLEM 12]
Define prod' to multiply up all the nats in a nat_tree.
For full credit, do not use recursion (keep the Definition, don't change to Fixpoint).
*)
Definition prod' := (* TODO *) 1.
(* [PROBLEM 13]
Define avg' to compute the arithmetic mean of all the nats in a nat_tree.
For full credit, use fold.
Hint: Use let and a pair.
*)
Definition avg' (nt: nat_tree) : nat :=
(* TODO (hint: use let) *)
0.
(* [PROBLEM 14]
Define mirror to flip all the branches in the tree:
5 5
/ \ / \
3 4 => 4 3
/ \ / \
1 6 6 1
(leaves are not displayed above)
*)
Fixpoint mirror (nt: nat_tree) : nat_tree :=
(* TODO *)
Leaf.
(* test if a nat appears in a given tree *)
Fixpoint mem (n: nat) (nt: nat_tree) : bool :=
match nt with
| Leaf => false
| Branch m l r =>
if nat_eq n m then
true
else if nat_lt n m then
mem n l
else
mem n r
end.
(* prove all the following lemmas *)
(* Warning! This first one may be tricky... *)
Lemma nat_eq_ok:
forall m n, nat_eq m n = true -> m = n.
Proof.
(* [PROBLEM 15] *)
Admitted.
Lemma nat_le_ok:
forall m n, nat_le m n = true -> m <= n.
Proof.
(* [PROBLEM 16] *)
Admitted.
(* Hint: use nat_le_ok *)
Lemma nat_lt_ok:
forall m n, nat_lt m n = true -> m < n.
Proof.
(* [PROBLEM 17] *)
Admitted.
(* Show that our nat equality decider is reflexive. *)
Lemma nat_eq_refl : forall n, nat_eq n n = true.
Proof.
(* [PROBLEM 18] *)
Admitted.
Theorem map_size : forall f t, size (map f t) = size t.
Proof.
(* [PROBLEM 19] *)
Admitted.
Theorem mirror_size : forall t, size (mirror t) = size t.
Proof.
(* [PROBLEM 20] *)
Admitted.
(*
We define the custom tactic break_if to help with some proofs below.
Don't worry about understanding the details for now.
Just remember that if you see an if-then-else, break_if will do case analysis on the branch condition and give you two subgoals: one where the branch condition was true and so the then branch was taken, and another where the branch condition was false and so the else branch was taken.
*)
Ltac break_if :=
match goal with
| |- context [ if ?cond then _ else _ ] => destruct cond as [] eqn:?
end.
Lemma mem_left : forall v l r, mem v l = true -> mem v (Branch v l r) = true.
Proof.
(* [PROBLEM 21] *)
Admitted.
Lemma mem_right : forall v l r, mem v r = true -> mem v (Branch v l r) = true.
Proof.
(* [PROBLEM 22] *)
Admitted.
(* using the previous lemmas and tactics, prove that insertion implies membership *)
Theorem insert_mem :
forall v t, mem v (insert v t) = true.
Proof.
(* [PROBLEM 23] *)
Admitted.
(* [PROBLEM 24]
Consider this alternate definition of fold:
*)
Fixpoint fold' {T: Type} (base: T) (f: T -> nat -> T) (nt: nat_tree) : T :=
match nt with
| Leaf => base
| Branch n l r => fold' (f (fold' base f l) n) f r
end.
(*
In a short English paragraph, describe how fold and fold' differ.
(* TODO write here *)
Optional Bonus (5 points):
What should be true about a particular f for the following to hold:
forall b nt, fold b f nt = fold' b f nt
(* TODO write here *)
*)