From aa9926492feaf8326f379469a555f77393fcd306 Mon Sep 17 00:00:00 2001 From: thery Date: Tue, 19 Mar 2019 14:26:11 +0100 Subject: - Addition to the Reals theory : - minus: lemmas `Rminus_eq_0` and `Rmult_minus_distr_r` - sin : sin_inj - cos : cos_inj - sqrt : lemmas `pow2_sqrt` and `inv_sqrt` - atan : lemmas `tan_inj`, `atan_eq0`, `atan_tan` and `tan_atan` - asin : definition and some basic properties - acos : definition and some basic properties --- doc/changelog/10-standard-library/00000-title.rst | 1 - doc/changelog/10-standard-library/09803-trigo.rst | 2 ++ 2 files changed, 2 insertions(+), 1 deletion(-) create mode 100644 doc/changelog/10-standard-library/09803-trigo.rst (limited to 'doc') diff --git a/doc/changelog/10-standard-library/00000-title.rst b/doc/changelog/10-standard-library/00000-title.rst index d517a0e709..a182366f03 100644 --- a/doc/changelog/10-standard-library/00000-title.rst +++ b/doc/changelog/10-standard-library/00000-title.rst @@ -1,3 +1,2 @@ **Standard library** - diff --git a/doc/changelog/10-standard-library/09803-trigo.rst b/doc/changelog/10-standard-library/09803-trigo.rst new file mode 100644 index 0000000000..10cb069a4c --- /dev/null +++ b/doc/changelog/10-standard-library/09803-trigo.rst @@ -0,0 +1,2 @@ + +- Addition to the Reals theory (`#09803 `_ by Laurent Théry): -- cgit v1.2.3 From 934c757b72fa9fdae5828068c7e8a050d1103a10 Mon Sep 17 00:00:00 2001 From: Michael Soegtrop Date: Sat, 7 Sep 2019 07:34:50 +0200 Subject: - Adjusted definitions and lemmas for asin and acos to what has been discussed - Added derivative for asin and acos - Added a few additional trigonometry lemmas - Added Lemmas for the derivative of a decreasing inverse function - Did some cleanup (move lemmas to the files where they belong) --- doc/changelog/10-standard-library/00000-title.rst | 1 + doc/changelog/10-standard-library/09803-trigo.rst | 2 -- doc/changelog/10-standard-library/9803-reals.rst | 14 ++++++++++++++ doc/stdlib/index-list.html.template | 1 + 4 files changed, 16 insertions(+), 2 deletions(-) delete mode 100644 doc/changelog/10-standard-library/09803-trigo.rst create mode 100644 doc/changelog/10-standard-library/9803-reals.rst (limited to 'doc') diff --git a/doc/changelog/10-standard-library/00000-title.rst b/doc/changelog/10-standard-library/00000-title.rst index a182366f03..d517a0e709 100644 --- a/doc/changelog/10-standard-library/00000-title.rst +++ b/doc/changelog/10-standard-library/00000-title.rst @@ -1,2 +1,3 @@ **Standard library** + diff --git a/doc/changelog/10-standard-library/09803-trigo.rst b/doc/changelog/10-standard-library/09803-trigo.rst deleted file mode 100644 index 10cb069a4c..0000000000 --- a/doc/changelog/10-standard-library/09803-trigo.rst +++ /dev/null @@ -1,2 +0,0 @@ - -- Addition to the Reals theory (`#09803 `_ by Laurent Théry): diff --git a/doc/changelog/10-standard-library/9803-reals.rst b/doc/changelog/10-standard-library/9803-reals.rst new file mode 100644 index 0000000000..86c5e45bc1 --- /dev/null +++ b/doc/changelog/10-standard-library/9803-reals.rst @@ -0,0 +1,14 @@ +- **Changed:** + Cleanup of names in the Reals theory: replaced `tan_is_inj` with `tan_inj` and replaced `atan_right_inv` with `tan_atan` - + compatibility notations are provided. Moved various auxiliary lemmas from `Ratan.v` to more appropriate places. + (`#9803 `_, + by Laurent Théry and Michael Soegtrop). + +- **Added:** to the Reals theory: + inverse trigonometric functions `asin` and `acos` with lemmas for the derivatives, bounds and special values of these functions; + an extensive set of identities between trigonometric functions and their inverse functions; + lemmas for the injectivity of sine and cosine; + lemmas on the derivative of the inverse of decreasing functions and on the derivative of horizontally mirrored functions; + various generic auxiliary lemmas and definitions for Rsqr, sqrt, posreal an others. + (`#9803 `_, + by Laurent Théry and Michael Soegtrop). diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index e64b4be454..7fa621c11c 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -558,6 +558,7 @@ through the Require Import command.

theories/Reals/Rtrigo_fun.v theories/Reals/Rtrigo1.v theories/Reals/Rtrigo.v + theories/Reals/Rtrigo_facts.v theories/Reals/Ratan.v theories/Reals/Machin.v theories/Reals/SplitAbsolu.v -- cgit v1.2.3