Lean 4 Documentation How to

Stream: general

[Kind Bubble]

Hi
I have finished the tutorial for Lean 4, but many features of Lean 4 outside of this tutorial are useful to me.

Where do I go for documentation on things like:

Trees in Lean 4
Categories in Lean 4
Functors in Lean 4
Hashmaps in Lean 4
etc.

[Moritz Doll]

There is a library overview for mathlib4, see for example
docs4#Std.HashMap docs4#Functor

[Jason Rute]

Lean 4 is still a work in progress, so often the docs that Moritz mentioned (as well as the code on github) is your best bet for documentation. But when you say "categories" what do you mean? Do you mean in programming, like applicative functors, maps, monads, etc? Or mathematical category theory, like categories, natural transformations, and Yoneda's lemma? In Lean 3 at least, these are two separate libraries. For example, in programming we have docs#functor and docs#is_lawful_functor (in the control library) and on the math side we have docs#category_theory.functor (in mathlib's category theory library). The later isn't ported yet as far as I'm aware. The control library however is in Lean4 already, e.g. docs4#LawfulFunctor.

[Jason Rute]

I would however hope that Functional Programming in Lean 4 would cover some of these topics when it is finished, like functors, hashmaps, and some examples of how to make your own tree-like data structures.

[Jason Rute]

I answered about trees in #general > tree .

[Jason Rute]

@Kind Bubble A warning about docs4#Std.HashMap. Usually in functional programming, data structures are immutable and persistent. Immutable means they can't change. Persistent means you can copy them without copying the whole structure in memory. Both properties let you keep track of the history of the structure. Persistent data structures are used (I assume) for both tactic state and the environment. That is why you can click anywhere on a Lean file and get information about that place in the code. When you apply a tactic, you don't overwrite the previous tactic state, you just add onto it. Lean's docs4#List is persistent.

Lean.4 has a trick which lets you use non-persistent data structures like docs4#Array in a way which mimics procedural code. If you create a new Array at the same time that you destroy a previous Array (by no longer having any references to that array), then you will not make a copy, and instead Lean will update your old array. In a language like Rust, the compiler keeps track of this "linear usage", but in Lean you have to do it yourself.

This is all to say, if you don't want to deal with that, then you may also want to use an alternative persistent key-value store like docs4#Std.RBMap (or docs4#Std.AssocList which has its own performance issues for large lists). (There is also a docs4#Std.RBSet as well for set datastructures.) (Honestly, if your example is small enough, then using HashMap is likely not a problem, but as the HashMap grows, note that a non-linear usage pattern where you have references to both the old map and new map at the same time, may lead to a lot of copying of a large object in memory.)

I don't know if this sort of thing is well-documented anywhere, but I mention it a bit more in this PA.SE answer.

[Jannis Limperg]

Also worth mentioning docs4#Lean.PersistentHashMap and docs4#Lean.PersistentHashSet in this context.