Write a tactic for prooving if two lists are permutations

Question

I am a beginner and I would like to write a tactic for proving if two lists are permutations.

For example, I would like to check the tactic with :

Goal (Permutation (1::3::4::2::nil) (2::4::1::3::nil))

I have written a function to sort a list and to check if 2 lists are equals but I have some troubles to write a tactic.

Could you help me please?

Answer 1

Oh. By write a tactic I thought you meant write a decision procedure to automate your proofs. And I thought you were refering to the Permutation relation defined in Coq.Sorting.Permutation.

If you just want to prove that your lists are permutations of each other, you can do it like so:

Definition Permutation : list nat -> list nat -> Prop :=
  fun l1 l2 => EqualS (sortL l1) (sortL l2).

Goal Permutation (1 :: 3 :: 4 :: 2 :: nil) (2 :: 4 :: 1 :: 3 :: nil).
Proof. lazy. tauto. Qed.

The definition of True is

Inductive True : Prop :=
  | I : True.

If you want to prove something more general, like

forall n1 n2 n3 n4, Permutation (n1 :: n2 :: n3 :: n4 :: nil) (n4 :: n3 :: n2 :: n1 :: nil)

you'll have to prove some facts about your functions first, like, for example,

forall n1 n2 l1, sortL (n1 :: n2 :: l1) = sortL (n2 :: n1 :: l1)
forall n1 l1 l2, EqualS (n1 :: l1) (n1 :: l2) <-> EqualS l1 l2

and you'll have to rewrite with those.