Library Coq.Sorting.PermutSetoid


Require Import Lia Relations Multiset SetoidList.

This file is deprecated, use Permutation.v instead.
Indeed, this file defines a notion of permutation based on multisets (there exists a permutation between two lists iff every elements have the same multiplicity in the two lists) which requires a more complex apparatus (the equipment of the domain with a decidable equality) than Permutation in Permutation.v.
The relation between the two relations are in lemma permutation_Permutation.
File Permutation concerns Leibniz equality : it shows in particular that List.Permutation and permutation are equivalent in this context.

Set Implicit Arguments.

Local Notation "[ ]" := nil.
Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..).

Section Permut.

From lists to multisets


Variable A : Type.
Variable eqA : relation A.
Hypothesis eqA_equiv : Equivalence eqA.
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
  | [] => 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_trans :
  forall l m n:list A, permutation l m -> permutation m n -> permutation l n.

Lemma permut_cons_eq :
  forall l m:list A,
    permutation l m -> forall a a', eqA a a' -> permutation (a :: l) (a' :: m).

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_eq :
  forall a a' l1 l2 l3 l4, eqA a a' ->
    permutation (l1 ++ l2) (l3 ++ l4) ->
    permutation (l1 ++ a :: l2) (l3 ++ a' :: l4).

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_eq :
  forall a a' l l1 l2, eqA a a' ->
    permutation l (l1 ++ l2) ->
    permutation (a :: l) (l1 ++ a' :: l2).

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.

we can use multiplicity to define InA and NoDupA.

Fact if_eqA_then : forall a a' (B:Type)(b b':B),
 eqA a a' -> (if eqA_dec a a' then b else b') = b.

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

Lemma permut_remove_hd_eq :
  forall l l1 l2 a b, eqA a b ->
    permutation (a :: l) (l1 ++ b :: l2) -> permutation l (l1 ++ l2).

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

Fact if_eqA_else : forall a a' (B:Type)(b b':B),
 ~eqA a a' -> (if eqA_dec a a' then b else b') = b'.

Fact if_eqA_refl : forall a (B:Type)(b b':B),
 (if eqA_dec a a then b else b') = b.

PL: Inutilisable dans un rewrite sans un change prealable.

Global Instance if_eqA (B:Type)(b b':B) :
 Proper (eqA==>eqA==>@eq _) (fun x y => if eqA_dec x y then b else b').

Fact if_eqA_rewrite_l : forall a1 a1' a2 (B:Type)(b b':B),
 eqA a1 a1' -> (if eqA_dec a1 a2 then b else b') =
               (if eqA_dec a1' a2 then b else b').

Fact if_eqA_rewrite_r : forall a1 a2 a2' (B:Type)(b b':B),
 eqA a2 a2' -> (if eqA_dec a1 a2 then b else b') =
               (if eqA_dec a1 a2' then b else b').

Global Instance multiplicity_eqA (l:list A) :
 Proper (eqA==>@eq _) (multiplicity (list_contents l)).

Lemma multiplicity_InA :
  forall l a, InA eqA a l <-> 0 < multiplicity (list_contents l) a.

Lemma multiplicity_InA_O :
  forall l a, ~ InA eqA a l -> multiplicity (list_contents l) a = 0.

Lemma multiplicity_InA_S :
  forall l a, InA eqA a l -> multiplicity (list_contents l) a >= 1.

Lemma multiplicity_NoDupA : forall l,
  NoDupA eqA l <-> (forall a, multiplicity (list_contents l) a <= 1).

Permutation is compatible with InA.
Lemma permut_InA_InA :
  forall l1 l2 e, permutation l1 l2 -> InA eqA e l1 -> InA eqA e l2.

Lemma permut_cons_InA :
  forall l1 l2 e, permutation (e :: l1) l2 -> InA eqA e l2.

Permutation of an empty list.
Lemma permut_nil :
  forall l, permutation l [] -> l = [].

Permutation for short lists.

Lemma permut_length_1:
  forall a b, permutation [a] [b] -> eqA a b.

Lemma permut_length_2 :
  forall a1 b1 a2 b2, permutation [a1; b1] [a2; b2] ->
    (eqA a1 a2) /\ (eqA b1 b2) \/ (eqA a1 b2) /\ (eqA a2 b1).

Permutation is compatible with length.
Lemma permut_length :
  forall l1 l2, permutation l1 l2 -> length l1 = length l2.

Lemma NoDupA_equivlistA_permut :
  forall l l', NoDupA eqA l -> NoDupA eqA l' ->
    equivlistA eqA l l' -> permutation l l'.

End Permut.

Section Permut_map.

Variables A B : Type.

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

Variable eqB : B->B->Prop.
Hypothesis eqB_dec : forall x y:B, { eqB x y }+{ ~eqB x y }.
Hypothesis eqB_trans : Transitive eqB.

Permutation is compatible with map.

Lemma permut_map :
  forall f,
    (Proper (eqA==>eqB) f) ->
    forall l1 l2, permutation _ eqA_dec l1 l2 ->
      permutation _ eqB_dec (map f l1) (map f l2).

End Permut_map.

Require Import Permutation.

Section Permut_permut.

Variable A : Type.

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

Lemma Permutation_impl_permutation : forall l l',
  Permutation l l' -> permutation _ eqA_dec l l'.

Lemma permut_eqA : forall l l', Forall2 eqA l l' -> permutation _ eqA_dec l l'.

Lemma permutation_Permutation : forall l l',
  permutation _ eqA_dec l l' <->
  exists l'', Permutation l l'' /\ Forall2 eqA l'' l'.

End Permut_permut.