# Library Coq.Sorting.PermutEq

This file is similar to PermutSetoid, except that the equality used here is Coq usual one instead of a setoid equality. In particular, we can then prove the equivalence between List.Permutation and Permutation.permutation.

Section Perm.

Variable A : Type.
Hypothesis eq_dec : forall x y:A, {x=y} + {~ x=y}.

Notation permutation := (permutation _ eq_dec).
Notation list_contents := (list_contents _ eq_dec).

we can use multiplicity to define In and NoDup.

Lemma multiplicity_In :
forall l a, In a l <-> 0 < multiplicity (list_contents l) a.

Lemma multiplicity_In_O :
forall l a, ~ In a l -> multiplicity (list_contents l) a = 0.

Lemma multiplicity_In_S :
forall l a, In a l -> multiplicity (list_contents l) a >= 1.

Lemma multiplicity_NoDup :
forall l, NoDup l <-> (forall a, multiplicity (list_contents l) a <= 1).

Lemma NoDup_permut :
forall l l', NoDup l -> NoDup l' ->
(forall x, In x l <-> In x l') -> permutation l l'.

Permutation is compatible with In.
Lemma permut_In_In :
forall l1 l2 e, permutation l1 l2 -> In e l1 -> In e l2.

Lemma permut_cons_In :
forall l1 l2 e, permutation (e :: l1) l2 -> In e l2.

Permutation of an empty list.
Lemma permut_nil :
forall l, permutation l nil -> l = nil.

When used with eq, this permutation notion is equivalent to the one defined in List.v.

Lemma permutation_Permutation :
forall l l', Permutation l l' <-> permutation l l'.

Permutation for short lists.

Lemma permut_length_1:
forall a b, permutation (a :: nil) (b :: nil) -> a=b.

Lemma permut_length_2 :
forall a1 b1 a2 b2, permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil) ->
(a1=a2) /\ (b1=b2) \/ (a1=b2) /\ (a2=b1).

Permutation is compatible with length.
Lemma permut_length :
forall l1 l2, permutation l1 l2 -> length l1 = length l2.

Variable B : Type.
Variable eqB_dec : forall x y:B, { x=y }+{ ~x=y }.

Permutation is compatible with map.

Lemma permutation_map :
forall f l1 l2, permutation l1 l2 ->
PermutSetoid.permutation _ eqB_dec (map f l1) (map f l2).

End Perm.