Fully qualify a shadowed name

Stream: general

[Patrick Stevens]

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]

Try _root_.add_lt_add_iff_left

[Yaël Dillies]

Why is docs#real.add_lt_add_iff_left even a thing?

[Reid Barton]

because it's used in the ordered_comm_ring instance--but it should be protected

[Yaël Dillies]

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

[Reid Barton]

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

[Yaël Dillies]

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]

Sometimes a lemma is just a lemma.

[Reid Barton]

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

[Reid Barton]

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]

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]

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]

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]

I think performance considerations can make inlining a bad idea

[Eric Wieser]

But you could make the lemma private

[Yaël Dillies]

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

[Eric Wieser]

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

[Reid Barton]

Huh?

[Reid Barton]

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]

(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]

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