The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 20/12/2016 17:45, Konstantin Weitz wrote:

> Is this definition of the real numbers safe to use or are there any edge
> cases that may allow me to prove False? 

It is safe. You might be able to prove surprising results, but False is
not part of them.

Note that, even if Rinv had been restricted to nonzero inputs, you could
still have defined the Rinv function from the standard library. So the
latter does not bring anything more to the table, except for ease of use
(partial functions are painful to use).

Here is an example. Even if Rinv_partial is a function that is defined
only for nonzero inputs, it can still be used to define a total function
extensionally equal to Rinv.

Definition Rinv_partial x (_: x <> R0) := Rinv x.
Definition Rinv' x :=
  match Req_EM_T x R0 with
  | right H => Rinv_partial x H
  | _ => Rinv 0
  end.
Lemma foo x : Rinv x = Rinv' x.
Proof.
  unfold Rinv'. now destruct Req_EM_T as [->|].
Qed.

> Are these still the real numbers? It seems that when we play the same
> trick for negative square roots, we extend the real numbers to the
> complex numbers.

You can extend the square root to negative numbers (and Coq standard
library actually does so), but that does not mean you get for free that
the square of the square root of a negative number is this negative
number. This property is available only for nonnegative numbers. So yes,
these are the real numbers.

> Can we use the same trick to add other real valued functions that are
> not necessarily defined for all inputs, such as infinite sums, limits, etc?

Yes, as long as you have some way to detect that you are outside the
domain of a function, you can conservatively extend this function to any
input.

So it is only a matter of which tools you allow for deciding whether an
input is inside the domain. For instance, constructive people rightfully
consider the Req_TM_T symbol I used above to be anathema. So they would
reject the existence of a total inverse function. (But they would allow
the existence of a total square root function.)

Best regards,

Guillaume