RPowSimp tactic questions

Stream: metaprogramming / tactics

[Alex Kontorovich]

I was playing around with the RPowSimp tactic from the "Symmetric Project" (from here) and was wondering if the following applications were in scope: (These examples are lifted from the PNT+ project, where this kind of stuff arises all the time, in fact even with complex bases and exponents...)

example {s A : ℝ} (s_nonzero : s ≠ 0) : Real.exp (s) ^ (A / s) = Real.exp A := by
  rpow_simp -- remains: ⊢ rexp s ^ (A * s⁻¹) = rexp A
  sorry

example {t σ : ℝ} (ht : 0 ≤ t) : t ^ (1 - σ) = t / t ^ (σ) := by
  rpow_simp -- remains: ⊢ t ^ (1 - σ) = t * t ^ (-σ)
  sorry

-- Even if you add the 1st power on `t`, it still doesn't see it
example {t σ : ℝ} (ht : 0 ≤ t) : t ^ (1 - σ) = t ^ 1 / t ^ (σ) := by
  rpow_simp -- remains: ⊢ t ^ (1 - σ) = t * t ^ (-σ)
  sorry

For comparison, the following examples work, though sometimes when combined with other tactics:

example (a x s : ℝ) (hx : 0 ≤ x): a / x ^ s = a * x ^ (-s) := by
  rpow_simp
  -- works

example {x y s : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) :
    x ^ s / y ^ s = (y / x) ^ (-s) := by
  rpow_simp -- remains: ⊢ x ^ s * y ^ (-s) = y ^ (-s) * x ^ (- -s)
  ring_nf

example {x y s : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) :
    x ^ (-s) / y ^ (-s) = (y / x) ^ s := by
  rpow_simp -- remains: ⊢ x ^ (-s) * y ^ (- -s) = y ^ s * x ^ (-s)
  ring_nf

example {s A : ℝ} (ePos : 0 < e) (s_nonzero : s ≠ 0) : (e ^ s) ^ (A / s) = e ^ A := by
  rpow_simp -- remains: ⊢ e ^ (s * A * s⁻¹) = e ^ A
  congr
  field_simp
  ring

Perhaps this is a question for @Patrick Massot ? (Is there an intention to contribute this tactic to Mathlib? If so, these may be useful test cases...) Thanks for your help!

[Patrick Massot]

I don’t think we included anything with exp so I am not surprised those don’t work. Are you sure the others are always true even in edge cases?

[Patrick Massot]

In any case this tactic was never polished and is clearly tested only on things that appeared in the project.

[Patrick Massot]

Resuming work on this and PRing to Mathlib is still on my todo list but with low priority so it may never happen if there is no extra motivation.

[Alex Kontorovich]

I think it would be quite useful (for PNT+) to have something like this, for what it's worth... (But of course it's well above my paygrade to make that happen...)

[Patrick Massot]

Having a new project needing it is clearly rising the priority. The issue with the symmetric project is that Mario and I wrote the tactic when the project was already completed, because Terry told me such a tactic would have been useful.

[Patrick Massot]

We can definitely try to ping @Mario Carneiro to see whether he wants to work on that.