I'm preparing a small report about Coq & Sets for teaching.

I have spent a few hours browsing the `Coq.Sets`

sub-library. Attached is a summary (in French, sorry) of what I have found.

It would be pretentious to judge this 30 year-old library by today's standards (I honestly think there are quite a few gems in it). However, I don't think many projects (if any) build on it and It's probably not advisable to do so.

What would you think about deprecating this part? (And then, maybe, for historical and/or sentimental purposes keep it in coq community?)

Coq.Sets.pdf

I think general sentiment around predicate sets is that they are great in a logic like HOL and *not great* in an intensional dependent type theory like Coq's. It's not obvious to me it (Ensembles/Sets) should be deprecated without a more general discussion of *what Stdlib is for* (see Roadmap PR which has something on this), but at least, there should be a big warning in the Stdlib documentation

there seem to be some users

https://github.com/search?q=Require+Ensembles+language%3Acoq&type=code

IDK how useful it is to them though

IMVHO the point with `Coq.Sets`

is what interface do users expect; in particular, do they expect membership to be boolean? Do they expect the sets to compute in some way?

Here is my 2 cents about the stdlib as a non-specialist user:

- factorize basic facts and types of general purpose so that there is a common ground for external projects
- serves as an introduction for beginners
- ideally also serves as a model

I am aware of the roadmap PR. This seems to go in the same way.

I was thinking of this part of the Roadmap PR:

Extract the prelude + a minimum set of components that alternative general libraries like MathComp and coq-stdpp need as a basis. Make sure that this reduced core stdlib component can evolve to allow other libraries to use newer features of Coq (like universe polymorphism, SProp and primitive projections).

Clearly, Ensembles/Sets would *not* be a part of this minimum set. So maybe best if it lives on in "Stdlib classic", but people don't need to depend on it at all.

I think it would be be difficult to find a maintainer for Sets/Ensembles outside of Coq, so pulling it out of Stdlib in effect likely means retiring it completely

