Library Coq.Sorting.PermutSetoid
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 PermutEq concerns Leibniz equality : it shows in particular
that List.Permutation and permutation are equivalent in this context.
Local Notation "[ ]" :=
nil.
Local Notation "[ a ; .. ; b ]" := (
a :: .. (
b :: []) ..).
Section Permut.
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_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).
we can use multiplicity to define InA and NoDupA.
PL: Inutilisable dans un rewrite sans un change prealable.
Permutation is compatible with InA.
Permutation of an empty list.
Permutation for short lists.
Bug omega: le "set" suivant ne devrait pas etre necessaire
Bug omega: idem
Permutation is compatible with length.
Permutation is compatible with map.