feat(data/tree): Add definitions about binary trees; special support …

…for `tree unit` (#16715)

Provide convenience API for `tree unit`. In particular, define a recursor for `tree unit` as well as other helper lemmas.

In addition, define common functions on binary trees such as `nodes`, `num_leaves`, `height`, and prove basic lemmas about these functions, such as the fact that the number of leaves is one more than the number of internal nodes and the height is at most the number of nodes.



Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

src/data/tree.lean

@@ -5,6 +5,7 @@ Authors: Mario Carneiro, Wojciech Nawrocki
 -/
 import data.rbtree.init
 import data.num.basic
+import order.basic
 
 /-!
 # Binary tree
@@ -13,6 +14,10 @@ Provides binary tree storage for values of any type, with O(lg n) retrieval.
 See also `data.rbtree` for red-black trees - this version allows more operations
 to be defined and is better suited for in-kernel computation.
 
+We also specialize for `tree unit`, which is a binary tree without any
+additional data. We provide the notation `a △ b` for making a `tree unit` with children
+`a` and `b`.
+
 ## References
 
 <https://leanprover-community.github.io/archive/stream/113488-general/topic/tactic.20question.html>
@@ -81,4 +86,56 @@ def map {β} (f : α → β) : tree α → tree β
 | nil := nil
 | (node a l r) := node (f a) (map l) (map r)
 
+/-- The number of internal nodes (i.e. not including leaves) of a binary tree -/
+@[simp] def num_nodes : tree α → ℕ
+| nil := 0
+| (node _ a b) := a.num_nodes + b.num_nodes + 1
+
+/-- The number of leaves of a binary tree -/
+@[simp] def num_leaves : tree α → ℕ
+| nil := 1
+| (node _ a b) := a.num_leaves + b.num_leaves
+
+/-- The height - length of the longest path from the root - of a binary tree -/
+@[simp] def height : tree α → ℕ
+| nil := 0
+| (node _ a b) := max a.height b.height + 1
+
+lemma num_leaves_eq_num_nodes_succ (x : tree α) : x.num_leaves = x.num_nodes + 1 :=
+by { induction x; simp [*, nat.add_comm, nat.add_assoc, nat.add_left_comm], }
+
+lemma num_leaves_pos (x : tree α) : 0 < x.num_leaves :=
+by { rw num_leaves_eq_num_nodes_succ, exact x.num_nodes.zero_lt_succ, }
+
+lemma height_le_num_nodes : ∀ (x : tree α), x.height ≤ x.num_nodes
+| nil := le_rfl
+| (node _ a b) := nat.succ_le_succ
+    (max_le
+      (trans a.height_le_num_nodes $ a.num_nodes.le_add_right _)
+      (trans b.height_le_num_nodes $ b.num_nodes.le_add_left _))
+
+/-- The left child of the tree, or `nil` if the tree is `nil` -/
+@[simp] def left : tree α → tree α
+| nil := nil
+| (node _ l r) := l
+
+/-- The right child of the tree, or `nil` if the tree is `nil` -/
+@[simp] def right : tree α → tree α
+| nil := nil
+| (node _ l r) := r
+
+/- Notation for making a node with `unit` data -/
+localized "infixr ` △ `:65 := tree.node ()" in tree
+
+/-- Recursion on `tree unit`; allows for a better `induction` which does not have to worry
+  about the element of type `α = unit` -/
+@[elab_as_eliminator]
+def unit_rec_on {motive : tree unit → Sort*} (t : tree unit) (base : motive nil)
+  (ind : ∀ x y, motive x → motive y → motive (x △ y)) : motive t :=
+t.rec_on base (λ u, u.rec_on (by exact ind))
+
+lemma left_node_right_eq_self : ∀ {x : tree unit} (hx : x ≠ nil), x.left △ x.right = x
+| nil h := by trivial
+| (a △ b) _ := rfl
+
 end tree