I was thinking about (we're now interpreting the sacred scriptures):

Identify consistent stdlib components that can be used independently from each other and that would be worth distributing as separate packages.

which looks perfectly adapted to this very autonomous piece of work.

Karl Palmskog said:

I was thinking of this part of the Roadmap PR:

Extract the prelude + a minimum set of components that alternative general libraries like MathComp and coq-stdpp need as a basis. Make sure that this reduced core stdlib component can evolve to allow other libraries to use newer features of Coq (like universe polymorphism, SProp and primitive projections).

It of course need to be agreed in the forthcoming CEP but in my mind "prelude + minimum set" means the current content of `theories/Init`

, point.

Karl Palmskog said:

I think it would be be difficult to find a maintainer for Sets/Ensembles outside of Coq, so pulling it out of Stdlib in effect likely means retiring it completely

Sorry, our posts were almost simultaneous. This library is very basic. It does not use a lot of abstraction. You never know, but I have a hard time thinking of many breakage for this (without completely breaking many bigger and more important projects).

Pierre Roux said:

It of course need to be agreed in the forthcoming CEP but in my mind "prelude + minimum set" means the current content of

`theories/Init`

, point.

This is slowly but surely diverging from the initial topic. (Why not?) I disagree. Things like PeanoNat, ZArith, for instance, should be somewhat "standard". It's important that people talk the same language. I actually want to read (outside of mathcomp world) `Nat.add_comm`

and know what people are talking about.

It of course need to be agreed in the forthcoming CEP but in my mind "prelude + minimum set" means the current content of theories/Init, point.

I think it would have enough for setoid rewrite too

maybe some program.wf too

even with few breakages, maintaining a Coq project separetely from Coq can be demanding, not least due to deprecations and tooling and the like. In this case, I think there are few people who are really relying on Ensembles/Sets for important work, so in the *best* case it will be sporadically maintained if spun off.

the main use case I have seen is for (1) proving strange paradox stuff and (2) proving some abstract non-computable theory correct that needs minimum-fluff sets

probably the main shortcoming is the seeming complete lack for refinement support, I'm pretty sure CoqEAL doesn't do it (provide means to prove an algorithm for Ensembles, get transfer to efficient red-black trees)

I'm also a bit afraid this part of the proposed roadmap serves as a pretext to leave the stdlib in its sorry state.

Karl Palmskog said:

probably the main shortcoming is the seeming complete lack for refinement support, I'm pretty sure CoqEAL doesn't do it (provide means to prove an algorithm for Ensembles, get transfer to efficient red-black trees)

I don't understand what you mean by "refinement support".

for computer scientists, the main use of abstract sets is to prove programs correct. However, if I write and prove correct my program wrt Ensembles, I get no automation for free to transfer this proof to computable sets

this is particularly annoying in Coq, where the "selling point" is to be able to do computation inside Coq itself

I really think this Coq.Sets part has nothing to do with Computer Science. It's mostly an experiment to see if one can reason about sets "close to math" in Coq, IMHO.

Pierre Rousselin said:

I'm also a bit afraid this part of the proposed roadmap serves as a pretext to leave the stdlib in its sorry state.

Well, as stated by the title, the goal is the exact contrary, but of course there is no guarantee of success.

I can say that HOL predicate sets (HOL4/Isabelle/HOL Light equivalent of Ensambles) are used extensively by computer scientists to prove programs correct

IMO it looks like a library about unary predicates, calling them sets doesn't fit very well

for example, a paper by a computer scientist only about predicate set encodings: https://link.springer.com/chapter/10.1007/3-540-44755-5_19

Pierre Roux said:

Well, as stated by the title, the goal is the exact contrary, but of course there is no guarantee of success.

Let's hope so, then.

Karl Palmskog said:

I can say that HOL predicate sets (HOL4/Isabelle/HOL Light equivalent of Ensambles) are used extensively by computer scientists to prove programs correct

Interesting. I will look at it.

From the paper:

Predicate sets are a standard modelling of sets in higher-order logic

This library in HOL4 has been maintained since 1989: https://github.com/HOL-Theorem-Prover/HOL/tree/develop/src/pred_set

don't you get bags (in lieu of sets) in the same way (encoding approach) for HoTT? I remember seeing some paper about this

Well, there is clearly no consensus about deprecation. What about using my little work to document `Coq.Sets`

better then?

Yet another use: a sub-library on Schutte's countable ordinals

https://github.com/coq-community/hydra-battles/tree/master/theories/ordinals/Schutte

I'm ok to deprecate in case I was unclear

I don't think it should be deprecated unless there is a replacement. For example, `MSet`

is not a replacement.

the "move outside of stdlib" idea has precedents elsewhere, FWIW

probably the current best "substitutes" are classical sets in MathComp Analysis and stdpp's propset

"it will die if nobody cares" was a feature there. I'm thinking of some parts of the old Scala 2 stdlib — Scala has also academic origins, and some modules were added in an ad-hoc way

moving Ensembles off the Coq repo is not what I would call deprecation. And anyway, this would require finding a maintainer

to just deprecate and then remove the code without any alternative or planned off-repo maintenance should in my view require a strong justification, e.g., high maintenance cost

but again it seems we are having these discussions because there is no established Stdlib policy on deprecation/removal (at least of whole collections of modules like this)

Is using Ensemble (or sets in general) a bad idea in Coq for computable functions? Since it doesn't seem to be that popular.

Don't they play very well with CIC or something?

To clarify, IMHO:

- Sets in a "mathematical sense" are usually encoded as predicates in CIC. Some things are painful to write. One thing which comes to mind is, "how to consider a subset of a subset?", "how to use finite sets easily?"
- Sets in a more "computer science sense", that is homogeneous finite sets, have multiple implementations (and I'm not expert here), if you need those, you probably don't want to use Ensemble.

The major problem with Ensemble, I think, is that it's not polished enough. The API is strange and old. If you're on the mathcomp side of things, you'll be much better with math-comp/classical/classical_sets.

If you're not and you love typeclasses, consider stdpp/sets.

If you like neither typeclasses nor math-comp, I still think writing your own predicate-based file would be better than using Ensemble.

The zorns-lemma library already is a large extension of Coq.Sets. So if Coq.Sets is moved out of stdlib, it might make sense to move it into zorns-lemma.

Even if a consensus arises, that the stdlib should contain predicate based sets, I agree with @Pierre Rousselin, that the current Coq.Sets could be improved. Which parts in particular would probably need to be worked out.

for the record, Zorn's lemma currently lives here: https://github.com/coq-community/topology/tree/master/theories/ZornsLemma

Since I'm not that involved with other Coq projects, I wouldn't want to take Coq.Sets into zorns-lemma *and* be in charge of redesigning it.

It would be fine IMHO to preserve the current Coq.Sets with an unchanged API in the topology/zorns-lemma repo *and* prepare a replacement / redesign elsewhere.

Last updated: Oct 13 2024 at 01:02 UTC