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:
theories/ordinals/OrdinalNotations/ON_Generic.v
the ON
class assumes the comparison is decidable and the underlying strict order is well-founded.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 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.
@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: Mar 28 2024 at 15:01 UTC