feat: implement rpow norm_num extension (#9893)

* Implements a norm_num extension for `a ^ b` where `a` and `b` are reals. Unlike in the mathlib3 version, there is no restriction on the positivity of `a`.
* Moves commented-out tests from test/norm_num_ext.lean into a new file test/norm_num_rpow.lean, to keep the dependencies of norm_num_ext.lean lightweight.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author: dwrensha

Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

@@ -905,56 +905,82 @@ section Tactics
 /-!
 ## Tactic extensions for real powers
 -/
-
-
--- namespace NormNum
-
--- open Tactic
-
--- theorem rpow_pos (a b : ℝ) (b' : ℕ) (c : ℝ) (hb : (b' : ℝ) = b) (h : a ^ b' = c) :
--- a ^ b = c := by
---   rw [← h, ← hb, Real.rpow_nat_cast]
--- #align norm_num.rpow_pos NormNum.rpow_pos
-
--- theorem rpow_neg (a b : ℝ) (b' : ℕ) (c c' : ℝ) (a0 : 0 ≤ a) (hb : (b' : ℝ) = b) (h : a ^ b' = c)
---     (hc : c⁻¹ = c') : a ^ (-b) = c' := by
---   rw [← hc, ← h, ← hb, Real.rpow_neg a0, Real.rpow_nat_cast]
--- #align norm_num.rpow_neg NormNum.rpow_neg
-
--- /-- Evaluate `Real.rpow a b` where `a` is a rational numeral and `b` is an integer.
--- (This cannot go via the generalized version `prove_rpow'` because `rpow_pos` has a
--- side condition; we do not attempt to evaluate `a ^ b` where `a` and `b` are both negative because
--- it comes out to some garbage.) -/
--- unsafe def prove_rpow (a b : expr) : tactic (expr × expr) := do
---   let na ← a.to_rat
---   let ic ← mk_instance_cache q(ℝ)
---   match match_sign b with
---     | Sum.inl b => do
---       let (ic, a0) ← guard (na ≥ 0) >> prove_nonneg ic a
---       let nc ← mk_instance_cache q(ℕ)
---       let (ic, nc, b', hb) ← prove_nat_uncast ic nc b
---       let (ic, c, h) ← prove_pow a na ic b'
---       let cr ← c
---       let (ic, c', hc) ← prove_inv ic c cr
---       pure (c', (expr.const `` rpow_neg []).mk_app [a, b, b', c, c', a0, hb, h, hc])
---     | Sum.inr ff => pure (q((1 : ℝ)), expr.const `` Real.rpow_zero [] a)
---     | Sum.inr tt => do
---       let nc ← mk_instance_cache q(ℕ)
---       let (ic, nc, b', hb) ← prove_nat_uncast ic nc b
---       let (ic, c, h) ← prove_pow a na ic b'
---       pure (c, (expr.const `` rpow_pos []).mk_app [a, b, b', c, hb, h])
--- #align norm_num.prove_rpow norm_num.prove_rpow
-
--- /-- Evaluates expressions of the form `rpow a b` and `a ^ b` in the special case where
--- `b` is an integer and `a` is a positive rational (so it's really just a rational power). -/
--- @[norm_num]
--- unsafe def eval_rpow : expr → tactic (expr × expr)
---   | q(@Pow.pow _ _ Real.hasPow $(a) $(b)) => b.to_int >> prove_rpow a b
---   | q(Real.rpow $(a) $(b)) => b.to_int >> prove_rpow a b
---   | _ => tactic.failed
--- #align norm_num.eval_rpow norm_num.eval_rpow
-
--- end NormNum
+namespace Mathlib.Meta.NormNum
+
+open Lean.Meta Qq
+
+theorem isNat_rpow_pos {a b : ℝ} {nb ne : ℕ}
+    (pb : IsNat b nb) (pe' : IsNat (a ^ nb) ne) :
+    IsNat (a ^ b) ne := by
+  rwa [pb.out, rpow_nat_cast]
+
+theorem isNat_rpow_neg {a b : ℝ} {nb ne : ℕ}
+    (pb : IsInt b (Int.negOfNat nb)) (pe' : IsNat (a ^ (Int.negOfNat nb)) ne) :
+    IsNat (a ^ b) ne := by
+  rwa [pb.out, Real.rpow_int_cast]
+
+theorem isInt_rpow_pos {a b : ℝ} {nb ne : ℕ}
+    (pb : IsNat b nb) (pe' : IsInt (a ^ nb) (Int.negOfNat ne)) :
+    IsInt (a ^ b) (Int.negOfNat ne) := by
+  rwa [pb.out, rpow_nat_cast]
+
+theorem isInt_rpow_neg {a b : ℝ} {nb ne : ℕ}
+    (pb : IsInt b (Int.negOfNat nb)) (pe' : IsInt (a ^ (Int.negOfNat nb)) (Int.negOfNat ne)) :
+    IsInt (a ^ b) (Int.negOfNat ne) := by
+  rwa [pb.out, Real.rpow_int_cast]
+
+theorem isRat_rpow_pos {a b : ℝ} {nb : ℕ}
+    {num : ℤ} {den : ℕ}
+    (pb : IsNat b nb) (pe' : IsRat (a^nb) num den) :
+    IsRat (a^b) num den := by
+  rwa [pb.out, rpow_nat_cast]
+
+theorem isRat_rpow_neg {a b : ℝ} {nb : ℕ}
+    {num : ℤ} {den : ℕ}
+    (pb : IsInt b (Int.negOfNat nb)) (pe' : IsRat (a^(Int.negOfNat nb)) num den) :
+    IsRat (a^b) num den := by
+  rwa [pb.out, Real.rpow_int_cast]
+
+/-- Evaluates expressions of the form `a ^ b` when `a` and `b` are both reals.-/
+@[norm_num (_ : ℝ) ^ (_ : ℝ)]
+def evalRPow : NormNumExt where eval {u α} e := do
+  let .app (.app f (a : Q(ℝ))) (b : Q(ℝ)) ← Lean.Meta.whnfR e | failure
+  guard <|← withNewMCtxDepth <| isDefEq f q(HPow.hPow (α := ℝ) (β := ℝ))
+  haveI' : u =QL 0 := ⟨⟩
+  haveI' : $α =Q ℝ := ⟨⟩
+  haveI' h : $e =Q $a ^ $b := ⟨⟩
+  h.check
+  let (rb : Result b) ← derive (α := q(ℝ)) b
+  match rb with
+  | .isBool .. | .isRat _ .. => failure
+  | .isNat sβ nb pb =>
+    match ← derive q($a ^ $nb) with
+    | .isBool .. => failure
+    | .isNat sα' ne' pe' =>
+      assumeInstancesCommute
+      haveI' : $sα' =Q AddGroupWithOne.toAddMonoidWithOne := ⟨⟩
+      return .isNat sα' ne' q(isNat_rpow_pos $pb $pe')
+    | .isNegNat sα' ne' pe' =>
+      assumeInstancesCommute
+      return .isNegNat sα' ne' q(isInt_rpow_pos $pb $pe')
+    | .isRat sα' qe' nume' dene' pe' =>
+      assumeInstancesCommute
+      return .isRat sα' qe' nume' dene' q(isRat_rpow_pos $pb $pe')
+  | .isNegNat sβ nb pb =>
+    match ← derive q($a ^ (-($nb : ℤ))) with
+    | .isBool .. => failure
+    | .isNat sα' ne' pe' =>
+      assumeInstancesCommute
+      return .isNat sα' ne' q(isNat_rpow_neg $pb $pe')
+    | .isNegNat sα' ne' pe' =>
+      let _ := q(instRingReal)
+      assumeInstancesCommute
+      return .isNegNat sα' ne' q(isInt_rpow_neg $pb $pe')
+    | .isRat sα' qe' nume' dene' pe' =>
+      assumeInstancesCommute
+      return .isRat sα' qe' nume' dene' q(isRat_rpow_neg $pb $pe')
+
+end Mathlib.Meta.NormNum
 
 end Tactics
 

Mathlib/NumberTheory/Bertrand.lean

@@ -88,26 +88,20 @@ theorem real_main_inequality {x : ℝ} (n_large : (512 : ℝ) ≤ x) :
     exact (h.right_le_of_le_left'' h1 ((h1.trans h2).trans_le h0) h2 h0 (h4.trans h3)).trans h4
   refine' ⟨18, 512, by norm_num1, by norm_num1, n_large, _, _⟩
   · have : sqrt (2 * 18) = 6 := (sqrt_eq_iff_mul_self_eq_of_pos (by norm_num1)).mpr (by norm_num1)
-    rw [hf, log_nonneg_iff, this]
-    rw [one_le_div] <;> norm_num1
-    apply le_trans _ (le_mul_of_one_le_left _ _) <;> norm_num1
-    apply Real.rpow_le_rpow <;> norm_num1
-    apply rpow_nonneg; norm_num1
-    apply rpow_pos_of_pos; norm_num1
-    apply hf' 18; norm_num1
+    rw [hf _ (by norm_num1), log_nonneg_iff (by positivity), this, one_le_div (by norm_num1)]
     norm_num1
   · have : sqrt (2 * 512) = 32 :=
       (sqrt_eq_iff_mul_self_eq_of_pos (by norm_num1)).mpr (by norm_num1)
-    rw [hf, log_nonpos_iff (hf' _ _), this, div_le_one] <;> norm_num1
-    · conv in 512 => equals 2 ^ 9 => norm_num1
-      conv in 1024 => equals 2 ^ 10 => norm_num1
-      conv in 32 => rw [← Nat.cast_ofNat]
-      rw [rpow_nat_cast, ← pow_mul, ← pow_add]
-      conv in 4 => equals 2 ^ (2 : ℝ) => rw [rpow_two]; norm_num1
-      rw [← rpow_mul, ← rpow_nat_cast]
-      apply rpow_le_rpow_of_exponent_le
-      all_goals norm_num1
-    · apply rpow_pos_of_pos four_pos
+    rw [hf _ (by norm_num1), log_nonpos_iff (hf' _ (by norm_num1)), this,
+        div_le_one (by positivity)]
+    conv in 512 => equals 2 ^ 9 => norm_num1
+    conv in 2 * 512 => equals 2 ^ 10 => norm_num1
+    conv in 32 => rw [← Nat.cast_ofNat]
+    rw [rpow_nat_cast, ← pow_mul, ← pow_add]
+    conv in 4 => equals 2 ^ (2 : ℝ) => rw [rpow_two]; norm_num1
+    rw [← rpow_mul, ← rpow_nat_cast]
+    apply rpow_le_rpow_of_exponent_le
+    all_goals norm_num1
  #align bertrand.real_main_inequality Bertrand.real_main_inequality
 
 end Bertrand

test/norm_num_ext.lean

@@ -323,12 +323,6 @@ example : Nat.fib 65 = 17167680177565 := by norm_num1
 example : Nat.fib 100 + Nat.fib 101 = Nat.fib 102 := by norm_num1
 example : Nat.fib 1000 + Nat.fib 1001 = Nat.fib 1002 := by norm_num1
 
-/-
-example : (2 : ℝ) ^ (3 : ℝ) = 8 := by norm_num
-example : (1 : ℝ) ^ (20 : ℝ) = 1 := by norm_num
-example : (2 : ℝ) ^ (-3 : ℝ) = 1/8 := by norm_num
--/
-
 section big_operators
 
 variable {α : Type _} [CommRing α]

test/norm_num_rpow.lean

@@ -0,0 +1,15 @@
+/-
+Copyright (c) 2021 Mario Carneiro All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro, David Renshaw
+-/
+import Mathlib.Analysis.SpecialFunctions.Pow.Real
+
+example : (2 : ℝ) ^ (3 : ℝ) = 8 := by norm_num1
+example : (1 : ℝ) ^ (20 : ℝ) = 1 := by norm_num1
+example : (-2 : ℝ) ^ (3 : ℝ) = -8 := by norm_num1
+example : (1/5 : ℝ) ^ (2 : ℝ) = 1/25 := by norm_num1
+example : (-1/3 : ℝ) ^ (-3 : ℝ) = -27 := by norm_num1
+example : (1/2 : ℝ) ^ (-3 : ℝ) = 8 := by norm_num1
+example : (2 : ℝ) ^ (-3 : ℝ) = 1/8 := by norm_num1
+example : (-2 : ℝ) ^ (-3 : ℝ) = -1/8 := by norm_num1