Trees

Stream: new members

[Callum August]

Hello, I was wondering if anyone knows of any work on trees in Lean? I have looked at rbtree and mathlib tree.

[Johan Commelin]

Do you mean tree as in graph theory, or as in data structure?

[Johan Commelin]

I think there is theoretical overlap, but probably not much practical overlap

[Callum August]

As in the data structure

[Adam Topaz]

I don't really know much about this, and I don't really know what tree means, but I was under the impression that W-types subsume all possible definitions of tree.

[Adam Topaz]

src#W

[Christopher Iliffe Sprague]

Hi! I am new to Lean. My closest related experience is with Mathematica.
I am working on a special problem, and I am not sure whether I should use Mathematica or Lean.
I have a family of sets that are indexed by an ordered tree, and their relations between eachother depends on their indexing.
I need to prove that some of these sets are disjoint.
Should I stick with Mathematica or use Lean for this?

[Kevin Buzzard]

can you prove anything with Mathematica? What do you mean by prove?

[Christopher Iliffe Sprague]

Kevin Buzzard said:

can you prove anything with Mathematica? What do you mean by prove?

Thanks for your response! From what I've read you can use first-order logic to prove some thing like this: https://reference.wolfram.com/language/ref/FindEquationalProof.html.
By "prove", I mean state a theorem and prove it with a set of lemmas. Forgive me if I am not using the correct parlance.
From further reading, it seem Lean can do pretty much anything. So, now my question is: could I transfer what I produce in Lean to human-readable math in latex?

[Kevin Buzzard]

Oh, I didn't know Mathematica could do proofs like that -- that's why I was confused.

[Christopher Iliffe Sprague]

Kevin Buzzard said:

Oh, I didn't know Mathematica could do proofs like that -- that's why I was confused.

Could you give me a recommendation on where to start for coding ordered trees and families of sets (in Euclidan space) that are indexed by such a tree?

[Bryan Gin-ge Chen]

We have a page of learning resources here. I recommend working through the Natural Number Game and some of the other tutorials to see what it's like to use Lean.

[Huỳnh Trần Khanh]

could I transfer what I produce in Lean to human-readable math in latex?

I'm afraid you have to do that manually—currently there are no usable tools and Lean proofs are not intended to be read outside of a Lean-aware text editor. Tactics can mutate the context and the mutations can be pretty hard to trace without the infoview, which is the right pane in Visual Studio Code with the Lean extension and the Lean web interface.