# Zulip Chat Archive

## Stream: new members

### Topic: Substitution notation

#### Pedro Minicz (Jul 03 2020 at 03:58):

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 (Jul 03 2020 at 04:08):

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 (Jul 03 2020 at 04:09):

The `/`

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

#### Kenny Lau (Jul 03 2020 at 04:10):

```
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 (Jul 03 2020 at 04:10):

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 (Jul 03 2020 at 04:10):

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 (Jul 03 2020 at 04:11):

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

#### Pedro Minicz (Jul 03 2020 at 04:14):

The following notation works:

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

But using `:=`

looks fishy.

#### Pedro Minicz (Jul 03 2020 at 04:20):

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 (Jul 03 2020 at 04:21):

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

#### Pedro Minicz (Jul 03 2020 at 04:22):

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 (Jul 03 2020 at 04:23):

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 (Jul 06 2020 at 21:07):

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

#### Pedro Minicz (Jul 06 2020 at 21:07):

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 (Jul 06 2020 at 21:24):

```
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 (Jul 06 2020 at 21:25):

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 (Jul 06 2020 at 21:36):

Could you change the binding power of `[`

and `]`

to be higher than function application?

#### Kyle Miller (Jul 06 2020 at 21:36):

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 (Jul 06 2020 at 21:38):

(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 (Jul 06 2020 at 21:40):

As a stopgap:

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

#### Pedro Minicz (Jul 06 2020 at 21:41):

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 (Jul 06 2020 at 21:42):

and was it left-binding or right-binding?

#### Pedro Minicz (Jul 06 2020 at 21:42):

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 (Jul 06 2020 at 21:42):

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

#### Reid Barton (Jul 06 2020 at 21:43):

See `data.opposite`

for example

#### Pedro Minicz (Jul 06 2020 at 21:43):

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

#### Reid Barton (Jul 06 2020 at 21:43):

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 (Jul 06 2020 at 21:43):

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 (Jul 06 2020 at 21:51):

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 (Jul 06 2020 at 21:53):

Yakov Pechersky said:

and was it left-binding or right-binding?

I am not sure.

#### Pedro Minicz (Jul 06 2020 at 21:54):

Changing the precedence of `[`

to `std.prec.max_plus`

solved the issue. Maybe the printer/parser mismatch should be investigated further.

Last updated: May 14 2021 at 04:22 UTC