An interface for constructive and computable real numbers.
All of its instances are isomorphic (see file ConstructiveRealsMorphisms).
For example it is implemented by the Cauchy reals in file
ConstructivecauchyReals and also implemented by 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.
Constructive reals are setoids, which custom equality is defined as
x == y iff (x <= y /\ y <= x).
It is hard to quotient constructively to get the Leibniz equality
on the real numbers. In "Sheaves in Geometry and Logic",
MacLane and Moerdijk show a topos in which all functions R -> Z
are constant. Consequently all functions R -> Q are constant and
it is not possible to approximate real numbers by rational numbers.
WARNING: this file is experimental and likely to change in future releases.