Are there any tactics/tools/libraries for fully automating proofs about `Permutation`

s 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.
```

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

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