precedence of Nat.factorial

Stream: mathlib4

[Floris van Doorn]

Can we fix the precedence of ! so that the following works:

import Mathlib.Data.Nat.Factorial.Basic

open Nat
example (h : False) : ∃ n : ℕ, n ≠ n := by
  use 3 ! -- function expected
  contradiction

example (n : ℕ) (h : False) : ℕ × ℕ := by
  constructor
  exact n ! -- function expected
  exact 0

now it works if we replace 3 ! by 3! or (3 !) (and only the second option is available for n !).

[Edward van de Meent]

what should this parse as, then?

def foo (n:Nat) (b:Bool) : True := trivial

#check foo 3 ! true

[Violeta Hernández]

If 3! works then I don't think there's any problem here

[Yaël Dillies]

Edward van de Meent said:

what should this parse as, then?

def foo (n:Nat) (b:Bool) : True := trivial

#check foo 3 ! true

As garbage, I would say. Can we force the user to not put a space before ! for the factorial notation, and after for the Bool notation?

[Eric Wieser]

Only if we force (n)! instead of n !

[Kevin Buzzard]

But we can write a*b instead of a * b. This issue with factorial has always made me a bit sad but I don't understand the details enough. Is it something to do with the fact that get! is now a thing?

[Edward van de Meent]

i think you might be able to force it if you write it as a parser?

[Eric Wieser]

Yes, the fact that function names are now allowed to end in ! is exactly the problem with n!

[Eric Wieser]

note that if we made the rule "try the name n! then try factorial n", there would be a footgun for people writing x.get! who didn't realize that X.get! doesn't exist

[Eric Wieser]

The current behavior combined with autoImplicit is pretty nasty:

import Mathlib

example : ∃ n : Nat, n! < n :=  ⟨_, Nat.lt_add_one _⟩

[Floris van Doorn]

Edward van de Meent said:

what should this parse as, then?

def foo (n:Nat) (b:Bool) : True := trivial

#check foo 3 ! true

I didn't even realize that the problem I had with ! was because of Boolean negation. The error message is so unhelpful...

[Edward van de Meent]

Eric Wieser said:

The current behavior combined with autoImplicit is pretty nasty:

import Mathlib

example : ∃ n : Nat, n! < n :=  ⟨_, Nat.lt_add_one _⟩

A: there is a number $n$ that is greater than $n!$

B: oh really? how do you know?

A: just define $n := n! + 1$ and you're done

:man_facepalming:

[Floris van Doorn]

Eric Wieser said:

Only if we force (n)! instead of n !

Actually, this notation is not too bad. I will just tell my students that parentheses are mandatory.

[Floris van Doorn]

Eric Wieser said:

The current behavior combined with autoImplicit is pretty nasty:

Personally I'm not worried about this, since autoImplicit is plenty nasty by itself. I want to like it, it's just too easy to mess up.

[Johan Commelin]

Wait till you see what autoImplicit! does (-;

[Violeta Hernández]

(n)! instead of n! will also be helpful if anyone ever wants to do stuff with double factorials

[Ruben Van de Velde]

Like docs#Nat.doubleFactorial ?

[Edward van de Meent]

surprisingly, i think that would have less issues because that notation uses a different(‼) symbol.

[Edward van de Meent]

(see what i did there) :upside_down:

[Matthew Ballard]

Are people opposed to some unicode trickery here?

[Edward van de Meent]

i think in general people should try and not use unicode symbols which can easily be confused for other more common ones...

[Edward van de Meent]

notation should be readable, not just (hover-to-find-out-what-it-means)-able

[Ruben Van de Velde]

At least we have hover, unlike math papers :)

[Edward van de Meent]

i know, but that should not discourage us from trying to be clear

[Kyle Miller]

I remember @Johan Commelin and I made a n! elaborator a while back. It's a big hack, but it does improve the experience. Edit: Found it: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/New.20.60propose.60.20tactic/near/351149815

The way it works is that overrides how constants are elaborated. It tries searching for n!. That fails, notices there's a ! at the end, then tries searching for n. If that succeeds, it wraps it in Nat.factorial.

(Yes @Kevin Buzzard, this is because get! etc. are supported as names now.)

[Kyle Miller]

