Stream: Hydras & Co. universe

Topic: Library for countability?


view this post on Zulip Lessness (Mar 14 2023 at 20:03):

In the theories/ordinals/Schutte/Countable.v file of hydra-battles, there is an ad-hoc formalization of countable Prop-based sets. The question is "is there already such a formalization in the Coq libraries ?"

(from PM by Pierre Castéran)

Is this task important/good right now? If yes, I'm going to take a look at this file and then explore if there's some library that does the same job...

view this post on Zulip Stéphane Desarzens (Jun 25 2023 at 06:56):

At coq-community/topology, i.e., in the coq-zorns-lemma package, we have something similar. https://github.com/coq-community/topology/blob/master/theories/ZornsLemma/CountableTypes.v

view this post on Zulip Stéphane Desarzens (Jun 25 2023 at 06:57):

But we use "actual functions" instead of "subsets of the cartesian product" for most purposes.

view this post on Zulip Pierre Castéran (Jun 25 2023 at 09:06):

The Schutte/Countablelibrary was made as a helper for building the adaptation to Coq of Schütte's axiomatisation of countable ordinals.
I think it would worth studying whether the Schuttelibrary could be adapted to CountableTypes.
Otherwise, both libraries could be made closer (same constructions and theorem names) for readability and documentation's sake.

view this post on Zulip Stéphane Desarzens (Jun 25 2023 at 12:15):

Do you use axioms like LEM or extensionality of Ensembles? They are used heavily in coq-zorns-lemma.

view this post on Zulip Stéphane Desarzens (Jun 25 2023 at 12:16):

Do you mean that you want Schutte to depend on CountableTypes?

view this post on Zulip Stéphane Desarzens (Jun 25 2023 at 12:17):

(if it is possible)

view this post on Zulip Pierre Castéran (Jun 25 2023 at 13:36):

1) Yes I use LEM, extensionality of Ensembles, and (heavily) Logic.Epsilon. I admit also Schütte's axioms :

- there exists a well-ordered  set Ord
-  every subset X of Ord is countable iff X  is strictly bounded by some element of Ord.

The abuse of the epsilon and iota operators helps us to define functions on ordinals.
Some explanations pages 161-184 of this pdf

2) If it's possible, it would be nice to have a "standard" library on countables sets. Otherwise, if there are incompatibilities,
it's always worth to document the comparison.

view this post on Zulip Stéphane Desarzens (Jun 25 2023 at 18:53):

Hmm. In CountableTypes an ensemble U : Ensemble A is countable, if its sigma-type { a : A | In U a } is countable, which means that there is an injection { a : A | In U a} → nat. On the other hand, Schutte/Countable defines U : Ensemble A to be countable, if there is a relation nat → A → Prop which is "surjective onto U".
There would need to be some technical glue (using constructive indefinite description) to bridge between the two definitions.

Because coq-zorns-lemma already contains many elementary constructions and results about Ensemble, I think it would fit to be/become the library which you describe.

view this post on Zulip Stéphane Desarzens (Jun 25 2023 at 18:57):

Provided we "build a bridge" between the libraries.

view this post on Zulip Pierre Castéran (Jun 25 2023 at 19:45):

To be precise, the definition we took is also the existence of an injective relation, and the characterization with surjection is a lemma.
Perhaps we could create a branch of the project for trying to make the Schutte sub-library require CountableTypes.

view this post on Zulip Stéphane Desarzens (Jun 25 2023 at 19:56):

Oh, sorry for the mistake.
Yeah, why not try that out?
I'm away the next few weeks, but by the end of July I'm available to help out.

view this post on Zulip Pierre Castéran (Jun 26 2023 at 05:18):

That’s OK with me! I won’t be able to start until beginning of August either.
@Lessness Are you still interested in this adaptation? You’re welcome!

view this post on Zulip Lessness (Jun 29 2023 at 18:01):

Too much stuff going on (in life etc.). Most probably, I won't be able to participate at least few weeks.

End of July / beginning of August is okay, will write that down somewhere.

view this post on Zulip Stéphane Desarzens (Jul 30 2023 at 14:22):

I started a sketch in PR #156, if anyone wants to have a look at it.

