Prove the completeness of real numbers from logical axiom sig_not_dec

[VincentSe]

Kind: feature.

Prove the completeness of real numbers from logical axiom sig_not_dec. Now the classical real numbers only have logical axioms and quotient axioms.

Move some lemmas about rational numbers into the QArith part of the stdlib.

Also add an interface for constructive real numbers, as well as its opaque implementation by Cauchy reals. The classical reals are now a quotient of this opaque term.

[herbelin]

I made a rather superficial review but this is interesting and it looks good.

I vaguely wonder whether sig_not_dec and its use over a formula quantified over sequences is reducible to LPO?

Maybe worth to have the move of lemmas over Q in a separate commit if not too complicated to do.

[herbelin]

In a longer term, I would be tempted to move sig_forall_dec_T and sig_not_dec_T in a more generic part of the library (e.g. in Decidable.v) but this would require some effort of consistent naming to do at the same time, so this shall be for a later step.

Another remark in passing about the terminology "decidable" made a long time ago in the standard library: The standard definition of "decidable" from computability theory is the existence of a provably total deciding recursive function. This happens to coincide with {A}+{~A} in the context of constructive mathematics where a model of recursive functions is intended but it starts to be disputable in the presence of axioms invalidating the model of recursive functions. So, I believe that another terminology should eventually be found. However, I don't have a good solution. Maybe using the expression "semantically decidable" (but it is a bit long).

[VincentSe]

The last commit of ConstructiveReals.CRlt shows that the proofs are more complicated in sort Set (we have to juggle between CRltEpsilon and CRltForget for example). Inside the ConstructiveCauchyReals implementation, working in Set gives us access to more information, that does speed up functions such as linear_order_T.

However, proofs in ConstructiveRIneq, more elegant and abstract because they cannot see the implementation behind the opaque term CR, are doomed (for this same reason) to have the computation speed of the worst possible implementation of ConstructiveReals. In practice it probably means that abstract constructive reals based on ConstructiveRIneq will never compute in decent speed.

So what do you think is the best sort for ConstructiveReals.CRlt ? Leaving it in Prop would acknowledge that the abstract constructive reals do not compute.

[spitters]

I'd be inclined to go for CRlt in Type, as it is a Sigma01 statement.
[ However, by definitive description we could also put it in Prop. ]

[VincentSe]

@spitters I now wonder if the real numbers interface is a good idea at all. Do you remember what was the motivation for it in C-CoRN ?

Consider the heart of real number computation, function ConstructiveRIneq.RQ_limit x n, that computes the rational approximation within 1/n of real number x. It starts from the rational upper bound b, then computes the linear_order_T on all b - k/(2n) until it finds a rational number within 1/n of x.

This algorithm is ridiculously slow. For each k, linear_order_T involves computing the Cauchy sequence of x within 1/2n, ie re-doing the exact same computations. Whereas if you knew that real numbers are implemented as Cauchy sequences, then you would only compute the sequence once within 1/n and the approximation would be over (not even using the bound b). So this number of k's is the wasted acceleration ratio, and it is linear in the precision asked (you want 3 digits, it's 1000 times slower). A trichotomy between the lower and upper bounds would reduce this waste from linear to logarithmic, but it is still very sad.

If we want good performance, we'd take your "faster" implementation of C-CoRN, make it the exposed definition of real numbers, and code every computation bulldog-style to it. So : no abstractions, no type classes, no records, no nothing. The downside of this is if one day we find an even faster implementation than "faster", we'll have to rewrite everything.

A middle ground would be to add redundant performance functions in the interface. Typically RQ_limit would be in the interface, so that each implementation hard wires the fastest version it has.

[ppedrot]

If we want good performance, we'd take your "faster" implementation of C-CoRN, make it the exposed definition of real numbers, and code every computation bulldog-style to it. So : no abstractions, no type classes, no records, no nothing. The downside of this is if one day we find an even faster implementation than "faster", we'll have to rewrite everything.

