Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: Autogenerating `differentiable.exp` etc


view this post on Zulip Yury G. Kudryashov (Nov 06 2020 at 20:48):

I want to write a tactic (a command and/or an attribute) that will autogenerate lemmas like docs#differentiable.cexp from docs#complex.has_deriv_at_exp

view this post on Zulip Yury G. Kudryashov (Nov 06 2020 at 20:48):

Any hints will be very welcome.

view this post on Zulip Rob Lewis (Nov 06 2020 at 20:54):

What are the parameters here? Should it work when exp is changed to a different function? Or for the different differentiability statements below?

view this post on Zulip Rob Lewis (Nov 06 2020 at 20:56):

One possible example to follow is the is_poly attribute from the Witt vector project. You apply it to a theorem and it derives some related theorems in different forms, basically what you're looking for. https://github.com/leanprover-community/mathlib/blob/master/src/ring_theory/witt_vector/is_poly.lean#L444

view this post on Zulip Rob Lewis (Nov 06 2020 at 20:56):

It might not be a perfect comparison though.

view this post on Zulip Yury G. Kudryashov (Nov 06 2020 at 23:07):

Yes, it should work for different infinitely smooth functions. Ideally, it should also work with functions like log automatically adding ≠ 0 assumptions but this is not required for the first version of the attribute.


Last updated: May 09 2021 at 21:10 UTC