The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

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