Use ZornsLemma for def of Countable sets

[Columbus240]

Initial discussion on Zulip: https://coq.zulipchat.com/#narrow/stream/344515-Hydras-.26-Co.2E-universe/topic/Library.20for.20countability.3F/near/341893039 The file theories/ordinals/Schutte/Countable.v provides some theory about countable Ensemble. The coq-zorns-lemma package contains very similar results already. This commit is a first try to use as many results from coq-zorns-lemma as possible, instead of defining them in here.

This commit still contains some rough edges:

• The lemma countable_singleton can be moved to ZornsLemma.
• In some files we can't use From ZornsLemma Require Import CountableTypes. because it messes up the set of open scopes. I consider this a bug of ZornsLemma and will look into it.
• All edits have been done in Countable.v, but statements like image_as_Im could be moved to ordinals/Schutte/PartialFun.v.
• ~~The following lemmas could be removed from Countable.v, if at the corresponding places we'd use the corresponding lemma of ZornsLemma: countable_union, countable_inclusion, countable_union_qcq~~
• The following lemmas could be incorporated in coq-zorns-lemma, instead of introducing them here: countable_empty, countable_singleton, seq_range_countable.
• ~~The proof of countable_bij_fun and countable_bij uses a very rough translation between fun_bijection and ZornsLemma.FunctionProperties.bijective.~~
• ZornsLemma defines implicit arguments for most operations on Ensembles like Union, Full_set, etc. Somehow this is infectuous and now also appeared in Countable.v. We might want to change this behaviour of ZornsLemma. What is the right change to ZornsLemma? Change all Require Export EnsemblesImplicit to Require Import EnsemblesImplicit? Edit: The approach using Require Import does not work. The Arguments infect all files that transitively Import them.

[Columbus240]

The Nix CI seems to fail, because the opam package coq-zorns-lemma has to be added. I'm not sure how. What to do?

@Casteran, the def. of Countable in ZornsLemma is such, that some proofs of it need proof-irrelevance. The def. used in hydra-battles before this PR doesn't need it. Do you care whether the axiom Classical_Prop.classic or ProofIrrelevance.proof_irrelevance is used in the proofs? By ClassicalFacts, one could derive proof_irrelevance from classic.

In some files we can't use From ZornsLemma Require Import CountableTypes. because it messes up the set of open scopes. I consider this a bug of ZornsLemma and will look into it.

[Casteran]

Hi, The sub-library ordinals/Schutte/ already imports Classical (+ a few more axioms from Logic.Epsilon). If there is a solution using ClassicalFacts (which looks to be axiom-free), It should be OK (for this sub-library) ?

Perhaps it could be different if we build classes for effective « ordinal notations », which may be in the pure-CIC part of Coq ? In which case, perhaps MatcComp’s notion of countability could be useful.

About implicits: I’m fine with using ZornsLemma’s conventions in hydra-battles, if it’s OK.

Thanks again.

Le 19 août 2023 à 13:06, Columbus240 @.***> a écrit :

The Nix CI seems to fail, because the opam package coq-zorns-lemma has to be added. I'm not sure how. What to do?

@Casteran https://github.com/Casteran, the def. of Countable in ZornsLemma is such, that most proofs of it need proof-irrelevance. The def. used in hydra-battles before this PR doesn't need it. Do you care whether the axiom Classical_Prop.classic or ProofIrrelevance.proof_irrelevance is used in the proofs? By ClassicalFacts https://coq.inria.fr/distrib/current/stdlib/Coq.Logic.ClassicalFacts.html#proof_irrelevance_cci, one could derive proof_irrelevance from classic.

In some files we can't use From ZornsLemma Require Import CountableTypes. because it messes up the set of open scopes. I consider this a bug of ZornsLemma and will look into it.

— Reply to this email directly, view it on GitHub https://github.com/coq-community/hydra-battles/pull/156#issuecomment-1684919805, or unsubscribe https://github.com/notifications/unsubscribe-auth/AJW6FCTLZRSUN7JB3OMP2ADXWCM5HANCNFSM6AAAAAA25HHMLA. You are receiving this because you were mentioned.

[Columbus240]

Ok, I'll leave the implicit arguments as is.

I think the remaining problems of this PR are related to the CI and the packaging. @Casteran, could you have a look at that?

[Casteran]

@Columbus240 Indeed there looks to be a packaging problem

  Error:  Package conflict!
    * Missing dependency:
      - coq (< 8.14~ | >= dev)
      not available because the package is pinned to version 8.15.2

@palmskog @Zimmi48 Could you have a look ?

[Columbus240]

Thank you!