I'm trying to figure out how to use the finset library from mathcomp.

From my understanding, running `Eval compute in (true \in [set true]).`

should yield `true`

, but it does not. Can anyone help me with the correct syntax?

Daniel I'm much afraid that finset won't work liek this

The definition of `[set ...]`

is "locked" , which means the library is not directly computational

you'll have to use some other libraries if you need to compute

Arthur Azevedo de Amorin used to have a nice one I htink

Thanks for the information. Would Cyril's finmap work for this?

IIRC it may not either, let me see

Well, actually it may have a better chance , cc @Cyril Cohen

Yup, the definition is locked, but using `inE`

allows you to compute a bit better as the underlying membership function is the one of the list.

Hi, in finmap and finset, `\in`

are locked. In both cases, the rationale is that mathcomp is computationally locked to spare the kernel and unification from unwanted unfoldings. The CoqEAL project goal was to trigger computations, unfortunately no-one added a refinement for finite sets yet.

Well, I think I don't actually need computation. It just happened to be the first thing I tried to see if I was understanding the library. I think finset or finmap will suffice for my current needs.

Thank you very much for your help.

Maybe soon I'll ping Cyril to help me try to add the refinement to CoqEAL, if I find some time to contribute.

I would be very interested in such refinements, in fact I have some draft lying out somewhere that we could use as an starting point.

Cool. I'll try to contact you soon so that we can work on that together

+1 for CoqEAL refinement of finsets (and e.g., MSets), would also be nice with one for finmap/FMap

Great!

@Karl Palmskog you don't have any of that already?

Are you using extraction to OCaml maps?

Indeed I had a quick look and I have two things:

- extraction to OCaml maps

- a sketch of refinement to Coq MSets etc...

It would be cool to axiomatize OCaml maps and add that too

in my developments that need extraction, I always use FMap and MSet, since they were designed to extract well

in fact recent work should allow us to actually model OCaml's map inside Coq

for abstract-only work I use finmap

One problem we will have is with the functorial interface, that's a bit painful to work

maybe we should get in touch with Arthur Azevedo and target his efficient map lib [ssr style] instead

yes, the functorial interface is an annoyance and why I use finmap whenever I can

I don't recall where the modernization of Coq's map

is

https://github.com/letouzey/coq-mmaps/

https://github.com/arthuraa/extructures

we need to get Arthur on gitter

very typical Coq situation: 5-6 competing and non-interoperable extensive libraries, each with different dependencies, Coq compatibility, results, etc.

finmap from stdpp works well too ...

compare to HOL4: finite maps were defined in early 90s, then modernized slightly around 2002, and left largely unchanged since then. I guess this is the advantage of a non-computational logic... I think Manuel Eberl said something to the effect of that he never cares what an Isabelle `num`

looks like, while Coq has a zoo of number representations

Actually most of the split here seems to the choice of type-classes / modules / canonicals etc...

This is a great pitfall, that we for example don't have a standard ordered and eqtype interface

stdlib2 should help with that

but indeed, I dunno

I'm still convinced that we don't have the right tooling to be able to consolidate libs effectively

still, I think the majority of the library panelists at the workshop concluded interoperability should not be a primary concern :upside_down:

My response would be: for basic pieces of CS it should be, at least.

I dunno what the meaning about interoperability is, but there was a time that for example `nat`

and `list`

where not shared by libs

it was not fun

it certainly seems to me to be a huge concern

I agree, but "interoperability research" is probably as cold as you can get (also funding wise)

as Pierre-Marie pointed out, standardization/interoperability through "locking people in a room" was pioneered by the Roman curia, making it old as dirt (and of similar status)

For once, Coq is no different than other languages in having lots of data structures. But there's fewer good reasons not to merge modernized maps.

Also, it's cool to have good maps for extraction, but should they be the default map?

Is it feasible to define orders once and write adapters packing them as typeclasses/CSs/modules?

I think the Java Collections framework is an example of how one can have a large selection of containers without (much) redundancy and with a unified design

One problem is that we are trying to make ocaml, haskell and maths interoperate at the same time. Most other projects dont have that problem.

Is the opam/dune sufficiently well developed to allow packaging? It would be possible to make several packages, but still have overlapping maintainers.

At least that was one of the goals when opam was introduced.

indeed I have several projects/repos which host several opam packages. It's possible but a bit limited now since composition doesn't work with `dune -p`

.

