Library Coq.Sorting.PermutSetoid



Require Import Omega Relations Multiset Permutation SetoidList.


This file contains additional results about permutations with respect to an setoid equality (i.e. an equivalence relation).

Section Perm.

Variable A : Type.
Variable eqA : relation A.
Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.

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

The following lemmas need some knowledge on eqA

Variable eqA_refl : forall x, eqA x x.
Variable eqA_sym : forall x y, eqA x y -> eqA y x.
Variable eqA_trans : forall x y z, eqA x y -> eqA y z -> eqA x z.

we can use multiplicity to define InA and NoDupA.

Lemma multiplicity_InA :
  forall l a, InA eqA a l <-> 0 < multiplicity (list_contents l) a.

Lemma multiplicity_InA_O :
  forall l a, ~ InA eqA a l -> multiplicity (list_contents l) a = 0.

Lemma multiplicity_InA_S :
  forall l a, InA eqA a l -> multiplicity (list_contents l) a >= 1.

Lemma multiplicity_NoDupA : forall l,
  NoDupA eqA l <-> (forall a, multiplicity (list_contents l) a <= 1).

Permutation is compatible with InA.
Lemma permut_InA_InA :
  forall l1 l2 e, permutation l1 l2 -> InA eqA e l1 -> InA eqA e l2.

Lemma permut_cons_InA :
  forall l1 l2 e, permutation (e :: l1) l2 -> InA eqA e l2.

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

Permutation for short lists.

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

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

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

Lemma NoDupA_equivlistA_permut :
  forall l l', NoDupA eqA l -> NoDupA eqA l' ->
    equivlistA eqA l l' -> permutation l l'.

Variable B : Type.
Variable eqB : B->B->Prop.
Variable eqB_dec : forall x y:B, { eqB x y }+{ ~eqB x y }.
Variable eqB_trans : forall x y z, eqB x y -> eqB y z -> eqB x z.

Permutation is compatible with map.

Lemma permut_map :
  forall f,
    (forall x y, eqA x y -> eqB (f x) (f y)) ->
    forall l1 l2, permutation l1 l2 ->
      Permutation.permutation _ eqB_dec (map f l1) (map f l2).

End Perm.