# Zulip Chat Archive

## Stream: new members

### Topic: notation associativity

#### kana (Feb 19 2021 at 21:38):

Is there a way to mark `notation`

as right-associative?

something like

```
right notation a `+++` b := a + b
#reduce a +++ b +++ c -- a + (b + c)
```

I want to write this without parens:

```
notation x `≡⟨` a `⟩` b := eq.trans (a : x = _) b
notation a `∎` := refl a
variable p : 1 = 2
variable q : 2 = 3
def x : 1 = 3 :=
1 ≡⟨ p ⟩ (2
≡⟨ q ⟩ (3 ∎))
```

#### kana (Feb 19 2021 at 21:48):

btw I know about calc-mode

```
def y : 1 = 3 :=
calc 1 = 2 : p
... = 3 : q
```

It is just for fun

#### Alex J. Best (Feb 19 2021 at 21:48):

There is infixr:

```
infixr `+++ `:25 := (+)
variables (a b c : ℕ)
#reduce a +++ b +++ c -- a + (b + c)
```

#### kana (Feb 19 2021 at 21:50):

But `infixr`

is very limited and can be used only for operators, as I know.

#### Alex J. Best (Feb 19 2021 at 21:53):

Ah yes I didn't see that your actual example takes 3 inputs

#### Alex J. Best (Feb 19 2021 at 21:59):

Well you can set priorities on individual parts of the notation, I have no sense of what the correct ones are but this works:

```
notation x `≡⟨`:100 a ` ⟩ ` b := eq.trans (a : x = _) b
notation a `∎`:20 := refl a
variable p : 1 = 2
variable q : 2 = 3
def x : 1 = 3 :=
1 ≡⟨ p ⟩ 2
≡⟨ q ⟩ 3 ∎
```

#### kana (Feb 19 2021 at 22:17):

Thanks! It really works!

```
notation x `≡⟨`:10 a ` ⟩ ` b := eq.trans (a : x = _) b
notation a `∎`:2 := refl a
def agda_like (a b c : ℕ) : (a + b) + c = c + (b + a) :=
(a + b) + c ≡⟨ nat.add_assoc _ _ _ ⟩ a + (b + c)
≡⟨ congr rfl (nat.add_comm _ _) ⟩ a + (c + b)
≡⟨ nat.add_comm _ _ ⟩ (c + b) + a
≡⟨ nat.add_assoc _ _ _ ⟩ c + (b + a)
∎
def tactic_mode (a b c : ℕ) : (a + b) + c = c + (b + a) :=
by rw [ nat.add_assoc
, nat.add_comm b
, nat.add_comm
, nat.add_assoc ]
def calc_mode (a b c : ℕ) : (a + b) + c = c + (b + a) :=
calc (a + b) + c = a + (b + c) : by rw nat.add_assoc
... = a + (c + b) : by rw nat.add_comm c b
... = (c + b) + a : by rw nat.add_comm
... = c + (b + a) : by rw nat.add_assoc
```

#### Kyle Miller (Feb 19 2021 at 22:20):

It's equivalent, but for the `∎`

, you can use `postfix`

:

```
postfix `∎`:2 := eq.refl
```

(I'm not sure which you'd want, but you can also make this have higher precedence than the bracket notation.)

#### Kyle Miller (Feb 19 2021 at 22:55):

Here's an interesting alternative to the Agda-like notation:

```
infixl ` >>> `:50 := trans
prefix `=`:50 := refl
lemma with_trans_comp (a b c : ℕ) : (a + b) + c = c + (b + a) :=
= (a + b) + c >>> nat.add_assoc _ _ _ >>>
= a + (b + c) >>> congr rfl (nat.add_comm _ _) >>>
= a + (c + b) >>> nat.add_comm _ _ >>>
= (c + b) + a >>> nat.add_assoc _ _ _ >>>
= (c + (b + a))
```

Having prefix `=`

