Simp does not solve a comm/assoc problem

Stream: new members

[Henning Dieterichs]

Why does simp fail here with simplify tactic failed to simplify? Clearly, the goal should be solvable by applying comm and assoc:

example { α: Type } [ decidable_eq α ] (r11: finset α) (r12: finset α) (r13: finset α) (r21: finset α) (r22: finset α) (r23: finset α):
    r11 ∪ (r12 ∪ (r13 ∪ (r21 ∪ (r22 ∪ r23)))) = r11 ∪ (r21 ∪ (r12 ∪ (r22 ∪ (r13 ∪ r23)))) :=
begin
    simp [finset.union_comm, finset.union_assoc],
end

[Reid Barton]

Because the simp algorithm isn't complete for such problems with these lemmas. Try adding finset.union_left_comm

[Henning Dieterichs]

Thanks, that worked! I would have never figured that out.

[Mario Carneiro]

The key to using simp is to look at the state where it got stuck and apply a lemma that will make progress from that state

[Kevin Buzzard]

If you rewrite associativity a lot, you end up with a U (b U c) terms, and then you've lost your chance to commute a and b. You can check that union_left_comm and union_comm between them can commute everything even if you've been over-zealous with associativity on a large term.

[Reid Barton]

One way to say it is that adding union_left_comm fixes the critical pair between (a U b) U c -> (b U a) U c and (a U b) U c -> a U (b U c)

[Kevin Buzzard]

Is this some confluent rewriting terminology?

[Mario Carneiro]

https://en.wikipedia.org/wiki/Critical_pair_(logic)

[Reid Barton]

right

[Cody Roux]

https://arxiv.org/abs/1106.4448

[Reid Barton]

oh we actually have something like this too now

[Reid Barton]

docs#tactic.interactive.ac_reflexivity

[Reid Barton]

there's also docs#tactic.interactive.assoc_rewrite but it's for associativity only

[Reid Barton]

When I looked there were approximately 0 uses of assoc_rw in mathlib, but I've been using it on a branch and it's been great