# Zulip Chat Archive

## Stream: general

### Topic: Fully qualify a shadowed name

#### Patrick Stevens (Apr 28 2022 at 17:19):

I'm just missing a silly bit of syntax here, but I'm having trouble in `data.real.sqrt`

because its import, `data.real.basic`

, defines `add_lt_add_iff_left`

which shadows the generic one (which is there in `mul`

form as `mul_lt_mul_iff_left`

) from `algebra.order.monoid_lemmas`

; so I can't work out how to use the rational version. How can I either exclude the one from `data.real.basic`

, or fully-qualify the one from `algebra.order.monoid_lemmas`

? E.g. I can't `apply algebra.order.monoid_lemmas.add_lt_add_iff_left`

because "unknown identifier `algebra.order`

".

#### Patrick Johnson (Apr 28 2022 at 17:42):

Try `_root_.add_lt_add_iff_left`

#### Yaël Dillies (Apr 28 2022 at 17:50):

Why is docs#real.add_lt_add_iff_left even a thing?

#### Reid Barton (Apr 28 2022 at 17:56):

because it's used in the `ordered_comm_ring`

instance--but it should be `protected`

#### Yaël Dillies (Apr 28 2022 at 18:00):

But it's only used once, so it should be inlined.

#### Reid Barton (Apr 28 2022 at 18:02):

(I mean maybe in this case, but not as a general principle)

#### Yaël Dillies (Apr 28 2022 at 18:04):

To be clear, such type-specific lemmas do exist, but only when they are not a special case of the general lemma. For example, docs#ennreal.add_lt_add or (maybe more visibly) docs#ennreal.add_lt_add_of_lt_of_le

#### Reid Barton (Apr 28 2022 at 18:04):

Sometimes a lemma is just a lemma.

#### Reid Barton (Apr 28 2022 at 18:04):

In fact, in math, it would be true most of the time.

#### Reid Barton (Apr 28 2022 at 18:31):

Like if the proof of the lemma was 50 lines and then the instance (using the lemma) was another 50 lines, it definitely wouldn't be sensible to inline the lemma just because the lemma can be deduced from the instance (as is often the case with lemmas).

#### Reid Barton (Apr 28 2022 at 18:32):

Personally, I think it's also nice to separate the bits that are dependent on the definition of the real numbers (like the lemma here) from the admistrative business of building instances, but that's not such a big deal (and I'm sure it is not being done consistently).

#### Eric Rodriguez (Apr 28 2022 at 18:34):

I feel like I'd even inline the 50-line long lemma, personally. To me, if a lemma comes from an instance, that's an instant area of possible generalisation.

#### Reid Barton (Apr 28 2022 at 18:40):

Eric Rodriguez said:

To me, if a lemma comes from an instance, that's an instant area of possible generalisation.

I don't understand what this means

#### Eric Wieser (Apr 28 2022 at 18:40):

I think performance considerations can make inlining a bad idea

#### Eric Wieser (Apr 28 2022 at 18:40):

But you could make the lemma private

#### Yaël Dillies (Apr 28 2022 at 18:41):

Having a specific lemma for a type is to me a big red flag for "Generalization here is hard".

#### Eric Wieser (Apr 28 2022 at 18:42):

(sometimes it's just hard for the unifier / instance resolution, not the mathematician; but those cases should have a docstring to clarify)

#### Reid Barton (Apr 28 2022 at 18:46):

Huh?

#### Reid Barton (Apr 28 2022 at 18:49):

Anyways I don't think whatever that is about is important--

In both programming and ordinary math, it's very common and generally good style to have top-level functions/lemmas that get used only once. Maybe in programming the function would not be part of the "public API", a concept which basically doesn't exist in Lean (and isn't really needed in informal math).

#### Eric Wieser (Apr 28 2022 at 19:00):

(my comment was regarding docs#smul_eq_mul vs docs#algebra.id.smul_eq_mul vs yet another `smul_eq_mul`

in a recent PR)

#### Reid Barton (Apr 28 2022 at 19:00):

Eric Rodriguez said:

if a lemma comes from an instance, that's an instant area of possible generalisation.

I think we must not be discussing the same kind of situation--here there is lemma which is going to be **used** to prove that the reals form an ordered ring (or whatever); and so, naturally, the lemma is also a general statement about ordered rings specialized to the reals--but you can't prove it that way in the first place, of course

Last updated: Dec 20 2023 at 11:08 UTC