Documentation

Mathlib.Data.Tree

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.

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.instInhabitedTree {α : Type u} :
    Equations
    • Tree.instInhabitedTree = { default := Tree.nil }
    def Tree.ofRBNode {α : Type u} :
    Std.RBNode αTree α

    Makes a Tree α out of a red-black tree.

    Equations
    Instances For
      def Tree.indexOf {α : Type u} (lt : ααProp) [DecidableRel lt] (x : α) :

      Finds the index of an element in the tree assuming the tree has been constructed according to the provided decidable order on its elements. If it hasn't, the result will be incorrect. If it has, but the element is not in the tree, returns none.

      Equations
      • One or more equations did not get rendered due to their size.
      • Tree.indexOf lt x Tree.nil = none
      Instances For
        def Tree.get {α : Type u} :
        PosNumTree αOption α

        Retrieves an element uniquely determined by a PosNum from the tree, taking the following path to get to the element:

        Equations
        Instances For
          def Tree.getOrElse {α : Type u} (n : PosNum) (t : Tree α) (v : α) :
          α

          Retrieves an element from the tree, or the provided default value if the index is invalid. See Tree.get.

          Equations
          Instances For
            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. TODO: implement Traversable Tree.

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

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

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

                The number of leaves of a binary tree

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

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

                  Equations
                  Instances For
                    theorem Tree.numLeaves_pos {α : Type u} (x : Tree α) :
                    def Tree.left {α : Type u} :
                    Tree αTree α

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

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

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

                      Equations
                      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) :