stdpp

Stream: iris-lean

[Bas Spitters]

What is the plan for porting the relevant parts of stdpp?
I understand it will depend on batteries, but not cslib. Does that seem correct?

[Markus de Medeiros]

There is currently no plan to port stdpp, we will evaluate what we need from stdpp on a case-by-case basis. For example, we did not port the gmap CMRA, we developed a CMRA for generic maps instead.

Iris-Lean does depend on batters but not cslib, yes. I can imagine writing a program logic for cslib languages at some point, but as of now I don't think that justifies another dependency.

[Bas Spitters]

So, you would expect cslib to make some duplication of the lean-iris-stdpp.

[Markus de Medeiros]

I'd like to avoid it if possible. As it stands it looks like there isn't much duplication in "core Iris". If down the road there is more substantial duplications, then we could either try to move it upstream to batteries (our common dependency) or downstream to an iris-lean-cslib.

[Markus de Medeiros]

The latter is the plan for Iris+mathlib stuff.

[Shreyas Srinivas]

Note that batteries is intended to morally serve the same role as stdpp

[Shreyas Srinivas]

So the right place to port something from stdpp is directly to batteries, after checking that the corresponding material doesn't already exist in some Data folder of mathlib. EDIT : or in the Lean/Std namespace of the main lean4 repository.

[Shreyas Srinivas]

Cslib is not playing quite the same role as stdpp. It's largely formalising CS curriculum stuff. It sits downstream of mathlib.

[Zongyuan Liu]

Is there a conclusion on what the correspondence of stdpp gmap is in Lean? I plan to port big_ops for maps, and am still not quite sure what I should use. Should I use the generic map API or a concrete map implementation?

[Markus de Medeiros]

Unless you really need something specific about gmaps, you should try to generalize the constructions to use the generic API.

[Michael Sammler]

I've been wondering about this question as well. My understanding is that ExtTreeMap is the closest analogue to gmap.
Is this the generic map API that you are referring to? At the moment this interface looks very minimal. Is it intended to be the equivalent of the FinMap interface of std++? (Note that there is discussion to get rid of FinMap in std++ since basically everyone uses gmap directly.)

[Markus de Medeiros]

I think it is good to use an interface (like the heap API you linked) rather than a specific type (like ExtTreeMap) wherever possible. In my work I have run into situations where the restrictions on gmap have been too restrictive (a countable type of keys, and having only finitely many elements allocated at once) and as a consequence I've had to redevelop all the theory on top of gmaps to use a different data structure.

The API is indeed relatively close to FinMap.

[Zongyuan Liu]

I actually prefer removing this layer of abstraction and just using the closest thing to gmap. A concrete map with a rich API simplifies and speeds up porting. IMHO, catching up with Iris-Rocq is more important at this project stage.

[Markus de Medeiros]

Do you have an example of somewhere that gmap is easier than using generic API? My experience with the heap_view CMRA is exactly the opposite

[Markus de Medeiros]

In Iris-Rocq they do some strange proofs by induction over the number of allocated keys in a gmap. I suspect that this is to avoid classical logic, so we could technically avoid this with gmaps as well, but I also haven't encountered a case where using a concrete type instead would give any benefit

[Michael Sammler]

I think the main benefit of using an existing definition is that one does not need to duplicate / reprove the API. For example, a quick look at the lemmas of ExtTreeMap suggests that there are around ~700 theorems that one would want to / need to duplicate. (The Std lib seems to indeed duplicate all these lemmas for the 4+ different maps using a process I do not understand.)

[Markus de Medeiros]

I could get behind that! I did not know much about Std.ExtTreeMap but the restrictions on the type seem pretty liberal which is good.

[Markus de Medeiros]

Do these tree maps have an analogue of "allocation" for maps with infinitely many unallocated values? I don't see any such thing.

[Markus de Medeiros]

Ah, I see there are a number of lemmas for finding keys of a certain size Std.ExtTreeMap.maxKey and this Std.ExtTreeMap.filterMap which I think is enough to simulate it.

I'd guess that the Ordering field is always able to be trivially instantiated, so I think the only way this is less general than the one we've implemented is about the universe levels of Ext(D)TreeMap with respect to the keys and values. But somehow I doubt this is a problem. I can give porting the old stuff to the Std maps a try sometime.

[Michael Sammler]

Indeed, I think giving Ext(D)TreeMap a try sounds like the best option to find out how well it works. If someone has experience with the different map types and their advantages and disadvantages, please chime in! I would be interested.

[Markus de Medeiros]

Ah--If I'm understanding the code correctly, Ext(D)TreeMaps can only represent maps that have a finite number of allocated elements. For example, I don't believe that there is a way to represent a heap with keys in the natural numbers that has every odd element allocated. Even if this sounds silly, this kind of thing is done in probability (splitting sources of randomness, for example) and I think it's important that we keep the library of Iris CMRA's as generalized as we reasonably can.

