cancel add + canonically ordered?

Stream: general

[Peter Nelson]

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*}
[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]

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]

Yeah you're putting two unrelated monoid structures on M

[Peter Nelson]

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

[Kevin Buzzard]

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]

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]

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

[Eric Wieser]

was docs#ordered_semiring that nonsense?

[Peter Nelson]

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]

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]

(using extends, I mean)

[Peter Nelson]

Is this because canonically_ordered_add_monoid is extending two different typeclasses?

[Eric Wieser]

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]

Eric Wieser said:

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 α].

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]

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]

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]

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]

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.