The Coq mailing list

["Kyle Stemen" <ncyms8r3x2 AT snkmail.com>]

Because of the ln function, Rpower x (1/3) only matches the cube root for x > 0.

It seems like if I'm building up the cube root function and all associated lemmas, it may be easier to define it as the inverse of x^3, like how Rsqrt is defined.

I really appreciate the example of how to use psatzl. I haven't found any good examples of using reals in coq, so I'm learning through trial and error and examples like that.

I can't find much documentation on psatzl. Was it renamed to lra?

On Wed, Nov 19, 2014 at 5:14 AM, bertot Yves.Bertot-at-inria.fr |coq-club/Example Allow| <jxk10gdqut AT sneakemail.com> wrote:

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.