4

In Coq, we can formalize the concept of the limit of a function defined on R by defining a function lim of type (R -> R) -> R -> R -> Prop as follows:

Require Import Coq.Reals.Reals.
Open Scope R.

Definition lim (f : R -> R) (c : R) (L : R) :=
  forall (eps : R), 0 < eps -> exists (del : R), 0 < del /\
  (forall (x : R), 0 < R_dist x c < del -> R_dist (f x) L < eps).

We can then prove that the limit is unique:

Theorem lim_unique (f : R -> R) (c : R) (L M : R) :
  lim f c L -> lim f c M -> L = M.

However in math, we normally write limits using an equals sign, like "lim x->c f(x) = L". This works because of the uniqueness of limits, so the property of = being an equivalence relation is compatible with this new implicitly-defined meaning of = that we introduce in the notation "lim x->c f(x) = L".

Is it possible to define limits in this way in Coq? More specifically, can we define a function lim2 of type (R -> R) -> R -> R such that lim2 f c = L if and only if lim f c L?

Anton Trunov
  • 15,074
  • 2
  • 23
  • 43
Ben
  • 470
  • 1
  • 6
  • 18
  • 1
    Sure you can, even if you need to use an axiom for it, but it doesn't really matter as Coq Reals actually make use of the axiom already. The most convenient way is to define limits to operate over the extended real line, that is, `R \cup {-inf, +inf}` ; I recommend you have a look to the Coquelicot Coq library and papers where this work is actually done. [I could post a solution here but it would just copying and pasting from that lib] – ejgallego Jun 11 '17 at 18:34
  • 1
    See in particular "Limits and Continuity" in http://coquelicot.saclay.inria.fr/html/Coquelicot.Coquelicot.html – ejgallego Jun 11 '17 at 18:38
  • @ejgallego Please do post! It'll promote the Coq ecosystem and lower the entrance barrier for everybody! – Anton Trunov Jun 11 '17 at 18:46
  • @ejgallego so ultimately the definition depends on `LimSup_seq`, which depends on `sig_proj1`, which depends on `sig`. I'm not sure I understand what `sig` is doing though. The definition says that {x : T | P x} has type Prop, but what does it mean for this object to be true? Does it mean that the set is nonempty? Where does the uniqueness of the limit come into this definition? – Ben Jun 11 '17 at 19:24
  • @Ben Maybe [this question](https://stackoverflow.com/q/41461247/2747511) can help with `sig_proj1` and `sig`. – Anton Trunov Jun 11 '17 at 20:54
  • `{r : R | lim f r}` is usually read as "there exists an `r` such that is the limit for `f`". – ejgallego Jun 11 '17 at 21:07
  • 1
    @Ben here a bit more explanation on how you go from your first definition of limit to the functional one: roughly, you first test whether `exists L, lim f c L` is provable or not. That requires the excluded middle. Assume the limit exists, then you can use a choice principle to get the witness, we are good. Now, on the second case, the limit doesn't exists, then we return 0, or pi, or any other arbitrary value! We don't really care, as the function only makes sense when the limit exists. You could actually make the limit function to return an option type, but it makes its use more cumbersome. – ejgallego Jun 12 '17 at 00:46

0 Answers0