As a side note, I've been always envious of Isabelle's Archive of Formal Proofs. Have there been attempts to provide a Coq counterpart thereof? Would that be even feasible?

Tadeusz Litak said:

As a side note, I've been always envious of Isabelle's Archive of Formal Proofs. Have there been attempts to provide a Coq counterpart thereof? Would that be even feasible?

Our closest equivalent to AfP is the `released`

Coq OPAM archive. There's also Coq's CI with 2,2+ million LOC. Also, I'm personally not envious of the fact that almost any Isabelle code outside of AfP is effectively dead... As described by Kohlhase and Rabe here, once an ecosystem without central control reaches a certain size, distributed maintenance becomes the only option.

Coq has an official compatibility policy (effort is spent on not unnecessarily breaking old projects in new versions), to my knowledge there is nothing similar for Isabelle. This trades off speed of development for death-of-non-AfP-projects.

@Arthur Azevedo de Amorim you are here!

We were discussing about how to have better computable maps, maybe doing a refinement

What's the status of your libs

Maybe a possibility would be to have a `coq-computable-containers`

that would glue together coqEAL, mathcomp- etc...

and provide a complete package for those with the kind of needs we discussed here

@Cyril Cohen @Maxime Dénès what is the status of CoqEAL with respect to parametricity? Should it be rebased on top of the meta-coq parametricity plugin?

(Arriving late here...)

In Extructures I decided to lock many of the definitions to avoid the computational blowup @Cyril Cohen was talking about. But I did leave some of the definitions unlocked when they allow for good reduction behavior. For instance, `x \in fset1 y`

reduces to `x \in [:: y]`

because we do not have to sort a one-element list to build a set.

My library is stable, but as far as I know I am the main active user, so it could use more development. I haven't tried extracting anything from it in a while, though I might need this again soon.

One issue with Extructures is that many operations (e.g. lookup) have linear complexity, whereas an optimized implementation would be logarithmic. I don't know if there is a better extensional representation if we want to stay within the base logic.

@Karl Palmskog @Emilio Jesús Gallego Arias next to extraction, did you also consider computation within coq (say native_compute or certicoq). It's slightly different from extraction...

I tried to get my small propositional proof checker from Huth and Ryan's book to do computation in Coq, but in the end I ran out of cycles due to functorial interface of FMap... the idea was that one would demonstrate both extraction and computation for the same code.

@Arthur Azevedo de Amorim I started developing finmap in 2013 and published it on github for the first time in 2015, I had not realized until now you had been developing a **very** similar library in parallel. I think in that case the "we should not try too much having interoperability" from the panel discussion does not apply here, since the design principles are identical. My two goals were to define the category of cubes (for cubical type theory) and nominal types (https://github.com/lewer/nominal-coq) (which were both abandoned on the way). I realized I missed your paper and work on nominal types, which is IMO very impressive by the way. Now, I really wish we could merge our work. WDYT?

This topic was moved here from #Coq users > How to use finset by Cyril Cohen

Yup, @Arthur Azevedo de Amorim has done incredible work however I think it was not publicized enough in the wider community

I think we should also give credit for that he actually put releases on exstructures in the Coq opam archive (albeit the name does not easily signal finite maps). Many :thumbs_up: if it can be unified with finmap.

@Cyril Cohen Yes, a merge could be useful! I actually started developing extructures in 2014. If I had known about finmap back then I would probably not have started it. The one thing to figure out is how much support for execution and small-scale reflection the library should provide...

@Arthur Azevedo de Amorim the "parti pris" I took when I started the library was that the library would be 100% proof oriented i.e. no computation beyond the trivial part, (as you mentionned for `\in [fset x]`

except in my case since I do not rely on ordering, it's less clear to me that it possible), and any computation whatsoever should come from refinements to `FMap`

(or whatever computes).

the rationale is: if complicated stuff are not going to compute (because we want to prevent reduction in unification and conversion), then let's not bother to compute simple things too, for which lists would be enough.

@Arthur Azevedo de Amorim if “extensional representation” means that coq equality = extensional equality, stdpp achieves that with sublinear complexity for maps and sets using a form of tries (https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/gmap.v)

(i guess finmap too, but don’t know)

However, an inductive T cannot contain a gset / gmap of T nowadays; for some reason, the validity proofs make that non-strictly positive. So AFAIK in that case you’re stuck with (association) lists.

Last updated: Jul 15 2024 at 20:02 UTC