Library Coq.Sorting.PermutSetoid
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.
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.
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.
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.