I'm not sure how serious I am about actually overriding the const elaborator here... Foolish users who have created notations relying on hacks have been causing me headaches recently. :smile:

[Kyle Miller]

If anyone wants to have fun with it, here's an updated version:

code for x! notation

import Lean
import Mathlib.Data.Nat.Factorial.Basic

namespace Nat.Factorial!
open Lean Elab Term Meta

@[scoped term_elab ident]
def elabIdentFactorial : TermElab
  | stx@`($name:ident), expectedType? => do
    let view := extractMacroScopes name.getId
    let .str parent s := view.name | throwUnsupportedSyntax
    unless s.endsWith "!" do throwUnsupportedSyntax
    let normal ← Term.observing <| elabIdent stx expectedType?
    if normal matches .error .. then
      let name' := MacroScopesView.review { view with name := .str parent (s.dropRight 1) }
      let factorial ← Term.observing <| elabTerm (← `(Nat.factorial $(mkIdent name'))) expectedType?
      if factorial matches .ok .. then
        return ← Term.applyResult factorial
    Term.applyResult normal
  | _, _ => throwUnsupportedSyntax

end Factorial!

open scoped Nat.Factorial!

variable (x : Nat)
#check x ! -- x ! : ℕ
#check x!  -- x ! : ℕ
#check List.get! [1,2,3] 0 -- [1, 2, 3].get! 0 : ℕ

The macro scope manipulation is to get things like this to "work":

set_option quotPrecheck false in
notation "factfun" => fun x => x!

#check factfun -- fun x ↦ x ! : ℕ → ℕ

[Floris van Doorn]

I used that hack in my course last year, but decided against it this year. Was sad to see the issue at the top if this thread, but I told them to write (n)! with parentheses.

[Eric Wieser]

Should we add noWs to the factorial parser so that n ! is illegal?

[Kyle Miller]

This looks like it'll require a core fix for the parenthesizer. Having noWs would make it pretty print as n! at the moment.

import Lean
import Batteries.Data.Nat.Basic

syntax term noWs "?" : term
macro_rules
  | `($(t)?) => `(Nat.sqrt $t)
@[app_unexpander Nat.sqrt]
def unexpandNatSqrt : Lean.PrettyPrinter.Unexpander
  | `($_ $t) => `($(t)?)
  | _ => throw ()

#check 5?
-- 5?
#check fun x : Nat => (x)?
-- fun x ↦ x? : Nat → Nat

[Kyle Miller]

There's not a clear fix. Parenthesis insertion occurs in a phase before formatting, but this lexical issue can only be detected at formatting time.

[Floris van Doorn]

Eric Wieser said:

Should we add noWs to the factorial parser so that n ! is illegal?

Banning it outright might be a little extreme (although I'm not against it), but we can start by saying it is the preferred way to write the factorial function, and pointing out the danger of writing n ! in the docstring for the notation.
Then we should also fix the ~300 occurrences found by regex [^a-zA-Z][a-z] ![^[=!] in Mathlib.

[Eric Wieser]

This seems to work @Kyle Miller:

import Lean
import Batteries.Data.Nat.Basic

syntax term noWs "?" : term
macro_rules
  | `($(t)?) => `(Nat.sqrt $t)
@[app_unexpander Nat.sqrt]
def unexpandNatSqrt : Lean.PrettyPrinter.Unexpander
  | `($_ ($t)) => `(($(t))?)
  | `($_ $t) => `(($(t))?)
  | _ => throw ()

#check 5?
-- (5)?
#check (1 + 5)?
-- (1 + 5)?
#check fun x : Nat => (x)?
-- fun x ↦ (x)? : Nat → Nat

(yes, it's a hack, but not an awful one)

[Kyle Miller]

@Floris van Doorn Your original example's problem seems to be that use doesn't require that the terms coming after it to say after the column that use starts on. In fact, this is legal:

example (h : False) : ∃ n : ℕ, n ≠ n := by
  use
  1
  contradiction

[Kyle Miller]

This is not just a problem with use. Pretty much any tactic taking a term has no column requirements:

example (h : False) : ∃ n : ℕ, n ≠ n := by
  refine
⟨1, ?_⟩
  contradiction

[Kyle Miller]

It's parsing yours as 3 (! contradiction) using the not syntax, even though contradiction is on its own line in the correct column and looking very much like it should be a tactic.

[Floris van Doorn]

Yes, I think a lot of tactics don't require that, and it's somewhat reasonable since the expression argument is mandatory, so usually there is no ambiguity. I think it's fine to consistently add this to tactic parsers, but that is a pretty big change.
I've seen some beginners write

calc ... = ... := by apply
    foo

but I think it's fine to disallow that.

[Floris van Doorn]

Floris van Doorn said:

Banning it outright might be a little extreme (although I'm not against it), but we can start by saying it is the preferred way to write the factorial function, and pointing out the danger of writing n ! in the docstring for the notation.
Then we should also fix the ~300 occurrences found by regex [^a-zA-Z][a-z] ![^[=!] in Mathlib.

If we want this, here is the docstring change: #18085

[Kyle Miller]

The idea to make factorial use noWs is sort of a hack because the issue here is from a ! b being ambiguous. Using noWs is making use of the following feature of application parsing:

#check (not)! true
--          ^ error because function applications require whitespace after the function
#check (not) ! true
-- !!true

[Kyle Miller]

If anyone can figure out how to change the second notation to get the third #eval to print 9, then you've cracked the problem for factorial notation:

notation:max "~" b:40 => b + 1
notation:max n:max "~" => n ∘ n

#eval (·*3) (~ 1)   -- 6
#eval ((·*3) ~) 1   -- 9
#eval (·*3) ~ 1     -- want 9, but it's 6

[Floris van Doorn]

How bad would it to not allow a space in the Boolean negation notation !b? I expect we don't want to go that route, but at least that would not be ambiguous since names cannot start with !.

[Floris van Doorn]

Kyle Miller said:

If anyone can figure out how to change the second notation to get the third #eval to print 9, then you've cracked the problem for factorial notation:

Like this? However, this would require parentheses in f !b.

notation:max n:max "~" => n ∘ n
notation:1022 "~" b:40 => b + 1 -- or lower 1022

#eval (·*3) (~ 1)   -- 6
#eval ((·*3) ~) 1   -- 9
#eval (·*3) ~ 1     -- now 9

[Floris van Doorn]

What if !b has precedence max and ! b (with space) has precedence <1022 :thinking:
(I think you can start ignoring me, I think I'm starting to sound more like a monkey on a typewriter than usual.)

[Kyle Miller]

Hmm, notation:lead "~" b:40 => b + 1 works too. I'm a :monkey: too though

[Kyle Miller]

(Ah, and lead is 1022, so makes sense...)

[Floris van Doorn]

Floris van Doorn said:

How bad would it to not allow a space in the Boolean negation notation !b? I expect we don't want to go that route, but at least that would not be ambiguous since names cannot start with !.

Empirically, in the Lean 4 repo there are 700 hits for [^\]a-zA-Z-0-9]![(a-zA-Z] (and almost all of them are Boolean negation) and only 5 hits for [^\]a-zA-Z-0-9]! (including a trailing space) (4 of them in a test) (both patterns only include *.lean files).
So code-style wise there seems to be already a firmly established code style to not add a space after the Boolean negation !. But it's up to the FRO to decide whether they want to enforce this (especially if the main reason is to avoid a pretty obscure interaction with Nat.factorial).

[Bryan Gin-ge Chen]

To keep #18085 moving along, what are the possible options here? Should we have a poll about whether to prefer (n)! over n ! in mathlib, or are there some other issues that could / should be resolved in core that I missed?

[Kyle Miller]

lean4#5824 and lean4#5826 are two experiments, the first is changing the precedence of boolean !, and the second is making it require whitespace. I think the first solution is makes more sense than the second, but I'm not sure if or when we'd change core notation. We need some sort of cooperation with core to solve the issue of confusing error message, no matter how we decide to parenthesize factorial in mathlib.

[Kyle Miller]

Bryan Gin-ge Chen said:

(n)! over n !

At least with the second, (n !) can be used in the use example to avoid the confusing error.

[Jireh Loreaux]

#18085 is apparently still blocked on this discussion. I would prefer to simply merge it.

If another maintainer seconds this motion, please just merge it.

[Jz Pan]

Matthew Ballard said:

Are people opposed to some unicode trickery here?

Do you mean full width one ！ ?

[Kevin Buzzard]

I don't know the history of \| for divisibility, but I could imagine it was: "mathematicians wanted a symbol for divisibility and | was taken for set notation so they used \|". In Lean 4 the situation is analogous: mathematicians want a symbol for factorial, but now ! is taken already so we use some unicode hack \! and just tell people that it's because ! means something else in core Lean.

[Kevin Buzzard]

There seem to be several variants available: https://www.amp-what.com/unicode/search/exclamation

[Ruben Van de Velde]

Oh, we could use :exclamation:

[Kyle Miller]

Unicode trickery is sad, but it really would help solve the problem.

There's nǃ (pronounced "enn alveolar click")

The full-width exclamation n！ would help distinguish n！！ from n‼, but it does look a bit funny.

[Eric Wieser]

Kevin Buzzard said:

I don't know the history of \| for divisibility, but I could imagine it was: "mathematicians wanted a symbol for divisibility and | was taken for set notation so they used \|".

I think it's more likely "Unicode decided that the existing | character used in computer code was semantically different from the divides symbol used in mathematics, so they allocated a symbol for it".

[Kevin Buzzard]

My (probably weak) argument against that was that in LaTeX we use | in both $\{x\,|\,x^2=2\}$ and $5\,|\,15$.

[Patrick Massot]

You should use \mid for the first one.

[Patrick Massot]

instead of managing space by hand.

[Michael Stoll]

Patrick Massot said:

You should use \mid for the first one.

For divisibility, too (IMO). Note that non-divisibility is \nmid.

[Kevin Buzzard]

Patrick Massot said:

You should use \mid for the first one.

Ha ha I knew this but felt it weakened my argument :-) In fact you should use \mid for the second one too, as it's a binary operator.

[Kyle Miller]

/poll Straw poll: What should we do about Nat.factorial notation?
Wait and hope that Lean core does something to help
The current situation (writingn ! and having unexpected parse errors) is fine
Switch to ǃ (alveolar click)
Switch to ！ (two-character-width exclamation)
Switch to ❗ (emoji)
Use a more ridiculous option: 🆙 (votes for this count as "abstain")

[Kyle Miller]

(A "straw poll" means this is a non-binding vote. It's just to get a sense of what people thing is acceptable.)

[Julian Berman]

Can you straw-disambiguate the first two options, what's the difference between "wait for Lean core" and "leave things as-is"? Does the second one mean someone thinks there's no issue whatsoever?

[Kyle Miller]

Yes, second means no issue whatsoever. The situation is fine as-is, people should just learn to deal with it.

[Kyle Miller]

I meant to have that one come first, since all the others involve change (except for n🆙, which I hope we'll never do).

[Kyle Miller]

There's a variant to #18085 @Floris van Doorn. What if the notation required parentheses like

syntax "(" term ")" noWs "!"

[Kevin Buzzard]

My vote for the alveolar click is contingent on it being acceptable to make \! produce this character (right now in VS Code it produces ¡, so this line needs changing).

[Kyle Miller]

Me too @Kevin Buzzard

[Julian Berman]

Isn't the solution then to make \! produce ! and now done? if only...

[Floris van Doorn]

If we go for (n)!, there are indeed questions whether we want to enforce it, or only encourage it.

[Floris van Doorn]

Is it better to have syntax "(" term ")" noWs "!" over syntax term noWs "!" (other than the pretty-printer not round-tripping), since the latter allows 2!?

[Kyle Miller]

No that doesn't work, see the first example in this thread @Julian Berman

[Aaron Hill]

I personally dislike the fact that mathlib uses very similar characters like | and ∣, and I hope that we don't add more. In particular, I think people will see 'n <alveolar click>' when reading code, interpret it as being 'n!' with the usual exclamation point, and see a confusing error when they try it out themselves.

[Eric Wieser]

I think using similar characters is ok if they are unicode-approved for their purpose (divides vs regular|), but less so if we're abusing graphically similar but semantically inappropriate characters like alveolar click.

[Eric Wieser]

That is, unless we start a movement to read factorial out loud with such a click

[Kevin Buzzard]

Aaron Hill said:

I personally dislike the fact that mathlib uses very similar characters like | and ∣, and I hope that we don't add more. In particular, I think people will see 'n <alveolar click>' when reading code, interpret it as being 'n!' with the usual exclamation point, and see a confusing error when they try it out themselves.

I don't buy this argument because n! already gives a confusing error!

[Aaron Hill]

I think adjusting the lean-core behavior would be the right solution to that parse error, rather than introducing a new way to write factorial

[Aaron Hill]

Also, I think the experience for users is worse when they get an error trying to replicate exisiting (working) code due to using the wrong unicode character

[Aaron Hill]

If I hadn't seen this thread and I saw '(n+1)!=(n+1)*n<alveolar click>', I would expect that the same '!' character was used twice, and not two distinct (but intentionally visually similar) characters

[Kevin Buzzard]

The change would universally replace factorial with the click, so the same character would be used twice. In my experience people don't trip up on divisibility because they look at code in mathlib and see what symbol is used. I don't think that the core devs have any interest in changing how they use ! (all this get! stuff is a core part of the naming convention there) and "mathematicians have used it in another way for hundreds of years" will not convince them, they have far more important things to worry about. So we have to work around their decisions in mathlib and changing the symbol is the lesser of all the evils which has been suggested as far as I can see. I totally appreciate your objections but the "use another unicode character" approach is a solution which has worked fine in other parts of number theory and if we add the explanation that you use \! to the factorial docstring then I think we should be fine.

[Aaron Hill]

Would we deprecate ! In favor of <click>, or allow both but exclusively use <click> inside of mathlib itself?

[Kevin Buzzard]

docs#Nat.factorial is in mathlib and it would just be a case of changing the notation and then removing all the horrible spaces in the theorems like factorial_succ (n : ℕ) : (n + 1)! = (n + 1) * n !.

[Aaron Hill]

I mean, would downstream users eventually use <click> as the only supported factorial notation?

[Kevin Buzzard]

If this change were to be made then yes, just like downstream users don't use the | symbol on their keyboard to talk about divisibility.

[Kevin Buzzard]

Downstream users would of course be free to define their own notation using ! and then they'll run into the parsing problems which we currently face in mathlib because of core's decision to allow ! in identifiers and the clash with boolean not (also in core and also unlikely to be changeable).

[Julian Berman]

"mathematicians have used it in another way for hundreds of years" will not convince them

This is a bit of a strawman isn't it (by which I mean I don't think the choice is presumed to be "convince core not to call things get!, it's "make get! work, and make n! work when n! is not an identifier)? The actual shape of a core change I presume would be something more like "allow suffix notations a chance at parsing something that looks like an identifier if that identifier ends up not existing", and though I have never written anything like one I would bet there are some other cases where this might be useful beyond this specific math notation.

Anyways I get that it's annoying and perhaps "we can hack around this" is very attractive (and maybe even the right solution given how long the wait) but I also don't think that using crazy confusable characters has zero ongoing cost (which is even why I felt comfortable voting personally).

[Julian Berman]

Eric Wieser said:

note that if we made the rule "try the name n! then try factorial n", there would be a footgun for people writing x.get! who didn't realize that X.get! doesn't exist

what do you mean by this? as in someone would get strange errors in a file where n! meant factorial and then tried .get! on something where it didn't exist (but .get does) and then the errors say things about taking factorials of some function? Isn't the "fix" there "just"™ "when a second error happens, show the first error (the identifier one)"?

[Eric Wieser]

I'm thinking of the case where the user thinks both get and get! exist, but in fact only the former does (they haven't written it yet, they put it in the wrong namespace, etc). If they're unfortunate enough to have foo.get : Nat, then they are in for a nasty surprise when their naturals are way bigger than intended.

[Kim Morrison]

(Aside, I'm progressively getting rid of get! across multiple namespaces. Users should use xs[i]! notation, and where the functions need to exist they are being renamed get!Internal.)

[Kim Morrison]

I expect that there will still be identifiers ending with ! after this, however.

[Jz Pan]

Kim Morrison said:

Users should use xs[i]! notation

Same problem, if users think both [ ] and [ ]! exist, but only [ ] exists and is of type Nat

[Kim Morrison]

My position all along has been that there is nothing wrong with the word factorial, and the benefits of notation for it are outweighed by the downsides...