feat: positivity extension for Real.rpow (#4486)

This PR introduces a positivity extension for `Real.rpow`. It is located at the same place as the mathlib3 version, namely in `Analysis/SpecialFunctions/Pow/Real.lean`.

Note that the two tests I left commented out fail, but due to coercions from `ℝ≥0∞` not working yet.

Author: dupuisf

Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

@@ -10,6 +10,7 @@ Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne, Sébasti
 ! if you have ported upstream changes.
 -/
 import Mathlib.Analysis.SpecialFunctions.Pow.Complex
+import Qq
 
 
 /-! # Power function on `ℝ`
@@ -99,6 +100,8 @@ theorem rpow_pos_of_pos {x : ℝ} (hx : 0 < x) (y : ℝ) : 0 < x ^ y := by
 theorem rpow_zero (x : ℝ) : x ^ (0 : ℝ) = 1 := by simp [rpow_def]
 #align real.rpow_zero Real.rpow_zero
 
+theorem rpow_zero_pos (x : ℝ) : 0 < x ^ (0 : ℝ) := by simp
+
 @[simp]
 theorem zero_rpow {x : ℝ} (h : x ≠ 0) : (0 : ℝ) ^ x = 0 := by simp [rpow_def, *]
 #align real.zero_rpow Real.zero_rpow
@@ -699,8 +702,7 @@ theorem exists_rat_pow_btwn {α : Type _} [LinearOrderedField α] [Archimedean 
 
 end Real
 
--- Porting note: tactics removed
--- section Tactics
+section Tactics
 
 -- /-!
 -- ## Tactic extensions for real powers
@@ -756,32 +758,36 @@ end Real
 
 -- end NormNum
 
--- namespace Tactic
-
--- namespace Positivity
-
--- /-- Auxiliary definition for the `positivity` tactic to handle real powers of reals. -/
--- unsafe def prove_rpow (a b : expr) : tactic strictness := do
---   let strictness_a ← core a
---   match strictness_a with
---     | nonnegative p => nonnegative <$> mk_app `` Real.rpow_nonneg_of_nonneg [p, b]
---     | positive p => positive <$> mk_app `` Real.rpow_pos_of_pos [p, b]
---     | _ => failed
--- #align tactic.positivity.prove_rpow tactic.positivity.prove_rpow
-
--- end Positivity
-
--- open Positivity
-
--- /-- Extension for the `positivity` tactic: exponentiation by a real number is nonnegative when
--- the base is nonnegative and positive when the base is positive. -/
--- @[positivity]
--- unsafe def positivity_rpow : expr → tactic strictness
---   | q(@Pow.pow _ _ Real.hasPow $(a) $(b)) => prove_rpow a b
---   | q(Real.rpow $(a) $(b)) => prove_rpow a b
---   | _ => failed
--- #align tactic.positivity_rpow tactic.positivity_rpow
-
--- end Tactic
-
--- end Tactics
+namespace Mathlib.Meta.Positivity
+
+open Lean Meta Qq
+
+/-- Extension for the `positivity` tactic: exponentiation by a real number is positive (namely 1)
+when the exponent is zero. The other cases are done in `evalRpow`. -/
+@[positivity (_ : ℝ) ^ (0 : ℝ), Pow.pow (_ : ℝ) (0 : ℝ), Real.rpow (_ : ℝ) (0 : ℝ)]
+def evalRpowZero : Mathlib.Meta.Positivity.PositivityExt where eval {_ _} _ _ e := do
+  let .app (.app (f : Q(ℝ → ℝ → ℝ)) (a : Q(ℝ))) (_ : Q(ℝ)) ← withReducible (whnf e)
+    | throwError "not Real.rpow"
+  guard <|← withDefault <| withNewMCtxDepth <| isDefEq f q(Real.rpow)
+  pure (.positive (q(Real.rpow_zero_pos $a) : Expr))
+
+/-- Extension for the `positivity` tactic: exponentiation by a real number is nonnegative when
+the base is nonnegative and positive when the base is positive. -/
+@[positivity (_ : ℝ) ^ (_ : ℝ), Pow.pow (_ : ℝ) (_ : ℝ), Real.rpow (_ : ℝ) (_ : ℝ)]
+def evalRpow : Mathlib.Meta.Positivity.PositivityExt where eval {_ _} zα pα e := do
+  let .app (.app (f : Q(ℝ → ℝ → ℝ)) (a : Q(ℝ))) (b : Q(ℝ)) ← withReducible (whnf e)
+    | throwError "not Real.rpow"
+  guard <|← withDefault <| withNewMCtxDepth <| isDefEq f q(Real.rpow)
+  let ra ← core zα pα a
+  match ra with
+  | .positive pa =>
+      have pa' : Q(0 < $a) := pa
+      pure (.positive (q(Real.rpow_pos_of_pos $pa' $b) : Expr))
+  | .nonnegative pa =>
+      have pa' : Q(0 ≤ $a) := pa
+      pure (.nonnegative (q(Real.rpow_nonneg_of_nonneg $pa' $b) : Expr))
+  | _ => pure .none
+
+end Mathlib.Meta.Positivity
+
+end Tactics

test/positivity.lean

@@ -1,6 +1,7 @@
 import Mathlib.Data.Complex.Exponential
 import Mathlib.Data.Real.Sqrt
 import Mathlib.Analysis.Normed.Group.Basic
+import Mathlib.Analysis.SpecialFunctions.Pow.Real
 
 /-! # Tests for the `positivity` tactic
 
@@ -167,11 +168,12 @@ example [LinearOrderedSemifield α] (a : α) : 0 < a ^ (0 : ℤ) := by positivit
 -- example {a b : Cardinal.{u}} (ha : 0 < a) : 0 < a ^ b := by positivity
 -- example {a b : Ordinal.{u}} (ha : 0 < a) : 0 < a ^ b := by positivity
 
--- example {a b : ℝ} (ha : 0 ≤ a) : 0 ≤ a ^ b := by positivity
--- example {a b : ℝ} (ha : 0 < a) : 0 < a ^ b := by positivity
--- example {a : ℝ≥0} {b : ℝ} (ha : 0 < a) : 0 < a ^ b := by positivity
+example {a b : ℝ} (ha : 0 ≤ a) : 0 ≤ a ^ b := by positivity
+example {a b : ℝ} (ha : 0 < a) : 0 < a ^ b := by positivity
+example {a : ℝ≥0} {b : ℝ} (ha : 0 < a) : 0 < a ^ b := by positivity
 -- example {a : ℝ≥0∞} {b : ℝ} (ha : 0 < a) (hb : 0 ≤ b) : 0 < a ^ b := by positivity
 -- example {a : ℝ≥0∞} {b : ℝ} (ha : 0 < a) (hb : 0 < b) : 0 < a ^ b := by positivity
+example {a : ℝ} : 0 < a ^ 0 := by positivity
 
 -- example {a : ℝ} (ha : 0 < a) : 0 ≤ ⌊a⌋ := by positivity
 -- example {a : ℝ} (ha : 0 ≤ a) : 0 ≤ ⌊a⌋ := by positivity