(* CIS670, Homework 4 *)
(* Try to do this assignment "from memory" as much as possible,
without peeking at CPDT. If you need a hint, reread the
appropriate sections in CPDT without touching the keyboard, then
close the book and try again. *)
Module BinaryTrees.
Inductive binary : Set :=
| leaf : nat -> binary
| node : (binary * binary) -> binary.
(* TODO:
- write down the type of the induction principle that Coq will
generate for [binary] (without asking Coq for help)
- use Coq to check your answer
- write down the type of the _most natural / useful_ induction
principle for [binary]
- construct a term that has this type
*)
End BinaryTrees.
(* *************************************************************** *)
Module InfiniteBranchingTrees.
Inductive tree : Set :=
| leaf : tree
| node : (nat -> tree) -> tree.
(* TODO:
- Build a suitable induction principle (by hand) *)
End InfiniteBranchingTrees.
(* *************************************************************** *)
Module RB.
(* Here is a simple datatype declaration describing one of the key
structural properties of red-black trees -- the fact that both
children of a red node must be black. *)
Inductive node : Set :=
| R : red -> node
| B : black -> node
with red : Set :=
| RN : nat -> black -> black -> red
with black : Set :=
| BL : black
| BN : nat -> node -> node -> black.
(* TODO:
- write down the type of the _most natural / useful_ induction
principle for [node]
- use [Scheme] to construct a term that has this type
- construct another term of this type without using [Scheme]
*)
End RB.