Wochoice

[Tragicus]

(reopening of #1173 )

Adds a proof of Zorn's lemma, Hausdorff maximal principle and the well ordering principle.

Motivation for this change

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[proux01]

FTR, this is a reopening of #1173 following my unwanted merge there.

[affeldt-aist]

I think that we'd like to use wochoice.v in classical_sets.v but the simple fact of Require Importing wochoice in classical_sets.v leads to:

File "./theories/derive.v", line 5, characters 0-79:
Error: Universe inconsistency. Cannot enforce
mathcomp.field.algebraics_fundamentals.48897 <= Coq.ssr.ssrfun.107 because
Coq.ssr.ssrfun.107 < Num.ArchimedeanField.type.u0
<= mathcomp.field.algebraics_fundamentals.48897.

I vaguely remember that we already ran into that kind of problem. What can I do?

[affeldt-aist]

@proux01 @CohenCyril any quick hint? (We are in the process of deriving our Zorn's lemmas from Georges'.)

[proux01]

The first difficulty is to understand where the universe constraint(s) comes from. The best way I know to find out is to use Print Universes Subgraph a b. https://coq.inria.fr/doc/V8.19.0/refman/addendum/universe-polymorphism.html#coq:cmd.Print-Universes with a and b the two problematic universes and perform a dichotomy with requires (then inlining the problematic one or pursuing the dichotomy in the given file, and so on). Once the source of the issue is found, it should be understood if it is intrinsic to the statement or could be removed by modifying the proof / some definition.

[affeldt-aist]

@proux01 Thank you for the pointer! (I didn't know.)

I was able to avoid the universe inconsistency without really understanding it by just removing useless Require Import's, which means that I have just postponed the problem. :-/

As far as the PR is concerned, I just tried to derive existing Zorn's lemmas using @ggonthier 's to avoid duplicates.

There is certainly more to do since some definitions in pred duplicate existing definitions in set (upper_bound vs. ubound, nonempty, etc.).

[affeldt-aist]

There is certainly more to do since some definitions in pred duplicate existing definitions in set (upper_bound vs. ubound, nonempty, etc.).

This topic was discussed during a mathcomp-analysis-dev meeting:

https://github.com/math-comp/analysis/wiki/2024-04-16-Meeting

The conclusion was to integrate this PR, keeping bool/Prop duplicates, favoring Prop in general
and using local patches to connected with bool precicates.

[affeldt-aist]

This PR newly introduces difficult standard lemmas that we have been able to use to revise and shorten classical_sets.v. Sure, it introduces definitions that are likely to move to MathComp and that are bool-variants of existing definitions in Prop but we won't clear that up in the very near future so we'd better merge and come back to it imo.

[affeldt-aist]

@ggonthier ok with merging?

[affeldt-aist]

@Tragicus had a look (including the changelog) so I might merge today to release.