The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Dear Michael,

This design question is fundamentally the same (but in a more complex
case) as the choice of defining 1/0=0 in the natural number domain.
This is something that incidentally continues to confuse beginners not
just in Coq but in other pure functional languages as well
(https://discourse.elm-lang.org/t/integer-division-by-zero/2923). The
alternatives are indeed dependently-typed functions (as highlighted by
Joseph), but also functions returning values of type option. In both
case, this breaks composability and is thus inconvenient.

The three solutions (dependently-typed functions, functions which
return an option and total functions) are all weird compared to the
usual “undefined” behavior of math. So it seems to me that the ideal
solution would be to actually emulate this “undefined” behavior by
raising an exception. Pierre-Marie Pédrot has worked on adding
exceptions to CIC without breaking consistency and has a plugin to do
that (that I've never tried). I don't know how far we are from having
exceptions in mainline Coq...

Théo

Le ven. 1 févr. 2019 à 10:38, Soegtrop, Michael
<michael.soegtrop AT intel.com>
 a écrit :
>
> Dear Joseph,
>
>
>
> thanks for the detailed explanation of the design considerations!
>
>
>
> So in short the story is that all real functions with domain restrictions 
> are extended to total functions over the complete R by returning some value 
> which is convenient in most situations. E.g. for asin I could return –PI/2 
> or PI/2 for out of domain arguments, so that I can prove that the function 
> is everywhere continuous and that the result of asin is limited to –PI/2 to 
> PI/2 without requiring domain restrictions. And when it comes to proving 
> that my definition of asin has a certain taylor expansion or derivative, I 
> limit the argument range of asin to –1 … 1. Or alternatively I could return 
> 1/0 for out of range asin, which possibly would allow me to prove that the 
> derivative of asin x equals 1/sqrt(1-x^2) everywhere, but then I would need 
> a domain restriction for the lemma which shows that asin x is bounded.
>
> This design leads to that one can prove:
>
>
>
> Require Import Reals.
>
> Require Import Psatz.
>
> Open Scope R_scope.
>
>
>
> Lemma sqrt_minus_one_is_zero: sqrt (-1) = 0.
>
> Proof.
>
>   unfold sqrt.
>
>   destruct (Rcase_abs (-1)) as [H|H].
>
>   - reflexivity.
>
>   - contradict H; lra.
>
> Qed.
>
>
>
> I am not sure if I like that one can prove sqrt(-1) = 0, even if this does 
> not lead to a prove of that x=0 solves x²=-1. It is an interesting system – 
> a bit weird, but I guess one gets used to it over time. As I said, in 
> practice the reals as defined in Coq are very convenient to use and I 
> understand that one has to pay some price for that (like sqrt(-1)=0).
>
>
>
> Best regards,
>
>
>
> Michael
>
>
>
> Intel Deutschland GmbH
> Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
> Tel: +49 89 99 8853-0, www.intel.de
> Managing Directors: Christin Eisenschmid
> Chairperson of the Supervisory Board: Nicole Lau
> Registered Office: Munich
> Commercial Register: Amtsgericht Muenchen HRB 186928