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'.
Global Instance Permutation_in' :
Proper (
Logic.eq ==> @
Permutation A ==> iff) (@
In A) | 10.
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').
Global Instance Permutation_app' :
Proper (@
Permutation A ==> @
Permutation A ==> @
Permutation A) (@
app A) | 10.
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 :
core.
Theorem Permutation_app_comm :
forall (
l l' :
list A),
Permutation (
l ++ l') (
l' ++ l).
Local Hint Resolve Permutation_app_comm :
core.
Lemma Permutation_app_rot :
forall l1 l2 l3:
list A,
Permutation (
l1 ++ l2 ++ l3) (
l2 ++ l3 ++ l1).
Local Hint Resolve Permutation_app_rot :
core.
Lemma Permutation_app_swap_app :
forall l1 l2 l3:
list A,
Permutation (
l1 ++ l2 ++ l3) (
l2 ++ l1 ++ l3).
Local Hint Resolve Permutation_app_swap_app :
core.
Lemma Permutation_app_middle :
forall l l1 l2 l3 l4,
Permutation (
l1 ++ l2) (
l3 ++ l4)
->
Permutation (
l1 ++ l ++ l2) (
l3 ++ l ++ l4).
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 :
core.
Lemma Permutation_Add a l l' :
Add a l l' -> Permutation (
a::l)
l'.
Theorem Permutation_middle :
forall (
l1 l2:
list A)
a,
Permutation (
a :: l1 ++ l2) (
l1 ++ a :: l2).
Local Hint Resolve Permutation_middle :
core.
Lemma Permutation_middle2 :
forall l1 l2 l3 a b,
Permutation (
a :: b :: l1 ++ l2 ++ l3) (
l1 ++ a :: l2 ++ b :: l3).
Local Hint Resolve Permutation_middle2 :
core.
Lemma Permutation_elt :
forall l1 l2 l1' l2' (
a:
A),
Permutation (
l1 ++ l2) (
l1' ++ l2')
->
Permutation (
l1 ++ a :: l2) (
l1' ++ a :: l2').
Theorem Permutation_rev :
forall (
l :
list A),
Permutation l (
rev l).
Global Instance Permutation_rev' :
Proper (@
Permutation A ==> @
Permutation A) (@
rev A) | 10.
Theorem Permutation_length :
forall (
l l' :
list A),
Permutation l l' -> length l = length l'.
Global Instance Permutation_length' :
Proper (@
Permutation A ==> Logic.eq) (@
length A) | 10.
Global Instance Permutation_Forall (
P :
A -> Prop) :
Proper (
(@
Permutation A) ==> Basics.impl) (
Forall P) | 10.
Global Instance Permutation_Exists (
P :
A -> Prop) :
Proper (
(@
Permutation A) ==> Basics.impl) (
Exists P) | 10.
Lemma Permutation_Forall2 (
P :
A -> B -> Prop) :
forall l1 l1' (
l2 :
list B),
Permutation l1 l1' -> Forall2 P l1 l2 ->
exists l2' :
list B, Permutation l2 l2' /\ Forall2 P l1' l2'.
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'.
Theorem Permutation_nil_app_cons :
forall (
l l' :
list A) (
x :
A),
~ Permutation nil (
l++x::l').
Ltac InvAdd :=
repeat (
match goal with
|
H:
Add ?
x _ (
_ :: _) |-
_ =>
inversion H;
clear H;
subst
end).
Ltac finish_basic_perms H :=
try constructor;
try rewrite perm_swap;
try constructor;
trivial;
(
rewrite <-
H;
now apply Permutation_Add) ||
(
rewrite H;
symmetry;
now apply Permutation_Add).
Theorem Permutation_Add_inv a l1 l2 :
Permutation l1 l2 -> forall l1' l2',
Add a l1' l1 -> Add a l2' l2 ->
Permutation l1' l2'.
Theorem Permutation_app_inv (
l1 l2 l3 l4:
list A)
a :
Permutation (
l1++a::l2) (
l3++a::l4)
-> Permutation (
l1++l2) (
l3 ++ l4).
Theorem Permutation_cons_inv l l' a :
Permutation (
a::l) (
a::l')
-> Permutation l l'.
Theorem Permutation_cons_app_inv 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 l l1 l2 :
Permutation (
l1 ++ l) (
l2 ++ l)
-> Permutation l1 l2.
Lemma Permutation_app_inv_m l l1 l2 l3 l4 :
Permutation (
l1 ++ l ++ l2) (
l3 ++ l ++ l4)
->
Permutation (
l1 ++ l2) (
l3 ++ l4).
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 Permutation_vs_elt_inv :
forall l l1 l2 a,
Permutation l (
l1 ++ a :: l2)
-> exists l' l'', l = l' ++ a :: l''.
Lemma Permutation_vs_cons_inv :
forall l l1 a,
Permutation l (
a :: l1)
-> exists l' l'', l = l' ++ a :: l''.
Lemma Permutation_vs_cons_cons_inv :
forall l l' a b,
Permutation l (
a :: b :: l')
->
exists l1 l2 l3, l = l1 ++ a :: l2 ++ b :: l3 \/ l = l1 ++ b :: l2 ++ a :: l3.
Lemma NoDup_Permutation l l' :
NoDup l -> NoDup l' ->
(forall x:
A,
In x l <-> In x l') -> Permutation l l'.
Lemma NoDup_Permutation_bis l l' :
NoDup l ->
length l' <= length l -> incl l l' -> Permutation l l'.
Lemma Permutation_NoDup l l' :
Permutation l l' -> NoDup l -> NoDup l'.
Global Instance Permutation_NoDup' :
Proper (@
Permutation A ==> iff) (@
NoDup A) | 10.
End Permutation_properties.
Section Permutation_map.
Variable A B :
Type.
Variable f :
A -> B.
Lemma Permutation_map l l' :
Permutation l l' -> Permutation (
map f l) (
map f l').
Global Instance Permutation_map' :
Proper (@
Permutation A ==> @
Permutation B) (
map f) | 10.
Lemma Permutation_map_inv :
forall l1 l2,
Permutation l1 (
map f l2)
-> exists l3, l1 = map f l3 /\ Permutation l2 l3.
Lemma Permutation_image :
forall a l l',
Permutation (
a :: l) (
map f l')
-> exists a', a = f a'.
Lemma Permutation_elt_map_inv:
forall l1 l2 l3 l4 a,
Permutation (
l1 ++ a :: l2) (
l3 ++ map f l4)
-> (forall b,
a <> f b) ->
exists l1' l2', l3 = l1' ++ a :: l2'.
Global Instance Permutation_flat_map (
g :
A -> list B) :
Proper (
(@
Permutation A) ==> (@
Permutation B)) (
flat_map g) | 10.
End Permutation_map.
Lemma nat_bijection_Permutation n f :
bFun n f ->
Injective f ->
let l :=
seq 0
n in Permutation (
map f l)
l.
Section Permutation_alt.
Variable A:
Type.
Implicit Type a :
A.
Implicit Type l :
list A.
Alternative characterization of permutation
via nth_error and nth
Permutation definition based on transpositions for induction with fixed length