Daniel Sousa (Jul 07 2020 at 16:52): Daniel Sousa (Jul 07 2020 at 16:52):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?
Emilio Jesús Gallego Arias (Jul 07 2020 at 18:58):Daniel I'm much afraid that finset won't work liek this
Emilio Jesús Gallego Arias (Jul 07 2020 at 18:58):The definition of [set ...] is "locked" , which means the library is not directly computational
Emilio Jesús Gallego Arias (Jul 07 2020 at 18:59):you'll have to use some other libraries if you need to compute
Emilio Jesús Gallego Arias (Jul 07 2020 at 18:59):Arthur Azevedo de Amorin used to have a nice one I htink
Daniel Sousa (Jul 07 2020 at 19:02):Thanks for the information. Would Cyril's finmap work for this?
Emilio Jesús Gallego Arias (Jul 07 2020 at 20:29):IIRC it may not either, let me see
Emilio Jesús Gallego Arias (Jul 07 2020 at 20:30):Well, actually it may have a better chance , cc @Cyril Cohen
Emilio Jesús Gallego Arias (Jul 07 2020 at 20:46):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.
Cyril Cohen (Jul 07 2020 at 20:52):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.
Daniel Sousa (Jul 07 2020 at 21:23):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.
Emilio Jesús Gallego Arias (Jul 07 2020 at 22:18):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.
Daniel Sousa (Jul 08 2020 at 07:47):Cool. I'll try to contact you soon so that we can work on that together
Karl Palmskog (Jul 08 2020 at 08:06):+1 for CoqEAL refinement of finsets (and e.g., MSets), would also be nice with one for finmap/FMap
Emilio Jesús Gallego Arias (Jul 08 2020 at 09:19):Great!
Emilio Jesús Gallego Arias (Jul 08 2020 at 09:19):@Karl Palmskog you don't have any of that already?
Emilio Jesús Gallego Arias (Jul 08 2020 at 09:19):Are you using extraction to OCaml maps?
Emilio Jesús Gallego Arias (Jul 08 2020 at 09:19):Indeed I had a quick look and I have two things:
Emilio Jesús Gallego Arias (Jul 08 2020 at 09:19): Emilio Jesús Gallego Arias (Jul 08 2020 at 09:20): Emilio Jesús Gallego Arias (Jul 08 2020 at 09:20):It would be cool to axiomatize OCaml maps and add that too
Karl Palmskog (Jul 08 2020 at 09:20):in my developments that need extraction, I always use FMap and MSet, since they were designed to extract well
Emilio Jesús Gallego Arias (Jul 08 2020 at 09:20):in fact recent work should allow us to actually model OCaml's map inside Coq
Karl Palmskog (Jul 08 2020 at 09:20):for abstract-only work I use finmap
Emilio Jesús Gallego Arias (Jul 08 2020 at 09:21):One problem we will have is with the functorial interface, that's a bit painful to work
Emilio Jesús Gallego Arias (Jul 08 2020 at 09:21):maybe we should get in touch with Arthur Azevedo and target his efficient map lib [ssr style] instead
Karl Palmskog (Jul 08 2020 at 09:21):yes, the functorial interface is an annoyance and why I use finmap whenever I can
Emilio Jesús Gallego Arias (Jul 08 2020 at 09:21):I don't recall where the modernization of Coq's map
Emilio Jesús Gallego Arias (Jul 08 2020 at 09:22):is
Karl Palmskog (Jul 08 2020 at 09:22):https://github.com/letouzey/coq-mmaps/
Emilio Jesús Gallego Arias (Jul 08 2020 at 09:23):https://github.com/arthuraa/extructures
Emilio Jesús Gallego Arias (Jul 08 2020 at 09:23):we need to get Arthur on gitter
Karl Palmskog (Jul 08 2020 at 09:27):very typical Coq situation: 5-6 competing and non-interoperable extensive libraries, each with different dependencies, Coq compatibility, results, etc.
Bas Spitters (Jul 08 2020 at 09:32):finmap from stdpp works well too ...
Karl Palmskog (Jul 08 2020 at 09:33):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
Emilio Jesús Gallego Arias (Jul 08 2020 at 09:42):Actually most of the split here seems to the choice of type-classes / modules / canonicals etc...
Emilio Jesús Gallego Arias (Jul 08 2020 at 09:43):This is a great pitfall, that we for example don't have a standard ordered and eqtype interface
Emilio Jesús Gallego Arias (Jul 08 2020 at 09:43):stdlib2 should help with that
Emilio Jesús Gallego Arias (Jul 08 2020 at 09:43):but indeed, I dunno
Emilio Jesús Gallego Arias (Jul 08 2020 at 09:44):I'm still convinced that we don't have the right tooling to be able to consolidate libs effectively
Karl Palmskog (Jul 08 2020 at 09:53):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.
Emilio Jesús Gallego Arias (Jul 08 2020 at 09:59):I dunno what the meaning about interoperability is, but there was a time that for example nat and list where not shared by libs
Emilio Jesús Gallego Arias (Jul 08 2020 at 09:59):it was not fun
Emilio Jesús Gallego Arias (Jul 08 2020 at 09:59):it certainly seems to me to be a huge concern
Karl Palmskog (Jul 08 2020 at 10:00):I agree, but "interoperability research" is probably as cold as you can get (also funding wise)
Karl Palmskog (Jul 08 2020 at 10:03):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)
Paolo Giarrusso (Jul 08 2020 at 10:15):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.
Paolo Giarrusso (Jul 08 2020 at 10:16):Also, it's cool to have good maps for extraction, but should they be the default map?
Paolo Giarrusso (Jul 08 2020 at 10:17):Is it feasible to define orders once and write adapters packing them as typeclasses/CSs/modules?
Karl Palmskog (Jul 08 2020 at 10:18):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
Bas Spitters (Jul 08 2020 at 10:31):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.
Karl Palmskog (Jul 08 2020 at 10:42):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.
Tadeusz Litak (Jul 08 2020 at 10:46):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?
Karl Palmskog (Jul 08 2020 at 10:48):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.
Emilio Jesús Gallego Arias (Jul 08 2020 at 11:41):@Arthur Azevedo de Amorim you are here!
Emilio Jesús Gallego Arias (Jul 08 2020 at 11:41):We were discussing about how to have better computable maps, maybe doing a refinement
Emilio Jesús Gallego Arias (Jul 08 2020 at 11:41):What's the status of your libs
Emilio Jesús Gallego Arias (Jul 08 2020 at 11:42):Maybe a possibility would be to have a coq-computable-containers
Emilio Jesús Gallego Arias (Jul 08 2020 at 11:42):that would glue together coqEAL, mathcomp- etc...
Emilio Jesús Gallego Arias (Jul 08 2020 at 11:42):and provide a complete package for those with the kind of needs we discussed here
Bas Spitters (Jul 08 2020 at 11:46):@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?
Arthur Azevedo de Amorim (Jul 08 2020 at 11:48):(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.
Bas Spitters (Jul 08 2020 at 11:53):@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...
Karl Palmskog (Jul 08 2020 at 12:14):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.
Cyril Cohen (Jul 08 2020 at 12:37):@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?
Notification Bot (Jul 08 2020 at 12:55):This topic was moved here from #Coq users > How to use finset by Cyril Cohen
Emilio Jesús Gallego Arias (Jul 08 2020 at 13:27):Yup, @Arthur Azevedo de Amorim has done incredible work however I think it was not publicized enough in the wider community
Karl Palmskog (Jul 08 2020 at 13:28):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.
Arthur Azevedo de Amorim (Jul 08 2020 at 15:21):@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...
Cyril Cohen (Jul 08 2020 at 15:23):@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).
Cyril Cohen (Jul 08 2020 at 15:25):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.
Paolo Giarrusso (Jul 08 2020 at 20:21):@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)
Paolo Giarrusso (Jul 08 2020 at 20:21):(i guess finmap too, but don’t know)
Paolo Giarrusso (Jul 08 2020 at 20:23):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: Apr 20 2024 at 13:01 UTC