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...

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

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

The `Schutte/Countable`

library 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 `Schutte`

library could be adapted to `CountableTypes`

.

Otherwise, both libraries could be made closer (same constructions and theorem names) for readability and documentation's sake.

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

.

Do you mean that you want `Schutte`

to depend on `CountableTypes`

?

(if it is possible)

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.

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.

Provided we "build a bridge" between the libraries.

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`

.

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.

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!

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.

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

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

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)

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 `opam`

distribution (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`

.

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

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

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.

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.

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

in `dune`

, it can be added like this:

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

Thanks a lot! I'll try this.

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)

@Stéphane Desarzens you need to add it into the `dune`

files, since CI is using Dune

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

Ah, not in the root directory?

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

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.

Won't it work, if the `flags`

are added in https://github.com/Columbus240/topology/blob/v8.17/dune ?

unfortunately, there can't be a top-level `dune`

file like that

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

and each `dune`

is independent of other `dune`

files

so I advise to remove the root `dune`

. In the root, there should only be `dune-project`

Sorry, I misspelled it. I meant `dune-project`

Thank you for the explanations.

`dune-project`

only contains some basic metadata, it can't contain `flags`

, which is specific to `dune`

and `coq.theory`

inside `dune`

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..

Thanks a lot!

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

- In `theories/ordinals/Schutte/Well_Orders.v, the definition (in classical logic + epsilon operator) I followed the most as possible Schutte's book's definitions.
- In
`theories/ordinals/OrdinalNotations/ON_Generic.v`

the`ON`

class assumes the comparison is decidable and the underlying strict order is well-founded.

Perhaps it could be desirable to make the second a sub-class of the first (or, better, a sub-class of`ZornsLemma`

's ?

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

(this was not easy to find out)

ah, the `env`

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

Folders can even add flags if they use :standard

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

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

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

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

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

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

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

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

the description of versions is pretty vague, so 0.4 won't require `theories`

/deps stuff?

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

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

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

We use 0.6 and even 0.7 should be fine I think

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)

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

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

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.

you could locally redeclare arguments as non-implicit

In a way, writing a file `EnsemblesExplicit`

for `ZornsLemma`

which contains `clear implicits`

for all relevant notions, then importing this in hydra-battles?

I think that should work, yes

I'm done with the patch already which uses`EnsemblesImplicit`

, 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.

@Stéphane Desarzens

I'm fine with using `ZornsLemma`

’s conventions about Implicits in `hydra-battles`

, if it’s OK.

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

)

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

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

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

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

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

CI :exploding_head: ...

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

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

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.

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!

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!).

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: ).

Yes, it will prevent the doc updates.

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.

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:

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

@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 `updateDoc`

branch (PR `#161`

). Please feel free to correct any error or add missing information.

Thanks again for this improvement.

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

.

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?

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

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