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.
permtrans (c ++ f).
permtrans ((a ++ b) ++ f).
rewrite <- (app_assoc).
permtrans (b ++ d ++ e).
permtrans (d ++ b ++ e).
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.
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).
Hypothesis H : Permutation l1 l2.
Goal Permutation (l1 ++ l3) (l3 ++ l2).
For this approach to work, there should be no occurrences of the
:: operator, and it probably doesn’t scale all that well to many list variables, but no decidable equality is required.