## Stream: general

### Topic: cancel add + canonically ordered?

#### Peter Nelson (Apr 01 2021 at 12:22):

I'm trying to prove something about an ordered add_comm monoid which is both canonically ordered and has additive cancellation. But when I include both instances as hypotheses, it seems like lean is getting confused about which zero and which has_le.leI mean. I'm not sure whether this is just some sort of diamond problem, or I am actually handling two unrelated structures on the same set.

For example, I get an error when I try to invoke the theorem zero_le from canonically_ordered_monoid; see below. It works fine if I remove the ordered_cancel_add_comm_monoid instance. Can someone advise me how to set things up so I have the set of assumptions from both instances on a common ordered_add_comm_monoid?

import tactic

example {M : Type*}
(x : M):
false :=
begin
have : 0 ≤ x := zero_le x,
-- fails, but works ok if the first instance is removed from hypotheses.
end


#### Peter Nelson (Apr 01 2021 at 12:24):

Here is the error in all its glory.

invalid type ascription, term has type
@has_le.le M
(@preorder.to_has_le M
(@partial_order.to_preorder M
0
x
but is expected to have type
@has_le.le M
(@preorder.to_has_le M (@partial_order.to_preorder M (@ordered_cancel_add_comm_monoid.to_partial_order M _inst_1)))
0
x


#### Kevin Buzzard (Apr 01 2021 at 12:24):

Yeah you're putting two unrelated monoid structures on M

#### Peter Nelson (Apr 01 2021 at 12:25):

I thought so - is there a way to take the union of both sets of axioms for these structures without doing this?

#### Kevin Buzzard (Apr 01 2021 at 12:26):

You either make a new typeclass with instances implying that it's both of the other typeclass, or just use one typeclass and add the extra axioms as assumptions and then make an instance of the other typeclass manually

#### Kevin Buzzard (Apr 01 2021 at 12:27):

Your error in all its glory just says "I have _inst_1 on the left hand side and _inst_2 on the right hand side and these are unrelated" (look at the end of each term on either side of the =)

#### Kevin Buzzard (Apr 01 2021 at 12:29):

Didn't we decide that one typeclass around here was a load of old nonsense recently?

#### Eric Wieser (Apr 01 2021 at 12:30):

was docs#ordered_semiring that nonsense?

#### Peter Nelson (Apr 01 2021 at 12:57):

What is the value of the extends that is used in defining various strengthenings of ordered_add_comm_monoid? Would this kind of problem not go away if canonically_ordered_add_monoid was defined like this:

class canonically_ordered_add_monoid (α : Type*) [ordered_add_comm_monoid α] [order_bot α] :=
(le_iff_exists_add : ∀ a b : α, a ≤ b ↔ ∃ c, b = a + c)


class canonically_ordered_add_monoid (α : Type*) extends ordered_add_comm_monoid α, order_bot α :=
(le_iff_exists_add : ∀ a b : α, a ≤ b ↔ ∃ c, b = a + c)


?

#### Peter Nelson (Apr 01 2021 at 13:00):

By way of comparison, in my one and only PR, I added a typeclass defined as follows:

class has_exists_add_of_le (α : Type u) [ordered_add_comm_monoid α] : Prop :=
(exists_add_of_le : ∀ {a b : α}, a ≤ b → ∃ (c : α), b = a + c)


and this allowed the instances to fire seamlessly in settings where we wanted some structure plus this one extra axiom. This made it through the PR process - is there some reason it should have been done the other way?

#### Peter Nelson (Apr 01 2021 at 13:01):

(using extends, I mean)

#### Peter Nelson (Apr 01 2021 at 13:08):

Is this because canonically_ordered_add_monoid is extending two different typeclasses?

#### Eric Wieser (Apr 01 2021 at 13:37):

I think there are two arguments against that approach

1. Something something exponential blowup of term length
2. People don't like writing [ordered_add_comm_monoid α] [order_bot α] [canonically_ordered_add_monoid α] in their lemma statements because it's long. A more extreme example would be [has_mul α] [has_one α] [mul_one_class α] [mul_assoc_class α] instead of [monoid α].

#### Greg Price (Apr 01 2021 at 16:52):

Eric Wieser said:

1. People don't like writing [ordered_add_comm_monoid α] [order_bot α] [canonically_ordered_add_monoid α] in their lemma statements because it's long. A more extreme example would be [has_mul α] [has_one α] [mul_one_class α] [mul_assoc_class α] instead of [monoid α].

Or to expand out what that approach might mean for a canonically ordered, cancellative, additive monoid: something like [has_add α] [has_zero α] [add_zero_class α] [add_assoc_class α] [add_comm_class α] [preorder α] [partial_order α] [ordered_add_comm_monoid α] [has_bot α] [order_bot α] [canonically_ordered_add_monoid α] [add_left_cancel_class α] [add_right_cancel_class α] [ordered_cancel_add_comm_monoid α].

#### Greg Price (Apr 01 2021 at 16:54):

I.e. that's what you get if not only is canonically_ordered_add_monoid defined like this:

class canonically_ordered_add_monoid (α : Type*) [ordered_add_comm_monoid α] [order_bot α] :=
(le_iff_exists_add : ∀ a b : α, a ≤ b ↔ ∃ c, b = a + c)


but also ordered_add_comm_monoid is defined in a similar way, and so on.

#### Eric Wieser (Apr 01 2021 at 17:06):

Right, exactly. Having said that, in lean 4 it's looking like you could define something like

class monoid extends has_mul α, has_one α, mul_one_class α, mul_assoc_class α

instance monoid.of_parts [p : has_mul α] [q : has_one α] [r : mul_one_class α] [s : mul_assoc_class α] : monoid α := {..p, ..q, ..r, ..s}


and it won't cause a loop, unlike lean 3. That means that you are free to switch back and forth between the shorthand names when you don't need to be precise, and the long list when you need something with no shorthand name

#### Greg Price (Apr 01 2021 at 17:36):

Here, I think it would mean you could write something like [add_comm_monoid α] [order_bot α] [is_canonically_ordered_add_monoid α] [is_ordered_cancel_add_comm_monoid α].

I.e. you'd rewrite a definition like the existing

class canonically_ordered_add_monoid (α : Type*) extends ordered_add_comm_monoid α, order_bot α :=
(le_iff_exists_add : ∀ a b : α, a ≤ b ↔ ∃ c, b = a + c)


to something like

class is_canonically_ordered_add_monoid (α : Type*) [ordered_add_comm_monoid α] [order_bot α] :=
(le_iff_exists_add : ∀ a b : α, a ≤ b ↔ ∃ c, b = a + c)


and similarly ordered_add_comm_monoid and so on.
And both the is_canonically_ordered_add_monoid and is_ordered_cancel_add_comm_monoid would end up using the common [add_comm_monoid α] and [order_bot α], and at the same time you'd get to invoke things that needed a [canonically_ordered_add_monoid α], because Lean would be able to produce the needed instance.