is_absolute_value

Stream: general

[Eric Rodriguez]

I've just opened #16190, which tidies (a bit) the file with absolute values. However, theree is currently two ways of spelling this in mathlib; docs#absolute_value (bundled), and docs#is_absolute_value (unbundled). Do people see any reason we should keep the unbundled version around? It makes it harder to work with things like fun_like, for a start, and is not in the style of mathlib. Plus, the current way this is implemented is via code duplication - I tidied this a bit in this PR, but it's not perfect (there's lemma disparity between both versions in both naming and existence)

[Eric Rodriguez]

cc @Anne Baanen @Mario Carneiro who are listed as authors

[Anne Baanen]

Yeah, my intention was to replace the unbundled with the bundled version, or at least to prefer the bundled version in further developments.

[Eric Rodriguez]

I'm making a start on #16340; the diff mostly seems great to me, but one thing we get that's bad is that we need to use absolute_value.abs a lot more than abs now, which is unwieldy. I'm pretty much removing all the basic mapping lemmas from absolute_value, too, and delegating them to fun_like versions (the only one I'm undecided on is docs#is_absolute_value.map_div, which turns into docs#map_div₀)

[Eric Rodriguez]

Also, how can you set up simps to use the fun_like coercion? Currently I'm just creating simp lemmas manually :/

[Yaël Dillies]

Yes you can, but I don't know how to.

[Yaël Dillies]

Oh btw I'm adding some classes that are relevant to absolute_value in #16227 so we should coordinate the two PRs.

[Eric Rodriguez]

Sure, I'll try make it dependent; I may keep some of the dot notation around still, though, as it's a lot shorter than map_add_le_add for example.

[Eric Rodriguez]

the current approach I'm following is bundling and only then removing the class; #16347 is the first step for complex.abs.