# Zulip Chat Archive

## 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.le`

I 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*}
[ordered_cancel_add_comm_monoid M]
[canonically_ordered_add_monoid M]
(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
(@ordered_add_comm_monoid.to_partial_order M
(@canonically_ordered_add_monoid.to_ordered_add_comm_monoid M _inst_2))))
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)
```

instead of this

```
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

- Something something exponential blowup of term length
- 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:

- 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):

That does sound helpful!

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)
class canonically_ordered_add_monoid (α : Type*) extends ordered_add_comm_monoid α, order_bot α, is_canonically_ordered_add_monoid α
instance canonically_ordered_add_monoid.of_parts (α : Type*) [p : ordered_add_comm_monoid α] [q : order_bot α] [r : is_canonically_ordered_add_monoid α] : canonically_ordered_add_monoid α := {..p, ..q, ..r}
```

and similarly `ordered_add_comm_monoid`

and so on.

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

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.

Last updated: May 15 2021 at 02:11 UTC