Problem 55

(Intermediate 🌟🌟) Construct completely balanced binary trees.

In a completely balanced binary tree, the following property holds for every node: The number of nodes in its left subtree and the number of nodes in its right subtree are almost equal, which means their difference is not greater than one.

Write a function cbalTree to construct completely balanced binary trees for a given number of nodes. The predicate should generate all solutions via backtracking.

inductive BinTree (α : Type) where
  | empty : BinTree α
  | node : α → BinTree α → BinTree α → BinTree α
deriving Repr

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

def BinTree.depth {α : Type} : BinTree α → Nat
| .empty => 0
| .node _ l r => 1 + max l.depth r.depth

def BinTree.isBalanced {α : Type} : BinTree α → Bool
  | .empty => true
  | .node _ l r =>
    l.isBalanced ∧ r.isBalanced ∧
    Int.natAbs ((l.depth : Int) - (r.depth : Int)) ≤ 1

/-- 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

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

#eval (cbalTree 3).length = 1
#eval (cbalTree 3)|>.map BinTree.isBalanced |>.and
#eval (cbalTree 4)|>.map BinTree.isBalanced |>.and
#eval (cbalTree 4).length = 4
#eval (cbalTree 5)|>.map BinTree.isBalanced |>.and
#eval (cbalTree 6)|>.map BinTree.isBalanced |>.and
#eval (cbalTree 7).length = 1