API for association lists

Stream: CSLib

[Chris Henson]

I would like to encourage a common interface for typing contexts as association lists. As I use this more heavily in my upcoming PR for locally nameless System F, I'd like some advice on what existing infrastructure to use and upstreaming helpful API. I see three places with existing work:

• docs#List.lookup for product types with BEq keys.
• Mathlib.Data.List.Sigma for dependent pairs with DecidableEq keys.
• Std.Data.Internal.List.Associative for dependent pairs with BEq keys.

I have avoided Std.Data.Internal.List because of its nature as an implementation detail for hash maps, though it does have some nice API that feels awkward to duplicate elsewhere. Currently we are using Mathlib.Data.List.Sigma, as it also has some helpful definitions about non-duplicated keys. Does this sound like the right approach? If so, I can upsteam some additional lemmas and grind annotations that have been useful.

I also had the thought that it would be nice to have scoped GetElem and GetElem? instances for docs#List.dlookup, but I guess this is problematic when dealing with keys that are natural numbers.

[Julia Scheaffer]

there is also docs#Lean.AssocList but that seems to be very similar to List.lookup's functionality.

[Kim Morrison]

I would encourage improving the API of Mathlib.Data.List.Sigma for now, and then if someone (e.g. the FRO in Std, or a separate library) wants to build out a non-Mathlib associative list API we can at very least use that API there as reference.

It doesn't seem unreasonable to me to ask that Std.Data.Internal.List eventually becomes public, but it won't happen right away.

[Kim Morrison]

@Chris Henson, I wonder also if you might be interested in simply using ExtTreeMap rather than an association list.

[Chris Henson]

Okay, I will continue with Mathlib.Data.List.Sigma (and consider ExtTreeMap). After cleaning things up a bit, I got a lot of mileage out of adding grind to existing API there plus just a few additional lemmas. WIP here for anyone curious.

[Kim Morrison]

Excited to see a Mathlib PR with grind annotations for List.Sigma. :-)

[Chris Henson]

I have opened #30313 with some initial grind annotations and a few small lemmas.