view this post on Zulip Pierre Castéran (Jul 30 2023 at 20:19):

@Stéphane Desarzens Looks nice, thanks!
But opam tells me "The following dependencies couldn't be met:

- coq-zorns-lemma → coq < 8.13~" (I'm on 8.17.1).

view this post on Zulip Karl Palmskog (Jul 30 2023 at 20:31):

Zorn's lemma (and other contents of coq-zorns-lemma) is now part of coq-topology. The latest release of coq-topology has 8.16 as upper bound, but since this is a Coq-community we can ask them to do a new release (or change the upper bound if it works out of the box with 8.17)

view this post on Zulip Pierre Castéran (Aug 05 2023 at 16:27):

I managed to compile a clone of coq-community's topology (with Coq 8.17.1)
It worked when I added a #[export] in front of line 98 of ZornsLemma/InverseIImage.v
Additionally, a few deprecation warnings are triggrered.

@Stéphane Desarzens Could it be possible to fix that on the opamdistribution (allowing all coq versions < 8.18`)?

Btw, there is another duplicate: the notion of well-ordered set is both defined in hydra-battles and ZornsLemma.

view this post on Zulip Karl Palmskog (Aug 05 2023 at 18:39):

I can take care of doing a release of Topology, if this is needed, but would be good to see first if can just relax bounds of the last release

view this post on Zulip Stéphane Desarzens (Aug 08 2023 at 20:38):

I need to deal with other work, before I can spend time on this again. Maybe I have time over the weekend. Sorry to drop out of the conversation so suddenly (& for not recalling how ZornsLemma & Topology are packaged).

view this post on Zulip Stéphane Desarzens (Aug 17 2023 at 13:09):

Back again. I'll be able to _actually_ spend more time on this now. Thanks for your patience.

I'm not sure ZornsLemma can be released with compatibility for both Coq v8.12 and v8.17, because v8.17 requires every Hint Rewrite to have an explicit locality, but the first version which supports locality attributes on Hint Rewrite is v8.14.

view this post on Zulip Stéphane Desarzens (Aug 17 2023 at 13:13):

I plan to prepare a final release for the packages coq-zorns-lemma and coq-topology which supports v8.12 and v8.13, then fix the build for v8.17 and create new releases of coq-zorns-lemma and coq-topology which support v8.14 to v8.17.

view this post on Zulip Karl Palmskog (Aug 17 2023 at 13:16):

you can sidestep the hint locality issues in 8.16/8.17 be adding this, e.g., to _CoqProject:

-arg -w -arg -deprecated-hint-rewrite-without-locality
-arg -w -arg -deprecated-instance-without-locality

I would still recommend adding hint/instance localities though, but this means your "final" 8.12/8.13 release can be compatible with 8.16/8.17

view this post on Zulip Karl Palmskog (Aug 17 2023 at 13:17):

in dune, it can be added like this:

(flags (:standard
    -w -deprecated-hint-rewrite-without-locality
    -w -deprecated-instance-without-locality))

view this post on Zulip Stéphane Desarzens (Aug 17 2023 at 13:22):

Thanks a lot! I'll try this.

view this post on Zulip Stéphane Desarzens (Aug 17 2023 at 13:29):

It doesn't seem to work with 8.17, because there it is an error if one does not provide localities. (CI output: https://github.com/Columbus240/topology/actions/runs/5891540867/job/15978816379)

view this post on Zulip Karl Palmskog (Aug 17 2023 at 13:41):

@Stéphane Desarzens you need to add it into the dune files, since CI is using Dune

view this post on Zulip Karl Palmskog (Aug 17 2023 at 13:43):

for example: https://github.com/Columbus240/topology/blob/v8.17/theories/Topology/dune

(coq.theory
 (name Topology)
 (package coq-topology)
 (synopsis "General topology in Coq")
 (flags (:standard
    -w -deprecated-hint-rewrite-without-locality
    -w -deprecated-instance-without-locality)))

view this post on Zulip Stéphane Desarzens (Aug 17 2023 at 13:43):

Ah, not in the root directory?

view this post on Zulip Karl Palmskog (Aug 17 2023 at 13:43):

also here: https://github.com/Columbus240/topology/blob/v8.17/theories/ZornsLemma/dune

view this post on Zulip Karl Palmskog (Aug 17 2023 at 13:44):

The way it's set up, _CoqProject is for use on developers' local machines, which uses coq_makefile for convenience. Dune is used for CI and in opam packages.

view this post on Zulip Stéphane Desarzens (Aug 17 2023 at 13:45):

Won't it work, if the flags are added in https://github.com/Columbus240/topology/blob/v8.17/dune ?

view this post on Zulip Karl Palmskog (Aug 17 2023 at 13:46):

unfortunately, there can't be a top-level dune file like that

view this post on Zulip Karl Palmskog (Aug 17 2023 at 13:47):

you have two different packages in the repository, they each need their own dune

view this post on Zulip Karl Palmskog (Aug 17 2023 at 13:47):

and each dune is independent of other dune files

view this post on Zulip Karl Palmskog (Aug 17 2023 at 13:48):

so I advise to remove the root dune. In the root, there should only be dune-project

view this post on Zulip Stéphane Desarzens (Aug 17 2023 at 13:49):

Sorry, I misspelled it. I meant dune-project

view this post on Zulip Stéphane Desarzens (Aug 17 2023 at 13:49):

Thank you for the explanations.

view this post on Zulip Karl Palmskog (Aug 17 2023 at 13:50):

dune-project only contains some basic metadata, it can't contain flags, which is specific to dune and coq.theory inside dune

view this post on Zulip Stéphane Desarzens (Aug 17 2023 at 14:43):

It worked fine, with the flags Karl explained. I made a PR to the opam repo and will get back to hydra-battles when this is merged.
@Pierre Castéran , about the well-ordered sets: I'll see how much of the well-ordered sets can be taken from ZornsLemma. In topology#42 I sketched a different approach to the theory of well-orders (different definition, theory uses typeclasses). I think I have to re-read and merge this PR before it is "safe" for hydra-battles to use the theory of well-orders from ZornsLemma. Otherwise hydra-battles might need to adapt to changed definitions etc..

view this post on Zulip Pierre Castéran (Aug 17 2023 at 16:32):

Thanks a lot!
About well-ordered sets: Indeed, there are still two definitions in the hydra-battles project:

view this post on Zulip Paolo Giarrusso (Aug 17 2023 at 18:45):

@Karl Palmskog the root dune can configure default flags! Example:

(env
 (_ ; both release and dev modes
  (coq
   (flags
    (:standard
      ;see https://gitlab.mpi-sws.org/iris/iris/-/blob/master/_CoqProject
      -w -notation-overridden
      ; Similar to notation warnings.
      -w -custom-entry-overridden
      -w -redundant-canonical-projection
      -w -ambiguous-paths
      ; Turn warning on hints into error:
      -w +deprecated-hint-without-locality
      -w +deprecated-instance-without-locality
      -w +deprecated-tacopt-without-locality
      -w +future-coercion-class-field
      -w +unknown-option
 )))))

view this post on Zulip Paolo Giarrusso (Aug 17 2023 at 18:46):

(this was not easy to find out)

view this post on Zulip Karl Palmskog (Aug 17 2023 at 18:47):

ah, the env thing. OK, but is it really a good idea?

view this post on Zulip Paolo Giarrusso (Aug 17 2023 at 18:47):

Folders can even add flags if they use :standard

view this post on Zulip Paolo Giarrusso (Aug 17 2023 at 18:48):

We use it, and it seems well-behaved now — these days it's scoped per-project and does not cross to composed sub-projects

view this post on Zulip Karl Palmskog (Aug 17 2023 at 18:49):

and not tied to the Dune-Coq version, like 0.8?

view this post on Zulip Paolo Giarrusso (Aug 17 2023 at 18:51):

the proper scoping I'm talking about needed composition support — but it should be dune-coq 0.4

view this post on Zulip Paolo Giarrusso (Aug 17 2023 at 18:51):

quite a few of the things I'm saying were not true a while ago (dune-coq 0.3)

view this post on Zulip Karl Palmskog (Aug 17 2023 at 18:51):

OK, we are mostly using Dune-Coq 0.3 in Coq-community unfortunately

view this post on Zulip Karl Palmskog (Aug 17 2023 at 18:53):

things are looking pretty grim for Dune-Coq 1.0 currently due to the transitive deps thing

view this post on Zulip Paolo Giarrusso (Aug 17 2023 at 18:53):

Okay, combining that and composition might be a bad idea. But why? I understand 0.8 is a problem, but 0.4 has been out for months

view this post on Zulip Paolo Giarrusso (Aug 17 2023 at 18:53):

https://dune.readthedocs.io/en/latest/coq.html#coq-language-version

view this post on Zulip Karl Palmskog (Aug 17 2023 at 18:54):

the description of versions is pretty vague, so 0.4 won't require theories/deps stuff?

view this post on Zulip Paolo Giarrusso (Aug 17 2023 at 18:55):

It only requires listing deps in theories if you're composing them locally, but not for user-contrib

view this post on Zulip Paolo Giarrusso (Aug 17 2023 at 18:56):

IIRC, the difference is that you can compose libraries without removing dune-project files in subprojects, and dune-project files have sensible semantics

view this post on Zulip Karl Palmskog (Aug 17 2023 at 18:57):

I guess it might work in Coq-community then (0.4), but I'll have to test

view this post on Zulip Paolo Giarrusso (Aug 17 2023 at 18:58):

We use 0.6 and even 0.7 should be fine I think

view this post on Zulip Paolo Giarrusso (Aug 17 2023 at 19:00):

But I agree you'll need some testing for 0.4 <= coq-dune <= 0.7. Rodolphe Lepigre might remember more pitfalls, but you might want to move this subconvo before tagging him (or subscribe him)

view this post on Zulip Karl Palmskog (Aug 17 2023 at 19:00):

best to open a new topic in #Dune devs & users probably

view this post on Zulip Stéphane Desarzens (Aug 19 2023 at 09:06):

@Pierre Castéran in ZornsLemma the files EnsemblesImplicit and ImageImplicit declare a lot of implicit arguments on operations related to Ensemble. I couldn't figure out how to import files from ZornsLemma without also importing the implicit arguments, even if I only use Require Import inside ZornsLemma.
This causes a lot of minor changes throughout the ordinals directory of hydra-battles. Is that fine for you, or do you prefer the notation with the explicit arguments?

view this post on Zulip Stéphane Desarzens (Aug 19 2023 at 09:07):

IMHO, the stdlib should've declared the arguments as implicit. But introducing that now would be a breaking change. And I'm not sure whether Coq supports a "deprecation" of the old behaviour in this case.

view this post on Zulip Karl Palmskog (Aug 19 2023 at 09:10):

you could locally redeclare arguments as non-implicit

view this post on Zulip Stéphane Desarzens (Aug 19 2023 at 09:22):

In a way, writing a file EnsemblesExplicit for ZornsLemma which contains clear implicits for all relevant notions, then importing this in hydra-battles?

view this post on Zulip Karl Palmskog (Aug 19 2023 at 09:34):

I think that should work, yes

view this post on Zulip Stéphane Desarzens (Aug 19 2023 at 09:40):

I'm done with the patch already which usesEnsemblesImplicit, so we probably won't use it here. But it seems like a good addition to ZornsLemma when some other library wants to use it.

view this post on Zulip Pierre Castéran (Aug 28 2023 at 14:48):

@Stéphane Desarzens
I'm fine with using ZornsLemma’s conventions about Implicits in hydra-battles, if it’s OK.

view this post on Zulip Pierre Castéran (Sep 04 2023 at 05:47):

I succesfully checked PR156 on my computer (with coq.8.17.1 and after opam install coq-zorns-lemma)

view this post on Zulip Pierre Castéran (Sep 05 2023 at 07:46):

@Karl Palmskog @Théo Zimmermann @Stéphane Desarzens

I add and pushed on the branch PR156 an opam reference to zorns-lemma (but I'm not sure if it's OK) in meta.yml.
The CI failed (but may be for some other transient problems ?)

Unfortunately, I won't be able to work from tomorrow to the week-end.

view this post on Zulip Théo Zimmermann (Sep 05 2023 at 07:47):

I'll try to find some time during the week to have a look at this (not today though).

view this post on Zulip Théo Zimmermann (Sep 05 2023 at 07:48):

If you've only added the reference to meta.yml without regenerating the opam files, it won't take effect.

view this post on Zulip Karl Palmskog (Sep 05 2023 at 08:18):

I'll try to take a look early tomorrow if it's something easy I can fix

view this post on Zulip Pierre Castéran (Sep 11 2023 at 12:16):

Today, Docker CI works on PR156, but Nix CI failed (unable to find Zorns Lemma) on PR156.
CI :exploding_head: ...

view this post on Zulip Karl Palmskog (Sep 11 2023 at 12:19):

@Pierre Castéran I took a quick look, and there isn't much I can do on the opam/CI side. It looks like the problem is that the new version(s) of Zorn's Lemma aren't packaged in Nix yet. They might be "packaged" locally via Nix overrides I guess, but unfortunately we are going to need real Nix expertise like from @Théo Zimmermann to resolve.

view this post on Zulip Théo Zimmermann (Sep 11 2023 at 12:21):

Yeah, sorry for having delayed this issue for too long. I'll take a look at it today.

view this post on Zulip Théo Zimmermann (Sep 11 2023 at 15:33):

Actually version 10.2.0 of zorns-lemma is already in Nixpkgs, so this should be easy to add it to Hydras & Co.'s dependencies.

view this post on Zulip Théo Zimmermann (Sep 11 2023 at 15:34):

Hum, no, not so easy because of an issue that I haven't yet solved which prevented me from updating the Nixpkgs version used in Hydras & Co. actually!

view this post on Zulip Théo Zimmermann (Sep 12 2023 at 14:40):

FWIW, I still haven't fully figured out the problem with updating Nixpkgs, but this shouldn't prevent using zorns-lemma's latest version in Hydras & Co. I would submit a PR, but I cannot (I cannot even test it), because GitHub is unavailable to me now (I think this is a problem local to Télécom Paris!).

view this post on Zulip Pierre Castéran (Sep 12 2023 at 18:56):

Thanks! One last question for today.
Is it safe to merge into master now (and solve the Nixpkgs issue later) ? Will it forbid the documenation updating and spreading for some time (not a big deal, It's an assumed draft :grinning: ).

view this post on Zulip Théo Zimmermann (Sep 12 2023 at 19:12):

Yes, it will prevent the doc updates.

view this post on Zulip Théo Zimmermann (Sep 12 2023 at 19:12):

If you merge while the Nix CI is still broken, it would be best to temporarily remove the Nix workflow definition under .github/workflows I guess.

view this post on Zulip Pierre Castéran (Sep 12 2023 at 19:35):

Ok, I am presently working on Ackermann/goedel stuff, which doesn't depend on countable sets formalization.
.github/workflows content still looks quite cryptic to me, thus I would prefer not to merge now :fear:

view this post on Zulip Théo Zimmermann (Sep 12 2023 at 20:43):

@Pierre Castéran Finally, the Nix CI is fixed, so this is good to go!

view this post on Zulip Pierre Castéran (Sep 13 2023 at 12:09):

@Stéphane Desarzens
I started to update the doc in order to refer to the use of ZornsLemma (mainly p 161 and 349 of hydra.pdf).
It's on the updateDocbranch (PR #161). Please feel free to correct any error or add missing information.

Thanks again for this improvement.

view this post on Zulip Stéphane Desarzens (Sep 17 2023 at 09:13):

Thanks, I'll comment in the PR #161.

view this post on Zulip Pierre Castéran (Sep 17 2023 at 12:41):

Thanks for the corrections (merged into master) !
In order to make appear the dependency on ZornLemma in the README , is it enough to edit meta.yml?

view this post on Zulip Stéphane Desarzens (Sep 17 2023 at 13:32):

Yeah, I think so, if you regenerate the README afterwards using the template script.

view this post on Zulip Pierre Castéran (Sep 17 2023 at 14:31):

I pushed a branch updateReadme with updates to meta.yml and README.md.
The versions I gave for ZornsLemma is 10.2.0 or later. Is it correct ?


Last updated: Jun 17 2024 at 22:01 UTC