Extended domain of rpow (powr)

[binghe]

Hi,

Inspired by #1247, this PR extends the domain of rpow (powr :real -> real -> real). Previously rpow has the following definition:

   [rpow_def]  Definition (transcTheory)      
      ⊢ ∀a b. a powr b = exp (b * ln a)

Since ln a is only specified when 0 < a, the valid domain of a powr b is 0 < a and b arbitrary. (Outside this domain a powr b is an unspecified positive real.) But there are two more cases when a powr b is a (finite) real number:

1. a = 0 and 0 < b.
2. a is arbitrary and b is an integer.

Now I extend the definition of rpow (by new_specification) to cover the above cases:

   [powr_def]  Definition      
      ⊢ (∀a b. 0 < a ⇒ a powr b = exp (b * ln a)) ∧
        (∀b. 0 < b ⇒ 0 powr b = 0) ∧
        ∀a n. a powr &n = a pow n ∧ a powr -&SUC n = (a pow SUC n)⁻¹

With this new definition, the following theorems can be proved unconditionally (i.e. without requiring 0 < a for a powr b):

   [RPOW_0]  Theorem      
      ⊢ ∀a. a powr 0 = 1
   
   [RPOW_1]  Theorem      
      ⊢ ∀a. a powr 1 = a

But the following theorems now have to have the antecedent 0 < a for a powr b, because the old definition of rpow as a rewriting rule a powr b = exp (b * ln a) is no more available:

   [RPOW_ADD]  Theorem      
      ⊢ ∀a b c. 0 < a ⇒ a powr (b + c) = a powr b * a powr c
   
   [RPOW_ADD_MUL]  Theorem      
      ⊢ ∀a b c. 0 < a ⇒ a powr (b + c) * a powr -b = a powr c

The hardest part is to fix the proof of DIFF_RPOW by using some advanced results from real_topologyTheory (which has some minor updates):

   [DIFF_RPOW]  Theorem      
      ⊢ ∀x y. 0 < x ⇒ ((λx. x powr y) diffl (y * x powr (y − 1))) x

P. S. opening realLib instead of RealArith in real_topologyScript.sml greatly reduced the building time of real_topologyTheory by 100s, because the old, faster REAL_ARITH is tried first).

--Chun

[tjark]

Nice. Why the SUC in a powr -&SUC n = (a pow SUC n)⁻¹?

[binghe]

Nice. Why the SUC in a powr -&SUC n = (a pow SUC n)⁻¹?

I was thinking the case -&0 (= &0) is already covered by the other branch, thus is redundant. But perhaps without SUC the definition itself could serve better as rewriting rule. I will change it.

[someplaceguy]

Just a very minor observation:

When I first read this definition, the second branch (∀b. 0 < b ⇒ 0 powr b = 0) made me think that 0 powr 0 is not defined (like in Z3 and the usual exponentiation operation in math), but in fact it is defined by the third branch, and 0 powr 0 also equals zero because 0 pow 0 = 0. This means the second branch could in theory be strengthened to ∀b. 0 <= b ⇒ 0 powr b = 0, right? Of course, this would be redundant and wouldn't change the meaning of powr at all, so I'm not suggesting you change it, I was just pointing out this peculiarity :) Edit: this is not correct.

Thanks!

[someplaceguy]

Nice. Why the SUC in a powr -&SUC n = (a pow SUC n)⁻¹?

If we got rid of SUC then we'd have to add that a is conditional on not being zero, right? Otherwise 0 powr (-0) would be defined as being (0 pow 0)⁻¹ (which is not defined) instead of being equal to zero like it is now, right? Edit: apparently realinv 0 = 0, so I think my previous statement is not correct.

[binghe]

Just a very minor observation:

When I first read this definition, the second branch (∀b. 0 < b ⇒ 0 powr b = 0) made me think that 0 powr 0 is not defined (like in Z3 and the usual exponentiation operation in math), but in fact it is defined by the third branch, and 0 powr 0 also equals zero because 0 pow 0 = 0. This means the second branch could in theory be strengthened to ∀b. 0 <= b ⇒ 0 powr b = 0, right? Of course, this would be redundant and wouldn't change the meaning of powr at all, so I'm not suggesting you change it, I was just pointing out this peculiarity :)

Thanks!

No... according to the definition of pow, 0 pow 0 = 1:

   [real_pow]  Definition      
      ⊢ (∀x. x pow 0 = 1) ∧ ∀x n. x pow SUC n = x * x pow n

See also this Wikipedia article [1] (in short: "Zero to the power of zero, denoted by 0^0, is a mathematical expression that is either defined as 1 or left undefined, depending on context"). Although I'm a hater of division-by-zero (x / 0 = 0), I personally think 0 pow 0 = 1 is quite natural by the above recursive definition of pow.

If a = 0, the definition a powr -&SUC n = (a pow SUC n)⁻¹ will become realinv 0, which is what I didn't expect. I personally do not want to depend on realinv 0 = 0, but what does Z3's powr do in this case? (e.g. 0 powr -1)

[1] https://en.wikipedia.org/wiki/Zero_to_the_power_of_zero

[binghe]

Nice. Why the SUC in a powr -&SUC n = (a pow SUC n)⁻¹?

I have now updated the definition of powr with this one (equivalent to the previous but more friendly to rewriters):

|- (!a b. 0 < a ==> a powr b = exp (b * ln a)) /\
        (!b. 0 < b ==> 0 powr b = 0) /\
        (!a n. a powr &n = a pow n) /\
         !a n. a powr -&n = inv (a pow n)

I think there's no need to explicitly disable 0 powr -&n (= inv 0 = 0). If one day inv 0 were made unspecific (unlikely, many proofs may be broken), the above definition of powr will automatically eliminate the case "a = 0 and b negative integer" from its domain.

[someplaceguy]

No... according to the definition of pow, 0 pow 0 = 1:

Yes, you're right, of course! 😔
Sorry for the confusion!

[mn200]

Thanks both!