Incompatible subtraction on WithTop

Stream: mathlib4

[Daniel Weber]

docs#WithTop.linearOrderedAddCommGroupWithTop seems to be incompatible with docs#WithTop.instSub, which is quite confusing. Is this intentional, or should it be resolved somehow? How?
Example:

import Mathlib.Algebra.Order.Group.WithTop
import Mathlib.Algebra.Order.Sub.WithTop
import Mathlib.Algebra.Order.Group.Int

#eval @Sub.sub _ _ 0 (⊤ : WithTop ℤ)

#eval @Sub.sub _ LinearOrderedAddCommGroupWithTop.toSub 0 (⊤ : WithTop ℤ)

[Johan Commelin]

That seems bad. Afaict, it is not intentional.

[Johan Commelin]

I think the instSub should be changed into whatever the other instance needs.

[Daniel Weber]

I think instSub is intended mainly for the case that α is canonically ordered, perhaps that can just be added as an requirement to it?

[Johan Commelin]

Hmm, so you are saying that higher up in the hierarchy we need two genuinely different subtractions?

[Daniel Weber]

I'm not sure if it's actually used, but that seems to be the intention, yeah

[Johan Commelin]

Then I think instSub should become a defn, with a warning about this difference in its docstring

[Brendan Seamas Murphy]

Both instances seem suspicious to me. If I were to use WithTop (WithBot α) I would expect -⊤ = ⊥. Doesn't the existence of a LinearOrderedAddCommGroupWithTop make this impossible? I'm not sure how much of a headache refactoring this would cause for valuations

[Johan Commelin]

Good point, so we should make that instance a def as well. The whole API for valuations shouldn't need that instance. And we can use the general-instance-that-should-be-a-def to declare instances for special cases.

[Daniel Weber]

Brendan Seamas Murphy said:

Both instances seem suspicious to me. If I were to use WithTop (WithBot α) I would expect -⊤ = ⊥. Doesn't the existence of a LinearOrderedAddCommGroupWithTop make this impossible? I'm not sure how much of a headache refactoring this would cause for valuations

I'm not sure if this is problematic, as WithBot α isn't LinearOrderedAddCommGroup so this instance wouldn't apply.

[Brendan Seamas Murphy]

Oh, that's a fair point. I guess I'm still a little worried about having lemma statements floating around that involve two types of subtraction on the same type? It could get confusing to read. But maybe it's fine

[Ruben Van de Velde]

Do we need a WithTopBot?

[Sébastien Gouëzel]

I agree both instances are weird:

• In LinearOrderedAddCommGroupWithTop, we have -⊤ : = ⊤, but if would seem more natural to me to make it 0, because it's another natural junk value, which has the advantage of being smaller.
• In WithTop.instSub, if it happened that there was a bottom value then it would be more natural to set -⊤ equal to this bottom value.

Looking at the uses in Mathlib, I have the impression that the one in LinearOrderedAddCommGroupWithTop is maybe more natural, as it corresponds to the additivization of the usual 1/0 = 0 convention. So I also think that WithTop.instSub should become a definition to avoid the conflict (because we really want WithTop ℤ to be usable as a LinearOrderedAddCommGroupWithTop for valuation stuff).

[Sébastien Gouëzel]

Note that for EReal negation is defined by hand, probably to avoid this mess.

[Daniel Weber]

There is docs#WithTop.instNeg, it agrees with the LinearOrderedAddCommGroupWithTop

[Floris van Doorn]

Since both instances feel a bit unnatural, one option is to scope them both.

[Brendan Seamas Murphy]

Ruben Van de Velde said:

Do we need a WithTopBot?

I would be happy if we had that. We could even scope instances that behave like WithTop (WithBot α) vs WithBot (WithTop α)?

[Yaël Dillies]

It would be good if you un #xy ed by telling us what you want to do with the extended integers

[Daniel Weber]

I'm working with valuations, I want to construct an AddValuation K (WithTop ℤ) given (p : F) (hp : Prime p) [IsFractionRing F K]. I needed to prove

example : (0 : WithTop ℤ) - 1 = -1 := by
  convert (neg_eq_zero_sub ..).symm -- introduces `WithTop.instSub = SubNegMonoid.toSub`, which is false.

(I know how to prove this, rfl works, but in my use case instead of 0 there's a complicated expression and I want to change the goal to proving it's equal to 0)

[Sébastien Gouëzel]

I'm trying to remove the instance WithTop.instSub now.

[Richard Osborn]

Shouldn't WithTop.sub really be WithTop.hsub?
def WithTop.hsub [Sub α] : WithTop α → α → WithTop α

[Richard Osborn]

I think if the subtraction is order preserving, there shouldn't be any problems? (Although, I fully expect an edge case which will prove this wrong :big_smile: )

[Brendan Seamas Murphy]

(deleted)

[Brendan Seamas Murphy]

(sorry!)

[Sébastien Gouëzel]

Fixed in #13715. I keep the two instances, but make sure that they apply in disjoint situations by requiring a bottom element instead of a zero for the first instance.

[Johan Commelin]

@Sébastien Gouëzel Thanks for doing this!

[Daniel Weber]

I need to prove some lemmas about LinearOrderedAddCommGroupWithTop, and one of them is top_ne_zero, but it collides with existing docs#top_ne_zero when unscoped, and LinearOrderedAddCommGroupWithTop.top_ne_zero is really long. What's a good alternative name?