noninjective notations

Stream: general

[Mario Carneiro]

I could have sworn this was statically disallowed, but apparently you don't need to use the variables in a notation only once. The result is a dag-like pexpr that can be elaborated simultaneously to two different types:

def foo (a : int) (b : nat) : Prop := a = b

notation `F` x := foo x x

set_option pp.implicit true
set_option pp.numerals false
#check F (id 1)
-- foo (@id ℤ (@has_one.one ℤ int.has_one)) (@id ℕ (@has_one.one ℕ nat.has_one)) : Prop

Note the lack of coercion in the two instances of id 1, they are really different functions even though the term was only written once

[Mario Carneiro]

Only slightly less surprising is notations which don't use their arguments at all:

notation `G` x := true
#check G ((λ x, x x) (λ x, x x)) -- true : Prop

[Mario Carneiro]

I'm 99.9% sure we don't ever declare such notations in mathlib. Thoughts on banning them in a lean 3 patch? It will be helpful for the port.

[Patrick Massot]

I'm pretty sure you can go for it

[Patrick Massot]

And if it doesn't badly break current mathlib then we'll never look back

[Kevin Buzzard]

Indeed we'll never even notice or think to look back :-)

[Eric Wieser]

I actually tried to use a notation like this in https://github.com/leanprover-community/mathlib/pull/6152/files#diff-48c4d86a6f8902ed17b9728588594da05839379ca05b4dcabc31a3999850cf65R68-R69, but lean wasn't good at reducing it when I wanted it to

[Gabriel Ebner]

Mario Carneiro said:

I'm 99.9% sure we don't ever declare such notations in mathlib. Thoughts on banning them in a lean 3 patch? It will be helpful for the port.

This is 100% kosher in Lean 4, so I'm against banning it in Lean 3:

def foo (a : Int) (b : Nat) : Prop := a = b

notation "F" x => foo x x

set_option pp.all true in
#check F 0

[Gabriel Ebner]

Maybe the term goal feature should be adapted to show both expected types though. But the goal state already works:

#check F (by exact 0)
/-
▶ 2 goals

⊢ Int

⊢ Nat
-/

[Mario Carneiro]

Gabriel Ebner said:

Mario Carneiro said:

I'm 99.9% sure we don't ever declare such notations in mathlib. Thoughts on banning them in a lean 3 patch? It will be helpful for the port.

This is 100% kosher in Lean 4, so I'm against banning it in Lean 3:

It might be okay in lean 4, but I'm contemplating an implementation of the porting architecture that would really prefer for the mapping from written syntax to pexpr / expr to be 1-1 where possible. So it would be fine to introduce these notations post-port but for simplicity we would avoid them until then.

It's also just a weird thing to do, and it makes unexpansion a lot harder, so I don't think it deserves to exist.

[Gabriel Ebner]

I'm sure there will be other challenges as well once the porting architecture crosses the threshold from contemplation to evaluation.
This problem seems to be completely hypothetical, and I think it is easy to clean up if it pops up. I fully support removing notation `F` x := foo x x from mathlib when that happens.