What I Learned This Week: Real Numbers in Coq
WILTW #3
This week more or less concludes my search for a real number library in Coq, allowing me to get another project underway which needed real numbers!
Additionally I have been messing a little bit more with subset types, which should prove useful in the very near future.
Coquelicot
I was desperately searching for a real number library in Coq, and finally happened upon this one. What’s nice about this one is that it works with the built in real number library, essentially just extending it to have some of the stuff that I want, and it works with Coq 8.7! C-CoRN is probably a better option if you need anything heavyweight, but it seems to only work for Coq 8.5.2 at the moment, and I was actually having some problems finding the documentation (I know it exists, but I can’t find it for some reason…).
Coquelicot is a fairly simple library with a very straightforward Coqdoc. My only complaint so far is that it doesn’t seem to be on opam, but installing it manually was painless!
One thing that this library offers, which I’m hoping to use, is limits. So, I spent a bit of time unfolding the limit definitions so that I could understand it.
Understanding the filter definition of limits in Coquelicot
Coquelicot implements limits in terms of filters. The limits in Coquelicot are a bit more general than I need – they work on a number of spaces, and not just over the real numbers. This stuff is vaguely familiar from the topology classes of yore, but it has been a while!
So, my goal is to roughly understand the limit definition used in Coquelicot with respect to real numbers:
Definition filterlim {T U : Type} (f : T -> U) F G :=
filter_le (filtermap f F) G.
This definition relies very heavily on filters, which are described here.
Class Filter {T : Type} (F : (T -> Prop) -> Prop) := {
filter_true : F (fun _ => True) ;
filter_and : forall P Q : T -> Prop, F P -> F Q -> F (fun x => P x /\ Q x) ;
filter_imp : forall P Q : T -> Prop, (forall x, P x -> Q x) -> F P -> F Q
}.
A filter (F
in this case) is any predicate of type (T -> Prop)
-> Prop
An example of a filter is locally x
for some x
.
Definition locally (x : T) (P : T -> Prop) :=
exists eps : posreal, forall y, ball x eps y -> P y.
It has to be shown that this is a filter, i.e., the library defines
locally to be an instance of filter, and there is a proof that it
satisfies the axioms of Filter
.
It’s easy to see that the types match up, since locally x : (T ->
Prop) -> Prop
, which is exactly the type that Filter
takes.
ball
is part of the UniformSpace
module…
Record mixin_of (M : Type) := Mixin {
ball : M -> R -> M -> Prop ;
ax1 : forall x (e : posreal), ball x e x ;
ax2 : forall x y e, ball x e y -> ball y e x ;
ax3 : forall x y z e1 e2, ball x e1 y -> ball y e2 z -> ball x (e1 + e2) z
}.
So, ball
is a predicate which takes a centre in the space, a real
number for the radius, and another point which is within the
space. The proposition holds when the second point is within the
ball around the first point of the given radius.
ax1
, ax2
, ax3
are all axioms for dealing with balls:
ax1
: the centre of a ball is within the ball.ax2
: ify
is within a ball of radiuse
centred atx
, thenx
is within a ball of radiuse
centred aty
.ax3
: ify
is within a ball of radiuse1
centred atx
andz
is within a ball of radiuse2
centred aty
, then we can enlarge the ball atx
to have a radius ofe1 + e2
to ensure thatz
is within this ball as well.
Right now we don’t really care about these axioms, since we’re just
trying to figure out how Filter
’s are used in limits. So, again,
we have this thing which makes a filter:
Definition locally (x : T) (P : T -> Prop) :=
exists eps : posreal, forall y, ball x eps y -> P y.
Where:
ball : M -> R -> M -> Prop ;
locally x
restricts the use of this predicate to the
neighbourhood around x
. I.e., locally says that we can find a
small enough ball around x
such that the predicate P
always
holds for every point within the ball.
This leads us to this definition, which comes up in our limit.
Definition filter_le {T : Type} (F G : (T -> Prop) -> Prop) :=
forall P, G P -> F P.
We want to know, much like with the epsilon delta definition of a
limit, that when we get close to a point (within a sufficiently
small ball), the result of the function is within epsilon of the
limit point. So, it becomes useful to be able to map the function
over the ball, giving us the image of the function on the domain of
the ball. We would then want to be able to tell if this image is
contained within the ball around the limit point. So, it makes
sense to want a predicate like filter_le
which will show that one
filter is entirely contained within another.
I’m reading this as: a filter F
is less than or equal to a filter
G
if for any predicate P : T -> P
…
G P -> F P
This seems to mean that every point in G
is in F
. I suspect F
might be considered less than G
since it filters out a smaller
or equal portion?
Doesn’t really matter, though, because I think its use here is fairly intuitive. This is the Coquelicot for \(\lim_{t \rightarrow x} c = c\).
filterlim (fun t => c) (locally x) (locally c).
Which unfolds to these:
filter_le (filtermap (fun _ : R => c) (locally x)) (locally c)
filter_le (fun P : R -> Prop => locally x (fun _ : R => P c)) (locally c)
filtermap
maps every element of the space T
onto some space U
using a function f : T -> U
. I.e., every element goes through
this map before being filtered.
filter_le (filtermap (fun _ : R => c) (locally x)) (locally c)
means that everything in the neighbourhood of x
, which is then
passed through our constant function which maps to c
will
approach c
. Where approach c
means that the ball
of G
(locally c
) is contained within the ball of F
(the
neighbourhood around x
which is then mapped to c
), for
sufficiently sized balls.
Summary
Okay, so, in sum, the filters are basically just used to select a neighborhood around a point. The limit definition just wants the neighborhood of the function as values in the domain approach a point to be contained within a neighborhood of the limit point. This is essentially just the epsilon delta definition of a limit, so it’s really not too surprising!
Subset Types
I’m working on a small project for analyzing computational complexity in Coq, which I have dubbed Coqplexity.
While working on this project I have made some observations about subset types, and some additional benefits they have.
To begin with, I’m working with complexity classes, which have some constraints upon values. For instance many of the real constants have to be greater than 0.
I started out doing this:
Definition BigO (f : nat -> R) (g : nat -> R) :=
exists (c : R) (n0 : nat), forall (n : nat),
(c > 0) % R ->
n > n0 ->
(0 <= f n /\ f n <= c * g n) % R.
which is more or less the standard definition of big O, but I have encountered some problems, which lead me to reformulate this with subset types like so:
Definition BigO (f : nat -> R) (g : nat -> R) :=
exists (sc : {c : R | (c > 0) % R}) (n0 : nat), forall (n : nat),
let c := proj1_sig sc in
n > n0 ->
(0 <= f n /\ f n <= c * g n) % R.
It’s a little annoying having to destruct sigmas and whatnot, but there are a couple of big advantages to this definition. To start with, consider something like big theta:
Definition BigTheta (f : nat -> R) (g : nat -> R) :=
exists (c1 c2 : R), exists (n0 : nat), forall (n : nat),
(c1 > 0) % R ->
(c2 > 0) % R ->
n > n0 ->
(0 <= c1 * g n <= f n /\ f n <= c2 * g n) % R.
You end up with more and more hypotheses. One thing that’s worth noting is that these are all irritatingly similar! If you put this condition within the subset type then you don’t have to repeat the condition multiple times:
Definition BigTheta (f : nat -> R) (g : nat -> R) :=
exists (sc1 sc2 : {c : R | (c > 0) % R}), exists (n0 : nat), forall (n : nat),
let c1 := proj1_sig sc1 in
let c2 := proj1_sig sc2 in
n > n0 ->
(0 <= c1 * g n /\ c1 * g n <= f n <= c2 * g n) % R.
It’s a small example, but this could be a big deal if your predicate is particularly complicated, or if you have a lot of variables.
Another thing that I have noticed, which is probably a much bigger deal, is that these definitions are not quite the same!
See, without the subset types I have a theorem which takes two
hypotheses c1 > 0
, and c2 > 0
. Which means that if I want to use
this theorem, even just to prove something that relies only upon one
of these constants, then I have to prove that both of these
constants (which are already bound) are greater than 0, whereas if I
use the subset types I get a proof along with the constants that
they are greater than 0. Thus the second theorem is actually much
more useful!
Productivity
Interleave mode is an Emacs mode for taking notes alongside a PDF, and it is absolutely amazing! I find that it really helps me stay focused when reading through a paper / textbook, and switching between the buffers to take notes / read the PDF is actually just fiddly enough that it’s a kind of fidget. I highly recommend this if you ever need to really focus and get through something.