subtraction on natural numbers

Stream: maths

[Simon Hudon]

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]

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

[Mario Carneiro]

like so: ∸

[Simon Hudon]

Thanks! Is there a LaTeX command for that?

[Mario Carneiro]

wiki says \dot -

[Mario Carneiro]

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

[Simon Hudon]

Alright then

[Patrick Massot]

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]

Actually maybe using this symbol in Lean could make sense

[Patrick Massot]

It would help mathematicians notice this is not the right operation

[Kevin Buzzard]

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]

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

[Patrick Massot]

Yeah, this is not great either

[Patrick Massot]

Can we have both?

[Kevin Buzzard]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

I don't know

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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