abs_mul simp

Stream: mathlib4

[Violeta Hernández]

Is there a reason why docs#abs_mul isn't tagged as simp?

[Kenny Lau]

maybe you don't always want to simp it?

[Violeta Hernández]

Well, what kind of circumstances lead to that?

[Violeta Hernández]

I feel like f (g a b) = g (h a) (h b) is the quintessential form of a simp lemma, think e.g. docs#Nat.cast_add or docs#Nat.cast_mul

[Violeta Hernández]

So I don't get why we're excluding this one

[Ruben Van de Velde]

It may also be oversight, not sure

[Violeta Hernández]

I'll add the attribute and see if anything breaks

[Ruben Van de Velde]

Worth a try

[Kenny Lau]

Violeta Hernández said:

I feel like f (g a b) = g (h a) (h b) is the quintessential form of a simp lemma, think e.g. docs#Nat.cast_add or docs#Nat.cast_mul

i'm talking about abs in particular

[Kenny Lau]

I can't recall an example

[Violeta Hernández]

Well yeah, my point is I don't see anything specific about abs that'd make this attribute undesirable

[Ruben Van de Velde]

Do we have |a * a| = a * a as simp?

[Violeta Hernández]

docs#abs_sq

[Ruben Van de Velde]

Or |a| * |a| = a * a

[Violeta Hernández]

We don't, huh

[Violeta Hernández]

Oh nvm, docs#abs_mul_abs_self and docs#abs_mul_self are both simp

[Violeta Hernández]

I think for abs_sq the reason is that docs#abs_pow would conflict with it

[Violeta Hernández]

(on that note, it's odd we have both docs#abs_pow and docs#pow_abs)

[Violeta Hernández]

#28176 :fingers_crossed:

[Violeta Hernández]

Yeah, seems to build just fine, modulo simp warnings.

[Violeta Hernández]

On the topic of abs. Shouldn't docs#abs_by_cases be named abs_rec to match docs#max_rec ?