[Markus de Medeiros]

That said, the abstract heap interface only needs to be rich enough for internal clients, for example HeapView (already completed). I've added an issue iris-lean#105 to instantiate this interface with the Lean map types, so that external clients are free to use maps that have a more well-developed API if they want to do so. I also think we could use the Lean map types for IProp without any real loss of generality, and I agree with Zongyuan in this case that using a type closer to gmap could make the port go faster, so we should do it!

[Zongyuan Liu]

For example, I don't believe that there is a way to represent a heap with keys in the natural numbers that has every odd element allocated.

Does this imply a need for a generic interface based big_sepM for your heap points-tos? However, big_op for maps requires a rich API for the lemmas on its various operations.

[Markus de Medeiros]

Is there anything stopping us from having a generic interface? Big ops are just folds over finite data structures, whether you're folding to construct terms in the heap API or a concrete implementation seems immaterial.

I browsed big_ops.v and nothing jumped out to me as being missing, but I think you are more familiar than I am. Do you have examples of where using a specific map type would help?

[Michael Sammler]

Markus de Medeiros said:

Ah--If I'm understanding the code correctly, Ext(D)TreeMaps can only represent maps that have a finite number of allocated elements. For example, I don't believe that there is a way to represent a heap with keys in the natural numbers that has every odd element allocated. Even if this sounds silly, this kind of thing is done in probability (splitting sources of randomness, for example) and I think it's important that we keep the library of Iris CMRA's as generalized as we reasonably can.

How would you do this in Rocq? There also gmap also only represents finite maps. E.g. the ghost_map constructions are specific to gmap and cannot represent infinite maps. For me this has never been a problem, but I also never did any probablistic verification.

[Markus de Medeiros]

Yeah that's my problem exactly--I couldn't, without rewriting parts of the core Iris libraries.

[Markus de Medeiros]

Even though, mathematically, something like ghost map does (did) easily generalize beyond gmap.

[Michael Sammler]

I see, then it probably makes sense to define ghost_map over the generic interface as you already did. But I guess one would only use this interface if one actually needs this generality. For a concrete heap of like heaplang, one can still use ExtTreeMap and then just use the fact that it implements the generic interface. This means that the generic interface does not provide the full API of ExtTreeMap, but only what is necessary for ghost_map (which is hopefully a lot less).

[Ka Wing Li]

Excuse me, I want to use an extensional finite map inside an inductive definition. I am not sure which one to use. It seems I cannot use Std.Ext(D)TreeMap?

[Ka Wing Li]

In Rocq, I would simply use gmap.

[Ka Wing Li]

I tried the following but get error "application type mismatch"

inductive tm : Type where
| nat : ℕ → tm
| var : String → tm
| abs : String → tm → tm
| app : tm → tm → tm

inductive vl : Type where
| nat : ℕ → vl
| abs : Std.ExtTreeMap String vl → tm → vl

[Markus de Medeiros]

Interesting, when I use an association list List (String × vl) (which satisfies the abstract heap interface) it works. It also works for

inductive FiniteDomFunction (V : Type _)
| empty : FiniteDomFunction V
| set : String → V → FiniteDomFunction V → FiniteDomFunction V
| remove : String → FiniteDomFunction V → FiniteDomFunction V

inductive tm : Type where
| nat : ℕ → tm
| var : String → tm
| abs : String → tm → tm
| app : tm → tm → tm

inductive vl : Type where
| nat : ℕ → vl
| abs : FiniteDomFunction vl → tm → vl

which I have proven satisfies the abstract heaps interface in iris-lean#89. Thanks for pointing this out, sticking to the abstract heaps interface for the library seems to be a good idea.

[Markus de Medeiros]

If anyone understand the error in Ka Wing Lei's code I'd be curious to hear an explanation, it seems like something odd with the quotient in ExtTreeMap.

[Michael Sammler]

ExtTreeMap can indeed not be used with nested inductive definitions. The doc string recommends to use TreeMap.Raw instead. See here

These tree maps contain a bundled well-formedness invariant, which means that they cannot be used in nested inductive types. For these use cases, Std.TreeMap.Raw and Std.TreeMap.Raw.WF unbundle the invariant from the tree map.

[Zongyuan Liu]

Hi, I tried to port some of the big op stuff for lists, maps, and sets in my branch https://github.com/lzy0505/iris-lean/tree/big_op_map/set (using Claude’s help). To avoid using concrete map and set implementations, I defined abstract interfaces in Std/FiniteMap.lean and Std/FiniteSet.lean. These interfaces are quite complex. Are they even close to what we want?

[Markus de Medeiros]

