Stream: Coq users

Topic: Rpower zero


view this post on Zulip 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?

view this post on Zulip 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: Feb 04 2023 at 22:29 UTC