The Coq mailing list

[bertot <Yves.Bertot AT inria.fr>]

On 18/11/14 8:56 AM, 
ncyms8r3x2 AT snkmail.com
 wrote:
> I can't find a cube root function for reals in the standard library. Am I
> missing it?
>
> Is there another commonly used and more complete library for real numbers that
> you can recommend?
There is a function Rpower : R -> R -> R, It is more general than cube 
root.  As noted by B. Spitters, cube root can be implemented with the 
help of logarithm and exponential.  This is illustrated by the 
definition of Rpower:

Coq < Print Rpower.
Rpower = fun x y : R => exp (y * ln x)
     : R -> R -> R

Argument scopes are [R_scope R_scope]

There are a few theorems about Rpower, which may help you obtain most of 
the results you may want to consider.  If you want to compute this 
function, there is the problem that you can of course only compute 
approximations, so you are looking for ways to prove things like:

Lemma cubic_root_3_app1 :  14422 /10000 < Rpower 3 (1/3) < 14423/10000.

The work mentioned by Bas does provide a systematic way to do that. In 
the case of cubic roots you can do it in an ad-hoc way by using monotony 
properties of the power function.  However, this example also shows that 
not all handy theorems about Rpower are provided.

Here is an example.  I also use the tactic "psatzl R" which can compare 
quite efficiently values in R, as long as these values are given as 
fractions of integer constants.

Require Import Reals Psatz.

Lemma cubic_root_3_app1 : 14422 /10000 < Rpower 3 (1/3) < 14423/10000.
assert (Rpower_lt' : forall x y z, 0 < x < y -> 0 < z -> Rpower x z < 
Rpower y z).
 intros x y z xy z0; apply exp_increasing, Rmult_lt_compat_l; 
[assumption | ].
 apply ln_increasing; tauto.
assert (Rpower_3 : forall x, 0 < x -> Rpower x 3 = x ^ 3).
 intros x x0; replace 3 with (INR 3) by (simpl; ring).
 now rewrite Rpower_pow.

replace (14422/10000) with (Rpower (14422/10000) (3 * (1/3)))
 by (replace (3 * (1/3)) with 1 by field; rewrite Rpower_1; psatzl R).
replace (14423/10000) with (Rpower (14423/10000) (3 * (1/3)))
 by (replace (3 * (1/3)) with 1 by field; rewrite Rpower_1; psatzl R).
rewrite <- !Rpower_mult.
split; apply Rpower_lt'; try rewrite Rpower_3; try psatzl R.
Qed.