Library Coq.Sorting.Permutation

Require Import Relations.
Require Import List.
Require Import Multiset.
Require Import 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

Set Implicit Arguments.

Section defs.

From lists to multisets


  Variable A : Set.
  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)).
  Proof.
    simple induction l; simpl in |- *; auto with datatypes.
    intros.
    apply meq_trans with
      (munion (singletonBag a) (munion (list_contents l0) (list_contents m)));
      auto with datatypes.
  Qed.

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.
  Proof.
    unfold permutation in |- *; auto with datatypes.
  Qed.

  Lemma permut_sym :
    forall l1 l2 : list A, permutation l1 l2 -> permutation l2 l1.
  Proof.
    unfold permutation, meq; intros; apply sym_eq; trivial.
  Qed.

  Lemma permut_tran :
    forall l m n:list A, permutation l m -> permutation m n -> permutation l n.
  Proof.
    unfold permutation in |- *; intros.
    apply meq_trans with (list_contents m); auto with datatypes.
  Qed.

  Lemma permut_cons :
    forall l m:list A,
      permutation l m -> forall a:A, permutation (a :: l) (a :: m).
  Proof.
    unfold permutation in |- *; simpl in |- *; auto with datatypes.
  Qed.

  Lemma permut_app :
    forall l l' m m':list A,
      permutation l l' -> permutation m m' -> permutation (l ++ m) (l' ++ m').
  Proof.
    unfold permutation in |- *; intros.
    apply meq_trans with (munion (list_contents l) (list_contents m));
      auto using permut_cons, list_contents_app with datatypes.
    apply meq_trans with (munion (list_contents l') (list_contents m'));
      auto using permut_cons, list_contents_app with datatypes.
    apply meq_trans with (munion (list_contents l') (list_contents m));
      auto using permut_cons, list_contents_app with datatypes.
  Qed.

  Lemma permut_add_inside :
    forall a l1 l2 l3 l4,
      permutation (l1 ++ l2) (l3 ++ l4) ->
      permutation (l1 ++ a :: l2) (l3 ++ a :: l4).
  Proof.
    unfold permutation, meq in *; intros.
    generalize (H a0); clear H.
    do 4 rewrite list_contents_app.
    simpl.
    destruct (eqA_dec a a0); simpl; auto with arith.
    do 2 rewrite <- plus_n_Sm; f_equal; auto.
  Qed.

  Lemma permut_add_cons_inside :
    forall a l l1 l2,
      permutation l (l1 ++ l2) ->
      permutation (a :: l) (l1 ++ a :: l2).
  Proof.
    intros;
      replace (a :: l) with (nil ++ a :: l); trivial;
        apply permut_add_inside; trivial.
  Qed.

  Lemma permut_middle :
    forall (l m:list A) (a:A), permutation (a :: l ++ m) (l ++ a :: m).
  Proof.
    intros; apply permut_add_cons_inside; auto using permut_sym, permut_refl.
  Qed.

  Lemma permut_sym_app :
    forall l1 l2, permutation (l1 ++ l2) (l2 ++ l1).
  Proof.
    intros l1 l2;
      unfold permutation, meq;
        intro a; do 2 rewrite list_contents_app; simpl;
          auto with arith.
  Qed.

  Lemma permut_rev :
    forall l, permutation l (rev l).
  Proof.
    induction l.
    simpl; trivial using permut_refl.
    simpl.
    apply permut_add_cons_inside.
    rewrite <- app_nil_end. trivial.
  Qed.

Some inversion results.

  Lemma permut_conv_inv :
    forall e l1 l2, permutation (e :: l1) (e :: l2) -> permutation l1 l2.
  Proof.
    intros e l1 l2; unfold permutation, meq; simpl; intros H a;
      generalize (H a); apply plus_reg_l.
  Qed.

  Lemma permut_app_inv1 :
    forall l l1 l2, permutation (l1 ++ l) (l2 ++ l) -> permutation l1 l2.
  Proof.
    intros l l1 l2; unfold permutation, meq; simpl;
      intros H a; generalize (H a); clear H.
    do 2 rewrite list_contents_app.
    simpl.
    intros; apply plus_reg_l with (multiplicity (list_contents l) a).
    rewrite plus_comm; rewrite H; rewrite plus_comm.
    trivial.
  Qed.

  Lemma permut_app_inv2 :
    forall l l1 l2, permutation (l ++ l1) (l ++ l2) -> permutation l1 l2.
  Proof.
    intros l l1 l2; unfold permutation, meq; simpl;
      intros H a; generalize (H a); clear H.
    do 2 rewrite list_contents_app.
    simpl.
    intros; apply plus_reg_l with (multiplicity (list_contents l) a).
    trivial.
  Qed.

  Lemma permut_remove_hd :
    forall l l1 l2 a,
      permutation (a :: l) (l1 ++ a :: l2) -> permutation l (l1 ++ l2).
  Proof.
    intros l l1 l2 a; unfold permutation, meq; simpl; intros H a0; generalize (H a0); clear H.
    do 2 rewrite list_contents_app; simpl; intro H.
    apply plus_reg_l with (if eqA_dec a a0 then 1 else 0).
    rewrite H; clear H.
    symmetry; rewrite plus_comm.
    repeat rewrite <- plus_assoc; f_equal.
    apply plus_comm.
  Qed.

End defs.
For compatibilty
Notation permut_right := permut_cons.
Unset Implicit Arguments.