Automated reasoning about list permutations

Using Coq
1

Are there any tactics/tools/libraries for fully automating proofs about Permutations on lists, for example, like this:

Lemma ex : forall A (a:list A) b c d e f,
    Permutation (a ++ b) c ->
    Permutation (d ++ e) f ->
    Permutation (a ++ d ++ e ++ b) (f ++ c).

In working with a few of these, I’ve developed tactics to help guide the proof (e.g. below), but it seems like it might be possible to implement some type of algorithm, kind of how lia works for arithmetic.

Proof.
    intros.
    permtrans (c ++ f).
    permtrans ((a ++ b) ++ f).
    rewrite <- (app_assoc).
    apply Permutation_app_head.
    permtrans (b ++ d ++ e).
    permtrans (d ++ b ++ e).
Qed.
2

You can look at this or that. They are far from perfect but both solve your goal. The first one requires decidable equality.
It would be very nice to have something closer to lia (sound, complete, even certified) but I am not aware of better developments.

1 Like
3

It’s also possible to use the AAC Tactics plugin, here is an example from the tutorial:

  Variables (X : Type) (l1 l2 l3 : list X).

  Goal Permutation (l1 ++ l2) (l2 ++ l1).
    aac_reflexivity.
  Qed.

  Hypothesis H : Permutation l1 l2.

  Goal Permutation (l1 ++ l3) (l3 ++ l2).
    aac_rewrite H.
    aac_reflexivity.
  Qed.

For this approach to work, there should be no occurrences of the cons/:: operator, and it probably doesn’t scale all that well to many list variables, but no decidable equality is required.

1 Like