# Zulip Chat Archive

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

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

(bad linkifier, https://leanprover-community.github.io/mathlib_docs/data/list/defs.html#list.forall%E2%82%82)

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

(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' (=)`

?

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

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