Koundinya Vajjha (Dec 26 2020 at 05:27): Koundinya Vajjha (Dec 26 2020 at 05:27):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?
Guillaume Melquiond (Dec 26 2020 at 10:47):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: Oct 13 2024 at 01:02 UTC