dictionary / map type: ordset

Stream: general

[Mario Carneiro]

I've been playing around with conventional programming in lean lately (thank you Advent of Code), and it has made me realize that our capabilities with finite maps is quite limited. Currently, we have:

• native.rb_map: meta interface to a C++ implementation of red black trees
• rbmap: lean implementation of red black trees in core
• finmap: maps via association lists (in mathlib)
• finsupp: finitely supported functions (non computational)

The only one which is really suitable for computation is rbmap (finmap is too slow, since it is implemented with lists, although it is useful for specifications and verified computation), and it is implemented in core with basically only two operations: insert and find. And because the well-formedness condition is incorrect, you can't even implement more operations, like erase.

So I decided to start anew with weight balanced trees, as a direct port from Haskell's Data.Set. The result is the ordnode A type, which has a very complete set of operations for working with sets and maps. The library for ordset A is still under development but will incorporate the correct invariants on top of ordnode A so that the usual properties are provable.

PS: The names ordnode, ordset, ordmap are a bit inelegant, I'm open to suggestions.

[Gabriel Ebner]

ordset α does not seem to be isomorphic to finset α---is this intentional?

[Mario Carneiro]

I added the equivalence relatively recently (ordnode.equiv). I will change ordset to be a quotient of the current subtype

[Mario Carneiro]

Also it's not going to be isomorphic to finset A anyway, because of preorder stuff

[Mario Carneiro]

I think the ordsets over a linear order should be isomorphic to finset A

[Mario Carneiro]

(more precisely, over a total preorder, a ordset A can only represent a comparability antichain, i.e. x, y \in s and x <= y and y <= x implies x = y)

[Gabriel Ebner]

Yeah, with the quotient they should be isomorphic for total orders.

[Joe Hendrix]

I had my own version of rb trees while back (https://github.com/joehendrix/lean-containers/). It uses quotients so we can get a decidable equivalence relation.
I had to put it on hold for other projects, and only got around to insert (so it's close to the existing rbmap capabilities). I think it also probably doesn't work with the latest lean 3. Maps are implemented on top of sets.

[Edward Ayers]

I ported Coq's implementation of RB trees (sans proofs). I also didn't test it much so has bugs.
https://github.com/EdAyers/edlib/blob/master/rb.lean

[Edward Ayers]

For naming, I vote table