Hello, I just spent a few hours porting the fsets library to coq-8.11. While doing so, I also tried to suppress warnings. In particular there are a log of warnings at the time a module is imported where the system complains that one is trying to mask existing names. I don't know how to fix this problem. Does somebody have a quick hint on how to do this?

The code is visible at https://github.com/ybertot/fsets/tree/port-to-8.11

How's this different from the fsets in the stdlib?

I should have seen them, I can't remember how I missed them. Thanks.

Why do we keep a copy in coq-contribs, if they are included in the standard library?

At first glance, it seems there is more in the coq-contrib, like red-black trees. I will have to look deeper.

I always use MSet instead of FSet from stdlib. Red-black trees are available for MSet in particular.

however, FMap, which shares code with FSet, was never modernized like MSet was, and so FMap lacks red-black trees

@Karl Palmskog Do you have an example of using MSet that you can point me to?

@Yves Bertot this one is our most recent: https://github.com/palmskog/chip/blob/master/core/dfs_set.v#L113

the use case is described in our TACAS paper, p. 11: http://users.ece.utexas.edu/~gligoric/papers/PalmskogETAL20Chip.pdf

Great, this turns into an interesting discussion about finite sets and maps. I will rename the topic.

I have come to the conclusion that MathComp's sets and finite maps (via Cyril's finmap) are nearly always to be preferred for reasoning, but then I want to refine to executable code, and the functor-based ones from Filliatre and Appel (who did the red-black tree stuff) win out easily for OCaml execution

When you mention FMap, it seems this name appears only three comment lines in the Coq sources. Are using something taken from CompCert when you wish to use FMaps?

@Yves Bertot here is a file where I use `FMapInterface.S`

as an example: https://github.com/palmskog/fitch/blob/master/coq/fitch_metatheory.v (checked with Coq 8.11)

see here for the top-level interface with FMaps: https://github.com/palmskog/fitch/blob/master/coq/dyadic_ordered.v#L151

Thanks a lot for the pointers.

interestingly, I believe the particularly efficient finite map from binary Z that we use for implementing distributed key-value stores in Verdi was first implemented (or at least used) in CompCert and then moved to the stdlib (`FMapPositive`

), here is some code using this: https://github.com/uwplse/verdi/blob/master/lib/FMapVeryWeak.v

if I recall correctly it was extensively benchmarked when they developed Verdi against FMapAVL etc.

There are a couple of implementations here too:

https://gitlab.mpi-sws.org/iris/stdpp/-/tree/master/theories

Nice topic for stdlib2...

And of course in math-classes:

https://github.com/coq-community/math-classes/blob/master/theory/finite_sets.v

as can be seen by various traces, Pierre Letouzey was at some point working on a modernization of FMap similar to MSet (e.g., https://lists.gforge.inria.fr/pipermail/coq-commits/2015-March/014564.html). I even recall seeing a separate GitHub repo with code related to "MMap", I think it was in the 8.6/8.7 cycle

ah, here it is, and he still seems to be working on it: https://github.com/letouzey/coq-mmaps/ -- however, no red-black tree based finite map in that repo

I did a comparison where I implemented the same quite complex mutually recursive function that uses finite maps in both Coq and HOL4 (https://github.com/palmskog/fitch). My experience is that using functor-based maps are terrible for reasoning about high-level properties in a nice way. In HOL4, they have super-abstract finite maps that are are near-automatically refined by CakeML to verified assembly. If one could set up a workflow using `mathcomp-finmap`

and then refinement via, say, CoqEAL to FMap/MMap and then to extracted OCaml, that workflow would likely be comparable to the HOL4 one.

There;s a parallel discussion on coqclub about this topic. I wonder whether there is technology to create that link.

ah, for efficiency there's also https://github.com/thtuerk/MSetsExtra (`coq-msets-extra`

in OPAM) which optimizes a lot for specific cases

we can at least ping in @Gregory Malecha here

Nice about stdpp’s implementation is that they use typeclasses — Robbert tried at some point to extract them, with some success, but they’re not optimized for computing with them _in Coq_ at the moment

(I worked a bit on that, but more engineering remains to be done; there are discussions in Iris’s Mattermost and maybe on the bug tracker, I could dig them up if anybody is interested)

Last updated: Jun 16 2024 at 02:41 UTC