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 = 0would be a poor tradeoff.
Last updated: Feb 04 2023 at 22:29 UTC