Reducibility, rewrite etc

Stream: general

[Neil Strickland]

I am proving some lemmas about commuting elements. I define commute a b := a * b = b * a, then prove things like commute a b → commute a c → commute a (b * c); this seems like a very natural idiom to use. However, with this framework, if I have h : commute a b then rw [h] fails with rewrite tactic failed, lemma is not an equality nor a iff. It does not help to mark the definition of commute with @[reducible]. You can do change _ = _ at h, rw [h] but that is awkward. Is there a standard approach to this kind of thing?

[Kenny Lau]

@[algebra, class]
structure is_commutative : Π (α : Type u), (α → α → α) → Prop
fields:
is_commutative.comm : ∀ {α : Type u} (op : α → α → α) [c : is_commutative α op] (a b : α), op a b = op b a

[Kenny Lau]

it's already in core

[Kenny Lau]

I would just unfold commute

[Chris Hughes]

rw (show _ = _, from h) is what I would do.

[Neil Strickland]

is_commutative is universally quantified:

@[algebra] class is_commutative (α : Type u) (op : α → α → α) : Prop :=
(comm : ∀ a b, op a b = op b a)

I am looking at particular pairs of elements that commute even though they live in a noncommutative structure. I don't think that that is in core or mathlib at the moment.

[Sebastien Gouezel]

What about

def commute {α : Type*} [ring α] (a b : α) : Prop := a * b = b * a

lemma commute.eq {α : Type*} [ring α] {a b : α} (h : commute a b) : a * b = b * a := h

example {α : Type*} [ring α] {a b : α} (h : commute a b) : a * b = b * a :=
by rw h.eq

[Neil Strickland]

That's promising. I will try that.

[Kenny Lau]

maybe make it a structure once and for all