Does `set_option hygiene false` not work with `notation3`?

Stream: general

[Shreyas Srinivas]

I have an #mwe below:

import Mathlib

namespace Playground

set_option hygiene false

/- This works but produces no unexpanders
infixl:65 " + " => add
-/

/- Doesn't work here
notation3:65 (priority := 1001) a:66 " + " b:65 => add a b
-/

class MyNewAlgebra (α : Type) where
  add : α → α → α
  add_assoc : ∀ a b c : α, add a (add b c) = add (add a b) c

notation3:65 (priority := 1001) a:66 " + " b:65 => MyNewAlgebra.add a b

end Playground

When I set_option hygiene false,I can declare notation using infixl before declaring the function that it denotes. But this doesn't work with notation3 and I am forced to use the function name add to define add_assoc. Is there a way around this?

[Kyle Miller]

Does local notation3 work?

[Shreyas Srinivas]

Nope. Same error:

import Mathlib

namespace Playground

set_option hygiene false

/- This works but produces no unexpanders
infixl:65 " + " => add
-/


local notation3:65 (priority := 1001) a:66 " + " b:65 => MyNewAlgebra.add a b


class MyNewAlgebra (α : Type) where
  add : α → α → α
  add_assoc : ∀ a b c : α, add a (add b c) = add (add a b) c

--notation3:65 (priority := 1001) a:66 " + " b:65 => MyNewAlgebra.add a b

end Playground

[Shreyas Srinivas]

Error message : unknown identifier 'MyNewAlgebra.add'

[Kyle Miller]

Oh, I see, I thought you were using hygiene for another purpose.

This isn't supported by notation3 since it elaborates the RHS to generate a delaborator.

[Shreyas Srinivas]

I want to use the notation for add inside the typeclass

[Kyle Miller]

Unfortunately that's not something you can do with notation3, since it needs to know how to resolve add as a global constant to generate the delaborator.

[Shreyas Srinivas]

I recall that Mario was able to accomplish something like this for inductive types when helping Philip Wadler to port plfa to lean.

[Kyle Miller]

Using notation3?

[Shreyas Srinivas]

I'll try to find that thread though IIRC you did recommend it there.

[Kyle Miller]

You could follow notation3's advice and use (prettyPrint := false), then define your own app_unexpander or delaborator later.

[Shreyas Srinivas]

That defeats the purpose of using notation3

[Shreyas Srinivas]

At least for me, the free lunch (unexpander) is the reason to use notation3

[Kyle Miller]

There's just no way notation3 can have any information about what add is before MyNewAlgebra is defined, so there's no way it can construct the delaborator.

[Kyle Miller]

infixl and notation generate unexpanders though, and hygiene controls whether it does any name resolution checking when defining the unexpander. (It doesn't seem to work in this context though.)

[Shreyas Srinivas]

I tried notation and infixl first and was not getting unexpanders since in proof mode (it was much bigger than this)

[Kyle Miller]

Unexpanders are keyed to the global constant name, and a problem is that add isn't a global constant so it's not adding an unexpander.

A future version of infix/notation will give a warning when it doesn't create an unexpander.

[Kyle Miller]

Found the thread you mentioned. Mario used local infix: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Prettyprinting.20the.20result.20of.20an.20.23eval/near/403046669

[Kyle Miller]

Notice needing to declare the notation twice. First, as local infix in a section for use inside the types, and again as actual infix now that the definitions exist.

[Shreyas Srinivas]

It doesn't seem to work for me:

import Mathlib

namespace Playground

set_option hygiene false

local notation:65 (priority := 1001) a:66 " + " b:65 => add a b

class MyNewAlgebra (α : Type) where
  add : α → α → α
  add_assoc : ∀ a b c : α, a + b + c = (a + b) + c

open MyNewAlgebra

--Uncommenting the below line leads to ambiguous notation
-- notation:65 (priority := 1001) a:66 " + " b:65 => MyNewAlgebra.add a b

lemma test_unexpander [MyNewAlgebra α] (a b c : α) : a + (b + c) = (a + b) + c := by
  -- no unexpander
  sorry
end Playground

[Shreyas Srinivas]

Oh wait I am missing a section

[Shreyas Srinivas]

Yes that worked. Thanks a lot :)

[Shreyas Srinivas]

I do wish it was simpler than this.

[Shreyas Srinivas]

For anyone looking for this in the future, here's a working version:

import Mathlib

namespace Playground

set_option hygiene false

section Temp

local notation:65 (priority := 1001) a:66 " + " b:65 => add a b

class MyNewAlgebra (α : Type) where
  add : α → α → α
  add_assoc : ∀ a b c : α, a + b + c = (a + b) + c

end Temp

open MyNewAlgebra

notation:65 (priority := 1001) a:66 " + " b:65 => MyNewAlgebra.add a b

lemma test_unexpander [MyNewAlgebra α] (a b c : α) : a + (b + c) = (a + b) + c := by
  sorry
end Playground