Zulip Chat Archive

Stream: maths

Topic: subtraction on natural numbers


view this post on Zulip Simon Hudon (Apr 11 2018 at 02:15):

Is there a name and notation to distinguish between subtraction on natural numbers and subtraction on integers? This is for my dissertation rather than a Lean proof

view this post on Zulip Mario Carneiro (Apr 11 2018 at 02:37):

Subtraction on natural numbers is sometimes called "monus" and denoted with a subtraction sign with a dot over it, like the top half of an american division sign

view this post on Zulip Mario Carneiro (Apr 11 2018 at 02:38):

like so: ∸

view this post on Zulip Simon Hudon (Apr 11 2018 at 02:38):

Thanks! Is there a LaTeX command for that?

view this post on Zulip Mario Carneiro (Apr 11 2018 at 02:39):

wiki says \dot -

view this post on Zulip Mario Carneiro (Apr 11 2018 at 02:40):

you will probably have to play with spacing to get it to look nice

view this post on Zulip Simon Hudon (Apr 11 2018 at 02:40):

Alright then

view this post on Zulip Patrick Massot (Apr 11 2018 at 06:49):

Short answer: use unicode-math and type ∸
Long answer: if for some reason, you don't want to use unicode-math, use its documentation: http://mirrors.ctan.org/macros/latex/contrib/unicode-math/unimath-symbols.pdf search for "dot above" and get to page 17 where you see that ∸ is translated to \dotminus. The problem is that you need to find which package defines this (an information which is irrelevant if you go with unicode-math). Very quick google latex dotminus brings: https://tex.stackexchange.com/questions/360069/what-symbol-for-primitive-recursive-cutoff-minus

view this post on Zulip Patrick Massot (Apr 11 2018 at 06:50):

Actually maybe using this symbol in Lean could make sense

view this post on Zulip Patrick Massot (Apr 11 2018 at 06:50):

It would help mathematicians notice this is not the right operation

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 06:51):

I think there's an argument for using some sort of modification on all the total extensions of the usual functions as well ;-)

view this post on Zulip Mario Carneiro (Apr 11 2018 at 06:51):

It's a thought, but I'd hate to have to explain to newcomers why 3 - 2 = 1 doesn't work

view this post on Zulip Patrick Massot (Apr 11 2018 at 06:51):

Yeah, this is not great either

view this post on Zulip Patrick Massot (Apr 11 2018 at 06:51):

Can we have both?

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 06:51):

Yes but I have to explain why 2 - 3 gets evaluated as something wrong, which is worse

view this post on Zulip Patrick Massot (Apr 11 2018 at 06:52):

Like, the lib uses the funny symbol but users can still use -

view this post on Zulip Patrick Massot (Apr 11 2018 at 06:52):

And when they complain about 2 - 3 we tell them about ∸

view this post on Zulip Patrick Massot (Apr 11 2018 at 06:52):

I don't know

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 06:52):

I am not seriously advocating changes to - and /, however it was the realisation that I could think about them in this way which made me realise that the "make it total" system would not lead to contradictions.

view this post on Zulip Mario Carneiro (Apr 11 2018 at 06:52):

It's in core, so this isn't changing anyway

view this post on Zulip Mario Carneiro (Apr 11 2018 at 06:53):

this would break too much of the "programming" part of lean I think

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 06:53):

Maybe obscure unicode characters which look the same and can be redefined by users is the best option :-)

view this post on Zulip Mario Carneiro (Apr 11 2018 at 06:53):

it would be hard to support a separate notation without a separate constant, and that would then mess up simp lemmas and such

view this post on Zulip Mario Carneiro (Apr 11 2018 at 06:54):

It's plausible that you could make a local notation (for @has_sub.sub nat _) work

view this post on Zulip Mario Carneiro (Apr 11 2018 at 06:57):

My favorite way to reason about 2 - 3 is to consider that 2 - 3 : nat (since - is a binary op on nat) so it can't possibly be the "right" answer. Now just consider, what's the next best option?

view this post on Zulip Mario Carneiro (Apr 11 2018 at 06:58):

I think it suffices to just remind people that this isn't a partial function


Last updated: May 11 2021 at 15:12 UTC