coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: [Coq-Club] Why is the signature of sqrt R->R ?
- Date: Thu, 31 Jan 2019 16:46:42 +0000
- Accept-language: de-DE, en-US
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga14.intel.com
- Dlp-product: dlpe-windows
- Dlp-reaction: no-action
- Dlp-version: 11.0.400.15
- Ironport-phdr: 9a23:+e9yGBNYsczKAurzyacl6mtUPXoX/o7sNwtQ0KIMzox0Ivj7rarrMEGX3/hxlliBBdydt6oUzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlLiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSkHKTA37X3XhMJzgqJavB2uqAdyzJTIbIyRLvdyYr/Rcc4cSGFcXshRTStBAoakYocBEuQBOvhXr4bhp1sUqhu+HRGgD/7oxD9JmnD23bc13PolEQ3IwQctGNcOsHXIo9X1LqgdT+S1wLPTzTXEcfxW1iv96JLPchA5uvyMXLRwcdbPxkkrDQ/KklKQqYn8Mj6Ty+8DvW+b7+96WuKujW4qswBxoj6zxsgyjonFnJ8axU7C+C5kw4g1PcW1RFN/bNK6CpddtyGXO5F2T888WW1kpTs2x70etZKmfSUHxo4ryhDRZvCdbYSF7BbuWPyMLTp7mn5pYK+zihe2/ES61OHxVsa53ExUoiZfk9TBtnYA3AHJ5MedUPty5EKh1C6P1w/N7uFEJlg5la/UK5E737I9mYAfsUXFHi/qhkr2iLWaeVkj+uit8+jnY7PmqYGAN4Jslw3zNroilta/DOk4KAQDX3aX9f6h2LH+/UD1WLBKgec3kqndvpDaP8MbpquhDg9Q04Ys9xa/AC2439Qch3UHN1VFdwyIj4j1IVHOJ+j4AOy+g1SqjDdk2fTGMqf9DZXKK3jPiK3hcqpl605A1AozyshS6I5TCrEYOf78RkvxtMHDARIiKAy1w+PnCM1n2Y8EWGKPBLWZMKLIvlOS6OIvObrEWIhA8j36Mr0u4+PkpX4/g14UO6ezl9NDY3ehW/9iPk+xYHz2g95HH31c7SQkS+m/wmaFXDFPfXGqG+oZ5zo7AY+iR8+XQ4GmgLWM2GGgGZBZenpBEniNF2vlc8OPXPJaO3HaGdNojjFRDevpcIQmzxz77FarmYoiFfLd/2gjjbym0dF04+PJkhRrrG51CdiQ1yeGSGQmxzpUFQ9z57h2pAlG8nnGybJx2qUKFNpP6vcPWQA/Z8aFkr5KTuvqUweERe+nDVarRtL/XmM0Qdton5kPZVpwH5OpiRWRhyc=
|
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 |
- [Coq-Club] Why is the signature of sqrt R->R ?, Soegtrop, Michael, 01/31/2019
- Re: [Coq-Club] Why is the signature of sqrt R->R ?, Joseph Tassarotti, 01/31/2019
Archive powered by MHonArc 2.6.18.