Automation for list.perm

Stream: general

[Neil Strickland]

What's the best approach for this goal?

lemma L (a b c d : ℕ) :  ([a,b,c,d] : multiset ℕ) = ([d,a,c,b] : multiset ℕ) := sorry

Here is the proof that we want to synthesise, but of course we do not want to write it by hand.

begin
  apply quotient.sound,
  let h := calc
    [d,a,c,b] ≈ [a,d,c,b] : list.perm.swap a d [c,b]
    ... ≈ [a,c,d,b] : list.perm.skip a (list.perm.swap c d [b])
    ... ≈ [a,c,b,d] : list.perm.skip a (list.perm.skip c (list.perm.swap b d []))
    ... ≈ [a,b,c,d] : list.perm.skip a (list.perm.swap b c [d]),
  exact h.symm
end

The abel tactic can do it after a tiny translation:

begin
  change (multiset.cons a 0) +
         (multiset.cons b 0) +
         (multiset.cons c 0) +
         (multiset.cons d 0) =
         (multiset.cons d 0) +
         (multiset.cons a 0) +
         (multiset.cons c 0) +
         (multiset.cons b 0) ,
  abel,
end

Presumably it should be very easy to automate that first step. I might take it as a baby exercise in tactic programming if no one suggests any better approach.

[Johan Commelin]

@Neil Strickland Here's the same thing as your second version, but more concise

begin
  change {a} + {b} + {c} + {d} = {d} + {a} + {c} + {b},
  abel,
end

[Johan Commelin]

A little helper tactic would certainly be useful.