Stream: Coq users

Topic: About Finite Sets in coq-contribs and stdlib


view this post on Zulip Yves Bertot (May 14 2020 at 15:14):

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?

view this post on Zulip Yves Bertot (May 14 2020 at 15:16):

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

view this post on Zulip Gaëtan Gilbert (May 14 2020 at 15:29):

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

view this post on Zulip Yves Bertot (May 14 2020 at 16:54):

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

view this post on Zulip Maxime Dénès (May 14 2020 at 16:55):

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

view this post on Zulip Yves Bertot (May 14 2020 at 17:00):

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

view this post on Zulip Karl Palmskog (May 14 2020 at 17:05):

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

view this post on Zulip Karl Palmskog (May 14 2020 at 17:06):

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

view this post on Zulip Yves Bertot (May 14 2020 at 17:06):

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

view this post on Zulip Karl Palmskog (May 14 2020 at 17:08):

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

view this post on Zulip Karl Palmskog (May 14 2020 at 17:09):

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

view this post on Zulip Yves Bertot (May 14 2020 at 17:10):

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

view this post on Zulip Karl Palmskog (May 14 2020 at 17:11):

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

view this post on Zulip Yves Bertot (May 14 2020 at 17:13):

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?

view this post on Zulip Karl Palmskog (May 14 2020 at 17:14):

@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)

view this post on Zulip Karl Palmskog (May 14 2020 at 17:15):

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

view this post on Zulip Yves Bertot (May 14 2020 at 17:21):

Thanks a lot for the pointers.

view this post on Zulip Karl Palmskog (May 14 2020 at 17:22):

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.

view this post on Zulip Bas Spitters (May 14 2020 at 17:32):

There are a couple of implementations here too:
https://gitlab.mpi-sws.org/iris/stdpp/-/tree/master/theories
Nice topic for stdlib2...

view this post on Zulip Bas Spitters (May 14 2020 at 17:33):

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

view this post on Zulip Karl Palmskog (May 14 2020 at 17:49):

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

view this post on Zulip Karl Palmskog (May 14 2020 at 17:49):

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

view this post on Zulip Karl Palmskog (May 14 2020 at 18:05):

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.

view this post on Zulip Bas Spitters (May 14 2020 at 18:35):

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

view this post on Zulip Karl Palmskog (May 14 2020 at 18:38):

ah, for efficiency there's also https://github.com/thtuerk/MSetsExtra (coq-msets-extra in OPAM) which optimizes a lot for specific cases

view this post on Zulip Karl Palmskog (May 14 2020 at 18:38):

we can at least ping in @Gregory Malecha here

view this post on Zulip Paolo Giarrusso (May 20 2020 at 11:56):

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

view this post on Zulip Paolo Giarrusso (May 20 2020 at 11:57):

(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: Jan 31 2023 at 14:03 UTC