Is it possible to have genuine abbreviations?

Stream: new members

[Ching-Tsun Chou]

Consider the following definition:

variable (x y z : ℕ)
abbrev foo := x + y + z

Subsequently the term foo denotes a function foo : ℕ → ℕ → ℕ → ℕ, not the sum x + y + z. To refer to that sum, I need to write foo x y z. After all, abbrevis just a variant of def. But is it possible to have a genuine abbreviation or "macro" so that I can write foo for the expression x + y + z?

Needless to say, in the actual use case I have in mind, the identifiers and expressions involved are more complicated than those in the above example and I hope a genuine abbreviation mechanism can improve the readability of my code.

[Niels Voss]

In Lean 3, there used to be a parameter command which did something similar, but it was removed in Lean 4 for reasons I don't quite understand. You can probably do something like local notation "foo" => x + y + z, and I know this is possible to implement using macros.

[Ching-Tsun Chou]

Is this documented somewhere or there are examples I can look at?

[Niels Voss]

I'm not sure, sorry. One thing to watch out for is this bug #general > Local notation leads to hidden sorry. It's possible it has been fixed, but I haven't checked recently.

[Niels Voss]

I think the bug is still present

[Jakub Nowak]

Macro also works macro "foo" : term => (x + y + z)`.

[Jakub Nowak]

import Mathlib

variable (x y z : ℕ)

macro "foo" : term  => `(x + y + z)

abbrev bar := x + y + z

theorem foobar : foo = bar x y z := by rfl

-- doesn't work (as expected)
-- theorem foobar2 x y z : foo = bar x y z := by rfl

[Jovan Gerbscheid]

Yes, you can do it as follows using local notation:

local notation "foo" x:max y:max z:max => x + y + z
variable (x y z : Nat)

example : foo x y z = foo y z x := by
  omega

The local just means that the notation isn't defined globally. Writing x:max instead of x tells Lean about the precedence it needs to use to parse x. Without this, it would think that foo x y z is foo (x y z), i.e. x applied to y and z.

[Ching-Tsun Chou]

I'm not sure that's what I wanted. What I wanted is to write foo for the expression x + y + z without having to mention any of x, y, and z.

[Kyle Miller]

I suggest searching for examples of local notation in mathlib. There are plenty that capture variables defined in variables.

[Terence Tao]

One compromise that works for me is to place all ambient variables inside a custom class that one then exports back to the environment, and also introduces as a variable instance. Abbreviations then depend on that class instance, but that is handled invisibly and so it becomes visually indistinguishable from a "genuine" abbreviation. Example:

import Mathlib

class Data where
  x:ℕ
  y:ℕ
  z:ℕ

export Data (x y z)

variable [Data]

abbrev foo := x + y + z

example : foo = x + y + z := rfl