From ed989ff568099019c6533a4d94b27d852a5710d8 Mon Sep 17 00:00:00 2001 From: prakol16 Date: Mon, 23 Jan 2023 10:09:01 +0000 Subject: [PATCH] feat(data/tree): Add definitions about binary trees; special support for `tree unit` (#16715) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- src/data/tree.lean | 57 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 57 insertions(+) diff --git a/src/data/tree.lean b/src/data/tree.lean index 6e3e388016a30..50c55cd712a64 100644 --- a/src/data/tree.lean +++ b/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 @@ -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