Documentation

Mathlib.Data.Tree.Basic

Binary tree #

Provides binary tree storage for values of any type, with O(lg n) retrieval. See also Lean.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.

TODO #

Implement a Traversable instance for Tree.

References #

https://leanprover-community.github.io/archive/stream/113488-general/topic/tactic.20question.html

inductive Tree (α : Type u) :

A binary tree with values stored in non-leaf nodes.

Instances For
    instance instDecidableEqTree :
    {α : Type u_1} → [inst : DecidableEq α] → DecidableEq (Tree α)
    Equations
    • instDecidableEqTree = decEqTree✝
    instance instReprTree :
    {α : Type u_1} → [inst : Repr α] → Repr (Tree α)
    Equations
    • instReprTree = { reprPrec := reprTree✝ }
    instance Tree.instInhabited {α : Type u} :
    Equations
    • Tree.instInhabited = { default := Tree.nil }
    def Tree.map {α : Type u} {β : Type u_1} (f : αβ) :
    Tree αTree β

    Apply a function to each value in the tree. This is the map function for the Tree functor.

    Equations
    Instances For
      def Tree.numNodes {α : Type u} :
      Tree α

      The number of internal nodes (i.e. not including leaves) of a binary tree

      Equations
      • Tree.nil.numNodes = 0
      • (Tree.node a a_1 a_2).numNodes = a_1.numNodes + a_2.numNodes + 1
      Instances For
        def Tree.numLeaves {α : Type u} :
        Tree α

        The number of leaves of a binary tree

        Equations
        • Tree.nil.numLeaves = 1
        • (Tree.node a a_1 a_2).numLeaves = a_1.numLeaves + a_2.numLeaves
        Instances For
          def Tree.height {α : Type u} :
          Tree α

          The height - length of the longest path from the root - of a binary tree

          Equations
          • Tree.nil.height = 0
          • (Tree.node a a_1 a_2).height = max a_1.height a_2.height + 1
          Instances For
            theorem Tree.numLeaves_eq_numNodes_succ {α : Type u} (x : Tree α) :
            x.numLeaves = x.numNodes + 1
            theorem Tree.numLeaves_pos {α : Type u} (x : Tree α) :
            0 < x.numLeaves
            theorem Tree.height_le_numNodes {α : Type u} (x : Tree α) :
            x.height x.numNodes
            def Tree.left {α : Type u} :
            Tree αTree α

            The left child of the tree, or nil if the tree is nil

            Equations
            • Tree.nil.left = Tree.nil
            • (Tree.node a a_1 a_2).left = a_1
            Instances For
              def Tree.right {α : Type u} :
              Tree αTree α

              The right child of the tree, or nil if the tree is nil

              Equations
              • Tree.nil.right = Tree.nil
              • (Tree.node a a_1 a_2).right = a_2
              Instances For
                def Tree.unitRecOn {motive : Tree UnitSort u_1} (t : Tree Unit) (base : motive Tree.nil) (ind : (x y : Tree Unit) → motive xmotive ymotive (Tree.node () x y)) :
                motive t
                Equations
                Instances For
                  theorem Tree.left_node_right_eq_self {x : Tree Unit} (_hx : x Tree.nil) :
                  Tree.node () x.left x.right = x