feat: Add FiniteMap interface#131
feat: Add FiniteMap interface#131lzy0505 wants to merge 3 commits intoleanprover-community:masterfrom
Conversation
src/Iris/Std/FiniteMap.lean
Outdated
| /-- The type `M` represents a finite map from keys of type `K` to values of type `V`. -/ | ||
| class FiniteMap (K : outParam (Type u)) (M : Type u' → Type _) where | ||
| /-- Lookup a key in the map, returning `none` if not present. | ||
| Corresponds to Rocq's `lookup`. -/ |
There was a problem hiding this comment.
Remove all such "corresponds to" comments. This is not something we promise to maintain.
| namespace Iris.Std | ||
|
|
||
| /-- The type `M` represents a finite map from keys of type `K` to values of type `V`. -/ | ||
| class FiniteMap (K : outParam (Type u)) (M : Type u' → Type _) where |
There was a problem hiding this comment.
FiniteMap must be integrated with the Store hierarchy somehow.
There are two ways we could relate FiniteMap and the heaps API:
- We could make FiniteMap extend Store, in which case I believe that all fields except toList and ofList are derivable, or
- We could treat FiniteMap as the "ground truth" and provide heap/store/allocheap/unboundedheap instances based on this construction, as appropriate. In this case, your lemmas which also apply in the infinite case should be generalized.
The former would avoid potentially confusing duplicates (Store.get vs FiniteMap.get?), at the cost of more engineering work. The latter is closer to the current implementation and possibly has more definitional equalities when instantiated with a concrete instance, ie. FiniteMap.empty would be defeq to Std.TreeMap.Raw.empty instead of a derived form like ofList [].
What are your thoughts on this?
There was a problem hiding this comment.
In case 1, the API would look very similar to the RepFunStore and IsoFunStore classes in Heaps, except instead of being represented as a function, it would be represented as a list (maybe quotiented by duplication)
|
|
||
| /-- Two Nodup lists with the same membership are permutations of each other. | ||
| Corresponds to Rocq's `NoDup_Permutation`. -/ | ||
| theorem perm_of_nodup_of_mem_iff {α : Type _} [DecidableEq α] |
There was a problem hiding this comment.
Extremely verbose, there is no reason for so many have statements. Please cleanup AI proofs.
| namespace Iris.Std.List | ||
|
|
||
| /-- For a Nodup list, erasing an element removes it completely. -/ | ||
| theorem not_mem_erase_self_of_nodup {α : Type _} [DecidableEq α] (x : α) (l : List α) |
|
|
||
| /-- Map a function over all values in the map. | ||
| Corresponds to Rocq's `fmap` (notation `f <$> m`). -/ | ||
| def map (f : V → V') : M V → (M V') := |
There was a problem hiding this comment.
Why are map/filtermap/filter derived from the FiniteMap interface but fold is not? Fold could just as easily be implemented as a list fold over the toList list.
| ((toList m).filter (fun kv => φ kv.1 kv.2)) | ||
|
|
||
| /-- Laws for kmap operation. -/ | ||
| class FiniteMapKmapLaws (K : outParam (Type u)) (K' : outParam (Type u)) (M : Type u' → Type _) (M' : Type u' → Type _) |
There was a problem hiding this comment.
I also feel like this must be derivable?
| ((toList m).map (fun (k, v) => (f k, v))) | ||
|
|
||
| /-- Laws for map_seq operation. -/ | ||
| class FiniteMapSeqLaws (M : Type u → Type _) [FiniteMap Nat M] [FiniteMapLaws Nat M] where |
| export FiniteMapKmapLaws (toList_kmap) | ||
| export FiniteMapSeqLaws (toList_map_seq) | ||
|
|
||
| namespace FiniteMapLaws |
There was a problem hiding this comment.
General comment: please golf these AI proofs. They are verbose and have lots of redundant forward reasoning. These doesn't improve readability, and are harder to maintain, so should be removed.
|
|
||
| variable {K : Type u} {V : Type u'} {M : Type u' → Type _} | ||
| variable [DecidableEq K] [FiniteMap K M] [FiniteMapLaws K M] | ||
|
|
There was a problem hiding this comment.
Having all of these lemmas is great! I notice however that many of them also apply to infinite maps. Once we nail down the relationship between infinite heaps and finite maps, we should go through and generalize what we can.
src/Iris/Std/FiniteMap.lean
Outdated
| cases h2 : get? m2 k | ||
| · simp | ||
| cases h' : get? (ofList ((toList m1).filterMap (fun (ki, vi) => | ||
| match get? m2 ki with |
There was a problem hiding this comment.
This is Option.map. I hate it when the AI generates stuff like this.
2 participants
Description
This PR introduces a finite map interface inspired by
stdpp’sfin_map. It also includes various ported stdpp lemmas used in #113.Checklist
PORTING.mdas appropriateauthorssection of any appropriate files