## Stream: maths

### Topic: subtraction on natural numbers

#### 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

#### 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

like so: ∸

#### Simon Hudon (Apr 11 2018 at 02:38):

Thanks! Is there a LaTeX command for that?

#### Mario Carneiro (Apr 11 2018 at 02:39):

wiki says \dot -

#### Mario Carneiro (Apr 11 2018 at 02:40):

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

Alright then

#### 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

#### Patrick Massot (Apr 11 2018 at 06:50):

Actually maybe using this symbol in Lean could make sense

#### Patrick Massot (Apr 11 2018 at 06:50):

It would help mathematicians notice this is not the right operation

#### 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 ;-)

#### 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

#### Patrick Massot (Apr 11 2018 at 06:51):

Yeah, this is not great either

#### Patrick Massot (Apr 11 2018 at 06:51):

Can we have both?

#### 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

#### Patrick Massot (Apr 11 2018 at 06:52):

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

#### Patrick Massot (Apr 11 2018 at 06:52):

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

I don't know

#### 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.

#### Mario Carneiro (Apr 11 2018 at 06:52):

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

#### Mario Carneiro (Apr 11 2018 at 06:53):

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

#### 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 :-)

#### 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

#### Mario Carneiro (Apr 11 2018 at 06:54):

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

#### 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?

#### 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