Notation introduces sorry

Stream: mathlib4

[Patrick Massot]

The following Lean 3 code works as expected:

import linear_algebra.finrank
import analysis.normed_space.basic

noncomputable theory
open finite_dimensional

variables {E : Type*} [normed_add_comm_group E] [normed_space ℝ E] {F : Type*} [normed_add_comm_group F]
  [normed_space ℝ F]

local notation `d` := finrank ℝ F

variable {p : fin (d + 1) → F}

def bar := p 0

Now let's translate to Lean 4 using mathport:

import Mathlib.LinearAlgebra.Finrank
import Mathlib.Analysis.NormedSpace.Basic

noncomputable section
open FiniteDimensional

variable {E : Type _} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type _} [NormedAddCommGroup F]
  [NormedSpace ℝ F]

local notation "d" => finrank ℝ F

variable {p : Fin (d + 1) → F}

def bar := p 0

This gives the warning declaration uses 'sorry' and the expected type panel indeed shows p : Fin (sorryAx ℕ true + 1) → F. Any idea how to fix this?

[Matthew Ballard]

notation3?

[Patrick Massot]

No impact.

[Jireh Loreaux]

@Damiano Testa didn't you run into this once? I don't remember the issue.

[Matthew Ballard]

I suppose you don't want to go full macro?

[Damiano Testa]

Ah, something like this rings a bell. It probably was in a WittRing file.

[Patrick Massot]

I want to port the sphere eversion project. This issue is distracting me in my fight against the Lean 4 simplifier. So I have nothing against macros, I simply want something that works.

[Damiano Testa]

Some interaction with local and notation.

[Damiano Testa]

Let me try to dig it up.

[Damiano Testa]

This is what I was thinking. I have not checked whether it is relevant, though (but may have to leave soon, so I am putting here, just in case I disappear!)

[Kyle Miller]

set_option hygiene false

[Damiano Testa]

Indeed, Kyle reached the same solution that Floris did in the other thread!

[Kevin Buzzard]

I think that Patrick of all people would like to think that he is writing hygienic code! Why do we have to turn it off?

[Adam Topaz]

you just need to turn it off in the notation:

set_option hygiene false in
local notation "d" => finrank ℝ F

[Kyle Miller]

@Adam Topaz Did you test that?

[Adam Topaz]

yes

[Kyle Miller]

For me I get "unknown identifier d" later on

[Adam Topaz]

oh I'm wrong.

[Damiano Testa]

Really? I thought that the local disappeared after the in.

[Adam Topaz]

autoimplicit is biting me again!

[Kyle Miller]

It's good to know that notation3 fails here too. It might be fixable there...

I think the problem is that the F in the definition of the local notation is different from the F when the variables get introduced later. They need to have way to link them up.

@Kevin Buzzard "hygiene" refers to whether substitution is safe from accidental name capturing. It's a feature that's being turned off, not a check that's being turned off. Turning it off makes it so that F in the notation can refer to the F that gets introduced when def processes all the variables. We want F in the notation to refer to the newly bound F.

[Kyle Miller]

@Kevin Buzzard Here's a hopefully illuminating example of what hygiene is about:

notation "wrap " t => fun (x : Unit) => t
#eval let x := 2; (wrap x) ()
-- 2

set_option hygiene false in
notation "wrap' " t => fun (x : Unit) => t
#eval let x := 2; (wrap' x) ()
-- ()

The first one expands to effectively let x := 2; (fun (x' : Unit) => x) (), but the second expands to let x := 2; (fun (x : Unit) => x) ().

[Patrick Massot]

Thank everyone. Indeed it seems disable hygiene helps here.

[Anatole Dedecker]

Would it make sense to ask for local notation to be unhygienic with respect to objects already in the local scope? More generally, is there a way to say that a notation is unhygienic in some argument but hygienic for others?

[Kyle Miller]

What's been puzzling me is that there are many other examples in mathlib of using local notation to capture a variable, but somehow this one fails. This might actually be a problem with the variable command and how it elaborates binders.

I've noticed that while Patrick's example fails and inserts a sorry, this is OK:

import Mathlib.LinearAlgebra.Finrank
import Mathlib.Analysis.NormedSpace.Basic

noncomputable section
open FiniteDimensional

variable {E : Type _} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type _} [NormedAddCommGroup F]
  [NormedSpace ℝ F]

local notation "d" => finrank ℝ F

def bar {p : Fin (d + 1) → F} := p 0

[Kyle Miller]

Here's a #mwe:

import Lean

variable (x : Nat)
local notation "Finx" => Fin x

def val (y : Finx) : Nat := y

variable (y : Finx)

-- Declaration uses sorry:
def val' : Nat := y

[Kyle Miller]

(@Sebastian Ullrich Here's some sort of interaction between how variable works, macros, and hygiene that leads to a surprising result. If you turn off hygiene for the notation then val' elaborates without sorry.)

[Anatole Dedecker]

Oh okay, so actually the macro system is smart enough as long as we don't use variables

[Sebastian Ullrich]

Kyle Miller said:

Here's a #mwe:

Thanks, lean4#2535