Zulip Chat Archive

Stream: new members

Topic: Why are two simps needed here?

Terence Tao (Oct 20 2023 at 16:10):

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
    apply Differentiable.exp

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

Alex J. Best (Oct 20 2023 at 16:35):

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 (Oct 20 2023 at 16:40):

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 (Oct 20 2023 at 16:42):

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


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 (Oct 20 2023 at 17:17):

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]

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 (Oct 21 2023 at 22:39):

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 (Oct 21 2023 at 22:46):

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 (Oct 22 2023 at 16:27):

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

Kyle Miller (Oct 22 2023 at 16:36):

@Adomas Baliuka Invite sent!

Last updated: Dec 20 2023 at 11:08 UTC