Should div_pow be simp

Stream: general

[Yaël Dillies]

Just noting that docs#div_pow is simp while docs#mul_pow isn't. Whichever one we prefer, we should make the same decision for both.

[Yaël Dillies]

According to Kyle's affine rule, they should not be simp since the RHS has more occurrences of the free n than the LHS.

[Kyle Miller]

I'm sure this isn't my rule, but generally you don't want simp lemmas that distribute because they can lead to exponential blowup. If you make sure general simp lemmas are "affine" (the logic version, not the algebra one) then you avoid this blowup.

[Kyle Miller]

div_pow seems suspect as a simp lemma: (a / b) ^ n = a ^ n / b ^ n

[Johan Commelin]

But we do have map_add : f (x + y) = f x + f y as a simp lemma, right? This goes against the "affine rule"...

[Johan Commelin]

But it does match closely with my intuitive was of "solving a problem by simplifying".

[Kyle Miller]

Yeah, docs#map_add is suspect too. I think it's usually harmless because most of the time f is close to being a constant, or at least it's not very complex.

[Kyle Miller]

Imagine though that f stands for some complicated expression and you try to do simp to f (x + y + z + w). You'd get a goal that has four copies of this complicated expression, which is likely not simpler than what you started with. Maybe if you're lucky f x, f y, etc. reduce in some nice way, but you can't count on that.

[Kyle Miller]

I'd be in favor of having a simp set for applying distribution lemmas (@[simp_distrib] or something?). There's a lot more we could be doing with curated simp sets that aren't good global simp lemmas.

[Johan Commelin]

It would also be interesting to test my intuition: what happens if we flip map_add and map_mul (and similar lemmas) around. Generally speaking, will mathlib as a whole become longer or shorter after such a refactor?

[Johan Commelin]

Maybe one reason that is in favour of the current setup: if you have hx : x \in ker f, then simp [hx] can make progress in the current setup, whereas it seems to get more complicated in the reverse scenario.

[Yaël Dillies]

Johan Commelin said:

It would also be interesting to test my intuition: what happens if we flip map_add and map_mul (and similar lemmas) around. Generally speaking, will mathlib as a whole become longer or shorter after such a refactor?

I think it just won't compile. Eg simp currently can prove f (x + 1) = f x + 1 when f is a ring_hom, but with your change it wouldn't.

[Johan Commelin]

[sorry, german train caused this post to have a delay] Of course, if you have h : x + y \in ker f then the reverse scenario would be better, but that just seems less likely to happen in practice, I think. (Yes, even more appeal to intuition.)

[Kyle Miller]

If we have a simp_distrib simp set, then simp [simp_distrib] would prove this.

There could also be f (x + 1) = f x + 1 and f (1 + x) = 1 + f x simp lemmas without falling afoul of the affine rule

[Eric Wieser]

That doesn't scale very well for things like f (x + 1 + x) which works just fine with the current set

[Kyle Miller]

What would you want that to simplify to? f x + 1 + f x?

Is that simpler? If f takes $f$ Exprs and x takes $x$ Exprs, then f (x + 1 + x) has on the order of $f+2x$ Exprs and f x + 1 + f x has on the order of $2f + 2x$, so your term has gotten bigger by $f$ Exprs.

[Kyle Miller]

It also scales perfectly well if you have an additional simp set that you invoke explicitly, like simp [simp_distrib]. (Because you just apply distribution, not because you have multitudinous ... + 1 + ... lemmas of course.)

[Eric Wieser]

I'm thinking about things like the tensor product where once you distribute everything you end up with terms like f (a ⊗ b) which almost always simplifies

[Eric Wieser]

I'd be somewhat more in favor of distrib being enabled by default but being able to use simp [-distrib] or similar to opt out