Stream: general

Topic: deriv neg lemmas

Yaël Dillies (Sep 24 2021 at 10:41):

Why are docs#deriv_within.neg, docs#deriv.neg, docs#fderiv_within_neg, docs#fderiv_neg about (λ y, -f y) and not -f? Historical artifact?

Reid Barton (Sep 24 2021 at 10:44):

I think it is more useful in practice

Yaël Dillies (Sep 24 2021 at 10:46):

Hmm... right now I wanted to change deriv (-f) into -deriv f and had to use convert. Wouldn't call that useful.

Reid Barton (Sep 24 2021 at 10:47):

why did you have -f though

Reid Barton (Sep 24 2021 at 10:47):

The lemmas are designed to compute deriv of a lambda with a complicated body

Eric Wieser (Sep 24 2021 at 10:48):

You can use docs#pi.neg_def to rewrite

Yaël Dillies (Sep 24 2021 at 10:48):

That's just how it is. See the proof of docs#concave_on_of_deriv_antitone

Eric Wieser (Sep 24 2021 at 10:48):

Or at least, you should be able to... seems it's missing unlike docs#pi.add_def (edit: added in #9361)

Reid Barton (Sep 24 2021 at 10:49):

Well anyways "doesn't work for my specific use case" doesn't contradict "is more useful".

Yaël Dillies (Sep 24 2021 at 10:50):

Well I guess I can align.

Reid Barton (Sep 24 2021 at 10:50):

The same reason it doesn't work for you is the reason that your version wouldn't work for the intended purposes of deriv.neg

Reid Barton (Sep 24 2021 at 10:51):

of course, we could have both!

Reid Barton (Sep 24 2021 at 10:57):

If you want to compute deriv (\lam x, exp (- x^2)) or something, then after applying docs#deriv_exp, higher-order unification will leave you with deriv (\lam x, - x^2) so that's the form we want docs#deriv.neg to match

Yaël Dillies (Sep 24 2021 at 11:01):

Yeah okay. Thanks!

Last updated: Dec 20 2023 at 11:08 UTC