tree

Stream: general

[Kind Bubble]

Where can I find the Lean 4 documentation for trees?

[Jason Rute]

There are so many ways to define a tree both in math and in code. You need to provide more information about what you are looking for. First, is this for programming or theorem proving? If programming, what kind of trees and why do you think there would be a standard library for trees. Most languages don’t have trees or graphs in their std library. If for theorem proving, most of that hasn’t been ported yet to lean 4, but the same questions remain: what kind of trees and for what use case? I bet there is some work in various types of trees in mathlib for lean 3 which you can browse.

[Jason Rute]

(deleted)

[Jireh Loreaux]

Well, we have docs4#Lean.RBTree

[Jason Rute]

In lean 3, I found docs#tree and docs#bin_tree which are both definitions of binary trees.

[Jason Rute]

(To be clear, when I said most stand libraries don’t have trees, I meant a general purpose one-size fits all “tree”. They often have specific tree based data structures like heaps, red-black trees, tries, etc.)

[Jason Rute]

Also, the Inductive Types section of Theorem proving in Lean 4 has examples of both binary trees and trees with an arbitrary number of children (including finitely and countably infinite branching trees). Those would probably help you get started for your particular use case.

[Jason Rute]

@Kind Bubble One more comment on trees. Many inductive structures in functional programming naturally form trees. For example, a basic expression made of variables, a unary operator, and a binary operator forms a syntax tree.

inductive MyExpr where
  | variable (varname : String) : MyExpr
  | plus (leftExpr : MyExpr) (rightExpr : MyExpr) : MyExpr
  | negative (expr : MyExpr) : MyExpr