equalities via equivalences

Stream: general

[Eric Wieser]

I've had multiple situations now where there are two possible ways I might want to state a lemma, where the second is just the first with the equivalence moved to the other side.

lemma foo : e x = y := sorry
lemma foo' : x = e.symm y := by simpa only [e.eq_symm_apply] using foo -- or whatever the lemma is really called

Depending on which way we want to rewrite, both versions are useful
Some places this comes up:

• associativity of the kronecker product, with e = matrix.reindex (equiv.prod_assoc _ _ _) (equiv.prod_assoc) (docs#matrix.kronecker_map_assoc)
• associativity of tuple concatenation, with e = fin.cast (add_assoc _ _ _)

Should we have a x =[e] y notation for this type of thing, so that foo.symm gives foo' and we don't have to state both?

[Patrick Massot]

That would be really hard to read.

[Eric Wieser]

The notation =[e] you mean?

[Patrick Massot]

Yes

[Eric Wieser]

Expanding on the above, with a different notation of x = y via e

class has_canonical_symm {α β : Type*} (f : α → β) (f_inv : out_param (β → α)) :=
(left_inv : left_inverse f_inv f)
(right_inv : right_inverse f_inv f)

def has_canonical_symm.equiv {α β : Type*} (f : α → β) {f_inv : out_param (β → α)}
  [has_canonical_symm f f_inv] : α ≃ β :=
⟨f, f_inv, has_canonical_symm.left_inv, has_canonical_symm.right_inv⟩

@[priority 1001]
instance has_canonical_symm.add_right_neg {A : Type*} [add_group A] (a : A) :
  has_canonical_symm (equiv.add_right (-a)) (equiv.add_right a) :=
⟨λ x, by simp, λ x, by simp⟩

instance has_canonical_symm.add_right {A : Type*} [add_group A] (a : A) :
  has_canonical_symm (equiv.add_right a) (equiv.add_right (-a)) :=
⟨λ x, by simp, λ x, by simp⟩

def eq_via {α β : Type*} (a : α) (b : β) (f : α → β) : Prop := f a = b

notation x ` = ` y ` via ` e := eq_via x y e

def eq_via.symm {α β : Type*} {a : α} {b : β} {f : α → β} {f_inv : β → α}
  [has_canonical_symm f f_inv] (h : a = b via f) : b = a via f_inv :=
((has_canonical_symm.equiv f).eq_symm_apply.mpr h).symm

variables (h : (1 : ℤ) = 2 via (equiv.add_right 1))

#check h  -- h : 1 = 2 via ⇑(equiv.add_right 1)
#check h.symm  -- h : 2 = 1 via ⇑(equiv.add_right (-1))
#check h.symm.symm  -- h : 1 = 2 via ⇑(equiv.add_right 1)

where has_canonical_symm is really just a generalization of docs#ring_hom_inv_pair

[Scott Morrison]

I really don't like = being the symbol here!

[Eric Wieser]

I'm not at all attached to =, if you suggest another symbol I'm happy to adjust the above; I'm asking more about whether this sort of API would be useful

[Scott Morrison]

Maybe something using ↦? But I might be dubious about this with any symbol.

[Gabriel Ebner]

To clarify, my thumbs-up is for ↦. That's the symbol I'd use on paper.

[Eric Wieser]

I suppose the other option is that eq_via.symm just becomes dot notation on eq

[Eric Wieser]

Then we don't need any special syntax, but we still have something to conveniently turn x = f y into y = f_inv x

[Eric Wieser]

But I think that runs into unification trouble, since f is no longer distinguishable from y by the type alone

[Gabriel Ebner]

The advantage of a separate definition is that it is preserved by simp. f y can easily turn into x.

[Eric Wieser]

I adjusted the notation above. I also am sure the precedence is wrong, but that's a problem for if we think this is worth pursuing

[Sebastian Reichelt]

I'd vote for the original x =[e] y because it matches HoTT and it makes symmetry and transitivity really obvious. (But I'm not a mathlib contributor.)

[Eric Wieser]

The argument against that notation is that when e becomes long it becomes awfully hard to read x and y, which are arguably the interesting piece

[Sebastian Reichelt]

That's true. BTW, if e was an equality instead of an equivalence, it would be e ▸ x = y. Maybe it's possible to use something similar? Just an idea.

[Reid Barton]

Related, but using equalities instead of equivs:
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/heq.20alternative/near/213656799

[Eric Wieser]

Which is probably an argument against using = in this notation, since the meaning in that thread is probably closer to what you'd expect