Zulip Chat Archive

Stream: new members

Topic: Redefine precedence of `infix`


view this post on Zulip Pedro Minicz (Jul 28 2020 at 03:26):

How can I redefine the precedence of infixr declarations? I want to make A ⇒ B :: Γ parse as (A ⇒ B) :: Γ in a file where logic.relator is imported (via other imports).

import logic.relator

-- _ `⇒`:40 _:39 := relator.lift_fun #1 #0
#print notation 

-- Works, but parenthesis are needed.
infixr `` := (+)
#print notation  -- _ `⇒`:40 _:39
#check (1  2) :: []

-- Doesn't work.
#print notation  -- _ `⇒`:40 _:39
infixr ``:80 := (+)

-- Works, but parenthesis are still needed
notation A ``:80 B := A + B
#print notation  -- _ `⇒`:80 _:39
#check (1  2) :: []

view this post on Zulip Yury G. Kudryashov (Jul 28 2020 at 03:33):

As far as I understand (I may be wrong) once the precedence is defined, you can't redefine it.

view this post on Zulip Yury G. Kudryashov (Jul 28 2020 at 03:34):

But you can use another symbol.

view this post on Zulip Utensil Song (Jul 28 2020 at 03:51):

I have a related issue, (\wedge) is reserved in init.core:

reserve infixr `  `:35

I need it as wedge product (in exterior algebra), and I don't understand why it's right-associative, and I want a similar precedence to *.

view this post on Zulip Utensil Song (Jul 28 2020 at 03:52):

I got the following #mwe working but I don't know if it's idiomatic or if there would be consequences:

import tactic.localized
open tactic

universe u

namespace domain

class has_wedge (α : Type u) := (wedge : α  α  α)

localized "infix ∧:70 := has_wedge.wedge" in domain

end domain

namespace userland

open domain
open_locale domain

-- I'm being lazy here to define a dummy wedge
instance nat.to_has_wedge : has_wedge  := {
  wedge := (*)
}

#eval 2  3 -- 6

end userland

view this post on Zulip Utensil Song (Jul 28 2020 at 03:55):

A direct consequence is that I can't use "logical and" in userland anymore.

view this post on Zulip Pedro Minicz (Jul 28 2020 at 03:57):

Yury G. Kudryashov said:

As far as I understand (I may be wrong) once the precedence is defined, you can't redefine it.

Precedence can be redefined. I have improved the example a little, to show what Lean thinks the precedence is in each stage.

view this post on Zulip Pedro Minicz (Jul 28 2020 at 03:58):

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Substitution.20notation/near/202767176

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

If you can't get it to work maybe using a slightly different symbol like curly logical and would be a workaround? (or of course my favourite, U+1F9C0 :cheese: CHEESE WEDGE)

view this post on Zulip Yury G. Kudryashov (Jul 28 2020 at 04:00):

@Pedro Minicz Then I was wrong.

view this post on Zulip Yury G. Kudryashov (Jul 28 2020 at 04:01):

I don't think that reusing a symbol for two different operations is a good idea.

view this post on Zulip Yury G. Kudryashov (Jul 28 2020 at 04:03):

I mean, we have lots of this in mathematics but I think that in Lean we should try to come up with different notation each time.

view this post on Zulip Yury G. Kudryashov (Jul 28 2020 at 04:03):

Or at least with a notation that does not conflict with core notation.

view this post on Zulip Yury G. Kudryashov (Jul 28 2020 at 04:05):

I mean, it's possibly OK to have two conflicting localized notations in different areas of mathematics but reusing core notation is probably a bad idea.

view this post on Zulip Utensil Song (Jul 28 2020 at 04:10):

OK, I can live with

-- \curlywedge ⋏
-- \curlyvee ⋎

but I wonder if the situation is changed in Lean 4

view this post on Zulip Pedro Minicz (Jul 28 2020 at 04:29):

Yury G. Kudryashov said:

I don't think that reusing a symbol for two different operations is a good idea.

I agree with that. The thing is, I am never using relator.lift_fun in my current project, so the notation being taken is just an undesirable side-effect of using mathlib.

view this post on Zulip Yury G. Kudryashov (Jul 28 2020 at 04:52):

Possibly should be made a localized notation in mathlib.

view this post on Zulip Eric Wieser (Jul 28 2020 at 06:52):

In @Utensil Song's case, the two operator uses could be distinguished by type alone - is this something lean could handle, where if it fails to find has_and, it tries a new operator precedence / associativity and tries has_wedge?

view this post on Zulip Utensil Song (Jul 28 2020 at 07:06):

My experiment shows that Lean is not smart enough to do "notation polymorphism".

view this post on Zulip Yury G. Kudryashov (Jul 28 2020 at 07:11):

Of course, we can misuse has_and for wedge but this seems strange.

view this post on Zulip Utensil Song (Jul 28 2020 at 07:17):

lemma dummy : 2  3 = 6 := rfl

/-
failed to synthesize type class instance for
⊢ has_wedge Prop
-/
lemma dummy' : (2  3 = 6)  (2  9 = 18) := sorry

view this post on Zulip Utensil Song (Jul 28 2020 at 07:20):

Yury G. Kudryashov said:

Of course, we can misuse has_and for wedge but this seems strange.

We can't since we need another bunch of structures on has_wedge and should not apply to has_and......

view this post on Zulip Eric Wieser (Jul 28 2020 at 07:23):

I'm inclined to agree with Yury - if we're willing to accept weird precedence and associativity, aliasing has_wedge to has_and would work just fine - the structure isn't attached to the operators anyway, just like add_monoid contains the structure you'd expect to associate with has_add.

view this post on Zulip Johan Commelin (Jul 28 2020 at 07:33):

Maybe we should rename the class to has_wedge :grinning:

view this post on Zulip Utensil Song (Jul 28 2020 at 07:43):

@Eric Wieser Unfortunately we can't accept weird precedence and associativity, they would cause much more problem than a clean slate like using and .

view this post on Zulip Utensil Song (Jul 28 2020 at 07:45):

Of course, we can experiment to see how far it can go, the above is just an intuition, and it's better to avoid the problems for now and focus on what matters.


Last updated: May 14 2021 at 02:15 UTC