An interface for constructive and computable real numbers.
All of its instances are isomorphic (see file ConstructiveRealsMorphisms).
For example it contains the Cauchy reals implemented in file
ConstructivecauchyReals and the sumbool-based Dedekind reals defined by
Structure R := {
lower : Q -> Prop;
upper : Q -> Prop;
lower_proper : Proper (Qeq ==> iff) lower;
upper_proper : Proper (Qeq ==> iff) upper;
lower_bound : { q : Q | lower q };
upper_bound : { r : Q | upper r };
lower_lower : forall q r, q < r -> lower r -> lower q;
lower_open : forall q, lower q -> exists r, q < r /\ lower r;
upper_upper : forall q r, q < r -> upper q -> upper r;
upper_open : forall r, upper r -> exists q, q < r /\ upper q;
disjoint : forall q, ~ (lower q /\ upper q);
located : forall q r, q < r -> { lower q } + { upper r }
}.
see github.com/andrejbauer/dedekind-reals for the Prop-based
version of those Dedekind reals (although Prop fails to make
them an instance of ConstructiveReals).
Any computation about constructive reals, can be worked
in the fastest instance for it; we then transport the results
to all other instances by the isomorphisms. This way of working
is different from the usual interfaces, where we would rather
prove things abstractly, by quantifying universally on the instance.
The functions of ConstructiveReals do not have a direct impact
on performance, because algorithms will be extracted from instances,
and because fast ConstructiveReals morphisms should be coded
manually. However, since instances are forced to implement
those functions, it is probable that they will also use them
in their algorithms. So those functions hint at what we think
will yield fast and small extracted programs.