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: if y is within a ball of radius e centred at x, then x is within a ball of radius e centred at y.
  • ax3: if y is within a ball of radius e1 centred at x and z is within a ball of radius e2 centred at y, then we can enlarge the ball at x to have a radius of e1 + e2 to ensure that z 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.

Copyright © 2023 Calvin Beck