Tactic/strategy for `deriv`?

Stream: Is there code for X?

[Vasily Ilin]

What is the recommended way of computing straightforward but tedious derivatives? E.g.

noncomputable
def g (t:ℝ) x := (√(2 * π * t))⁻¹ * rexp (- x^2 / (2 * t))
lemma deriv_g_t {x : ℝ} (ht : t > 0) : deriv (fun t => g t x) t = (g t x) * (-1/t + x^2/t^2) := by
  sorry

I thought simp should do it but it did not work.

[Kenny Lau]

either aesop should work, or grind should work, or someone will have to write a custom tactic

[Kenny Lau]

i know that limit is one of the requested tactics, which may or may not be related

[Kenny Lau]

i think the community would benefit greatly if more people learned metaprogramming

[Etienne Marion]

Just for fun here is the "by hand" proof (note that I had to add a factor 2 for the computation to be correct):

import Mathlib

open scoped Real

noncomputable
def g (t:ℝ) x := (√(2 * π * t))⁻¹ * rexp (- x^2 / (2 * t))
lemma deriv_g_t {x t : ℝ} (ht : t > 0) : deriv (fun t => g t x) t = (g t x) * (-1/t + x^2/t^2) / 2 := by
  simp_rw [g]
  rw [deriv_fun_mul, deriv_fun_inv'', deriv_sqrt, deriv_const_mul, deriv_id'', deriv_exp,
    deriv_fun_div, deriv_const, deriv_const_mul, deriv_id'']
  · grind
  any_goals fun_prop (disch := positivity)
  all_goals positivity

[Kenny Lau]

then this feels like aesop would work after we add all those lemmas to aesop's database

[Ruben Van de Velde]

Does fun_prop prove it if you write it with HasDeriv maybe?

[Chris Henson]

The bullet can just be grind.

[Etienne Marion]

Ruben Van de Velde said:

Does fun_prop prove it if you write it with HasDeriv maybe?

HasDerivAt is not tagged with fun_prop.

[Etienne Marion]

Chris Henson said:

The bullet can just be grind.

Good catch! I am still not used to what grind can or cannot do. I edited my message accordingly.

[Christian Merten]

I think @Tomas Skrivan's data_synth tactic can compute derivatives (relevant thread: #mathlib4 > `data_synth` tactic for derivatives, bounds, compilation ... )

[Vasily Ilin]

Christian Merten said:

I think Tomas Skrivan's data_synth tactic can compute derivatives (relevant thread: #mathlib4 > `data_synth` tactic for derivatives, bounds, compilation ... )

Is it already in mathlib? Seems not, right?

[Vasily Ilin]

@Etienne Marion , I get

1 goal
t x : ℝ
ht : t > 0
⊢ -(2 * π * (fun x ↦ 1) t / (2 * √(2 * π * t))) / √(2 * π * t) ^ 2 * rexp (-x ^ 2 / (2 * t)) +
    (√(2 * π * t))⁻¹ * (rexp (-x ^ 2 / (2 * t)) * ((0 * (2 * t) - -x ^ 2 * (2 * (fun x ↦ 1) t)) / (2 * t) ^ 2)) =
  (√(2 * π * t))⁻¹ * rexp (-x ^ 2 / (2 * t)) * (-1 / t + x ^ 2 / t ^ 2) / 2
`grind` failed
case grind.2.2.2.2.2.2.2.1
t x : ℝ
ht : 0 < t
h : ¬-(2 * π * 1 * (2 * √(2 * π * t))⁻¹) * (√(2 * π * t) ^ 2)⁻¹ * rexp (-x ^ 2 * (2 * t)⁻¹) +
      (√(2 * π * t))⁻¹ * (rexp (-x ^ 2 * (2 * t)⁻¹) * ((0 * (2 * t) - -x ^ 2 * (2 * 1)) * ((2 * t) ^ 2)⁻¹)) =
    (√(2 * π * t))⁻¹ * rexp (-x ^ 2 * (2 * t)⁻¹) * (-1 * t⁻¹ + x ^ 2 * (t ^ 2)⁻¹) * 2⁻¹
h_1 : ¬2 * √(2 * π * t) = 0
h_2 : ¬√(2 * π * t) ^ 2 = 0
h_3 : ¬2 * t = 0
h_4 : ¬√(2 * π * t) = 0
h_5 : ¬(2 * t) ^ 2 = 0
h_6 : ¬t = 0
h_7 : ¬t ^ 2 = 0
h_8 : 2 * t = 2 * √(2 * π * t)
⊢ False

for grind.

[Etienne Marion]

@Vasily Ilin The code I posted works in the web editor, maybe your mathlib is not up to date.

[Etienne Marion]

To be more precise, it works on latest Mathlib (4.24.0-rc1) but fails on stable Mathlib (4.23.0).

[Eric Wieser]

Here's another manual proof:

lemma deriv_g_t {x t : ℝ} (ht : t > 0) : deriv (fun t => g t x) t = (g t x) * (-1/t + x^2/t^2) / 2 := by
  have : HasDerivAt  (fun t => g t x) _ t
  · simp_rw [g]
    apply HasDerivAt.fun_mul
    · apply_rules [HasDerivAt.fun_inv, HasDerivAt.sqrt, HasDerivAt.const_mul, hasDerivAt_id]
      all_goals positivity
    · apply_rules [HasDerivAt.exp, HasDerivAt.fun_inv, HasDerivAt.const_mul, hasDerivAt_id]
      all_goals positivity
  convert this.deriv using 1
  simp_rw [g]
  grind

[Eric Wieser]

Note this one also computes the derivative for you