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
contents of a list
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).
For compatibilty