Library Coq.Sorting.Permutation
List permutations as a composition of adjacent transpositions
Some facts about Permutation
Permutation over lists is a equivalence relation
Compatibility with others operations on lists
Theorem Permutation_in :
forall (
l l' :
list A) (
x :
A),
Permutation l l' ->
In x l ->
In x l'.
Lemma Permutation_app_tail :
forall (
l l' tl :
list A),
Permutation l l' ->
Permutation (
l++tl) (
l'++tl).
Lemma Permutation_app_head :
forall (
l tl tl' :
list A),
Permutation tl tl' ->
Permutation (
l++tl) (
l++tl').
Theorem Permutation_app :
forall (
l m l' m' :
list A),
Permutation l l' ->
Permutation m m' ->
Permutation (
l++m) (
l'++m').
Add Parametric Morphism : (@
app A)
with signature @
Permutation A ==> @
Permutation A ==> @
Permutation A
as Permutation_app'.
Qed.
Lemma Permutation_add_inside :
forall a (
l l' tl tl' :
list A),
Permutation l l' ->
Permutation tl tl' ->
Permutation (
l ++ a :: tl) (
l' ++ a :: tl').
Lemma Permutation_cons_append :
forall (
l :
list A)
x,
Permutation (
x :: l) (
l ++ x :: nil).
Local Hint Resolve Permutation_cons_append.
Theorem Permutation_app_comm :
forall (
l l' :
list A),
Permutation (
l ++ l') (
l' ++ l).
Local Hint Resolve Permutation_app_comm.
Theorem Permutation_cons_app :
forall (
l l1 l2:
list A)
a,
Permutation l (
l1 ++ l2) ->
Permutation (
a :: l) (
l1 ++ a :: l2).
Local Hint Resolve Permutation_cons_app.
Theorem Permutation_middle :
forall (
l1 l2:
list A)
a,
Permutation (
a :: l1 ++ l2) (
l1 ++ a :: l2).
Local Hint Resolve Permutation_middle.
Theorem Permutation_rev :
forall (
l :
list A),
Permutation l (
rev l).
Add Parametric Morphism : (@
rev A)
with signature @
Permutation A ==> @
Permutation A as Permutation_rev'.
Theorem Permutation_length :
forall (
l l' :
list A),
Permutation l l' ->
length l = length l'.
Theorem Permutation_ind_bis :
forall P :
list A ->
list A ->
Prop,
P [] [] ->
(
forall x l l',
Permutation l l' ->
P l l' ->
P (
x :: l) (
x :: l')) ->
(
forall x y l l',
Permutation l l' ->
P l l' ->
P (
y :: x :: l) (
x :: y :: l')) ->
(
forall l l' l'',
Permutation l l' ->
P l l' ->
Permutation l' l'' ->
P l' l'' ->
P l l'') ->
forall l l',
Permutation l l' ->
P l l'.
Ltac break_list l x l' H :=
destruct l as [|
x l'];
simpl in *;
injection H;
intros;
subst;
clear H.
Theorem Permutation_nil_app_cons :
forall (
l l' :
list A) (
x :
A),
~ Permutation nil (
l++x::l').
Theorem Permutation_app_inv :
forall (
l1 l2 l3 l4:
list A)
a,
Permutation (
l1++a::l2) (
l3++a::l4) ->
Permutation (
l1++l2) (
l3 ++ l4).
Theorem Permutation_cons_inv :
forall l l' a,
Permutation (
a::l) (
a::l') ->
Permutation l l'.
Theorem Permutation_cons_app_inv :
forall l l1 l2 a,
Permutation (
a :: l) (
l1 ++ a :: l2) ->
Permutation l (
l1 ++ l2).
Theorem Permutation_app_inv_l :
forall l l1 l2,
Permutation (
l ++ l1) (
l ++ l2) ->
Permutation l1 l2.
Theorem Permutation_app_inv_r :
forall l l1 l2,
Permutation (
l1 ++ l) (
l2 ++ l) ->
Permutation l1 l2.
Lemma Permutation_length_1_inv:
forall a l,
Permutation [a] l ->
l = [a].
Lemma Permutation_length_1:
forall a b,
Permutation [a] [b] ->
a = b.
Lemma Permutation_length_2_inv :
forall a1 a2 l,
Permutation [a1;a2] l ->
l = [a1;a2] \/ l = [a2;a1].
Lemma Permutation_length_2 :
forall a1 a2 b1 b2,
Permutation [a1;a2] [b1;b2] ->
a1 = b1 /\ a2 = b2 \/ a1 = b2 /\ a2 = b1.
Lemma NoDup_Permutation :
forall l l',
NoDup l ->
NoDup l' -> (
forall x:
A,
In x l <-> In x l') ->
Permutation l l'.
End Permutation_properties.
Section Permutation_map.
Variable A B :
Type.
Variable f :
A ->
B.
Add Parametric Morphism : (
map f)
with signature (@
Permutation A) ==> (@
Permutation B) as Permutation_map_aux.
Lemma Permutation_map :
forall l l',
Permutation l l' ->
Permutation (
map f l) (
map f l').
End Permutation_map.