Not that I enjoy playing Cassandra, but I distinctly remember warning you against this tension between abstraction and performance for real computations at TYPES...

[VincentSe]

@ppedrot So what is your recommendation in this case? Abstraction or speed? Anyway I'm almost certain we do not want to expose my ConstructiveCauchyReals. They are a good proof that constructive reals are consistent, but they do not compute with decent speed. So we must hide them behind some sort of abstraction for the moment.

[ppedrot]

@VincentSe I am not a specialist, but the impression I had was that it is not realistic to hope for a generic, efficient implementation of reals. In particular believing that constructing a real in proof mode will lead to something that computes in practice is but wishful thinking.

It seems you almost always prefer some floating-point implementation where the precision is quantified once over the whole library, and that uses clever approximating algorithms for the functions you're interested in.

Which means that, for the case at hand, abstraction is the only viable alternative.

[VincentSe]

@ppedrot Yes, that is my opinion too. Anyway I don't have anything fast enough to offer at the moment, so we keep the interface.

Next question, in the interface, do we put CRlt in sort Prop or Type ? Prop would simplify proofs, and can always recover Type by constructive_indefinite_ground_description_nat. However Prop is pretty much game over for computations, because of those useless and very slow constructive_indefinite_ground_description_nat.

[spitters]

The motivation of the corn reals was not computation.
This was done later with fast and faster (math-classes).
Since the reals are unique upto iso, we can use that to transport from one structure to another.
To do very fast implementations, one would probably use something like MPFR and perhaps use parametricity (as in CoqEAL) to connect it to the constructive reals.

[VincentSe]

Hi @herbelin, I don't think there will be more reviews about these changes. All comments and suggestions are integrated, can you merge now ? Again, this PR is not the last one about real numbers...

[herbelin]

Hi, I added a few more comments. Also, if I want to work with constructive reals only, is the recommended way to Require Import ConstructiveRIneq?

[herbelin]

I don't think there will be more reviews about these changes. All comments and suggestions are integrated, can you merge now ? Again, this PR is not the last one about real numbers...

I'm proposing to merge in the middle of next week, assuming that it'll be enough time for people like @silene to comment if they want, even if in vacation. I'm assigning in the meantime.

[spitters]

These are Dedekind reals with extra structure. They've been studied by Auke Booij. Using countable choice the dedekind sand Cauchy numbers are equivalent. from my phone

…

On Fri, Aug 16, 2019, 11:24 Vincent Semeria ***@***.***> wrote: ***@***.**** commented on this pull request. ------------------------------ In theories/Reals/ConstructiveReals.v <#10632 (comment)>: > @@ -0,0 +1,119 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) +(************************************************************************) + +(* An interface for constructive and computable real numbers. + All of its elements are isomorphic, for example it contains Sumbool-based Dedekind reals (replace the or by a sumbool in the located hypothesis). They're computable and isomorphic to the Cauchy reals. I proposed them to Andrej, but he said he wanted to keep the possibly non computable Dedekind reals. I think he wants to study abstract Stone duality, which is a way to "compute" those Prop-based numbers. I don't exactly know what this means though. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#10632?email_source=notifications&email_token=AABTNTVU7YEB2TZBNNEHQE3QE3BCPA5CNFSM4IJYKHMKYY3PNVWWK3TUL52HS4DFWFIHK3DMKJSXC5LFON2FEZLWNFSXPKTDN5WW2ZLOORPWSZGOCBZ2NDI#discussion_r314770031>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AABTNTWRMGFKPIVJMOPMVBLQE3BCPANCNFSM4IJYKHMA> .

[VincentSe]

Hello @herbelin, it has been a week so we have not not @silene agrees. Shall we go classical and conclude that @silene agrees ? Anyway can you merge now ?

[herbelin]

Sorry for the delay. I'm going to merge it soon.

[VincentSe]

Thanks Hugo