Substitution notation

Stream: new members

[Pedro Minicz]

I am having trouble defining notation for substitution. I want M[x/N] = subst x N M and M[x/N][y/L] = (M[x/N])[y/L].

axioms (term : Type) (M N : term)
axiom subst : ℕ → term → term → term

notation M `[` x `/` N `]` := subst x N M -- Unsure about this definition.

#check M [ 0 / N ] -- Fails: `command expected`.

[Alex J. Best]

I think your problem is a conflict with some built in notation, I suggest you pick a different unicode character.

axioms (term : Type) (M N : term)
axiom subst : ℕ → term → term → term

notation M `😀` x `😃` N `😀` := subst x N M -- Unsure about this definition.

#check M 😀 0 😃N 😀 -- works

[Alex J. Best]

The / seems to be the problem though, you could try setting the priority higher also

[Kenny Lau]

axioms (term : Type) (M N : term)
axiom subst : ℕ → term → term → term

notation M ` [ ` x ` // ` N ` ]` := subst x N M -- Unsure about this definition.

#check M [ 0 // N ] -- M [ 0 // N ] : term

[Kyle Miller]

For example, setting a low precedence level

notation M `[`:1 x `↦`:1 N `]`:1 := subst x N M -- Unsure about this definition.

#check M [ 0 ↦ N ] -- OK

[Kenny Lau]

I found that setting a precendence level of [ or ] causes all [ and ] globally to change precendence, so maybe it is best not to change it

[Kyle Miller]

It probably has a good precedence level for this application to begin with, I suppose.

[Pedro Minicz]

The following notation works:

notation M ` [` x ` := ` N `]` := subst x N M

But using := looks fishy.

[Pedro Minicz]

All suggestions seem to break down with M [ 0 // M [ 0 // M ] ] (M [ 0 // (M [ 0 // M ]) ] works).

I remember seeing something that seem to solve this exact problem (resetting the precedence inside the notation or something like that), but I don't remember exactly.

[Kyle Miller]

notation M `[` x `//` N:0 `]` := subst x N M

#check M [ 0 // M [0 // M]]

[Pedro Minicz]

Changing the priority of [ breaks it.

axioms (term : Type) (M N : term)
axiom subst : ℕ → term → term → term

notation M ` [ ` x ` // ` N ` ]` := subst x N M

#check M [ 0 // M [ 0 // M ] ]

notation M ` [ `:0 x ` // ` N ` ]` := subst x N M

#check M [ 0 // M [ 0 // M ] ] -- Fails.

[Pedro Minicz]

The following works. Apparently the precedence of [ can't be less than N's.

notation M ` [ `:1 x ` // ` N:0 ` ]` := subst x N M

#check M [ 0 // M [ 0 // M ] ]

[Pedro Minicz]

Is it possible to have a "postfix with more arguments"?

[Pedro Minicz]

I am using notation M `[` x ` := ` L `]` := subst x L M for my substitution notation. In goals, Lean displays f M[x := L] for f (M[x := L]), however, if I write f M[x := L] Lean parses it as (f M)[x := L], which makes sense, because of the precedence of function application.

[Pedro Minicz]

axiom term : Type
axiom shift : term → term
axiom subst : (ℕ → term) → term → term
axiom σ : ℕ → term → ℕ → term

notation M `[` x ` := ` L `]` := subst (σ x L) M

axiom problematic (x : ℕ) (L R : term) :
  shift (L[x := L]) = shift R[x + 1 := shift R]

#check problematic -- `shift L[x := L] = (shift R)[x + 1 := shift R]`!!

-- The type of this axiom is what `#check problematic` displays, which is different from `problematic`.
axiom problematic' : ∀ (x : ℕ) (L M : term),
  shift M[x := L] = (shift M)[x := L]

#check problematic'

[Pedro Minicz]

This leads to my question: can I have something like postfix `[` x ` := ` L `]` := subst x L, so that Lean parses what I write as it displays goals?

[Yakov Pechersky]

Could you change the binding power of [ and ] to be higher than function application?

[Kyle Miller]

Is the issue that it's not parsing the way you expect it to? What would the fully parenthesized version of problematic be?

[Kyle Miller]

(I'm guessing you want the substitution brackets to have higher precedence than function application, which Yakov addresses. I've heard changing binding power of something like [ and ] can mess up parsing elsewhere, though.)

[Yakov Pechersky]

As a stopgap:

axiom problematic (x : ℕ) (L R : term) :
  shift (L[x := L]) = shift $ R[x + 1 := shift R]

[Pedro Minicz]

Yakov Pechersky said:

Could you change the binding power of [ and ] to be higher than function application?

I've tried setting the precedence of [ to :max (if that is what you mean by binding power), didn't solve the issue.

[Yakov Pechersky]

and was it left-binding or right-binding?

[Pedro Minicz]

Kyle Miller said:

Is the issue that it's not parsing the way you expect it to? What would the fully parenthesized version of problematic be?

The issue is the mismatch between Lean's parser and printer. I've expanded the example, should make things clearer.

[Reid Barton]

well there's your problem--you need to set it higher than that! :upside_down:

[Reid Barton]

See data.opposite for example

[Pedro Minicz]

Naming seems to imply it shouldn't be possible. I'll give it a try.

[Reid Barton]

Disclaimer: I have no idea what will happen with [] specifically, but there are plenty of other bracket characters available if you need them...

[Floris van Doorn]

In flypitch we used

notation t `[`:max s ` // `:95 n `]`:0 := fol.subst_term t s n

https://github.com/flypitch/flypitch/blob/c762ba89b7ca4d3e014aee0dc89d804454c38808/src/fol.lean#L357

[Kyle Miller]

Pedro Minicz said:

The issue is the mismatch between Lean's parser and printer. I've expanded the example, should make things clearer.

I see. It doesn't seem to be a good thing that the parser/pretty-printer doesn't round trip here. I've modified your example a bit to demonstrate the issue a little clearer:

axiom term : Type
axiom shift : term → term
axiom subst : (ℕ → term) → term → term
axiom σ : ℕ → term → ℕ → term

notation M `[` x ` := ` L `]` := subst (σ x L) M

axiom problematic (x : ℕ) (L : term) :
  ∃ R, shift (L[x := L]) = R

#check problematic -- ∀ (x : ℕ) (L : term), ∃ (R : term), shift L[x := L] = R

axiom problematic' (x : ℕ) (L : term) :
  ∃ R, shift L[x := L] = R

#check problematic' -- ∀ (x : ℕ) (L : term), ∃ (R : term), (shift L)[x := L] = R

[Pedro Minicz]

Yakov Pechersky said:

and was it left-binding or right-binding?

I am not sure.

[Pedro Minicz]

Changing the precedence of [ to std.prec.max_plus solved the issue. Maybe the printer/parser mismatch should be investigated further.