notation associativity

Stream: new members

[kana]

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]

btw I know about calc-mode

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

It is just for fun

[Alex J. Best]

There is infixr:

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

[kana]

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

[Alex J. Best]

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

[Alex J. Best]

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]

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]

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]

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]

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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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]

It's useful hearing about lt.trans_le -- I didn't realize the mixed transitivity lemmas were aliased.