Applying commutativity in "normal form" order

Stream: metaprogramming / tactics

[Geoffrey Irving]

Say I have a term like a ∪ b ∪ c ∪ d ∪ a. I'd like to be able to automatically reassociate and commutate things so that the two as end up next to each other, so that I can then use a ∪ a = a. Is there a way to use simp, union_comm, and union_assoc to do this kind of sorting? I don't care what the order of the terms is, as long as there is some reasonable total order.

[Eric Wieser]

You'll need a simproc here I think

[Eric Wieser]

Where you check if Expr.lt says one is ordered before the other, and apply the comm lemma otherwise

[Henrik Böving]

You can use ac_nf for this assuming your operations implement the associativity and commutativity typeclaaa

[Geoffrey Irving]

Oh, neat! ac_nf is great. And then docs#union_right_idem can finish things off.

[Robin Arnez]

Oh it should do that itself using Std.IdempotentOp but it seems like that instance is missing...

[Robin Arnez]

Huh what

import Mathlib.Data.Set.Basic

instance : Std.IdempotentOp (Union.union : Set α → _ → _) := ⟨Set.union_self⟩

def test (a b c d : Set Nat) : a ∪ b ∪ c ∪ d ∪ a = a ∪ b ∪ c ∪ d := by
  ac_nf
  ac_nf

Shouldn't ac_nf be an idempotent op?

[Bhavik Mehta]

It looks like the first one isn't changing the rhs, which is surprising to me