Should deriv_mul really be simp?

Stream: mathlib4

[Michael Rothgang]

I just checked:

• docs#deriv_mul is marked simp, but docs#fderiv_mul is not
• docs#deriv_comp, docs#fderiv_comp and docs#mfderiv_comp are not simp

Should deriv_mul really be marked simp?

[Michael Rothgang]

This was pointed out at the SLMath/ICARM workshop, and I just discovered that fderiv and deriv are not consistent here.

[Yury G. Kudryashov]

Some time ago, there was an effort to make simp compute derivatives using lemmas like deriv_mul.

[Kenny Lau]

I think we should use aesop instead of simp here

[Yury G. Kudryashov]

What aesop features are useful in this context?

[Yury G. Kudryashov]

I think that a better approach is to use something like fun_prop machinery to construct a HasDerivAt predicate, then get deriv from there. This way we don't need to repeat DifferentiableAt proofs over and over.

[Michael Rothgang]

Indeed, the right fix would be to get @Tomas Skrivan's data_synth tactic into mathlib. (I'll be very excited when that happens!!)

[Tomas Skrivan]

Yeah sorry I have not done that yet. I'm still struggling as I don't want to duplicate too much code between SciLean and Mathlib, but for SciLean I constantly need to adjust performance of data_synth as it needs to handle large expressions.

For the purpose of mathlib I think I will just extend fun_prop to properly handle meta variables in the goal like in HasFDeriv R f ?f x.

But do not expect anything too soon, I started a new job few weeks ago so I don't have much time for Lean any more.

[Yury G. Kudryashov]

Good luck at your new job! Are you looking for volunteers to port data_synth to Mathlib?

[Tomas Skrivan]

I think I have to do it myself. There is lots of experimental code that needs to be gutted and there are still some crucial things missing.