In the stdlib, the definition of `Rpower x y`

is defined as `exp (y* ln x)`

. I was curious as to the reason behind this choice: in particular, how does one go about proving this?

```
Theorem Rpower_base_0 : forall y, y>0 -> Rpower 0 y = 0.
```

I notice that all results involving Rpower tack on the additional hypothesis that the base of the exponentiation is strictly positive. How does one deal with the case where the base is zero?

You cannot prove `Rpower 0 y = 0`

, since you can prove `Rpower x y > 0`

. As to why it was defined this way, it is just because it is the most usual definition. Making the definition much more complicated just to cover the exceptional case `x = 0`

would be a poor tradeoff.

Last updated: Sep 23 2023 at 14:01 UTC