OrderedCancelCommMonoid extends

Stream: mathlib4

[Martin Dvořák]

We have (Algebra/Order/Monoid/Defs):

/-- An ordered commutative monoid is a commutative monoid
with a partial order such that `a ≤ b → c * a ≤ c * b` (multiplication is monotone)
-/
class OrderedCommMonoid (α : Type*) extends CommMonoid α, PartialOrder α where
  /-- Multiplication is monotone in an `OrderedCommMonoid`. -/
  protected mul_le_mul_left : ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b

And we have (Algebra/Order/Monoid/Cancel/Defs):

/-- An ordered cancellative commutative monoid
is a commutative monoid with a partial order,
in which multiplication is cancellative and monotone. -/
class OrderedCancelCommMonoid (α : Type u) extends CommMonoid α, PartialOrder α where
  /-- Multiplication is monotone in an ordered cancellative commutative monoid. -/
  protected mul_le_mul_left : ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b
  /-- Cancellation is compatible with the order in an ordered cancellative commutative monoid. -/
  protected le_of_mul_le_mul_left : ∀ a b c : α, a * b ≤ a * c → b ≤ c

Why isn't OrderedCancelCommMonoid defined extending OrderedCommMonoid instead of those two classes?

[Yaël Dillies]

This is probably an artifact of Scott's pre-port splitting.

[Yaël Dillies]

#8170

[Martin Dvořák]

What the heck do these errors mean?

Error: ./././Mathlib/Algebra/Order/Ring/InjSurj.lean:118:2: error: type mismatch
  StrictOrderedSemiring.add_le_add_left
has type
  ∀ (a b : β), a ≤ b → ∀ (c : β), c + a ≤ c + b : Prop
but is expected to have type
  ∀ (a b : β), a ≤ b → ∀ (c : β), c + a ≤ c + b : Prop
Error: ./././Mathlib/Algebra/Order/Ring/InjSurj.lean:132:2: error: type mismatch
  Ring.sub_eq_add_neg
has type
  ∀ (a b : β), a - b = a + -b : Prop
but is expected to have type
  ∀ (a b : β), a - b = a + -b : Prop
Error: ./././Mathlib/Algebra/Order/Ring/InjSurj.lean:150:2: error: type mismatch
  CommRing.mul_comm
has type
  ∀ (a b : β), a * b = b * a : Prop
but is expected to have type
  ∀ (a b : β), a * b = b * a : Prop
Error: ./././Mathlib/Algebra/Order/Ring/InjSurj.lean:164:2: error: type mismatch
  StrictOrderedSemiring.add_le_add_left
has type
  ∀ (a b : β), a ≤ b → ∀ (c : β), c + a ≤ c + b : Prop
but is expected to have type
  ∀ (a b : β), a ≤ b → ∀ (c : β), c + a ≤ c + b : Prop
Error: ./././Mathlib/Algebra/Order/Ring/InjSurj.lean:178:2: error: type mismatch
  StrictOrderedCommSemiring.mul_comm
has type
  ∀ (a b : β), a * b = b * a : Prop
but is expected to have type
  ∀ (a b : β), a * b = b * a : Prop
Error: ./././Mathlib/Algebra/Order/Ring/InjSurj.lean:194:2: error: type mismatch
  StrictOrderedRing.add_le_add_left
has type
  ∀ (a b : β), a ≤ b → ∀ (c : β), c + a ≤ c + b : Prop
but is expected to have type
  ∀ (a b : β), a ≤ b → ∀ (c : β), c + a ≤ c + b : Prop
Error: ./././Mathlib/Algebra/Order/Ring/InjSurj.lean:210:2: error: type mismatch
  LinearOrder.le_total
has type
  ∀ (a b : β), a ≤ b ∨ b ≤ a : Prop
but is expected to have type
  ∀ (a b : β), a ≤ b ∨ b ≤ a : Prop

[Alex J. Best]

I think you would have to open those files in vscode to see what the difference is, probably some overlapping instances being introduced on the same type somewhere

[Martin Dvořák]

I can see the PR compiles now!
:tada:
Thank you @Yaël Dillies very much!

[Yaël Dillies]

Yaël Dillies said:

This is probably an artifact of Scott's pre-port splitting.

To explain, @Scott Morrison you scattered the definitions of ordered monoids across three files, and at some pointOrderedCancelCommMonoid was not even importing OrderedCommMonoid anymore! I fixed that, because it led to weird TC failures, but didn't make them extend one another again.

[Martin Dvořák]

Can I mark your PR with "awaiting review" please? I would like to get it through soon!

[Yaël Dillies]

Whoops sorry that was an accident.

[Martin Dvořák]

Some time ago, there was a suggestion to define StrictOrderedCommMonoid.
It was supposed to be more general than OrderedCancelCommMonoid.
It turns out that, even though there are some examples of StrictOrderedCommMonoid that is not OrderedCancelCommMonoid at the same time, nobody cares about these weird structures.
As a conclusion, I think I will close #8158 and I will proceed with OrderedCancelCommMonoid instead.
Any objections to [not generalizing] it?

[Yaël Dillies]

No, I think that's fine.