The Coq mailing list

[Konstantin Weitz <weitzkon AT cs.washington.edu>]

I looked at Coq's standard real number library, and was surprised that the multiplicative inverse is defined even for 0 (I always thought that the inverse is only defined for non-zero arguments).

Parameter Rinv : R -> R.

It seems that the standard library compensates for this, by only specifying the behavior of the inverse for non-zero arguments.

Axiom Rinv_l : forall r:R, r <> 0 -> / r * r = 1.

Nethertheless, this means there is a real number assigned to 0/0:

Check 0/0.

And we can even prove simple theorems about division by 0. 

Goal 5 / 0 = (1/0) * 5.

  unfold Rdiv.

  rewrite Rmult_comm.

  rewrite Rmult_1_l.

  reflexivity.

Qed.

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

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.

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?