Finite Maps

[markusdemedeiros]

Description

More code derived from #131. This version generalizes many of the constructions to work with PartialMaps (where appropriate), eliminates several typeclasses as they can be derived as theorems. A TreeMap instance is provided.

The kmap and mapSeq ports are not yet complete but I would like to get feedback on this. There are also two theorems with universe issues we should solve at some point.

Fixes # (issue number)

Checklist

• My code follows the mathlib naming and code style conventions
• I have updated PORTING.md as appropriate
• I have added my name to the authors section of any appropriate files

Generative AI Guidelines

AI assistance is permitted when making contributions to Iris-Lean, however, generative AI systems tend to produce code which takes a long time to review.
Please carefully review your code to ensure it meets the following standards.

• Your PR should avoid duplicating constructions found in Iris-Lean or in the Lean standard library.
• have statements that do not aid readability or code reuse should be inlined.
• Your proofs should be shortened such that their overall structure is explicable to a human reader. As a goal, aim to express one idea per line.
• In general, proofs should not perform substantially more case splitting than their Rocq counterparts.

In our experience, a good place to begin refactoring is by re-arranging and combining independent tactic invocations.
We also find that pointing generative AI systems to the Mathlib code style guidelines can help them perform some of this refactoring work.

[markusdemedeiros]

@lzy0505 Your thoughts on this are appreciated!

[lzy0505]

I see you’re taking the minimal approach. However, I’m concerned that we’ll need to prove lots of lemmas for all the operations we define ourselves to make the interface usable, if the users are expected to interact with it most of the time. It seems to be a redundant work, given that the interface instances might already have their own implementations and associated lemmas that we can just use. Furthermore, this approach adds an extra learning burden. I imagine users are already familiar with some commonly used implementations.

This is why I suggested before that we should consider some commonly used implementations when designing the interface. For example, we could fix an implementation like TreeMap and try to reuse its existing theories as much as possible, only redefining operations when necessary.

Stepping back, what will this interface be used for? Do we truly need generality? For example, I can’t think of any scenarios where users need a custom map for big operations. Why can't we go more extreme, just using a concrete implementation?

[markusdemedeiros]

Thanks for the feedback!

Stepping back, what will this interface be used for? Do we truly need generality? For example, I can’t think of any scenarios where users need a custom map for big operations. Why can't we go more extreme, just using a concrete implementation?

Ya I grepped around Iris and I don't see anywhere in Iris that uses truly finite maps outside of defining the big ops, and the gset CMRA. Now unless I missed something, all of the lemmas from your big ops PR (except those regarding kmap and mapSeq atm) should be present here in some form, so since your big ops PR already builds off of this interface I'd imagine the theory is rich enough as is? In my experience I mostly interact with the BigOps API instead of the underlying map, so any definition for map/filter/etc will be interchangeable, but perhaps your experience differs here.

Big ops do fix a concrete type (list) and I do think that's the right way to go, there's no reason to define a separate BigOp for every FiniteMap when a FiniteMap defines a list. It seems really common for mathlib and stdlib types to implement a toList function, and that's exactly what my interface requires to turn a partial map into a finite map, so I like how the two work together. Like I said at some point before I just want to make sure it's easy to take your favorite finite type and do a big conjunction over it, and I think this structure accomplishes that.

However, I’m concerned that we’ll need to prove lots of lemmas for all the operations we define ourselves to make the interface usable, if the users are expected to interact with it most of the time. It seems to be a redundant work, given that the interface instances might already have their own implementations and associated lemmas that we can just use.

Point taken, but by my reading the lemmas about big ops are relatively simple and I think this interface is rich enough to cover them. Do you have a different view? Like, do you find yourself relying on properties that only hold on gmap often or do you (like me) just use the basic BigOp lemmas?

This is why I suggested before that we should consider some commonly used implementations when designing the interface. For example, we could fix an implementation like TreeMap and try to reuse its existing theories as much as possible, only redefining operations when necessary.

The problem with this is that if you don't redefine the operations, either need to fix a single type, or you need to specify all of the equations, and I think we agree that that is something we should avoid.

I don't like the idea of saying that TreeMaps are the only finite map. Now, if there is a need for some big-op-over-TreeMap specific lemmas I think that could be a fine idea, just like gmap does for Iris-Rocq. From my perspective, I want to like, take the separating conjunction over a finitely-supported probability distribution and not worry about if that type has a good analogue of zip. This design lets you do that.

Sorry for the essay. What are your thoughts? Do you have any more concrete issues or suggestions?

[lzy0505]

In my experience I mostly interact with the BigOps API instead of the underlying map, so any definition for map/filter/etc will be interchangeable, but perhaps your experience differs here.

While people may approach this differently, I generally avoid using BigOps with very complex operations, but instead constrain the map’s shape through the operations.
More concretely, I often write things like

