feat(push): push annotations for Real.log (leanprover-community#30039)

This PR adds `push` annotations, and tests for `Real.log`.

It also updates the `#push` and `#pull` commands so that they can take a discharger, and can take any head.

Author: JovanGerb

Mathlib/Analysis/SpecialFunctions/Log/Basic.lean

@@ -70,7 +70,7 @@ theorem le_exp_log (x : ℝ) : x ≤ exp (log x) := by
   · rw [exp_log_eq_abs h_zero]
     exact le_abs_self _
 
-@[simp]
+@[simp, push]
 theorem log_exp (x : ℝ) : log (exp x) = x :=
   exp_injective <| exp_log (exp_pos x)
 
@@ -96,25 +96,25 @@ theorem log_surjective : Surjective log := fun x => ⟨exp x, log_exp x⟩
 theorem range_log : range log = univ :=
   log_surjective.range_eq
 
-@[simp]
+@[simp, push]
 theorem log_zero : log 0 = 0 :=
   dif_pos rfl
 
-@[simp]
+@[simp, push]
 theorem log_one : log 1 = 0 :=
   exp_injective <| by rw [exp_log zero_lt_one, exp_zero]
 
 /-- This holds true for all `x : ℝ` because of the junk values `0 / 0 = 0` and `log 0 = 0`. -/
 @[simp] lemma log_div_self (x : ℝ) : log (x / x) = 0 := by
   obtain rfl | hx := eq_or_ne x 0 <;> simp [*]
 
-@[simp]
+@[simp, push]
 theorem log_abs (x : ℝ) : log |x| = log x := by
   by_cases h : x = 0
   · simp [h]
   · rw [← exp_eq_exp, exp_log_eq_abs h, exp_log_eq_abs (abs_pos.2 h).ne', abs_abs]
 
-@[simp]
+@[simp, push]
 theorem log_neg_eq_log (x : ℝ) : log (-x) = log x := by rw [← log_abs x, ← log_abs (-x), abs_neg]
 
 theorem sinh_log {x : ℝ} (hx : 0 < x) : sinh (log x) = (x - x⁻¹) / 2 := by
@@ -126,15 +126,17 @@ theorem cosh_log {x : ℝ} (hx : 0 < x) : cosh (log x) = (x + x⁻¹) / 2 := by
 theorem surjOn_log' : SurjOn log (Iio 0) univ := fun x _ =>
   ⟨-exp x, neg_lt_zero.2 <| exp_pos x, by rw [log_neg_eq_log, log_exp]⟩
 
+@[push]
 theorem log_mul (hx : x ≠ 0) (hy : y ≠ 0) : log (x * y) = log x + log y :=
   exp_injective <| by
     rw [exp_log_eq_abs (mul_ne_zero hx hy), exp_add, exp_log_eq_abs hx, exp_log_eq_abs hy, abs_mul]
 
+@[push]
 theorem log_div (hx : x ≠ 0) (hy : y ≠ 0) : log (x / y) = log x - log y :=
   exp_injective <| by
     rw [exp_log_eq_abs (div_ne_zero hx hy), exp_sub, exp_log_eq_abs hx, exp_log_eq_abs hy, abs_div]
 
-@[simp]
+@[simp, push]
 theorem log_inv (x : ℝ) : log x⁻¹ = -log x := by
   by_cases hx : x = 0; · simp [hx]
   rw [← exp_eq_exp, exp_log_eq_abs (inv_ne_zero hx), exp_neg, exp_log_eq_abs hx, abs_inv]
@@ -267,7 +269,7 @@ theorem log_eq_zero {x : ℝ} : log x = 0 ↔ x = 0 ∨ x = 1 ∨ x = -1 := by
 theorem log_ne_zero {x : ℝ} : log x ≠ 0 ↔ x ≠ 0 ∧ x ≠ 1 ∧ x ≠ -1 := by
   simpa only [not_or] using log_eq_zero.not
 
-@[simp]
+@[simp, push]
 theorem log_pow (x : ℝ) (n : ℕ) : log (x ^ n) = n * log x := by
   induction n with
   | zero => simp
@@ -276,12 +278,13 @@ theorem log_pow (x : ℝ) (n : ℕ) : log (x ^ n) = n * log x := by
     · simp
     · rw [pow_succ, log_mul (pow_ne_zero _ hx) hx, ih, Nat.cast_succ, add_mul, one_mul]
 
-@[simp]
+@[simp, push]
 theorem log_zpow (x : ℝ) (n : ℤ) : log (x ^ n) = n * log x := by
   cases n
   · rw [Int.ofNat_eq_natCast, zpow_natCast, log_pow, Int.cast_natCast]
   · rw [zpow_negSucc, log_inv, log_pow, Int.cast_negSucc, Nat.cast_add_one, neg_mul_eq_neg_mul]
 
+@[push]
 theorem log_sqrt {x : ℝ} (hx : 0 ≤ x) : log (√x) = log x / 2 := by
   rw [eq_div_iff, mul_comm, ← Nat.cast_two, ← log_pow, sq_sqrt hx]
   exact two_ne_zero
@@ -375,11 +378,13 @@ lemma log_multiset_prod {s : Multiset ℝ} (h : ∀ x ∈ s, x ≠ 0) :
   rw [← prod_toList, log_list_prod (by simp_all), sum_map_toList]
 
 open Finset in
+@[push]
 theorem log_prod {α : Type*} {s : Finset α} {f : α → ℝ} (hf : ∀ x ∈ s, f x ≠ 0) :
     log (∏ i ∈ s, f i) = ∑ i ∈ s, log (f i) := by
   rw [← prod_map_toList, log_list_prod (by simp_all)]
   simp
 
+@[push]
 protected theorem _root_.Finsupp.log_prod {α β : Type*} [Zero β] (f : α →₀ β) (g : α → β → ℝ)
     (hg : ∀ a, g a (f a) = 0 → f a = 0) : log (f.prod g) = f.sum fun a b ↦ log (g a b) :=
   log_prod fun _x hx h₀ ↦ Finsupp.mem_support_iff.1 hx <| hg _ h₀

Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

@@ -477,6 +477,9 @@ theorem inv_rpow (hx : 0 ≤ x) (y : ℝ) : x⁻¹ ^ y = (x ^ y)⁻¹ := by
 theorem div_rpow (hx : 0 ≤ x) (hy : 0 ≤ y) (z : ℝ) : (x / y) ^ z = x ^ z / y ^ z := by
   simp only [div_eq_mul_inv, mul_rpow hx (inv_nonneg.2 hy), inv_rpow hy]
 
+@[push low] /- Lower priority than `log_pow` and `log_zpow`.
+This is because otherwise the `pull` tactic will use `log_rpow` in places where it should
+use `log_pow` or `log_zpow`. -/
 theorem log_rpow {x : ℝ} (hx : 0 < x) (y : ℝ) : log (x ^ y) = y * log x := by
   apply exp_injective
   rw [exp_log (rpow_pos_of_pos hx y), ← exp_log hx, mul_comm, rpow_def_of_pos (exp_pos (log x)) y]

Mathlib/Tactic/Push.lean

@@ -317,17 +317,18 @@ which will print the `push head` form of `e`.
 
 `#push` understands local variables, so you can use them to introduce parameters.
 -/
-macro (name := pushCommand) tk:"#push " cfg:optConfig head:ident ppSpace e:term : command =>
-  `(command| #conv%$tk push $cfg $head:ident => $e)
+macro (name := pushCommand) tk:"#push" cfg:optConfig disch?:(discharger)? ppSpace head:term " => "
+    e:term : command =>
+  `(command| #conv%$tk push $cfg $[$disch?:discharger]? $head:term => $e)
 
 /--
 The syntax is `#push_neg e`, where `e` is an expression,
 which will print the `push_neg` form of `e`.
 
 `#push_neg` understands local variables, so you can use them to introduce parameters.
 -/
-macro (name := pushNegCommand) tk:"#push_neg " cfg:optConfig e:term : command =>
- `(command| #push%$tk $cfg Not $e)
+macro (name := pushNegCommand) tk:"#push_neg" cfg:optConfig ppSpace e:term : command =>
+ `(command| #push%$tk $cfg Not => $e)
 
 @[inherit_doc pull]
 elab "pull" disch?:(discharger)? head:(ppSpace colGt term) : conv => withMainContext do
@@ -341,8 +342,9 @@ which will print the `pull head` form of `e`.
 
 `#pull` understands local variables, so you can use them to introduce parameters.
 -/
-macro (name := pullCommand) tk:"#pull " head:ident ppSpace e:term : command =>
-  `(command| #conv%$tk pull $head:ident => $e)
+macro (name := pullCommand) tk:"#pull" disch?:(discharger)? ppSpace head:term " => " e:term :
+    command =>
+  `(command| #conv%$tk pull $[$disch?:discharger]? $head:term => $e)
 
 end Conv
 

MathlibTest/push.lean

@@ -2,7 +2,7 @@ import Mathlib.Tactic.Push
 import Mathlib.Data.Nat.Cast.Basic
 import Mathlib.Data.Set.Basic
 import Mathlib.Data.Set.Insert
-import Mathlib.Analysis.SpecialFunctions.Log.Basic
+import Mathlib.Analysis.SpecialFunctions.Pow.Real
 
 private axiom test_sorry : ∀ {α}, α
 
@@ -12,15 +12,15 @@ variable {p q r : Prop}
 
 /-- info: (q ∧ (p ∨ q)) ∧ r ∧ (p ∨ r) -/
 #guard_msgs in
-#push Or False ∧ p ∨ q ∧ r
+#push _ ∨ _ => False ∧ p ∨ q ∧ r
 
 /-- info: (p ∨ q) ∧ (p ∨ r) -/
 #guard_msgs in
-#push Or (p ∨ q) ∧ (p ∨ r)
+#push _ ∨ _ => (p ∨ q) ∧ (p ∨ r)
 
 /-- info: (p ∧ q ∨ q) ∨ p ∧ r ∨ r -/
 #guard_msgs in
-#push And (p ∨ True) ∧ (q ∨ r)
+#push _ ∧ _ => (p ∨ True) ∧ (q ∨ r)
 
 example {r : ℕ → Prop} : ∀ n : ℕ, p ∨ r n ∧ q ∧ n = 1 := by
   push ∀ n, _
@@ -38,7 +38,7 @@ example {r : ℕ → Prop} : ∃ n : ℕ, p ∨ r n ∨ q ∧ n = 1 := by
 
 /-- info: p ∨ ∃ x, q ∧ x = 1 -/
 #guard_msgs in
-#pull Exists p ∨ q ∧ ∃ n : ℕ, n = 1
+#pull ∃ _, _ => p ∨ q ∧ ∃ n : ℕ, n = 1
 
 /--
 info: DiscrTree branch for Or:
@@ -73,3 +73,31 @@ example : (fun x : ℕ ↦ x ^ 2 + 1 * 0 - 5 • 6) = id ^ 2 + 1 * 0 - 5 • 6 :
   simp only [pullFun]
 
 end lambda
+
+section log
+
+example (a b : ℝ) (ha : 0 < a) (hb : 0 < b) : Real.log (a * b) = Real.log a + Real.log b := by
+  pull (disch := positivity) Real.log
+  rfl
+
+variable (a b c : Real) (ha : 0 < a) (hc : 0 < c)
+
+/-- info: ↑4 * Real.log a + -Real.log c - b * Real.log a + b -/
+#guard_msgs in
+#push (disch := positivity) Real.log => Real.log (a ^ 4 * c⁻¹ / a ^ b * Real.exp b)
+
+/-- info: ∑ i ∈ Finset.Ioo 0 5, Real.log ↑i -/
+#guard_msgs in
+#push (disch := simp <;> grind) Real.log => Real.log (∏ i ∈ Finset.Ioo 0 5, (i : Nat))
+
+set_option pp.numericTypes true in
+/-- info: Real.log (a ^ (4 : ℝ) * c⁻¹ / a ^ b) + b -/
+#guard_msgs in
+#pull (disch := positivity) Real.log => 4 * Real.log a + -Real.log c - b * Real.log a + b
+
+set_option pp.numericTypes true in
+/-- info: Real.log (a ^ (4 : ℕ) * c⁻¹ / a ^ b) + b -/
+#guard_msgs in
+#pull (disch := positivity) Real.log => (4 : Nat) * Real.log a + -Real.log c - b * Real.log a + b
+
+end log