## Stream: general

### Topic: chaining equalities

#### Kevin Buzzard (Apr 03 2022 at 17:10):

Implementation of cool maths notation $a=b=c$:

import tactic

universe u

structure all_three_are_equal {α : Sort u} (a b c : α) : Prop :=
(hab : a = b)
(hbc : b = c)
(hac : a = c . tactic.interactive.cc)

notation a  =  b  =  c := all_three_are_equal a b c

#check 1 = 2 = 3 -- Prop


Should be fine, right? :-/

#### Kevin Buzzard (Apr 03 2022 at 17:13):

(My students keep wanting to do it) (hopefully next year I'll be teaching the course in Lean 4)

#### Trebor Huang (Apr 03 2022 at 17:25):

The next thing to do is all_four_are_equal, right? ;)

#### Reid Barton (Apr 03 2022 at 17:28):

Does this now break the ordinary =?

#### Kyle Miller (Apr 03 2022 at 17:50):

It's interesting how this gives you hac for transitivity.

Something I've thought about is having Lean parse chains of binary relations x1 R1 x2 R2 x3 R3 ... as x1 R1 x2 /\ x2 R2 x3 /\ x3 R3 x4 /\ .... That doesn't give you a way to get any consequences of transitivity though.

#### Patrick Johnson (Apr 03 2022 at 18:04):

import tactic

def eq' {α : Sort*} (s : list α) : Prop := ∀ (x y ∈ s), x = y
notation x  =  s:(foldr:50  =  (h t, h :: t) []) := eq' (x :: s)

example : 1 + 2 = 2 + 1 = 3 :=
by { rintro x hx y hy, simp * at * }


#### Kevin Buzzard (Apr 03 2022 at 19:13):

#check 1 = 1 -- eq' [1, 1] : Prop


erm...

#### Kyle Miller (Apr 03 2022 at 19:22):

There's precedent in languages to support special constructs like this to only a particular size (like Haskell and tuple notation). Maybe this is ok:

notation x1  =  x2  =  x3 := x1 = x2 ∧ x2 = x3
notation x1  =  x2  =  x3  =  x4 := x1 = x2 ∧ x2 = x3 = x4
notation x1  =  x2  =  x3  =  x4  =  x5 := x1 = x2 ∧ x2 = x3 = x4 = x5

example (x y z : ℕ) (h : x = y = z) : x = z :=
begin
-- prints as
-- h: x = y ∧ y = z
exact h.1.trans h.2,
end


Edit: This doesn't work for more than two equalities

#### Eric Wieser (Apr 03 2022 at 19:22):

Using docs#list.forall₂ would reduce better

(deleted)

#### Patrick Johnson (Apr 03 2022 at 19:31):

Kevin Buzzard said:

#check 1 = 1 -- eq' [1, 1] : Prop


erm...

That's easily fixable:

import tactic

def eq' {α : Sort*} (s : list α) : Prop := ∀ (x y ∈ s), x = y
notation x  =  y  =  s:(foldr:50  =  (h t, h :: t) []) := eq' (x :: y :: s)

#check 1 = 1      -- 1 = 1 : Prop
#check 1 = 1 = 1  -- eq' [1, 1, 1] : Prop


#### Patrick Johnson (Apr 03 2022 at 19:36):

I guess the question then is how to display eq' [1, 1, 1] as 1 = 1 = 1 in pp. I'm not sure.

#### Eric Wieser (Apr 03 2022 at 19:53):

Here's the version that reduces nicely:

def eq' {α : Sort*} : list α → Prop
| [] := true
| [x] := true
| [x, y] := x = y
| (x :: y :: z :: rest) :=
list.foldr (∧) (eq' (y :: z :: rest))  (list.map ((=) x) (y :: z :: rest))

notation x  =  s:(foldr:50  =  (h t, h :: t) []) := eq' (x :: s)

variables {w x y z : ℕ}

#reduce w = x = y = z
-- w = x ∧ w = y ∧ w = z ∧ x = y ∧ x = z ∧ y = z


#### Eric Wieser (Apr 03 2022 at 19:55):

Patrick Johnson said:

I guess the question then is how to display eq' [1, 1, 1] as 1 = 1 = 1 in pp. I'm not sure.

If you remove import tactic then pp does the right thing

#### Eric Wieser (Apr 03 2022 at 19:59):

In fact, import data.sym.basic is what breaks the pretty printing

#### Eric Wieser (Apr 03 2022 at 20:01):

notation x  =  y  =  s:(foldr:50  =  (h t, list.cons h t) []) := eq' (list.cons x $list.cons y$ s) fixes it, you have to disambiguate the ::

#### Eric Wieser (Apr 03 2022 at 20:05):

@Patrick Johnson, your definition is probably better than mine simply because it matches how docs#list.tfae is implemented (either that, or we should change tfae)

#### Kevin Buzzard (Apr 03 2022 at 20:05):

Eric Wieser said:

Here's the version that reduces nicely:

def eq' {α : Sort*} : list α → Prop
| [] := true
| [x] := true
| [x, y] := x = y
| (x :: y :: z :: rest) :=
list.foldr (∧) (eq' (y :: z :: rest))  (list.map ((=) x) (y :: z :: rest))

notation x  =  s:(foldr:50  =  (h t, h :: t) []) := eq' (x :: s)

variables {w x y z : ℕ}

#reduce w = x = y = z
-- w = x ∧ w = y ∧ w = z ∧ x = y ∧ x = z ∧ y = z


Surely "nicely" := "just need w=x, x=y, y=z"?

#### Eric Wieser (Apr 03 2022 at 20:06):

What's nice for production tends to be less nice for consumption

#### Eric Wieser (Apr 03 2022 at 20:07):

Probably you want some more recursion magic to convert what you describe into the long version

#### Eric Wieser (Apr 03 2022 at 20:09):

I guess the version you suggest is:

def eq' {α : Sort*} : list α → Prop
| [] := true
| [x] := true
| (x :: y :: rest) := list.foldr (∧) (x = y) (y :: rest)


(untested)

#### Yaël Dillies (Apr 03 2022 at 20:14):

Do you not simply want list.chain' (=)?

src#list.chain'

#### Eric Wieser (Apr 03 2022 at 20:17):

That's not defeq to and

#### Eric Wieser (Apr 03 2022 at 20:17):

Which may or may not matter

#### Patrick Johnson (Apr 03 2022 at 21:19):

Here is a proof that our definitions are equivalent.

Proof

Last updated: Dec 20 2023 at 11:08 UTC