math-comp
WIP Clean-up of lower classical layers
- [ ] ~~Obtain axioms from the std library~~ Keep the explicit list of additional axioms, and derive their standard consequences.
- [x] Remove ugly notation for
asbool - [x] Minimize the use of bool, and restrict it to plumbing with mathcomp. In particular, add better support for Prop predicates.
- [ ] Reorganize and complete the corpus of lemmas, in particular rewrite rules.
- [ ] Collect lemmas presently in other libraries, e.g. this ones in hierarchy
- [ ] Clean up the proof of Zorn-related lemmas
- [x] Move the generic choice mixin from
set.vto boolp.
Several items in this list were already addressed or in progress elsewhere, so the present branch will incorporate the relevant material.
@CohenCyril , @strub : Require Import from std lib or 3 axiom prelude? I vote for the first.
@CohenCyril corollary question: if we import axioms from std lib, is it important to keep your proof script for Diaconescu or shall we use the one from ClassicalEpsilon and have only one-liners here?
Require Import from std lib or 3 axiom prelude? I vote for the first.
I vote for the second, because it makes it clear which axioms we use exactly. Historically I opted for importing from stdlib, and I changed just before the Coq Workshop presentation, when I realized the previous instantiation of that I did mclassic did not rely on the axioms I thought I used...
Additional argument: when we switch to stdlib2, our independence from stdlib1 will be in our favor. :smile:
Additional argument: when we switch to stdlib2, our independence from stdlib1 will be in our favor. smile
This is clearly not our hardest dependency on stdlib1... and I bet that one will be one of the easiest to resolve.
But can you elaborate on the problem you encountered?
Side note, this WIP branch also remove mclassic and mextentionality which are mostly scars from our past experiments.
@amahboubi I did not realize immediately that I depended on proof irrelevance rather than diaconescu theorem + the axioms we already had.
Sure, it is an easy dependency to remove indeed, but why restoring it and wait rather than keeping as few dependencies as possible? Especially since it consists in less than 20 loc anyway. We can keep a reference to the stdlib in comments.
BTW, @drouhling is currently chasing the dependency in stdlib R if I am correct.
May be for a communication issue: it is the first time I read that analysis wants to keep as few dependencies as possible on stlib1. I am not yet 100% convinced and I do not believe in references by comments. But this specific issue is rather mundane and I think it does not worth spending much energy on it. My main ultimate goal here is to recover from the massive de-synchronization, in an efficient way. I was not thinking of the dependency on R, although it is really great that Damien is addressing this. E.g. mathcomp is requiring a few libraries from stdlib1.
@amahboubi I did not say that analysis (as a project) wants anything. I think we should wait for the meeting to decide such strategies for this repo. I was merely giving you my motivations for my "vote", I am sorry if that was unclear.
And wrt the dependency of mathcomp in stdlib1, this a distinct issue, which Maxime is already adressing.