noncomm_ring list of commuting

Stream: general

[Jireh Loreaux]

@Oliver Nash how hard do you think it would be to make it so that you could pass noncomm_ring a list of proofs that certain pairs of elements commute and it could use these? I don't have an explicit use case in mind at the moment, but I foresee it becoming quite useful as we embark into operator algebras.

[Oliver Nash]

I know very little about tactic writing. I did open the PR that added the noncomm_ring tactic but it was mostly @Scott Morrison who wrote it. Note that unlike ring it is a very simple tactic since not much is true without commutativity. Take a look and see.

[Oliver Nash]

It sounds like what you have in mind might well be served by just using good old simp.

[Oliver Nash]

To answer your question directly, it would very easy to have noncomm_ring accept a list of additional lemmas to try and apply but until we have some examples, I can't tell whether it would be worth allowing this.

[Oliver Nash]

Incidentally the tests are a good place to get a sense of what this tactic can solve at the moment.