deriv neg lemmas

Stream: general

[Yaël Dillies]

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]

I think it is more useful in practice

[Yaël Dillies]

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

[Reid Barton]

why did you have -f though

[Reid Barton]

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

[Eric Wieser]

You can use docs#pi.neg_def to rewrite

[Yaël Dillies]

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

[Eric Wieser]

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

[Reid Barton]

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

[Yaël Dillies]

Well I guess I can align.

[Reid Barton]

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]

of course, we could have both!

[Reid Barton]

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]

Yeah okay. Thanks!