The Coq mailing list

[Joseph Tassarotti <jtassaro AT andrew.cmu.edu>]

In my opinion, the benefit of making sqrt : R -> R is that you can write down formulas as they would appear on paper without having to insert proofs showing that all the arguments are in the domain. Now, as you say, in general, to apply many lemmas about these functions you're going to have to show that the arguments are in the domain, but at least they don't have to appear in the term. This is especially important when you want to do rewriting involving an _expression_ that occurs as an argument to sqrt. For example, if you had sqrt (x + y) and want to use commutativity of addition to rewrite this to sqrt (y + x), you can do this just with "rewrite". On the other hand, if sqrt took a proof that the argument was >= 0, and we had sqrt Hpf (x + y), where Hpf: (x + y) >= 0, then we can't just rewrite with the usual commutativity rule, because we also need to update the Hpf term to a proof showing that (y + x) >= 0. (Of course this can all be done, but there is a bit more overhead involved.)

As long as the restriction condition on the domain is decidable, you can always define a version that works on unrestricted domain just by first checking if the condition holds, and if it does, supplying the appropriate value, and otherwise returning an arbitrary value. The trick here is that if you can, try to set it up so that the arbitrary value you return will still preserve important properties, so that you can apply lemmas about them without a side condition that the argument is in bounds. This idea is explained quite nicely in section 4.5 of the Coquelicot paper (https://hal.inria.fr/hal-00860648/), where the authors define Lim_seq in such a manner that various equational rules hold even when the limit doesn't exist.

-Joe

On Thu, Jan 31, 2019 at 11:47 AM Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:

Dear Coq Users & Team,

 

in the last months I started to use the Reals in Coq quite a lot and from my point of view proving stuff with the existing definitions is reasonably straight forward.

 

Where I started to struggle and question my understanding of the Reals in Coq – which is cause of my education as physicist anyway a bit limited - is when I wanted to write a asin and acos function.

 

It is fairly easy to define these in the open interval -1 < x < 1 based on atan:

 

Definition asin_open s := atan(s/sqrt(1-s²)).

Definition acos_open c := PI/2 - asin_open(c).

 

and it is also easy to prove the most important lemmas, like that these are indeed the inverses of sin and cos.

 

Now I wanted to define these functions on the closed interval -1 <= x <= 1. This is also rather straight forward, but only if I have the domain restriction as pre condition, while I don’t need -1 < x < 1 as precondition for asin_open above.

 

Admittedly rather late I started to wonder why the signature of asin as defined above is R->R, although the function is only defined on the closed interval -1..1? This obviously goes back to sqrt also being defined on R->R.

 

All in all I must say I don’t really understand the domain restrictions for real functions in Coq. Lemmas involving division frequently (but not always) require that the denominator is non zero, but otherwise domain restrictions seem to be rare. Shouldn’t all functions with limited domain require that their arguments are in this domain?

 

Or is it so that it is not possible to prove anything (interesting) about expressions which contain real valued functions outside of their argument domain? If so I wonder if there is a way to define asin and acos so that they work on the closed interval without requiring a domain condition.

 

Some insight into the design considerations would be very much appreciated.

 

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