Simplifier behavior in computing derivatives

Stream: new members

[Keith Rush]

Hi all,

I'm poking around a bit with some basic complex analysis, and encountering some behavior which isn't quite mapping in my brain. The comments here led me to believe that the following example (inlined from lean live ) would work , but it does not. Can anyone give me any insight as to why not?

--Doesn't work; we have attempted to 'translate' the domain. I guess provable with composition + linear map.
--But why doesn't the simplifier know about it?
example (f: ℂ → ℂ) (z: ℂ) (hf: DifferentiableAt ℂ f z): DifferentiableAt ℂ (fun t: ℂ => f (z+t)) 0 := by
  --doesn't work, we get back 'simp made no progress'
  simp [hf]

[Yaël Dillies]

I don't think you can expect simp to work here because the lemma would need to be of the form DifferentiableAt ℂ (fun t ↦ f (z + t)) y ↔ DifferentiableAt ℂ (fun t ↦ f t) (z + y) and Lean would have a hard time applying this lemma since it would have to "unify" the function f, and higher order unification is undecidable.

[Yaël Dillies]

eg fun t ↦ (z + t) ^ 2 + (z + t) is of the form fun t ↦ f (z + t), but unification won't figure it out unless you tell it to try f := fun x ↦ x ^ 2 + x.

[Keith Rush]

I'm not sure I 100% grok, but will chase down what I can--what I get at the moment is effectively that there is a substitution which has to take place, and in the general case it may be difficult (OK, undecidable) to figure out if this substitution is valid or not. E.g. in your example it's clear that this variable rename / substitution is possible, but one can imagine an arbitrary rewrite of the terms which hides this possibility. I suppose this is why \alpha equivalence is natively supported (IIUC), but nothing else.

While I chase down my understanding here, perhaps a simpler example can help me on my way. AFAICT the first simp below works but the second doesn't, and it is beyond me at the moment to understand why:

--works
example (z: ℂ): DifferentiableAt ℂ (fun t: ℂ ↦ (t + z)) 0 := by simp

--doesn't work, simp made no progress
example (z: ℂ): DifferentiableAt ℂ (fun t: ℂ ↦ (z + t)) 0 := by simp

[Yaël Dillies]

Uh, interesting. What lemmas does the first one use? Maybe we're just missing another one.

[Keith Rush]

Using simp? yields for me:

example (z: ℂ) (u: ℂ): DifferentiableAt ℂ (fun t: ℂ ↦ (t + z)) u := by
 simp only [differentiableAt_id', differentiableAt_const, DifferentiableAt.add]

[Yaël Dillies]

Ah I know. It's because the other one beta reduces. Try simp (config := { beta := false })

[Keith Rush]

did a direct copy / paste to ensure im not getting the syntax wrong; im still getting simp made no progress. Confirming, this is what you're expecting me to try:

example (z: ℂ): DifferentiableAt ℂ (fun t: ℂ ↦ (z + t)) 0 := by
  simp (config := { beta := false })

[Yaël Dillies]

Sorry, eta, not beta

[Yaël Dillies]

Greek letters hard

[Keith Rush]

still nothing with

example (z: ℂ): DifferentiableAt ℂ (fun t: ℂ ↦ (z + t)) 0 := by
  simp (config := { eta := false })

Pulling things from the suggestions from simp? above, IIUC the following sequence closes the goal:

example (z: ℂ): DifferentiableAt ℂ (fun t: ℂ ↦ (z + t)) 0 := by
  apply DifferentiableAt.add
  apply differentiableAt_const
  apply differentiableAt_id
 ```
but im not sure if this is in any way helpful :smiley:

[Yaël Dillies]

What does the goal look like after the simp call?

[Keith Rush]

identical to before the call:

z: ℂ
⊢ DifferentiableAt ℂ (fun t => z + t) 0

if it's relevant, I'm on live.lean-lang.org for this, rather than a local install

[Keith Rush]

(also may be worth keeping in mind that i may be doing something _incredibly_ naive and dumb)

[Michael Stoll]

There are docs#HasDerivAt.comp_const_add and docs#HasDerivAt.comp_add_const, which might be helpful.
One could perhaps add iff versions; not sure if they would make good simp lemmas, though.