chaining equalities

Stream: general

[Kevin Buzzard]

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]

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

[Trebor Huang]

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

[Reid Barton]

Does this now break the ordinary =?

[Kyle Miller]

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]

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]

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

erm...

[Kyle Miller]

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]

Using docs#list.forall₂ would reduce better

[Eric Wieser]

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

[Eric Wieser]

(deleted)

[Patrick Johnson]

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]

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]

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]

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]

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

[Eric Wieser]

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]

@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]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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]

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

[Eric Wieser]

src#list.chain'

[Eric Wieser]

That's not defeq to and

[Eric Wieser]

Which may or may not matter

[Patrick Johnson]

Here is a proof that our definitions are equivalent.

Proof

import tactic
import tactic.induction

def eq₁ {α : Sort*} (s : list α) : Prop := ∀ (x y ∈ s), x = y

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

lemma eq_of_eq_cons {α : Sort*} {s : list α} {x : α}
  (h : eq₁ (x :: s)) : eq₁ s :=
λ a ha b hb, h a (by simp [ha]) b (by simp [hb])

lemma foldr_true {s : list Prop} :
  list.foldr and true s ↔ ∀ (P ∈ s), P :=
begin
  induction' s, { simp }, rw list.foldr, split; intro h,
  { rintro P h₁, cases h₁, { rw h₁, exact h.1 }, { apply ih.mp h.2 P h₁ } },
  { split, { apply h, simp }, { apply ih.mpr, rintro P h₁, apply h, simp [h₁] }},
end

lemma list_mem_cons_dup {α : Sort*} {s : list α} {x hd : α} :
  x ∈ (hd :: hd :: s) ↔ x ∈ (hd :: s) :=
by simp [list.mem_cons_iff]

lemma eq_cons_dup {α : Sort*} {s : list α} {hd : α} :
  eq₁ (hd :: hd :: s) ↔ eq₁ (hd :: s) :=
by simp [eq₁, list_mem_cons_dup]

lemma foldr_true_z {s : list Prop} {P : Prop}
  (h : list.foldr and P s) : P :=
by { induction' s, { exact h }, { exact ih h.2 }}

lemma eq_aux {α : Sort*} {s : list α} {x : α} :
  eq₁ (x :: s) ↔ list.foldr and (eq₁ s) (list.map (eq x) s) :=
begin
  induction' s, { simp [eq₁] },
  rw [list.map_cons, list.foldr_cons], split; intro h,
  { use h x (by simp) hd (by simp), have h₁ := eq_of_eq_cons h,
    have h₂ := eq_of_eq_cons h₁, have h₃ := ih.mp h₁,
    rw iff_of_true h₂ trivial at h₃, rw iff_of_true h₁ trivial,
    rw foldr_true at h₃ ⊢, rintro P hP, apply h₃,
    rw list.mem_map at hP ⊢, rcases hP with ⟨y, hy, rfl⟩,
    use [y, hy], ext, split; rintro rfl,
    { exact h x (by simp) hd (by simp) },
    { exact h hd (by simp) x (by simp) }},
  { rcases h with ⟨rfl, h⟩, rw eq_cons_dup, apply ih.mpr,
    have h₁ := foldr_true_z h, have h₂ := eq_of_eq_cons h₁,
    rw iff_of_true h₁ trivial at h, rwa iff_of_true h₂ trivial },
end

theorem eq₁_eq₂ {α : Sort*} {s : list α} : eq₁ s ↔ eq₂ s :=
begin
  induction' s, { simp [eq₁, eq₂] },
  cases' s with x s, { simp [eq₁, eq₂], },
  cases' s with y s, { simp [eq₁, eq₂], exact λ h, h.symm },
  rw [eq₂, ←ih, eq_aux],
end