I am using the Coquelicot library to describe a variety of proofs around real numbers.
For one of my experiments, I need to work with improper integrals, in particular, integrals where one of the bounds is at infinity. To state a theorem of dominated convergence, I need to express that I compute an integral where the bounds respect the natural order among real numbers. However, in Coquelicot the bounds of an improper integrals are described using filters. So it seems that we need to add a notion of order between the bounds.
A filter is a set of sets. In Coq, people often stay away from sets, and in Coquelicot the filters are actually represented by predicates (in other words, a set is actually described by the predicate that is true on all the elements of the set). So a set of real numbers is described by a function of type
R -> Prop
and a set of sets is described by a function of type
(R -> Prop) -> Prop
It is debatable that this habit of describing sets of sets by predicates on predicates actually makes the library more user-friendly, but there is a gain in generality that makes this idea really attractive.
To describe a point on the real line, a filter is actually a collection of sets that vanishes at this point. So in a sense, the elements of the filter are not important individually, it is the way they vanish that really matters. But the word “vanish” seem to imply that there is an evolution in time. How can one capture this evolution?
In practice, it is useful to look at the way things are expressed and proved to see how filters do work. Let us look at the filter that expresses the minus infinity bound. This filter is written
Rbar_locally m_infty
When checking whether a given predicate is accepted by this filter, what happens is the following:
Lemma dummy_test_Rbar_locally my_pred : Rbar_locally m_infty my_pred. Proof. unfold Rbar_locally.
my_pred : R -> Prop ============================ exists M : R, forall x : R, x < M -> my_pred x
To show that my_pred is accepted by the filter representing the minus infinity bound, it suffices to show that my_pred accepts all points beyond a given real number on the negative side of the real line. This also means any predicate accepting all numbers smaller than an arbitrary constant is accepted. Ultimately, even if we a negative value that is very far from 0, the subset of R that contains all the numbers smaller than this value is guaranteed to contain this subset. This how we can mean “tending toward minus infinity”.
Similarly, there exists a filter construction at_right, which describes the bound at the right of finite point on the real line. The filter at_right a accepts all the sets that are supersets of intersections of ball of a given non-zero radius and the positive half-line with lower-bound a. Here, ultimately, it is balls of decreasing diameter that express the notion of vanishing towards a.
So the sense of direction, or of evolution in time is given by the points going towards minus infinity for the first filter that we observed, Rbar_locally m_infty, and by the vanishing radius of a ball centered in a for the second filter.
How do we define an order between filters?
If fa and fb are two filters, they contain supersets of sets that vanish towards a and b, respectively. These supersets can be very large and in particular, even when a is smaller than b, there maybe a set accepted by fa that contains an element larger than an element of a set accepted by fb. We should avoid being trapped by looking at only one of the sets in each filter and manage to see what is given by the whole (actually infinite) collection of sets.
The solution that came to my mind is to combine two filters on R to obtain a filter on R2. The library provided such a capability, with a construction named filterprod. Intuitively, given two types A and B with elements a and b and filters fa and fb vanishing towards these points, we can construct a new filter on the cartesian product A*B, vanishing towards the pair (a,b). This filter is written
filter_prod fa fb
To express that two filters on the real line are ordered in a way similar to the conventional order on this line, I propose the following definition.
Definition filter_Rlt F G := exists m, filter_prod F G (fun p => fst p < m < snd p).
This definition relies on a witness that gives a real point between the two filters. I have yet to find whether this point is necessary, or whether one could do with just stating the first coordinate of a point should just be less than the second coordinate.
With this definition, I am able to show that different kinds of pairs of filters satisfy the “order”. It will probably be useful to show transitivity of this order, too. The current state of this experiment is visible at this address.
