## Stream: new members

### Topic: Redefine precedence of infix

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


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

#### Yury G. Kudryashov (Jul 28 2020 at 03:34):

But you can use another symbol.

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

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


#### Utensil Song (Jul 28 2020 at 03:55):

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

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

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

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

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

#### Yury G. Kudryashov (Jul 28 2020 at 04:00):

@Pedro Minicz Then I was wrong.

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

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

#### Yury G. Kudryashov (Jul 28 2020 at 04:03):

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

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

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

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

#### Yury G. Kudryashov (Jul 28 2020 at 04:52):

Possibly ⇒ should be made a localized notation in mathlib.

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

#### Utensil Song (Jul 28 2020 at 07:06):

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

#### Yury G. Kudryashov (Jul 28 2020 at 07:11):

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

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


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

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

#### Johan Commelin (Jul 28 2020 at 07:33):

Maybe we should rename the class to has_wedge :grinning:

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

#### 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: Dec 20 2023 at 11:08 UTC