Tactic for differentiation

Stream: new members

[Duncan Skahan]

Is there a tactic for proving things like this?

import Mathlib

open Complex

theorem derivative (x : ℝ) : deriv (fun x : ℝ ↦ exp (π*I * x)) x = π*I * exp (π*I * x) := by
  sorry

[Ruben Van de Velde]

Not that I'm aware of. Here are two proofs you might take a look at:

import Mathlib

open Complex

-- First attempt
theorem derivative (x : ℝ) : deriv (fun x : ℝ ↦ exp (π*I * x)) x = π*I * exp (π*I * x) := by
  conv_rhs => rw [mul_comm]
  apply HasDerivAt.deriv
  apply HasDerivAt.cexp
  convert HasDerivAt.const_mul (π * I) ?_ using 1
  apply (mul_one _).symm
  apply HasDerivAt.ofReal_comp
  exact hasDerivAt_id' x

-- Golf: combine the HasDerivAt to what mathlib thinks the derivative is,
-- and then use simp to show that it agrees with the statement
theorem derivative' (x : ℝ) : deriv (fun x : ℝ ↦ exp (π*I * x)) x = π*I * exp (π*I * x) := by
  apply HasDerivAt.deriv
  convert hasDerivAt_id' x |>.ofReal_comp.const_mul (π * I) |>.cexp using 1
  simp [mul_comm]

[Luigi Massacci]

Eventually mathlib should get fun_trans from scilean but not yet : (

[Etienne Marion]

Isn’t fun_prop intended for that kind of goals? Though I am not sure it will work here because there are many lemmas which are not tagged

[Michael Rothgang]

Luigi Massacci said:

Eventually mathlib should get fun_trans from scilean but not yet : (

There was a PR for that in February: #10594
I don't know it's precise state (it's marked as "work in progress"), but I for one would be excited to have that tactic land. And I'm pretty sure I'm not alone in that regard. CC @Tomas Skrivan

[Tomas Skrivan]

You can prove this using simp once differentiability and deriv theorems are added for Complex.ofReal'

import Mathlib

open Complex

@[fun_prop]
theorem differentiable_complex_ofReal' : Differentiable ℝ (fun x : ℝ => (x : ℂ)) := by
  intro x
  apply (HasDerivAt.ofReal_comp _).differentiableAt (x:=x) (f':=1)
  exact hasDerivAt_id' x

@[simp]
theorem deriv_complex_ofReal' : deriv (fun x : ℝ => (x : ℂ)) = fun _ => 1 := by
  funext x
  apply HasDerivAt.deriv
  apply HasDerivAt.ofReal_comp
  exact hasDerivAt_id' x

theorem derivative (x : ℝ) : deriv (fun x : ℝ ↦ exp (π*I * x)) x = π*I * exp (π*I * x) := by
  simp (disch := fun_prop)
  ring

[Tomas Skrivan]

Michael Rothgang said:

Luigi Massacci said:

Eventually mathlib should get fun_trans from scilean but not yet : (

There was a PR for that in February: #10594
I don't know it's precise state (it's marked as "work in progress"), but I for one would be excited to have that tactic land. And I'm pretty sure I'm not alone in that regard. CC Tomas Skrivan

I definitely want to finish that PR at some point, not sure when though ...

[Eric Wieser]

@Tomas Skrivan, do you have any plans to implement a tactic that follows the derivative' proof that @Ruben Van de Velde provides above?

[Tomas Skrivan]

I have a prototype of a tactic that solves the goal HasFDeriv R f ?f'. It produces f' which is assigned to ?f' and a proof term for HasFDeriv R f f'. I call it gtrans right now, here is a test of it.

In general, it solves a goal of the form P x1... xn ?y1 ... ?ym where P is some proposition with n+m arguments and the last m arguments are considered as "output" and can be meta variables.

However, it suffers from all the same issues as simp for computing derivatives. Similar tricks as in fun_prop needs to be used to make it seriously useful.

[Tomas Skrivan]

That test file also has an experiment with HasDerivOn f ?f' ?S which tries to synthesize the set on which f is actually differentiable. There is no guarantee that the set is maximal in any sense, the idea is that it should return the largest set on which it is obviously differentiable.

[Tomas Skrivan]

Eric Wieser said:

Tomas Skrivan, do you have any plans to implement a tactic that follows the derivative' proof that Ruben Van de Velde provides above?

Is this what you had in mind?

[Eric Wieser]

Yes, that sounds great! I was worried about your other messages hinting at only supporting a deriv/Differentiable-based approach, which I think works less generally.