Why are two simps needed here?

Stream: new members

[Terence Tao]

Why is one simp insufficient to prove this statement:

import Mathlib
import Mathlib.Tactic
import Mathlib.Analysis.SpecialFunctions.Pow.Real

example (a: ℝ) : Differentiable ℝ (fun (x:ℝ) ↦ (Real.exp x + a)) := by
    simp
    apply Differentiable.exp
    simp

Differentiable.exp is a simp lemma, so I would have thought simp would automatically invoke it.

[Alex J. Best]

docs#Differentiable.exp says that Differentiable ℝ fun x => Real.exp (f x) for all differentiable f, whereas your goal is Differentiable ℝ fun y => Real.exp y which doesnt have an f in so they are syntactically different. simp only does matching up to syntax, so it won't insert identity functions for instance, which is what we would want to happen implicitly here.
In this situation we normally make two lemmas for the library, like docs#Real.continuous_exp and docs#Continuous.exp one of which is compositional, and one which is just the statement about the literal exp function.

[Alex J. Best]

One thing you could do in this particular example is write

    simpa using Differentiable.exp (f := id)

but its hard to know that this would be needed without first writing the proof you wrote. Ideally we will at some point have a differentiability tactic that automates these proofs in the same way that we have continuity, but we don't have it yet.

[Mauricio Collares]

I don't necessarily recommend term mode proofs here, but to exemplify what Alex said about composability,

example (a: ℝ) : Differentiable ℝ (fun (x:ℝ) ↦ (Real.exp x + a)) := Real.differentiable_exp.add_const a

and

example (a: ℝ) : Differentiable ℝ (fun (x:ℝ) ↦ (Real.exp x + a)) := differentiable_id.exp.add_const a

both work (and the autocomplete is pretty good).

[Jireh Loreaux]

I believe the way to create the automation Alex is describing is to use aesop (Automated Extensible Search for Obvious Proofs), like so:

import Mathlib

open Real

attribute [aesop safe apply]
  Differentiable.add
  Differentiable.exp
  Real.differentiable_exp
  differentiable_id
  differentiable_const

example (a : ℝ) : Differentiable ℝ (fun x : ℝ ↦ exp x + a) := by aesop

aesop is new to Lean 4, and mathlib is not yet making use of it to its fullest extent. We are still learning some lessons about how to tag lemmas with aesop appropriately. I'm just adding this here to showcase that this kind of automation is possible, and lies in the relatively near future.

[Adomas Baliuka]

Should I request permission and PR the differentiability tactic which one gets from shamelessly copying continuity (it does basically what Jireh just showed)? I tried this out recently but the discussion about it died. There seemed to be some suboptimal things going on with continuity as well, so maybe one should wait. On the other hand, I'm not sure anyone is working on it (or if people are actually using continuity that much)...

[Alex J. Best]

YesI think you should definitely PR a differentiability tactic, that would be great!
I think these tactics are certainly useful enough to be worth writing (especially if the implementation with aesop is short)

[Adomas Baliuka]

Can I have PR-permissions then? GitHub username is "adomasbaliuka"

[Kyle Miller]

@Adomas Baliuka Invite sent!