A typeclass for nat subtraction

Stream: Is there code for X?

[Eric Wieser]

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]

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

[Eric Wieser]

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]

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

[Mario Carneiro]

We should call it monud :laughing:

[Eric Wieser]

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]

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

[Mario Carneiro]

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

[Adam Topaz]

Isn't there a pi.semiring instance?

[Adam Topaz]

Oh sorry, semiring doesn't have sub

[Adam Topaz]

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

[Eric Wieser]

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]

Do we have docs#cancellative_semiring ?

[Adam Topaz]

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]

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]

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]

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]

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