Stream: general

Topic: differentiability tactic

James Arthur (Mar 06 2021 at 10:42):

I created an adapted version of the continuity tactic for differentiable_at type goals, which is here: https://gist.github.com/jamesa9283/400a021c9fc6d3c862914ca7c1d0dace
and @Shing Tak Lam and I were talking about implementing similar things for measurability and integrability and talk of a more general analysis tactic to do all of these arose, is this a good idea? I feel it would be useful as I find the differentiability and continuity useful on their own so one that does all would be amazing in my opinion and I don't want to create three copies of basically the same thing.

simp {discharger := differentiability} also solves deriv goals, as probably expected.

Hanting Zhang (Mar 07 2021 at 02:08):

I think this is a good idea. In fact I wanted to do it but got scared at the prospect of writing tactics. :upside_down: I've run into places where I want to prove something is integrable and end up writing apply continuous.integrable, continuity or apply integrable.integrable_on, apply continuous.integrable, continuity, etc, a bunch of times.

Benjamin Davidson (Mar 07 2021 at 02:12):

I was thinking about this the other day. I don't know anything about tactics other than how to use them but I think some sort of integrability tactic would be great!

Bryan Gin-ge Chen (Mar 07 2021 at 02:16):

@James Arthur If you find the tactic useful, go ahead and make a PR! (You should add some tests in your PR as well, cf. the continuity tests.)

James Arthur (Mar 07 2021 at 08:00):

So I should PR differentiability on its own? Or develop a more general analysis tactic and then PR?

Scott Morrison (Mar 08 2021 at 05:09):

The tactic itself doesn't seem to have anything to do with analysis!

Scott Morrison (Mar 08 2021 at 05:09):

It would definitely be good to have a generalization.

Last updated: May 13 2021 at 18:26 UTC