The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 19/11/2014 14:14, bertot wrote:

> 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.

I feel compelled to show a more automatic proof:

Require Import Reals Interval_tactic.
Lemma cubic_root_3_app1 :
  (14422/10000 < Rpower 3 (1/3) < 14423/10000)%R.
Proof.
unfold Rpower.
split ; interval.
Qed.

Disclaimer: the "ln" function is not supported by any of the currently 
released version of CoqInterval, so the script above depends on the 
master branch of CoqInterval.

Best regards,

Guillaume