n+

Stream: general

[Kevin Buzzard]

Is it possible to have suffix notation n+ for Nat.succ n, like we have -n for integers?

[Kevin Buzzard]

I've heard it's big in computer science

[Adam Topaz]

Really?

[Adam Topaz]

What is -n supposed to be?

[Kevin Buzzard]

or is it a++? -n is neg n, right?

[Adam Topaz]

Oh ok yeah n++ is a thing.

[Kevin Buzzard]

it's suffix notation for succ, right?

[Adam Topaz]

Yeah I would hope that -n is neg n,

[Kevin Buzzard]

And now how do you name a + d+ = (a + d)+? :-/

[Kevin Buzzard]

wait maybe this doesn't fly for some reason I don't understand.

[Kevin Buzzard]

add_succ_eq_add_succ' is not a good look

[Adam Topaz]

It would be notation for succ, so it should follow the standard naming convention as if it was just the function being applied

[Kevin Buzzard]

Maybe prefix ++a notation is less confusing for beginners.

[Kevin Buzzard]

Oh I'm wrong, a + d+ = (a + d)+ is just called add_plus`

[Kevin Buzzard]

it's fine. I'm wondering whether I could change the name of the constructor to plus and try this n+ or +n notation to see if it's easier or harder.

[Adam Topaz]

FWIW, I do think it would be nice to have some programmy notations like n++, n += 37,etc. (especially if/when they make sense in a do block)

[Eric Rodriguez]

These notations traditionally increment n, so I think using them for succ would be confusing

[Mario Carneiro]

Notations I have seen for the successor function include: n', S(n) or S n, suc n, succ n, n+1. n+ is a new one to me

[Kevin Buzzard]

Oh maybe if n++ and ++n are misleading then n+ might be worth experimenting with? Like A+ is better than an A. Or do people think this is crazy? I know succ is traditional but I've never liked it; it gets giggles in schoolrooms and so when I'm building the naturals from scratch in front of an audience I always use S now. Yesterday when experimenting with new NNG worlds I found myself writing succ this which I didn't think was a good look, this was what sent me off on this postfix idea.

[Julian Berman]

There is also n⁺ to just mention another existing unicode character.

[Eric Wieser]

I think we might already use that notation for docs#PosPart

[Eric Wieser]

n⁺¹ seems slightly less crazy than n+, which makes n.succ.succ.succ n⁺¹⁺¹⁺¹

[Eric Wieser]

Of course this is still crazy, because (1⁺¹⁻¹ : Rat) is now 0.5 if we're not careful

[D. J. Bernstein]

How about spelling out successor, and encapsulating all the successor n theorems as n+1 theorems as soon as addition is defined, so that about 0% of users ever have to see the successor notation?

[Eric Wieser]

One place the name is really hard to avoid is induction n with | succ n := sorry

[Eric Wieser]

I don't think notation is legal there

[Eric Wieser]

Oh, and of course in all the theorem names!

[Eric Rodriguez]

In Lean3 we could do (n+1) := ... - does this not work in Lean4?

[Eric Wieser]

For match, yes; but the with clause on induction and cases matches goal names not expressions

[Kevin Buzzard]

In NNG we have the option to hack the induction tactic so that it gives n + 1 as the successor case; it's already hacked so that it gives 0 rather than MyNat.zero as the base case.

[Pedro Sánchez Terraf]

Julian Berman said:

There is also n⁺ to just mention another existing unicode character.

This one is also used (in the context of Cardinal) for Order.succ in the literature, and also for other sorts of set-theoretical successors.

[Eric Wieser]

Kevin Buzzard said:

In NNG we have the option to hack the induction tactic so that it gives n + 1 as the successor case; it's already hacked so that it gives 0 rather than MyNat.zero as the base case.

Sure, but separate to changing what the goal state displays, we'd also need to change the syntax of

induction n with
| zero => sorry
| succ n ih => sorry

[Pedro Sánchez Terraf]

Eric Wieser said:

n⁺¹ seems slightly less crazy than n+, which makes n.succ.succ.succ n⁺¹⁺¹⁺¹

And I've also seen things like $\kappa^{+n}$ in the same context.

[Kevin Buzzard]

In NNG I'm not going to use the pipe syntax at all. We're going to run induction n with d hd like in NNG3 and then have two goals, the first one of which is displayed and the second one of which is suppressed, and I'm not even going to ask the user to indent. I know that this is bad coding practice but I'm not teaching coding, I'm teaching proofs.

[Johan Commelin]

For the constructor, I would be happy to switch to S or successor. But this would require a change to core...

[Adam Topaz]

Eric Rodriguez said:

These notations traditionally increment n, so I think using them for succ would be confusing

It wouldn't be confusing if we could write

do
  let mut n := 30
  n++
  n += 6
  IO.println n

[Eric Wieser]

+= feels like slightly strange notation when assignment is := not =

[Johan Commelin]

All of humanity can be divided neatly into two classes: those who prefer +:= and those who prefer :+=.

[Niels Voss]

+:= might conflict with the proposed n+ notation, depending on how the left side of := is parsed. For this matter, n += 6 might be interpreted as a proposition.

[Jireh Loreaux]

In my opinion, this n+ idea is incredibly confusing. It just makes things look like they would be syntactically invalid. And regarding newcomers / students, I find that they already have a hard enough time distinguishing syntactically valid expressions from invalid ones, so there's no point adding to the confusion.

[Kevin Buzzard]

But -x - -x makes sense:

import Mathlib.Tactic

variable (x : Int) in
#check -x - -x -- -x - -x : ℤ

and it kind of looks confusing until you start thinking about it, and the + version is no different in terms of notation.

[Eric Rodriguez]

And in paper maths we get sign errors all the time! Imagine if we now get sign errors about + too...

[Kevin Buzzard]

I think that both prefix and suffix + should be valid syntax just to prove how arbitrary it is.

[Niels Voss]

Unary prefix + is valid in some languages as a "do nothing" operator (maybe used to emphasize something is positive or maybe to validate that a certain type is numeric in a macro. I think in C it can do coercions). But I don't think unary suffix + or - are valid in any language I'm aware of.

[Niels Voss]

What would n- mean?

[Joscha Mennicken]

How would x+ -x be interpreted?

[Siddhartha Gadgil]

A superscript looks fine. Allowing suffixes will lead to weird stuff like 3+ + 4 being valid (and 8).

[Martin Dvořák]

I'd vote for n⁺ if need be. I am completely fine with status quo.

[Julian Berman]

Niels Voss said:

Unary prefix + is valid in some languages as a "do nothing" operator (maybe used to emphasize something is positive or maybe to validate that a certain type is numeric in a macro. I think in C it can do coercions). But I don't think unary suffix + or - are valid in any language I'm aware of.

In some silly languages it's even valid as a "do something" operator:

⊙  ptpython3                                                                                                                                                                                                                                          julian@Airm
>>> class Foo:
...     def __pos__(self):
...         return 37
>>> +Foo()
37

[Niels Voss]

I mean it can be a valid "do something" operator in Lean as well, as well as in many other languages with operator overloading. But it doesn't do anything in math, I think.