# Library Coq.Sorting.PermutEq

Require Import Relations Setoid SetoidList List Multiset PermutSetoid Permutation.
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.