Binary tree get operation

In this file we define Tree.indexOf, Tree.get, and Tree.getOrElse. These definitions were moved from the main file to avoid a dependency on Num.

References

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

def Tree.indexOf {α : Type u_1} (lt : α → α → Prop) [DecidableRel lt] (x : α) : Tree α → Option PosNum

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

def Tree.get {α : Type u_1} : PosNum → Tree α → Option α

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

• bit0 - go to left child
• bit1 - go to right child
• PosNum.one - retrieve from here

Equations

• Tree.get x Tree.nil = none
• Tree.get PosNum.one (Tree.node a _t₁ _t₂) = some a
• Tree.get n.bit0 (Tree.node _a t₁ _t₂) = Tree.get n t₁
• Tree.get n.bit1 (Tree.node _a _t₁ t₂) = Tree.get n t₂

def Tree.getOrElse {α : Type u_1} (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

• Tree.getOrElse n t v = (Tree.get n t).getD v