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

[Casavaca]

Do we have chain equal in Lean 4? There's TFAE but that's for props.

[Mario Carneiro]

equalities are already all 'biconditional' so it's not nearly as involved to prove that several things are equal as it is with TFAE

[Mario Carneiro]

it basically comes down to a transitivity chain, and we have calc for that

[Asei Inoue]

I want this chaining equation notation.
Julia provides this to us.

[Alex J. Best]

@Asei Inoue do you mean https://docs.julialang.org/en/v1/manual/mathematical-operations/#Chaining-comparisons, it's much more helpful if you provide a reference, not everyone knows Julia

[Asei Inoue]

@Alex J. Best Thanks.

[Asei Inoue]

Is it as difficult to implement chaining equality as it was in Lean 3?

[Eric Wieser]

No, it's much easier to implement it in lean4 than it was in Lean 3

[Asei Inoue]

No, it's much easier to implement it in lean4 than it was in Lean 3

why we don't have chaining equality notation?

[Kyle Miller]

One thing to think about is that x < y < z ought to elaborate as let tmp := y; x < tmp ∧ tmp < z so that each argument evaluates at most once. That means you probably wouldn't use it theorem statements, instead just for programming.

[Asei Inoue]

so that each argument evaluates at most once. That means you probably wouldn't use it theorem statements, instead just for programming.

What makes this ingenuity necessary?

[Asei Inoue]

What is wrong if an argument is sometimes evaluated more than once?

[Kyle Miller]

Every language I know of that implements chained inequalities makes sure each argument is evaluated at most once (Julia and Python come to mind)

[Asei Inoue]

Can the implementation in Julia be imitated in Lean?

[Mario Carneiro]

In most cases I think the lean compiler doesn't need this ingenuity because it does CSE much more aggressively than non-FP languages

[Kyle Miller]

I suppose it works with do lifting too

[Mario Carneiro]

it doesn't work with dbg_trace but I think that's because dbg_trace is explicitly set to disable CSE

macro "chain" a:term:max b:term:max c:term:max : term => `($a < $b ∧ $b < $c)

def foo (a b : Nat) : Bool :=
  chain a (dbg_trace "hi"; 5) b

#eval foo 1 7
-- hi
-- hi
-- true

[Mario Carneiro]

macro "chain" a:term:max b:term:max c:term:max : term => `($a < $b ∧ $b < $c)

def bar (a : Nat) := dbg_trace "hi"; a
def foo (a b : Nat) : Bool :=
  chain a (bar 5) b

#eval foo 1 7
-- hi
-- true

[Eric Wieser]

Another trap is that (a = b) = (c = d) already means something else; and ≤ has a similar issue

[Eric Wieser]

But I think this is surmountable with a clever enough elaborator

[Eric Wieser]

It might require cooperation with the existing elaborators