Redefine precedence of `infix`

Stream: new members

[Pedro Minicz]

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) :: []

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

But you can use another symbol.

[Utensil Song]

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 *.

[Utensil Song]

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

[Utensil Song]

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

[Pedro Minicz]

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.

[Pedro Minicz]

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

[Alex J. Best]

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)

[Yury G. Kudryashov]

@Pedro Minicz Then I was wrong.

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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.

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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.

[Utensil Song]

OK, I can live with

-- \curlywedge ⋏
-- \curlyvee ⋎

but I wonder if the situation is changed in Lean 4

[Pedro Minicz]

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.

[Yury G. Kudryashov]

Possibly ⇒ should be made a localized notation in mathlib.

[Eric Wieser]

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?

[Utensil Song]

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

[Yury G. Kudryashov]

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

[Utensil Song]

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

[Utensil Song]

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

[Eric Wieser]

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.

[Johan Commelin]

Maybe we should rename the class to has_wedge :grinning:

[Utensil Song]

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

[Utensil Song]

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.