Library Coq.Sorting.Permutation
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
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
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)).
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).
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.
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