Keefer Rowan (May 28 2020 at 14:32):
I think overloading abs for ordered group and complex numbers is causing issues. Here's an example:
import data.complex.basic open complex example (a : ℂ) : a.abs = abs (a.re) := sorry
ambiguous overload, possible interpretations abs a.re ↑(a.re).abs Additional information: c:\Users\keefe\OneDrive\Documents\Lean\mathlib\src\test.lean:4:26: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because it failed to disambiguate overload using the expected type ℝ the following overloaded terms were applicable abs abs
I'm not sure how to deal with this, as writing
example (a : ℂ) : a.abs = abs (a.re : ℝ) := sorry doesn't help. My best guess is it has to do type class inference for
ordered_group and for coercion to and they have the same priority, or something like that. I don't know how to work around (a suggestion on that would be helpful), but it also seems like this is a problem worth fixing in mathlib too. Perhaps renaming complex abs, making it protected, or changing priorities? Since complex abs is a norm, it seems like we should make it protected and then canonically use the norm notation outside of the
basic file. Thoughts?
Reid Barton (May 28 2020 at 14:34):
Not an expert on this part of mathlib, but all your suggestions sound reasonable. As a local workaround, you can use
open complex (hiding abs) which would simulate it being
Reid Barton (May 28 2020 at 14:35):
Oh, I overlooked "renaming complex abs"--I don't think that one sounds reasonable :upside_down:
Since dot notation
a.abs unambiguously gives you
complex.abs, making it protected should be pretty much strictly better.
Keefer Rowan (May 28 2020 at 14:35):
Ok, didn't know that dot notation works for protected so figured protecting was on equal footing with renaming. That's good to know!
Patrick Massot (May 28 2020 at 14:41):
The current mathlib handling of abs and norm is not optimal. We should probably study what the mathcomp people did. They explain it in https://hal.inria.fr/hal-02463336
Yury G. Kudryashov (May 29 2020 at 00:15):
Do we need
complex.abs Why not use
Last updated: May 14 2021 at 22:15 UTC