Email Gateway (Aug 22 2022 at 11:12): Email Gateway (Aug 22 2022 at 11:12):From: Johannes Hölzl <hoelzl@in.tum.de>
Hi Noam,
for 2. you can not enforce anything, if you chose (THE x. False) it may
be also = 0 or = 1, you just can not prove it. This makes only sense if
you want to have the option to change the value later on. In a total
logic like HOL we usually fix it to a default value, like 0 (or in this
case 1).
I think a simpler definition of mrpow would be:
x ** y = (if y : Nats then x ^ nat (floor y)
else if - y : Nats then (1 / x) ^ nat (floor (-y))
else x powr y)
Then you can prove:
0 < x ==> x ** y = x powr y
x ** real n = x ^ n
x ** - real n = (1 / x) ^ n
Of course you get x ** 0 = 1, but just imagine that
(THE x. False) = 1 ;-)
Another question is:
What are your application for this operator?
Maybe an extension of ^ to integers would be enough?
ipow :: 'a::field => int => 'a
ipow x 0 = 1
ipow x (- n) = (1 / x) ^ n
ipow x (+ n) = x ^ n
- Johannes
Email Gateway (Aug 22 2022 at 11:12):From: noam neer <noamneer@gmail.com>
hi,
as far as I understand now, (THE x. False) is treated by the system as some
real number, fixed but unknown. u can prove things about it only if they
hold for all reals. this is quite satisfactory for me. also, I think the
behavior of 'powr' for negative base is quite similar- it is defined using
the logarithm of the base which is "undefined" in a very similar way. this
is different in Coq, where the real power behaves like u said and for
negative base returns 1.
thanx, noam
Email Gateway (Aug 22 2022 at 11:12):From: Johannes Hölzl <hoelzl@in.tum.de>
Hi Noam,
yes THE x. False, SOME x. False, SOME x. True, undefined. This are all
fixed but unknown values. The main reason I prefer a default value like
0 is that such functions are easier to handle.
For example to prove measurability of ln, or log one needs to prove that
the ln is _constant_ for x <= 0. So now "THE x. False" is not an
arbitrary value but this specific one. Imagine ln was defined to be
ln = SOME f. f = the_inv_on {0 <..} exp
then we can prove measurability only for the non-negative reals, which
is very annoying.
TL;DR using THE x. False or any other 'undefined' value is annoying and
does not buy you anything...
Email Gateway (Aug 22 2022 at 11:29):From: noam neer <noamneer@gmail.com>
hi,
I'm looking for a power operator for real numbers that is closer to the
mathematical conventions of real analysis than either ^ or powr. if we
denote it by **, my requirements from it are
0**y is undefined for y<=0.
(formally it can be (THE x. False). note that the definition of '0^0=1'
is appropriate in algebra, combinatorics and set theory, but not in
analysis.)
for negative base and real integer exponent (that is, reals in the set
Ints) the result should be the expected one.
(powr, which is defined using the logarithm of the base, doesn't
satisfy this.)
I'd like to know if anybody have already developed such an operator. If not
I guess I'll try it myself. a possible definition is
definition mrpow :: "real ⇒ real ⇒ real"
(infixr "**" 80)
where "x ** y == if x>0
then (x powr y)
else (if x=0
then (if y>0
then 0
else (THE z::real. False))
else (if y ∈ Ints
then (if y ≥ 0
then x ^(nat( floor y))
else (1/x)^(nat(- floor y)))
else (THE z::real. False)
)
)"
and if necessary I'll work on proving its properties until it is easy to
use. again any comments or suggestions are welcome.
Last updated: Apr 25 2024 at 08:20 UTC