Zulip Chat Archive

Stream: Is there code for X?

Topic: A typeclass for nat subtraction


view this post on Zulip Eric Wieser (Feb 20 2021 at 17:11):

It would be nice if fin 3 -> nat could inherit nat subtraction element wise, but there is no typeclass that axiomatizes nat subtraction, meaning that there are no lemmas that would automatically be applicable. docs#finsupp.nat_sub is something that could benefit from this.

view this post on Zulip Johan Commelin (Feb 20 2021 at 17:31):

You could still give pi-types an elementwise has_sub, right?

view this post on Zulip Eric Wieser (Feb 20 2021 at 17:59):

Yes, but it would be nice to show that a - 0 = a, a - a = 0, and 0 - a = 0 for the pi type too

view this post on Zulip Eric Wieser (Feb 20 2021 at 18:00):

And be able to use the same lemma name for those rewrites on both nat and pi-types-to-nat

view this post on Zulip Mario Carneiro (Feb 20 2021 at 18:01):

We should call it monud :laughing:

view this post on Zulip Eric Wieser (Feb 20 2021 at 18:02):

I guess I'm asking for two typeclasses, since the first two of those axioms are satisfied by add_group, but the latter diverges

view this post on Zulip Eric Wieser (Feb 20 2021 at 18:03):

So nat would implement saturated_sub, and both saturated_sub and add_group implement cancel_sub or something

view this post on Zulip Mario Carneiro (Feb 20 2021 at 18:04):

the first one seems like it should be an extension of add_cancel_monoid satisfying a + b - b = a

view this post on Zulip Adam Topaz (Feb 20 2021 at 18:07):

Isn't there a pi.semiring instance?

view this post on Zulip Adam Topaz (Feb 20 2021 at 18:07):

Oh sorry, semiring doesn't have sub

view this post on Zulip Adam Topaz (Feb 20 2021 at 18:08):

(yet another reason why no one should ever use nat sub...)

view this post on Zulip Eric Wieser (Feb 20 2021 at 18:27):

There are pi instances for most typeclasses - the issue is that there is no typeclass that nat subtraction satisfies, so pi instances can't inherit any lemmas about it

view this post on Zulip Adam Topaz (Feb 20 2021 at 18:35):

Do we have docs#cancellative_semiring ?

view this post on Zulip Adam Topaz (Feb 20 2021 at 18:36):

I guess not, but if we did you could define subtraction on such things similarly to nat subtraction (sending something to zero when it doesn't make sense)

view this post on Zulip Adam Topaz (Feb 20 2021 at 18:37):

Then define the ring-completion and prove that a cancellative semiring embeds in its ring completion, thereby generalizing a bunch of results about the interaction between nat and int

view this post on Zulip Kyle Miller (Feb 20 2021 at 18:38):

Here's some precedent https://en.wikipedia.org/wiki/Monus (the long version of @Mario Carneiro's suggested name might be comm_add_monoid_with_monus)

view this post on Zulip Kyle Miller (Feb 20 2021 at 18:41):

In this version, comm_add_monoid_with_monus starts with a comm_add_monoid whose addition operation defines a partial order, and then a - b is the least c that solves a <= b + c

view this post on Zulip Kyle Miller (Feb 20 2021 at 18:41):

I don't think this axiomatizes @Eric Wieser's original use case though.


Last updated: May 07 2021 at 18:19 UTC