Putting this in “Miscellaneous” for now because while it feels a bit like a proposal, it is really not important enough to make one formally; I’m just curious about the design consderations of the standard library.
constructive_indefinite_description, as postulated in
Coq.Logic.IndefiniteDescription, has the following type:
Definition indefinite_description :=
forall (A : Type) (P : A->Prop), ex P -> sig P.
This is straightforward enough, but I cannot help but compare it to another possible axiom which is even simpler in concept:
Definition simple_description :=
forall (A : Type), inhabited A -> A.
These two are provably equivalent:
Proposition simple_description_implies_indefinite_description :
simple_description -> indefinite_description.
intro d. repeat intro.
apply d; firstorder.
Proposition indefinite_description_implies_simple_description :
indefinite_description -> simple_description.
intro d. repeat intro.
apply proj1_sig with (P := λ _, True), d; firstorder.
Why is the former proposition, rather than the latter, the one given as an axiom in the standard library? It doesn’t really matter (that’s the whole point of being equivalent) but I find the latter just more aesthetic somehow in its directness, and it seems to be somewhat clearer (and more honest perhaps?) with regard to what the axiom ‘does’.
Indeed, your version is conceptually purer. That would be worth to rephrase the file
IndefiniteDescription.v from the
inhabited A -> A variant. If you feel so, you could propose a pull request.
For consistency’s sake, could we also rephrase
Logic.ClassicalEpsilon.v the same way ?
ClassicalEpsilon.v would indeed be a simple thing to do.
iota are defined in both files
ClassicalEpsilon.v. Would it be useful to share as much as possible the axioms and definitions of both files ?
If so, I may have a look at the beginng of September.
Would it be useful to share as much as possible the axioms and definitions of both files ?
ClassicalEpsilon.v can include
IndefiniteDescription.v but the
Epsilon.v makes otherwise assumptions a priori weaker than the assumptions in
ClassicalEpsilon.v (something like a form of independence of premisses vs full classical logic), so I don’t know how much could be shared. Both have different motivations.
huh confused about definite description here
I guess you would want
Definition unique A := forall (x y: A), x = y.
Axiom definite: forall A, inhabited A -> unique A -> A.
So I was going to say this doesn’t work well for extending to definite description but it might have a nice univalent interpretation.
unique is hProp.