Adding a CEP about Reals

[Villetaneuse]

Rendered: https://github.com/Villetaneuse/ceps/blob/clean_up_Reals/text/000-clean-up-Reals.md

[gares]

This other library https://github.com/math-comp/analysis is quite active, IMO this CEP should mention it and compare with it.

[Villetaneuse]

I added a paragraph about math-comp/analysis and another (small) one about C-Corn.

[herbelin]

The motivation is clear and I believe shared by a large part of the community, as witnessed by the existence of the LiberAbaci project: to provide a better Reals library useful for teaching mathematics to first year undergraduate students, alongside CoRN and mathcomp-analysis. The goals respectively pursued by these different libraries are all worth and, as a particular case, I'm strongly enthusiastic towards the directions mentioned in this Coq enhancement proposal.

Regarding function extensionality, I don't remember if it derives back from the classical axiomatization (Vincent Semaria might know). If it is convenient to use, I would not refrain from using it.

[herbelin]

Side remark: an indirectly-related issue is coq/coq#17877, which recommends a less linear graph of dependencies in Reals.

[Villetaneuse]

Yes, I had it in mind when writing the drawbacks. However I think documentation and user comfort > building time. I also think I could kill a lot of dependencies between files (but then some exports could also break external libraries).

[Villetaneuse]

Regarding function extensionality, I don't remember if it derives back from the classical axiomatization (Vincent Semaria might know). If it is convenient to use, I would not refrain from using it.

Yes, this is used for equality between Dedekind cuts here: https://github.com/coq/coq/blob/master/theories/Reals/ClassicalDedekindReals.v#L485

[herbelin]

Coquelicot and Flocq are already mentioned. Another library to be mentioned at the same time as CoRN is probably math-classes. Its primary goal is however orthogonal: it is to build a hierarchy of algebraic structures on top of type classes (like CoRN originally did using coercions, or mathcomp using coercions, canonical structures and specific packaging techniques). [Note: I'm however not expert on real numbers analysis as the authors of the different libraries would.]

[silene]

Regarding function extensionality, I don't remember if it derives back from the classical axiomatization

It was not there in the original axiomatization. This dependency was only added when computable real numbers were added, so as to able to redefine the classical real numbers as a quotient over them. That is why this axiom is not used in any other place, as they predates this change. (Originally, a dedicated, weaker, axiom was used, but it was so close from functional extensionality, that we finally chose to use the latter.)

[Villetaneuse]

Sorry I misread Hugo Herbelin's question. Guillaume Melquiond is right, it was added during the construction. To sum things up:

• The original axiomatization used no "logical" axiom, but axioms about real numbers themselves, in particular (strong) decidable equality between real numbers and a (strong) form of least upper bound existence. The Archimed property was also an axiom but it could have been derived (although not easily because Reals, even now, completely ignore the field of rational numbers)
• Later, some very smart people (maybe Guillaume Melquiond?) understood that these axioms entailed the limited principle of omniscience and the weak excluded middle (this is Rlogic.v)
• Finally, Vincent Semeria used the LPO, the WEM and functional extensionality to define the real numbers, so the "reverse maths" circle is complete modulo funext

[herbelin]

In the context of the reverse mathematics of the axiom of choice, there is a principle of weak extensionality:

∃H((∀f H(f) =_ext f)∧ (∀fg(f =_ext g) ⇒ H(f)=H(g)))

that is, there is, in any class of extensional functions, a representative of this class (see Carlström 2003). Could it be that this is this principle which exactly characterizes the classical axiomatization?

[CohenCyril]

The preexisting library coq-alternate-reals provided a structure realType for a real number object in type theory, and we indeed use it, rather than a specific implementation. There is an instanciation which uses Coq reals implementation: the famous Rstruct file).

Indeed the realType structure is used throughout the library, but that does not make the theory logically more general, since all realType objects should be isomorphic (the proof is not provided). The main reason is that we may want to apply theorems to both R and {x : C | x \is a Num.real} or {x : \bar R | x \is a fin_num}, but this happens to be not so essential and we might revert back to using an arbitrary implementation of the reals.

[Villetaneuse]

I must admit I did not have enough time to browse the math-comp/analysis as it deserves. Thank you very much for these corrections.

[Villetaneuse]

I have corrected the statements about math-comp and added a reference to math-classes and coq/coq#17877.

[JasonGross]

