Zulip Chat Archive

Stream: general

Topic: subtraction in canonically_ordered_add_monoid


view this post on Zulip Floris van Doorn (Sep 20 2020 at 19:34):

We have a couple instances of canonically_ordered_add_monoid, like nat, enat, nnreal, ennreal, cardinal, multiset, and almost all of them have a has_sub instance, and lemmas about them. In that case a - b is always the minimal c such that a <= b + c.
I think we should just redefine canonically_ordered_add_monoid so that it extends has_sub, and try to prove as much as we can in full generality, to avoid duplication in every individual instance.
There might be things that depend on the linearity of the order, but I see that we recently got canonically_linear_ordered_add_monoid, so we can prove some lemmas for that class. Side note: canonically_linear_ordered_add_monoid is defined but has no instances. We should upgrade some canonically_ordered_add_monoid instances to it.

view this post on Zulip Reid Barton (Sep 21 2020 at 11:33):

I guess it might be worth considering at the same time whether it would be better to have a has_monus or something instead.
Didn't Lean 4 make some change in this area? I forget what it was though.

view this post on Zulip Kevin Buzzard (Sep 21 2020 at 11:53):

Is it called monus because Patrick and I moan about it?

view this post on Zulip Floris van Doorn (Sep 21 2020 at 16:02):

Previous discussions about monus where here:
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/37
https://github.com/leanprover-community/lean/pull/381
No consensus was reached, but there were proponents of the change and (more?) proponents of the status quo.

I think I'll make this change while still using has_sub.


Last updated: May 13 2021 at 23:16 UTC