Stream: Is there code for X?

Topic: A typeclass for nat subtraction

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.

Johan Commelin (Feb 20 2021 at 17:31):

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

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

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

Mario Carneiro (Feb 20 2021 at 18:01):

We should call it monud :laughing:

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

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

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

Adam Topaz (Feb 20 2021 at 18:07):

Isn't there a pi.semiring instance?

Adam Topaz (Feb 20 2021 at 18:07):

Oh sorry, semiring doesn't have sub

Adam Topaz (Feb 20 2021 at 18:08):

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

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

Adam Topaz (Feb 20 2021 at 18:35):

Do we have docs#cancellative_semiring ?

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)

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

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)

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

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