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

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) :=

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