Finite maps

Stream: general

[Ben Sherman]

Is there a Lean (3) library for finite maps (i.e., key-value maps where finitely many keys are mapped to values)? I don't need performance, just reasoning really. But I'd also be fine if the key type requires decidable ordering (I would assume it would require at least decidable equality). Should I use this https://github.com/spl/lean-finmap?

[Reid Barton]

There's data.rbmap in the Lean standard library, does that meet your needs?

[Mario Carneiro]

There is also the finmap branch of leanprover-community which is porting Sean's work to mathlib

[Mario Carneiro]

and hash_map is also a finite map type

[Mario Carneiro]

on the non-computational side, finsupp is basically the type of finite maps (mapping everything out of domain to 0)

[Ben Sherman]

I'm looking for something that has unions and theorems about them. In this regard, both data.rbmap and data.hash_map are incomplete. And I do want to write programs, so finsupp is not what I'm looking for either. So it sounds like finmap is the way to go! Thanks for pointing me to the finmap branch of mathlib - I guess I'll use that. Thanks for the pointers, everyone!

[Mario Carneiro]

Ah, that's good to know. I'll work on adding unions to rbmap and hash_map