tactic#ring and monoid.pow

Stream: general

[Eric Wieser]

It looks like right now tactic#ring only works with monoid.has_pow, which means it doesn't work for things like docs#ulift.has_npow. How hard is this to fix?

[Eric Wieser]

Hmm, I can't make a #mwe, perhaps my problem in #13139 is to do with irreducibility

[Eric Wieser]

import algebra.ring.ulift
import tactic.ring

variables {R : Type*} [comm_ring R]

example (a : R)       : a^2 * a^3 = a * a^4 := by ring  -- ok
example (a : ulift R) : a^2 * a^3 = a * a^4 := by ring  -- fails

[Eric Wieser]

Ah, there we go, i forgot that a^2*a = a*a^2 was solvable by commutativity alone

[Anne Baanen]

There's also a monoid instance on ulift compatible with docs#ulift.has_pow right? Then the match P with `(monoid.has_pow) line can safely become is_def_eq P `(monoid.has_pow).

[Anne Baanen]

BTW, I believe the Coq community calls this design pattern "keyed matching": the key has_pow.pow should match literally while the has_pow instance should match by defeq.