bad instance for ordered add comm monoids?

Stream: mathlib4

[Jireh Loreaux]

@Mario Carneiro docs#StrictOrderedSemiring.to_charZero generalizes to:

instance (priority := 50) AddMonoidWithOne.instCharZero [AddMonoidWithOne α]
  [NeZero (1 : α)] [PartialOrder α] [CovariantClass α α (· + ·) (· < ·)] [ZeroLEOneClass α] :
    CharZero α where
  cast_injective := StrictMono.injective <| strictMono_nat_of_lt_succ fun n => by
    rw [Nat.cast_succ]
    apply lt_add_one

Is there an obvious reason that this should cause timeouts for the ring tactic? I mean, I realize I'm replacing just the one instance StrictOrderedSemiring α with a collection of 5 instances, so maybe it's just that? But perhaps you have added insight.

This generalization isn't totally insane by the way: it's essentially a StrictOrderedAddCommMonoidWithOne (that doesn't exist, but it could) where 0 ≠ 1. This is satisfied by nontrivial star ordered rings (and their subtypes of selfadjoint and positive elements).

[Jireh Loreaux]

This is causing me headaches in #4871.

[Yaël Dillies]

I don't think we should be using ZeroLEOneClass. Can you try defining StrictOrderedAddCommMonoidWithOne?

[Jireh Loreaux]

Yaël, my hesitation with that is we only have two examples at the moment: star ordered rings and ordered rings.

[Jireh Loreaux]

Seems like not enough to justify this addition to the algebra-order hierarchy.

[Yaël Dillies]

Ordered semirings, you mean? ℕ certainly is one.

[Jireh Loreaux]

Sure, ℕ is an ordered semiring, but that's the point: it satisfies the stronger condition. My question is: what examples do we have of ordered add comm monoids with one besides star ordered semirings and ordered semirings? If we have no other examples, is that enough to justfiy adding this concept?

[Yaël Dillies]

Strictly ordered add comm monoids with one, you mean? Sorry for being picky, but there are many classes around this area of the library.

[Yaël Dillies]

I think it's enough to justify adding this concept, yes

[Jireh Loreaux]

@Yaël Dillies I just opened #6310, but there are some issues which I am currently trying to sort out. Sorry for not being precise, let me try to be more so:

1. OrderedAddCommMonoidWithOne = AddCommMonoidWithOne + PartialOrder + CovariantClass (+) (≤) + 0 ≤ 1
2. OrderedAddCommGroupWithOne = AddCommGroupWithOne + PartialOrder + CovariantClass (+) (≤) + 0 ≤ 1

These classes are provided in the PR, and are satisfied by OrderedSemiring, OrderedRing, respectively, as well as StarOrderedRing R (where the underlying ring is a Semiring, or Ring, respectively), and even the subtypes selfAdjoint R and {x : R // 0 ≤ x}.

3. OrderedAddCommMonoidWithOne + CovariantClass (+) (<) + NeZero 1 suffices to establish the conclusion of docs#StrictOrderedSemiring.to_charZero.

One might call the thing listed in (3) above a StrictOrderedAddCommMonoidWithOne, but I have not defined that class.