Interesting... thanks for trying! Yes I agree that this interface is quite complicated. Since you're just defining a finite set as being in correspondence to a list, do you think the interface could be simplified (ie. define the basic operations in terms of the mapping into lists, so that an instance just has to provide this mapping?)

[Markus de Medeiros]

To put some concrete terms: I feel like we should be able to do a big separating conjunction over at least lists and a mathlib finset.

[Markus de Medeiros]

Just at a glance, the Iris part of this looks great :)

[Shreyas Srinivas]

I would taking Mathlib's approach and just defining

1. Set A as A -> Prop
2. Finite sets as below

structure FiniteSet A where
      set : A -> Prop
      fin : \exists n : Nat,  set \equiv Fin n

[Shreyas Srinivas]

I regularly use Finsets and they are a royal pain

[Shreyas Srinivas]

You might also have to define \equiv but you can see mathlib's version

[Shreyas Srinivas]

See : https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Finite/Defs.html

[Shreyas Srinivas]

and equiv is here : https://leanprover-community.github.io/mathlib4_docs/Mathlib/Logic/Equiv/Defs.html#Equiv

[Markus de Medeiros]

This is not an interface, and it confers no advantages over what Zongyuan has already implemented tbh.

I regularly use Finsets and they are a royal pain

You don't have to use Finsets if you don't want to. But as an example, if I want to define resources associated to network packets by taking a separating conjunction over SimpleGraph.edgeFinset then yes, it would be nice to be able to instantiate big ops with a finset.

[Shreyas Srinivas]

You can use the separating conjunction on the map you get from the Finite typeclass (Fin n -> set)

[Shreyas Srinivas]

you simply mark SimpleGraph.edgeSet with Finite (the typeclass in mathlib or from your interface definition)

[Shreyas Srinivas]

Trust me, you don't want to go down the Finset route for this. It is a road filled with pain.

[Shreyas Srinivas]

also you can always make it an interface with minor changes

[Markus de Medeiros]

To be clear, I think bikeshedding over which definition of finite to take as canonical is kind of pointless since they're all equivalent. Zongyuan: thanks for trying to write this interface--I trust your judgement on what the best implementation would look like. As long as it's not too hard to take some random finite data structure and do a big conjunction over it, I think that's good enough for iris-lean :)

[Zongyuan Liu]

Thanks for the feedback! I will see if I can simplify the interface, and instantiate the interface with some data structures to test it.

[Shreyas Srinivas]

Okay fair, but you should know this is a topic that comes up now and then. These definitions are very different under the hood and it makes a difference when writing API for them and using them.

Also Zongyuan thanks for this work :)

[Michael Sammler]

Thanks for exploring this, Zongyuan! It seems like you ported a lot of lemmas. How complete is the port of the lemmas? Are all bigop lemmas from Rocq Iris there or are some missing?

I also looked at the FiniteMap interface here and I am not sure about the motivation for it instead of using a concrete map (e.g. ExtTreeMap). Previously, Markus made a good point that there are cases where one wants to have non-finite maps, but these maps would not satisfy the FiniteMap interface since they are non-finite (and bigops crucially rely on finiteness).
Which instantiations for the FiniteMap interface do you have in mind?

[Zongyuan Liu]

How complete is the port of the lemmas? Are all bigop lemmas from Rocq Iris there or are some missing?

My goal was to port as many lemmas in Rocq's big_op.v as possible. So far, I have ported most of the lemmas (~90%) on big_[and/or/sep]L, big_sepL2, big_[sep/and]M, and big_sepS. The remaining ones are mostly blocked by missing BI definitions and laws. All results on big_sepM2, big_sepMS are missing at the moment.

I also looked at the FiniteMap interface here and I am not sure about the motivation for it instead of using a concrete map (e.g. ExtTreeMap).

Seemed like Markus wanted to use a generic interface for big ops, so I tried it. I was mostly following stdpp's fin_map.v. If we now all agree that the interface is too complex, I'm happy to switch to ExtTreeMap.

[Michael Sammler]

Zongyuan Liu said:

My goal was to port as many lemmas in Rocq's big_op.v as possible. So far, I have ported most of the lemmas (~90%) on big_[and/or/sep]L, big_sepL2, big_[sep/and]M, and big_sepS.

Very nice!

Zongyuan Liu said:

Seemed like Markus wanted to use a generic interface for big ops, so I tried it. I was mostly following stdpp's fin_map.v. If we now all agree that the interface is too complex, I'm happy to switch to ExtTreeMap.

That makes sense. I am not sure what the best approach is. I guess this heavily depends on whether in practice one will use always a single map type (e.g. ExtTreeMap) or a bunch of different maps (ExtTreeMap, ExtDTreeMap, ExtHashMap, ExtDHashMap). I don't have a good feeling for this.

Your interface currently forces the map to non-dependent. How hard do you think it would be to to support the type of values to depend on the type of keys? (I.e. modeling ExtDTreeMap instead of ExtTreeMap)

