Library Coq.Sorting.PermutEq


Require Import Relations Setoid SetoidList List Multiset PermutSetoid Permutation Lia.

Set Implicit Arguments.

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 Permutation.Permutation and PermutSetoid.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.