Tactic for simple inequalities involving real exponentation

Stream: general

[Thomas Bloom]

(posted an issue at https://github.com/leanprover-community/mathlib/issues/11374, reposting here at Mario's suggestion)

While norm_num can e.g. prove 1 < 2^2 (all naturals) or (1:\R) < (2:\R)^2, it fails with (1:\R) < (2:\R)^(2:\R).

Similarly(?), neither norm_num nor linarith can prove (x:R), (x>0) implies (2:R)^x < (3:R)^x.

It would be very convenient if norm_num (and/or linarith?) could work with simple inequalities involving real exponents like this.

(To clarify, I know how to prove these facts using simple lemmas from mathlib, e.g. real.rpow_le_rpow for the second, but it'd be great if there was a tactic that could tackle such trivial numerical facts automatically.)

[Mario Carneiro]

example : (1:ℝ) < (2:ℝ)^(2:ℝ) := by norm_num -- works as of #11382

example (x : ℝ) (h : 0 < x) : (2:ℝ)^x < (3:ℝ)^x :=
by apply real.rpow_lt_rpow; norm_num *

[Mario Carneiro]

it'd be great if there was a tactic that could tackle such trivial numerical facts

The problem is that the definition of "trivial" is extremely difficult to pin down. norm_num works when there are no variables; for monotonic functions mono sometimes works but rpow_lt_rpow has a side condition and I don't know how you expect to handle this

[Thomas Bloom]

Ah, fair enough, so perhaps the second is too much to hope for.

Is the first feasible? You pointed out in the linked comment that one can recast the 2:\R to a natural number 2 and then norm_num does work. Could that first step be incorporated into norm_num so that only one application is needed?

[Thomas Bloom]

Never mind, I see that you already addressed this in the first part of your comment! (Embarassing oversight, but apparently you can't delete your own replies on Zulip.)

[Mario Carneiro]

The first is done in #11382

[Mario Carneiro]

Do we have a has_pow rat int instance somewhere? The rpow norm_num extension supports this grammar, but previously the only thing was npow which corresponds to has_pow A nat; gpow works on groups so it's not suitable for group-with-zero type structures

[Yakov Pechersky]

No, we don't have has_pow complex real either, I don't think.

[Mario Carneiro]

Apparently we do: docs#div_inv_monoid.has_pow