Problem 58

Apply the generate-and-test paradigm to construct all symmetric, completely balanced binary trees with a given number of nodes.

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

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

variable {α : Type}

section
  /- pretty print of binary tree -/
  variable [ToString α]

  def String.addIndent (s : String) (depth : Nat) : String :=
    Nat.repeat (fun s => " " ++ s) depth s

  def BinTree.toString (tree : BinTree α) : String :=
    aux tree 2
  where
    aux (tree : BinTree α) (depth : Nat) : String :=
      match tree with
      | .node v .empty .empty => s!"leaf {v}"
      | .node v l r =>
        let ls := aux l (depth + 2)
        let rs := aux r (depth + 2)
        s!".node {v}\n" ++ s!"{ls}\n".addIndent depth ++ s!"{rs}\n".addIndent depth
      | .empty => "empty"

  instance {α : Type} [ToString α] : ToString (BinTree α) := ⟨BinTree.toString⟩
end

#eval BinTree.node 3 (.node 2 (leaf 1) .empty) (.node 5 .empty (leaf 7))

#eval BinTree.node 'x' (leaf 'x') (leaf 'x')

#eval BinTree.node 'x' .empty (leaf 'x')

#eval BinTree.node 'x' (leaf 'x') .empty

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

def BinTree.mirror (s t : BinTree α) : Bool :=
  match s, t with
  | .empty, .empty => true
  | .node _ a b, .node _ x y => mirror a y && mirror b x
  | _, _ => false

def BinTree.isSymmetric (t : BinTree α) : Bool :=
  match t with
  | .empty => true
  | .node _ l r => mirror l r

/-- construct all balanced, symmetric binary trees with given number of elements -/
def symCbalTrees (n : Nat) : List (BinTree Unit) :=
  sorry

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

#guard (symCbalTrees 5).length = 2
#guard (symCbalTrees 6).length = 0
#guard (symCbalTrees 7).length = 1
#guard (symCbalTrees 8).length = 0