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 ->
      Permutation.permutation _ eqB_dec (map f l1) (map f l2).

End Perm.