differentiability tactic

Stream: new members

[Ines Wright]

Hi,

I'm experimenting with a differentiability tactic in Lean 3, based almost exactly on the continuity tactic which already exists in Mathlib. I have a reasonable understanding of programming with monads but am unfamiliar with the specifics of Lean's tactic library. I include attached my differentiability tactic and an example at the bottom of the file of it behaving in a way I didn't intend.
My tactic isn't quite doing what I want it to do- instead of repeatedly applying differentiable.comp, it's unfolding differentiable to differentiable_at and then getting stuck. I don't think I want it to do this unfolding at all.
I suspect, because differentiable is a def and continuous is a structure, that's why I'm having this problem with differentiable and not continuous. But differentiable_at is also a definition, so my first question is does anyone have any idea why the tactic is unfolding the definition of differentiable but not differentiable_at ? As far as I can tell, both are semireducible. What's making the distinction between the two that one gets unfolded and one doesn't?
My second question is why is this happening at all? The algorithm from continuity as far as I can tell uses tidy with the continuity tactic, which in turn uses chain, and I've examined both and can't figure out where the unfolding actually comes from. Does anyone know where this is?
And finally of course- how do I fix this? Is there something wrong with my tactic that I don't understand or is it a deeper problem? I'm writing this as part of a project for Kevin Buzzard's class, so if the only real fixes to something like this would be in theory 'make differentiable a structure', I'd be fine with some kind of hack solution that makes the tactic work only for this project.

Thanks for the help.

differentiability.lean

[Rémy Degenne]

I suspect (without reading your code, just from the description) that your issue is similar to one I had when I adapted continuity to write a measurability tactic. You need to prevent the tactic from using intros when the goal has the form differentiable .... See the goal_is_not_measurable def here : https://github.com/leanprover-community/mathlib/blob/master/src/measure_theory/tactic.lean

[Ines Wright]

@Rémy Degenne wonderful, you're right, this helped a lot. I have one or two further questions:
Why does your measurability tactic require the lines
propositional_goal >> tactic.interactive.apply_assumption none {use_exfalso := ff} >> pure "apply_assumption {use_exfalso := ff}",
in order to get it to apply hypothesis to the goal, when continuity doesn't need this? As I needed to add this into my own tactic.
I can now solve goals of the form (f \comp g), but not of the form (\lambda x, f x + g x). This is exactly of one of the lemmas I have tagged with the differentiability attribute. Do you have any idea why this might be the case?

[Rémy Degenne]

If I remember correctly, I added this apply_assumption line to be able to close sub-goals for which we have assumptions in the context, which is something that continuity did not try to do. Thus if I am right, the reason for that line is not that I needed a fix that continuity did not need, it is that I wanted to improve on continuity.

For you second question, I don't have a quick answer. I don't have time to read your code right now, but I'll have a look later.

[Rémy Degenne]

A quick guess: did you check that you could apply the lemma by hand, that no instance was missing? I had several cases of measurability not working because the file I was in did not import some instance about the real numbers.

[Ines Wright]

Ah no my mistake entirely it was a typo! I was looking for the attribute differentiable and not differentiability in apply_rules... I think everything works how I'm hoping now! Thanks so much for the help