Zulip Chat Archive

Stream: general

Topic: Overloaded abs causing issues


view this post on Zulip 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

It throws:

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 C\mathbb{C} 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?

view this post on Zulip 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 protected.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (May 29 2020 at 00:15):

Do we need complex.abs Why not use has_norm?


Last updated: May 14 2021 at 22:15 UTC