Implement norm_num for rpow

[eric-wieser]

mathlib4/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

Lines 816 to 863 in 34bb97b

	-- 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

[dwrensha]

Implemented in #9893.

[dwrensha]

Closed by #9893.