Problem 59

Construct height-balanced binary trees.

/-- binary tree -/
inductive BinTree (α : Type) where
  | empty : BinTree α
  | node : α → BinTree α → BinTree α → BinTree α

deriving Repr

def leaf {α : Type} (a : α) : BinTree α := .node a .empty .empty

variable {α : Type} [ToString α]

def BinTree.height (t : BinTree α) : Nat :=
  match t with
  | .empty => 0
  | .node _ l r => 1 + max l.height r.height

/-- monad instance of `List` -/
instance : Monad List where
  pure := @List.pure
  bind := @List.bind
  map := @List.map

/-- construct all balanced binary trees which contains `x` elements -/
partial def cbalTree (x : Nat) : List (BinTree Unit) :=
  sorry

variable {β : Type}

def List.product (as : List α) (bs : List β) : List (α × β) := do
  let a ← as
  let b ← bs
  return (a, b)

/-- construct all balanced binary trees whose hight is `height`. -/
def hbalTrees (height : Nat) : List (BinTree Unit) :=
  sorry

-- The following codes are for test and you should not edit these.

#guard (hbalTrees 2 |>.length) = 2
#guard (hbalTrees 3 |>.length) = 4