WF(m) * [*map] k -> x \in m, P k x

where I need a rich FiniteMap API to define and reason about the WF predicate, and only use the basic BigOps API once I obtain facts on the map from the WF predicate.

Big ops do fix a concrete type (list) and I do think that's the right way to go, there's no reason to define a separate BigOp for every FiniteMap when a FiniteMap defines a list. It seems really common for mathlib and stdlib types to implement a toList function, and that's exactly what my interface requires to turn a partial map into a finite map, so I like how the two work together.

I also like this design, my point was whether we should add more operations as primitive to the interface.

Like I said at some point before I just want to make sure it's easy to take your favorite finite type and do a big conjunction over it, and I think this structure accomplishes that.

By carefully considering the design and keeping commonly used implementations in mind, I hope we can still make it relatively easy to instantiate the interface even with more primitive operations and equations.

Point taken, but by my reading the lemmas about big ops are relatively simple and I think this interface is rich enough to cover them. Do you have a different view? Like, do you find yourself relying on properties that only hold on gmap often or do you (like me) just use the basic BigOp lemmas?

My concern wasn’t about BigOps but rather for use cases beyond it, like the example at the top. For instance, in my project, I sometimes needed to use many map lemmas to derive complex results on my WF-like predicates. I’m worried the current API isn’t sufficient for that.

The problem with this is that if you don't redefine the operations, either need to fix a single type, or you need to specify all of the equations, and I think we agree that that is something we should avoid.

I’m not sure which is worse, specifying the equations v.s. (re)proving them. Is there a way to achieve a nice balance between the two? I tried to do something in this direction in my original PR though I didn’t do it well.

I don't like the idea of saying that TreeMaps are the only finite map. Now, if there is a need for some big-op-over-TreeMap specific lemmas I think that could be a fine idea, just like gmap does for Iris-Rocq. From my perspective, I want to like, take the separating conjunction over a finitely-supported probability distribution and not worry about if that type has a good analogue of zip. This design lets you do that.

Another design that would also work is to have a collection of typeclasses, each containing some operations. For example, we could have a base typeclass without zip and then instantiate it with your probability distribution. (Again I was trying something similar in my original PR.)

Just to reiterate my point, I do think that your compact interface is great and sufficient for BigOps. But having a FiniteMap interface for BigOps means that whenever the users want to use BigOps for a single map, they are forced to stick with the interface for everything that is related to the map. My concern is that your interface is not rich enough for that, and we would have to prove lots of lemmas to support all the possible use cases.

These are just my thoughts, and I hope they don’t get in the way. If you’re not convinced, I’m perfectly happy to keep the current design for now and revisit it in the future if necessary.

[markusdemedeiros]

Ty for the example and feedback! We're on the same page about most of what you bring up.

I’m not sure which is worse, specifying the equations v.s. (re)proving them.

Agreed. The main problems I found with trying to specify the typeclasses were that A) the maps might not be extensional, B) toList equations only hold up to permutation and C) the lemmas require uniqueness of the list elements. I guess you know this, but that makes writing down all the equations you want kind of messy.

where I need a rich FiniteMap API to define and reason about the WF predicate, and only use the basic BigOps API once I obtain facts on the map from the WF predicate.

Right, but the FiniteMaps API does not need to be involved with the manipulations your do about the map inside the WF predicate provided you've fixed a concrete instance like TreeMap. Something interesting about your example is that while the TreeMap-defined maps aren't equal to FiniteMap-defined maps, any lawful definition will be OFE equivalent, so you could actually prove a lifting lemma like the following to do the manipulations of your big op based on the facts you get from wp.

[*map] k -> x \in (m₁.zip m₂), P k x ⊣⊢ [*map] k -> x \in (FiniteMap.zip m₁ m₂), P k x

In fact you could even use a typeclass to define these liftings in general without making FiniteMap any more complex:

class Zip (M : Type _ → Type _) (K : Type _) [FiniteMap M K] where
  zip : M T₁ → M T₂ → M (T₁ × T₂)
  zip_iff {k v m₁ m₂} : (zip m₁ m₂) k = some v ↔ (FiniteMap.zip m₁ m₂) k = some v

Anyways, I'm getting the feeling now that we're converging on one of a few good options. We could try this lifting idea, we could try moving a couple more operations into the FiniteMaps API like you describe, or maybe we could even go back to your typeclasses and just use the FiniteMaps definitions as a scoped instance so I can define my weird ones for free.

How about this for a plan: I'll merge this and we can move onward to the big ops. In your work you can feel free to just use a concrete datatype so we can get more information about how big ops are used, and then I'll worry about generalizing it however is appropriate after. For the time being it'll be a bit of a FinMap/gmap situation, but as the Rocq version shows that's clearly not the end of the world :)

[lzy0505]

I also think we are converging. The plan sounds good. Thanks for the discussion!