(Context: I've come to use the Reals library in Coq mostly for the connection to primitive floats via flocq)

Another question not mentioned in this CEP is that of naming: the standard library structures on Q and R use a different naming scheme than those on Z, N, positive, nat. Namely, we have things like Rmax, Rminus, Rmult, Rplus, but Z.max, Z.sub, Z.mul, Z.add. (Personally I like the naming scheme in Nat, N, Pos, Z better than R and Q.)

[Villetaneuse]

(Context: I've come to use the Reals library in Coq mostly for the connection to primitive floats via flocq)

Another question not mentioned in this CEP is that of naming: the standard library structures on Q and R use a different naming scheme than those on Z, N, positive, nat. Namely, we have things like Rmax, Rminus, Rmult, Rplus, but Z.max, Z.sub, Z.mul, Z.add. (Personally I like the naming scheme in Nat, N, Pos, Z better than R and Q.)

While I absolutely agree with you (and when missing lemmas don't exist in Reals, I've tried to stick with ZArith names for instance), I think this would be incredibly hard to do this without breaking too many things. The best I can do is try to give somewhat consistent names.

Maybe it would be possible to add some module in Numbers, but not sure it wouldn't add too much complexity.

[JasonGross]

While I absolutely agree with you (and when missing lemmas don't exist in Reals, I've tried to stick with ZArith names for instance), I think this would be incredibly hard to do this without breaking too many things

What about the strategy of making new names for everything (maybe with a some sort of sed script?), and making deprecated, only parsing notations for all the constants with the old names? Then even if the aliases stick around for 5 or 10 years, any new changes could be consistently made with new names

[Villetaneuse]

There are certainly parts where there isn't even a beginning of naming scheme. So there, we can start anew. For RIneq, though, I'm really afraid by the sheer scale of it. And people working with Reals are accustomed to the names. Not sure they will be happy when good old Rmult_plus_distr_l starts disappearing from their Search.

But I can very well be mistaken (today I just broke 27 libraries with some deprecated files removal, this certainly clouds my mind). Please @coq/reals-library-maintainers feel free to enter this discussion about names.

[Villetaneuse]

Afterthought: it was mentioned by @herbelin at some point that maybe we could give alternative arguments for lemmas (e.g. to fix inconsistency). Maybe we could also have a system of alternative names: the same lemma with more than one name, and then the Search would give, for instance:

Rmult_comm:
R.mul_comm:
forall x y, x * y = y * x.

but this is way out of my competence level.

[ybertot]

I agree that I would like to have a naming scheme for theorems of real numbers that is closer to the one in Q, Z, or nat, because these have really improved on regularity.

[Villetaneuse]

I feel a bit stuck with this at the moment. @coq/reals-library-maintainers what's your opinion about the naming policy and more generally this CEP and coq/coq#18162
If we change the names, there are, imho, several issues and several paths:

1. create a module (in RIneq?) named R with the expected lemmas (R.mul_add, etc) from ZArith + the ones specific to Reals
   But then a lot of things need to go in this module and this makes a very monolithic part of Reals
   It's not clear to me how many module types (if any) should be used from Numbers and if it is desirable to add more modules. Also some of the basic lemmas are in RAxioms, others are in RIneq
2. Bother less and just keep the "vocabulary" of the rest of the stdlib, i.e. plus -> add, mult -> mul, reg -> cancel, so for instance Rplus_eq_reg_l would become Radd_cancel_l. Note that even this would be quite a big task : this is before Additions in RIneq and removal of Rpow_def coq#18162

$ grep '^Lemma' RIneq.v | grep -E 'mult|plus' | wc -l
153

[MSoegtropIMC]

I personally almost exclusively use my one set of wrapper lemmas for the reals in the standard library. I tend to write larger collection of lemmas for handling certain aspects, say manipulation of inequalities. It is much less work for me to write such libraries than to work with the standard library as is. It is not only the naming, but also the order of variables and premises and selection of implicit arguments which makes it hard for me to use standard library lemmas. I currently have e.g. a bit more than 300 lemmas for manipulating inequalities (high school stuff like multiply from the left or right, remove a factor from the left or right, do this in a hypothesis or premise, add or subtract inequalities, work with double inequalities (ranges), ...)

IMHO we should make a complete redesign - at least at first as wrapper for existing lemmas - and recommend to use these (by excluding the existing lemmas from Search). I would say that many library lemmas are more intended to prove basic facts about real arithmetic and analysis rather than to serve every day applications of such facts. Typically it takes me a lot of massaging of the goal and lengthy argument lists to do what I want with the library lemmas, which makes proofs tedious, maintenance intensive and hard to read. If there is interest we could have a short meeting and I can show examples of what I have. I can likely contribute this, but I have to ask.

[Villetaneuse]

Thank you very much for your answer. So this goes mostly in the direction pointed by Yves and Jason. I propose a lot (really a lot) of added lemmas in coq/coq#18162 to make life easier but I will close it shortly since there seems to be a consensus on even more drastic changes. These quality of life lemmas really make everything better.
You may take a look at this for instance: https://github.com/Villetaneuse/coq/blob/Reals_prototype/theories/Reals_prototype/SeqSeries_prototype.v.

After Yves' and Jason's comment, I extracted the relevant lemmas from Z that could serve as a basis (see the attached file).

Zlemmas_sorted_relevant.txt

I would very much like to have a meeting about this. I will have a lot of time next week after monday. I'm in CEST time zone. Maybe we can discuss the practical aspects of the meeting in zulip?

[Villetaneuse]

Just a quick update: this is not stale, but will take some time. We're discussing this with @MSoegtropIMC. We will start with an inventory of the relevant stdlib parts (Numbers, Arith, Reals themselves, ...)