Zulip Chat Archive

Stream: general

Topic: is_absolute_value


Eric Rodriguez (Aug 21 2022 at 21:32):

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 (Aug 21 2022 at 21:43):

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

Anne Baanen (Aug 22 2022 at 09:14):

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 (Sep 01 2022 at 03:01):

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 (Sep 01 2022 at 03:01):

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

Yaël Dillies (Sep 01 2022 at 06:48):

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

Yaël Dillies (Sep 01 2022 at 06:54):

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

Eric Rodriguez (Sep 01 2022 at 11:42):

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 (Sep 01 2022 at 20:14):

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


Last updated: Dec 20 2023 at 11:08 UTC