is certainly weird, but the main idea is to have a left-associative operator for composing transitive relations (I don't think one already exists?) and another operator to apply `refl`

so these hints can be easily inserted into the chain. It could just as easily be something like this:

```
infixl ` >>> `:50 := trans
postfix `∎`:51 := refl
lemma with_trans_comp (a b c : ℕ) : (a + b) + c = c + (b + a) :=
(a + b) + c ∎>>> nat.add_assoc _ _ _ >>>
a + (b + c) ∎>>> congr rfl (nat.add_comm _ _) >>>
a + (c + b) ∎>>> nat.add_comm _ _ >>>
(c + b) + a ∎>>> nat.add_assoc _ _ _ >>>
(c + (b + a)) ∎
```

#### Kyle Miller (Feb 19 2021 at 22:57):

What I think is interesting about it is that each individual part of the notation is useful by itself.

#### Mario Carneiro (Feb 20 2021 at 00:58):

the main idea is to have a left-associative operator for composing transitive relations (I don't think one already exists?)

Why does it have to be left associative? We do have a right associative operator for composing transitive relations: `(...).trans $ ...`

#### Kyle Miller (Feb 20 2021 at 03:26):

I thought maybe left associativity might help make nicer type errors while a proof is being written, but it's probably not actually the case.

That's true that `trans`

can be used like that, but I thought that there might be some generalized transitivity between different relations. Maybe something like this:

```
class has_rel_chain {α β γ : Type*} (r : α → β → Prop) (s : β → γ → Prop) (t : out_param $ α → γ → Prop) :=
(chain' {x : α} {y : β} {z : γ} (hxy : r x y) (hyz : s y z) : t x z)
lemma has_rel_chain.chain {α β γ : Type*} {r : α → β → Prop} {s : β → γ → Prop} {t : α → γ → Prop} [has_rel_chain r s t]
{x : α} {y : β} {z : γ} (hxy : r x y) (hyz : s y z) : t x z := has_rel_chain.chain' α β γ hxy hyz
infixr ` >>> `:50 := has_rel_chain.chain
instance has_rel_chain.eq₁ {α β : Type*} {r : α → β → Prop} : has_rel_chain eq r r :=
{ chain' := λ _ _ _ hxy hyz, by { rw hxy, exact hyz } }
instance has_rel_chain.eq₂ {α β : Type*} {r : α → β → Prop} : has_rel_chain r eq r :=
{ chain' := λ _ _ _ hxy hyz, by { rw ←hyz, exact hxy } }
instance has_rel_chain.trans {α : Type*} {r : α → α → Prop} [is_trans α r] : has_rel_chain r r r :=
{ chain' := λ _ _ _ hxy hyz, trans hxy hyz }
section
variables {α : Type*} [preorder α]
instance lt_of_lt_of_le.has_rel_chain : has_rel_chain ((<) : α → α → Prop) (≤) (<) :=
{ chain' := λ a b c (hab : a < b) (hbc : b ≤ c), lt_of_lt_of_le hab hbc }
instance lt_of_le_of_lt.has_rel_chain : has_rel_chain ((≤) : α → α → Prop) (<) (<) :=
{ chain' := λ a b c (hab : a ≤ b) (hbc : b < c), lt_of_le_of_lt hab hbc }
end
postfix ` ∎`:50 := eq.refl
def assert_rel {α β : Type*} (r : α → β → Prop) {a : α} {b : β} (h : r a b) := h
notation p `>>>[`:50 r `]` q := has_rel_chain.chain (assert_rel r p) q
example (a b c : ℕ) : (a + b) + c = c + (b + a) :=
(a + b) + c ∎>>> nat.add_assoc _ _ _
>>>[(=)] a + (b + c) ∎>>> congr rfl (nat.add_comm _ _)
>>>[(=)] a + (c + b) ∎>>> nat.add_comm _ _
>>>[(=)] (c + b) + a ∎>>> nat.add_assoc _ _ _
>>>[(=)] c + (b + a) ∎
-- The previous example but without the relation hints
example (a b c : ℕ) : (a + b) + c = c + (b + a) :=
(a + b) + c ∎>>> nat.add_assoc _ _ _ >>>
a + (b + c) ∎>>> congr rfl (nat.add_comm _ _) >>>
a + (c + b) ∎>>> nat.add_comm _ _ >>>
(c + b) + a ∎>>> nat.add_assoc _ _ _ >>>
c + (b + a) ∎
example (a : ℕ) (h : 1 ≤ a) : a ≤ a * a :=
a ∎>>> (nat.mul_one _).symm
>>>[(=)] a * 1 ∎>>> nat.mul_le_mul_left _ h
>>>[(≤)] a * a ∎
-- The previous example but without any hints
example (a : ℕ) (h : 1 ≤ a) : a ≤ a * a :=
(nat.mul_one _).symm >>> nat.mul_le_mul_left _ h
example (a b : ℕ) (h₁ : a < b) (h₂ : b ≤ 3) : a < 3 :=
h₁ >>> h₂
```

(The value/relation hints are just for fun, to see if it was possible using some composable operators. Something like `>>>`

seems potentially nice to have though.)

#### Mario Carneiro (Feb 20 2021 at 03:32):

Sebastian recently wrote something like this in the #lean4 stream for implementing `calc`

#### Mario Carneiro (Feb 20 2021 at 03:35):

You can actually get by pretty well using just dot notation to resolve different transitivity lemmas (possibly using `lt.trans_le`

for mixed transitivity lemmas), but probably if you need something this fancy you should just use `calc`

#### Kyle Miller (Feb 20 2021 at 03:48):

It's useful hearing about `lt.trans_le`

-- I didn't realize the mixed transitivity lemmas were aliased.

Last updated: Dec 20 2023 at 11:08 UTC