A quirk with `local notation`

Stream: lean4

[Damiano Testa]

This is something that took me some time to figure out while porting a file:

def FT (_n : Unit) : Type := Unit

variable {p : Unit}
local notation "F" => FT p

variable (x : F) (y : FT p)

example : x = x := by rfl  -- declaration uses 'sorry'
example : y = y := by rfl  -- works

#check x  -- `x : FT (sorryAx Unit true)`
#check y  -- `y : F`

The variable x has a sorry embedded where the p should be. I imagine that this is due to the fact that p is a local variable.

If you remove local from the notation, Lean complains with an unknown identifier (expected).
With local, Lean just forces through... (I would have preferred the same complaint!)

[Kevin Buzzard]

Right, you can't use variables in notation, but you're saying you can use them in local notation and they just cause chaos.

[Damiano Testa]

Yes, precisely. I would have preferred to get the same error that I had without the local also when local was inserted.

[Damiano Testa]

note that this happened exactly in Witt vectors: the setup is

variable {p : ℕ} [...stuff]

-- mathport name: expr𝕎
local notation "𝕎" => WittVector p   -- oh no!

[Kevin Buzzard]

Oh did that work in lean 3?

[Damiano Testa]

It did work, in the sense that it inserted the local variable p correctly, instead of a sorry.

[Damiano Testa]

There is a note:

/- We cannot make this `localized` notation, because the `p` on the RHS doesn't occur on the left
Hiding the `p` in the notation is very convenient, so we opt for repeating the `local notation`
in other files that use Witt vectors. -/

[Damiano Testa]

So, I guess that this is also a warning that this issue will crop up in later Witt vector files! :smile:

[Reid Barton]

maybe it can be made to work in Lean 4 with hygiene somehow?

[Damiano Testa]

To see the relevant code:

• in mathlib3 docs#witt_vector, (the actual line with the notation)
• in mathlib4 docs4#WittVector (the actual line with the notation).

[Damiano Testa]

Reid Barton said:

maybe it can be made to work in Lean 4 with hygiene somehow?

Maybe, I have not thought about how to fix it.

[James Gallicchio]

wondering if it would be better to introduce a let-bind notation to argument lists where you can do something like
def foo {p : Nat} (let W := WittVector p) [Bar W] := sorry
because then the variable statement can just have (let 𝕎 := WittVector p). I'd also find this occasionally useful for programming with really complicated types.

[Floris van Doorn]

Replying to an old thread, but you can do with when disabling hygiene:

def FT (_n : Unit) : Type := Unit

variable {p : Unit}

set_option hygiene false
local notation "F" => FT p

variable (x : F) (y : FT p)

example : x = x := by rfl  -- works
example : y = y := by rfl  -- works

#check x  -- `x : F`
#check y  -- `y : F`