Library Coq.Sorting.PermutEq

Require Import Omega.
Require Import Relations.
Require Import Setoid.
Require Import List.
Require Import Multiset.
Require Import Permutation.

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 List.Permutation and Permutation.permutation.

Section Perm.

  Variable A : Set.
  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.
  Proof.
    induction l.
    simpl.
    split; inversion 1.
    simpl.
    split; intros.
    inversion_clear H.
    subst a0.
    destruct (eq_dec a a) as [_|H]; auto with arith; destruct H; auto.
    destruct (eq_dec a a0) as [H1|H1]; auto with arith; simpl.
    rewrite <- IHl; auto.
    destruct (eq_dec a a0); auto.
    simpl in H.
    right; rewrite IHl; auto.
  Qed.

  Lemma multiplicity_In_O :
    forall l a, ~ In a l -> multiplicity (list_contents l) a = 0.
  Proof.
    intros l a; rewrite multiplicity_In;
      destruct (multiplicity (list_contents l) a); auto.
    destruct 1; auto with arith.
  Qed.

  Lemma multiplicity_In_S :
    forall l a, In a l -> multiplicity (list_contents l) a >= 1.
  Proof.
    intros l a; rewrite multiplicity_In; auto.
  Qed.

  Lemma multiplicity_NoDup :
    forall l, NoDup l <-> (forall a, multiplicity (list_contents l) a <= 1).
  Proof.
    induction l.
    simpl.
    split; auto with arith.
    intros; apply NoDup_nil.
    split; simpl.
    inversion_clear 1.
    rewrite IHl in H1.
    intros; destruct (eq_dec a a0) as [H2|H2]; simpl; auto.
    subst a0.
    rewrite multiplicity_In_O; auto.
    intros; constructor.
    rewrite multiplicity_In.
    generalize (H a).
    destruct (eq_dec a a) as [H0|H0].
    destruct (multiplicity (list_contents l) a); auto with arith.
    simpl; inversion 1.
    inversion H3.
    destruct H0; auto.
    rewrite IHl; intros.
    generalize (H a0); auto with arith.
    destruct (eq_dec a a0); simpl; auto with arith.
  Qed.

  Lemma NoDup_permut :
    forall l l', NoDup l -> NoDup l' ->
      (forall x, In x l <-> In x l') -> permutation l l'.
  Proof.
    intros.
    red; unfold meq; intros.
    rewrite multiplicity_NoDup in H, H0.
    generalize (H a) (H0 a) (H1 a); clear H H0 H1.
    do 2 rewrite multiplicity_In.
    destruct 3; omega.
  Qed.
Permutation is compatible with In.
  Lemma permut_In_In :
    forall l1 l2 e, permutation l1 l2 -> In e l1 -> In e l2.
  Proof.
    unfold Permutation.permutation, meq; intros l1 l2 e P IN.
    generalize (P e); clear P.
    destruct (In_dec eq_dec e l2) as [H|H]; auto.
    rewrite (multiplicity_In_O _ _ H).
    intros.
    generalize (multiplicity_In_S _ _ IN).
    rewrite H0.
    inversion 1.
  Qed.

  Lemma permut_cons_In :
    forall l1 l2 e, permutation (e :: l1) l2 -> In e l2.
  Proof.
    intros; eapply permut_In_In; eauto.
    red; auto.
  Qed.
Permutation of an empty list.
  Lemma permut_nil :
    forall l, permutation l nil -> l = nil.
  Proof.
    intro l; destruct l as [ | e l ]; trivial.
    assert (In e (e::l)) by (red; auto).
    intro Abs; generalize (permut_In_In _ Abs H).
    inversion 1.
  Qed.
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'.
  Proof.
    split.
    induction 1.
    apply permut_refl.
    apply permut_cons; auto.
    change (permutation (y::x::l) ((x::nil)++y::l)).
    apply permut_add_cons_inside; simpl; apply permut_refl.
    apply permut_tran with l'; auto.
    revert l'.
    induction l.
    intros.
    rewrite (permut_nil (permut_sym H)).
    apply Permutation_refl.
    intros.
    destruct (In_split _ _ (permut_cons_In H)) as (h2,(t2,H1)).
    subst l'.
    apply Permutation_cons_app.
    apply IHl.
    apply permut_remove_hd with a; auto.
  Qed.
Permutation for short lists.

  Lemma permut_length_1:
    forall a b, permutation (a :: nil) (b :: nil) -> a=b.
  Proof.
    intros a b; unfold Permutation.permutation, meq; intro P;
      generalize (P b); clear P; simpl.
    destruct (eq_dec b b) as [H|H]; [ | destruct H; auto].
    destruct (eq_dec a b); simpl; auto; intros; discriminate.
  Qed.

  Lemma permut_length_2 :
    forall a1 b1 a2 b2, permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil) ->
      (a1=a2) /\ (b1=b2) \/ (a1=b2) /\ (a2=b1).
  Proof.
    intros a1 b1 a2 b2 P.
    assert (H:=permut_cons_In P).
    inversion_clear H.
    left; split; auto.
    apply permut_length_1.
    red; red; intros.
    generalize (P a); clear P; simpl.
    destruct (eq_dec a1 a) as [H2|H2];
      destruct (eq_dec a2 a) as [H3|H3]; auto.
    destruct H3; transitivity a1; auto.
    destruct H2; transitivity a2; auto.
    right.
    inversion_clear H0; [|inversion H].
    split; auto.
    apply permut_length_1.
    red; red; intros.
    generalize (P a); clear P; simpl.
    destruct (eq_dec a1 a) as [H2|H2];
      destruct (eq_dec b2 a) as [H3|H3]; auto.
    simpl; rewrite <- plus_n_Sm; inversion 1; auto.
    destruct H3; transitivity a1; auto.
    destruct H2; transitivity b2; auto.
  Qed.
Permutation is compatible with length.
  Lemma permut_length :
    forall l1 l2, permutation l1 l2 -> length l1 = length l2.
  Proof.
    induction l1; intros l2 H.
    rewrite (permut_nil (permut_sym H)); auto.
    destruct (In_split _ _ (permut_cons_In H)) as (h2,(t2,H1)).
    subst l2.
    rewrite app_length.
    simpl; rewrite <- plus_n_Sm; f_equal.
    rewrite <- app_length.
    apply IHl1.
    apply permut_remove_hd with a; auto.
  Qed.

  Variable B : Set.
  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).
  Proof.
    intros f; induction l1.
    intros l2 P; rewrite (permut_nil (permut_sym P)); apply permut_refl.
    intros l2 P.
    simpl.
    destruct (In_split _ _ (permut_cons_In P)) as (h2,(t2,H1)).
    subst l2.
    rewrite map_app.
    simpl.
    apply permut_add_cons_inside.
    rewrite <- map_app.
    apply IHl1; auto.
    apply permut_remove_hd with a; auto.
  Qed.

End Perm.