[Markus de Medeiros]

Zongyuan Liu said:

Seemed like Markus wanted to use a generic interface for big ops, so I tried it. I was mostly following stdpp's fin_map.v. If we now all agree that the interface is too complex, I'm happy to switch to ExtTreeMap.

Yep, thanks again for trying this but I'm convinced now that's there's no advantage to this for big ops!

[Ka Wing Li]

ExtTreeMapand related kv map may not be the best idea. I wish we can have something like gmap. Unless a dependent KV map is required.

[Ka Wing Li]

Good job for the finmap interface btw.

[Michael Sammler]

Ka Wing Li said:

ExtTreeMapand related kv map may not be the best idea

Can you be more specific why?

[Ka Wing Li]

Ka Wing Li said:

Excuse me, I want to use an extensional finite map inside an inductive definition. I am not sure which one to use. It seems I cannot use Std.Ext(D)TreeMap?

In case one want to use the kv map in some inductive definition.

[Zongyuan Liu]

I simplified the FiniteMap interface dramatically and instantiated it with ExtTreeMap. I didn't just replace it with ExtTreeMap because the behaviours of some operations of ExtTreeMap are not aligned with gmap, so I think FiniteMap as a wrapper is necessary.

See the new FiniteMap in this draft PR

[Zongyuan Liu]

Michael Sammler said:

How hard do you think it would be to to support the type of values to depend on the type of keys?

I think it is possible to do it now

[Alex Bai]

What is the equivalence of base.v in Iris.Std? In particular, I was looking at @Zongyuan Liu https://github.com/leanprover-community/iris-lean/pull/113 and was trying to use some axioms like:

Class SemiSet A C `{ElemOf A C,
    Empty C, Singleton A C, Union C} : Prop := {
  not_elem_of_empty (x : A) : x ∉@{C} ∅; (* We prove
  [elem_of_empty : x ∈@{C} ∅ ↔ False] in [sets.v], which is more convenient for
  rewriting. *)
  elem_of_singleton (x y : A) : x ∈@{C} {[ y ]} ↔ x = y;
  elem_of_union (X Y : C) (x : A) : x ∈ X ∪ Y ↔ x ∈ X ∨ x ∈ Y
}.

[Zongyuan Liu]

I don’t believe it exists, and I don’t think we should port the entire file. I’ve only ported the minimum I need for the draft PR. What do you need from the file?

[Alex Bai]

I wanted to use this version of dom_insert that's in stdpp, which uses elem_of_union that comes from the SemiSet axiomatization

[Zongyuan Liu]

Alex Bai said:

I wanted to use this version of dom_insert that's in stdpp, which uses elem_of_union that comes from the SemiSet axiomatization

The elem_of_union is available at https://github.com/leanprover-community/iris-lean/pull/113/changes#diff-093a641124fa1dc70725f4e2829fdcb337bd27cb1d631f1abba016f8368e6e33R348. If your work is blocked by many missing set lemmas, I can try to create a separate PR for just FiniteSet and FiniteMap. This way they can be reviewed and merged first. Alternatively, if you only require a few set axioms, you can simply try using a set implementation for now.

[Markus de Medeiros]

If you break up the PR into smaller chunks, ideally with some that are ready to review, I could start reviewing stuff tomorrow

[Alex Bai]

Another thing that I want from base.v is leibniz equality:

(** The type class [LeibnizEquiv] collects setoid equalities that coincide
with Leibniz equality. We provide the tactic [fold_leibniz] to transform such
setoid equalities into Leibniz equalities, and [unfold_leibniz] for the
reverse.

Various std++ tactics assume that this class is only instantiated if [≡]
is an equivalence relation. *)
Class LeibnizEquiv A `{Equiv A} :=
  leibniz_equiv (x y : A) : x ≡ y → x = y.
Global Hint Mode LeibnizEquiv ! ! : typeclass_instances.

Lemma leibniz_equiv_iff `{LeibnizEquiv A, !Reflexive (≡@{A})} (x y : A) :
  x ≡ y ↔ x = y.
Proof. split; [apply leibniz_equiv|]. intros ->; reflexivity. Qed.

[Markus de Medeiros]

Might I ask why?

[Markus de Medeiros]

If the equivalence is OFE equivalence, the OFE Leibniz class does this. Another common way to identify equivalent terms is with a quotient, which may also serve your purposes.

[Markus de Medeiros]

Oh wait let me guess. Are you porting auth_auth_dfrac_op_inv_L?

[Alex Bai]

no not that, i was trying to rewrite based on set equivalences
(in particular I was looking into this)

[Markus de Medeiros]

Ah

[Markus de Medeiros]

Generally speaking, it's easiest to port rewrite H. into refine .trans (... H ...) ?_ assuming your ≡ is well behaved enough for that