(*
* This is the source code for lab 0 in 6.826. The assignment is
* borrowed from problem set 1 in Harvard's CS260r 2017 class by
* Eddie Kohler: http://www.read.seas.harvard.edu/~kohler/class/cs260r-17/
*)
Require Import Arith.
Require Import Omega.
Require Import Recdef.
Require Import List.
Require Import Program.Tactics.
Import ListNotations.
(* These comparison tactics are useful for this module. *)
Lemma compare_dec (n m:nat):
{n < m /\ n ?= m = Lt}
+ {n = m /\ n ?= m = Eq}
+ {n > m /\ n ?= m = Gt}.
Proof.
destruct (lt_eq_lt_dec n m); try destruct s.
- left; left; split; auto; apply nat_compare_lt; auto.
- left; right; split; auto; apply nat_compare_eq_iff; auto.
- right; split; auto; apply nat_compare_gt; auto.
Qed.
Ltac destruct_compare n m :=
let Hlt := fresh "Hlt" in
let Hc := fresh "Hc" in
let Hp := fresh "Hp" in
destruct (compare_dec n m) as [Hlt | Hlt];
try destruct Hlt as [Hlt | Hlt];
destruct Hlt as [Hp Hc].
(* A `nattree` is a tree of natural numbers, where every internal
node has an associated number and leaves are empty. There are
two constructors, L (empty leaf) and I (internal node).
I's arguments are: left-subtree, number, right-subtree. *)
Inductive nattree : Set :=
| L : nattree (* Leaf *)
| I : nattree -> nat -> nattree -> nattree. (* Internal nodes *)
(* Some example nattrees. *)
Definition empty_nattree := L.
Definition singleton_nattree := I L 0 L.
Definition right_nattree := I L 0 (I L 1 (I L 2 (I L 3 L))).
Definition left_nattree := I (I (I (I L 0 L) 1 L) 2 L) 3 L.
Definition balanced_nattree := I (I L 0 (I L 1 L)) 2 (I L 3 L).
Definition unsorted_nattree := I (I L 3 (I L 1 L)) 0 (I L 2 L).
(* Flatten a `nattree` into a list of nats using inorder traversal. *)
Function flatten (t:nattree) : list nat :=
match t with
| L => nil
| I l n r => flatten l ++ (n :: flatten r)
end.
Eval compute in flatten empty_nattree.
Eval compute in flatten singleton_nattree.
Eval compute in flatten right_nattree.
Eval compute in flatten left_nattree.
Eval compute in flatten balanced_nattree.
Eval compute in flatten unsorted_nattree.
(* EXERCISE: Complete this proposition, which should be `True`
iff `x` is located somewhere in `t` (even if `t` is unsorted,
i.e., not a valid binary search tree). *)
Function btree_in (x:nat) (t:nattree) : Prop :=
False.
(* EXERCISE: Complete these examples, which show `btree_in` works.
Hint: The same proof will work for every example.
End each example with `Qed.`. *)
Example btree_in_ex1 : ~ btree_in 0 empty_nattree.
Abort.
Example btree_in_ex2 : btree_in 0 singleton_nattree.
Abort.
Example btree_in_ex3 : btree_in 2 right_nattree.
Abort.
Example btree_in_ex4 : btree_in 2 left_nattree.
Abort.
Example btree_in_ex5 : btree_in 2 balanced_nattree.
Abort.
Example btree_in_ex6 : btree_in 2 unsorted_nattree.
Abort.
Example btree_in_ex7 : ~ btree_in 10 balanced_nattree.
Abort.
Example btree_in_ex8 : btree_in 3 unsorted_nattree.
Abort.
(* EXERCISE: Complete this function, which should return `true`
iff `x` is in the valid binary search tree `t` (and `false`
otherwise).
Note that this function returns `bool` (lower-case `true` and
`false`), not `Prop` (upper-case `True` and `False`), because
we imagine using it at execution time, not only in proofs. *)
Function binsearch (x:nat) (t:nattree) : bool :=
false.
(* EXERCISE: Complete these examples, which show `binsearch` works
on sorted trees but does not find some elements in unsorted trees.
End each example with `Qed.`. *)
Example binsearch_ex1 : binsearch 0 singleton_nattree = true.
Abort.
Example binsearch_ex2 : binsearch 3 right_nattree = true.
Abort.
Example binsearch_ex3 : binsearch 3 left_nattree = true.
Abort.
Example binsearch_ex4 : binsearch 3 balanced_nattree = true.
Abort.
Example binsearch_ex5 : binsearch 3 unsorted_nattree = false.
Abort.
(* In the rest of this module you will prove that your `binsearch`
is correct. There are two parts. First, we prove that if
`binsearch` returns true, then the searched-for number is in the
tree. *)
(* EXERCISE: Complete this lemma, which says that every nat that
bsearch can find is in the tree. *)
Lemma binsearch_in {x:nat} {t:nattree}:
binsearch x t = true -> btree_in x t.
Proof.
(* Remember the `destruct_compare n m` tactic! *)
Abort.
(* Then, we prove that if the searched-for number is in the
tree *and the tree is valid binary search tree*, then `binsearch`
returns true.
For this we need a definition of “valid binary search tree.”
It's important to choose a good definition. Think more like a prover
than an implementer. For proof purposes, use high-level lemmas
with less-complicated types, and don't worry about traversing the
tree multiple times. *)
(* EXERCISE: Complete this proposition, which is True iff every
number in the tree is `<= ub`. *)
Function btree_le (t:nattree) (ub:nat) : Prop :=
True.
(* EXERCISE: Complete this proposition, which is True iff every
number in the tree is `>= lb`. *)
Function btree_ge (t:nattree) (lb:nat) : Prop :=
True.
(* EXERCISE: Complete this proposition, which is True iff `t`
is a valid binary search tree---that is, an in-order traversal
visits the numbers in increasing order. *)
Function btree_sorted (t:nattree) : Prop :=
True.
(* EXERCISE: Complete this lemma, which says that every element
of a tree with an upper bound is `<=` that upper bound.
Note that the arguments are in {curly braces}, not (parens).
Arguments in curly braces are implicit; Coq will determine
them from context when the lemma is applied. *)
Lemma btree_in_le {x:nat} {t:nattree} {ub:nat}:
btree_in x t -> btree_le t ub -> x <= ub.
Proof.
(* You will probably find the `destruct_pairs` tactic useful.
This tactic unpacks long `and` chains `X /\ Y /\ ...` into
individual hypotheses. *)
Abort.
(* EXERCISE: Complete this lemma, which says that every element
of a tree with a lower bound is `>=` that lower bound. *)
Lemma btree_in_ge {x:nat} {t:nattree} {lb:nat}:
btree_in x t -> btree_ge t lb -> x >= lb.
Proof.
Abort.
(* EXERCISE: Complete this lemma, says which that in a binary
search tree, smaller elements are in left subtrees. *)
Lemma btree_sorted_in_left {x:nat} {l:nattree} {y:nat} {r:nattree}:
btree_sorted (I l y r) -> btree_in x (I l y r) -> x < y
-> btree_in x l.
Proof.
Abort.
(* EXERCISE: Complete this lemma, which says that in a binary
search tree, large elements are in right subtrees. *)
Lemma btree_sorted_in_right {x:nat} {l:nattree} {y:nat} {r:nattree}:
btree_sorted (I l y r) -> btree_in x (I l y r) -> x > y
-> btree_in x r.
Proof.
Abort.
(* EXERCISE: Complete the main lemma, which says that `binsearch`
can find every element in a binary search tree. *)
Lemma in_binsearch {x:nat} {t:nattree}:
btree_sorted t -> btree_in x t -> binsearch x t = true.
Proof.
Abort.
(* Finally, we relate the `flatten` function to the tree's contents.
The proposition `In x l` is True iff `x` is a member of `l`. *)
(* EXERCISE: Complete this lemma. *)
Lemma In_btree {x:nat} {t:nattree}:
btree_in x t <-> In x (flatten t).
Proof.
Abort.