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

`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
```

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 (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]
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 (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