## 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