Zulip Chat Archive

Stream: new members

Topic: Substitution notation


view this post on Zulip 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`.

view this post on Zulip 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

view this post on Zulip Alex J. Best (Jul 03 2020 at 04:09):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kyle Miller (Jul 03 2020 at 04:11):

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

view this post on Zulip Pedro Minicz (Jul 03 2020 at 04:14):

The following notation works:

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

But using := looks fishy.

view this post on Zulip 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.

view this post on Zulip Kyle Miller (Jul 03 2020 at 04:21):

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

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

view this post on Zulip 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.

view this post on Zulip 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 ] ]

view this post on Zulip Pedro Minicz (Jul 06 2020 at 21:07):

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

view this post on Zulip 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.

view this post on Zulip 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'

view this post on Zulip 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?

view this post on Zulip Yakov Pechersky (Jul 06 2020 at 21:36):

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

view this post on Zulip 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?

view this post on Zulip 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.)

view this post on Zulip 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]

view this post on Zulip 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.

view this post on Zulip Yakov Pechersky (Jul 06 2020 at 21:42):

and was it left-binding or right-binding?

view this post on Zulip 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.

view this post on Zulip Reid Barton (Jul 06 2020 at 21:42):

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

view this post on Zulip Reid Barton (Jul 06 2020 at 21:43):

See data.opposite for example

view this post on Zulip Pedro Minicz (Jul 06 2020 at 21:43):

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

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Pedro Minicz (Jul 06 2020 at 21:53):

Yakov Pechersky said:

and was it left-binding or right-binding?

I am not sure.

view this post on Zulip 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