Library Coq.Sorting.Permutation



Require Import Relations List Multiset Arith.

This file define a notion of permutation for lists, based on multisets: there exists a permutation between two lists iff every elements have the same multiplicities in the two lists.

Unlike List.Permutation, the present notion of permutation requires a decidable equality. At the same time, this definition can be used with a non-standard equality, whereas List.Permutation cannot.

The present file contains basic results, obtained without any particular assumption on the decidable equality used.

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

Finally, file PermutEq concerns Coq equality : this file is similar to the previous one, but proves in addition that List.Permutation and permutation are equivalent in this context. x


Section defs.

From lists to multisets


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

  Let emptyBag := EmptyBag A.
  Let singletonBag := SingletonBag _ eqA_dec.

contents of a list

  Fixpoint list_contents (l:list A) : multiset A :=
    match l with
      | nil => emptyBag
      | a :: l => munion (singletonBag a) (list_contents l)
    end.

  Lemma list_contents_app :
    forall l m:list A,
      meq (list_contents (l ++ m)) (munion (list_contents l) (list_contents m)).


permutation: definition and basic properties


  Definition permutation (l m:list A) :=
    meq (list_contents l) (list_contents m).

  Lemma permut_refl : forall l:list A, permutation l l.

  Lemma permut_sym :
    forall l1 l2 : list A, permutation l1 l2 -> permutation l2 l1.

  Lemma permut_tran :
    forall l m n:list A, permutation l m -> permutation m n -> permutation l n.

  Lemma permut_cons :
    forall l m:list A,
      permutation l m -> forall a:A, permutation (a :: l) (a :: m).

  Lemma permut_app :
    forall l l' m m':list A,
      permutation l l' -> permutation m m' -> permutation (l ++ m) (l' ++ m').

  Lemma permut_add_inside :
    forall a l1 l2 l3 l4,
      permutation (l1 ++ l2) (l3 ++ l4) ->
      permutation (l1 ++ a :: l2) (l3 ++ a :: l4).

  Lemma permut_add_cons_inside :
    forall a l l1 l2,
      permutation l (l1 ++ l2) ->
      permutation (a :: l) (l1 ++ a :: l2).

  Lemma permut_middle :
    forall (l m:list A) (a:A), permutation (a :: l ++ m) (l ++ a :: m).

  Lemma permut_sym_app :
    forall l1 l2, permutation (l1 ++ l2) (l2 ++ l1).

  Lemma permut_rev :
    forall l, permutation l (rev l).

Some inversion results.

  Lemma permut_conv_inv :
    forall e l1 l2, permutation (e :: l1) (e :: l2) -> permutation l1 l2.

  Lemma permut_app_inv1 :
    forall l l1 l2, permutation (l1 ++ l) (l2 ++ l) -> permutation l1 l2.

  Lemma permut_app_inv2 :
    forall l l1 l2, permutation (l ++ l1) (l ++ l2) -> permutation l1 l2.

  Lemma permut_remove_hd :
    forall l l1 l2 a,
      permutation (a :: l) (l1 ++ a :: l2) -> permutation l (l1 ++ l2).

End defs.

For compatibilty
Notation permut_right := permut_cons.