The Coq Proof Assistant

# Library Coq.Sorting.Permutation

# List permutations as a composition of adjacent transpositions

Require Import List Setoid Compare_dec Morphisms FinFun PeanoNat.
Import ListNotations. Set Implicit Arguments.
Section Permutation.
Variable A:Type.
Inductive Permutation : list A -> list A -> Prop :=
| perm_nil: Permutation [] []
| perm_skip x l l' : Permutation l l' -> Permutation (x::l) (x::l')
| perm_swap x y l : Permutation (y::x::l) (x::y::l)
| perm_trans l l' l'' :
Permutation l l' -> Permutation l' l'' -> Permutation l l''.
Local Hint Constructors Permutation : core.
Some facts about Permutation
Theorem Permutation_nil : forall (l : list A), Permutation [] l -> l = [].
Theorem Permutation_nil_cons : forall (l : list A) (x : A),
~ Permutation nil (x::l).
Permutation over lists is a equivalence relation
Theorem Permutation_refl : forall l : list A, Permutation l l.
Instance Permutation_refl' : Proper (Logic.eq ==> Permutation) id.
Theorem Permutation_sym : forall l l' : list A,
Permutation l l' -> Permutation l' l.
Theorem Permutation_trans : forall l l' l'' : list A,
Permutation l l' -> Permutation l' l'' -> Permutation l l''.
End Permutation.
#[global]
Hint Resolve Permutation_refl perm_nil perm_skip : core.
Local Hint Resolve perm_swap perm_trans : core.
Local Hint Resolve Permutation_sym Permutation_trans : core.
#[global]
Instance Permutation_Equivalence A : Equivalence (@Permutation A) := {
Equivalence_Reflexive := @Permutation_refl A ;
Equivalence_Symmetric := @Permutation_sym A ;
Equivalence_Transitive := @Permutation_trans A }.
Lemma Permutation_morph_transp A : forall P : list A -> Prop,
(forall a b l1 l2, P (l1 ++ a :: b :: l2) -> P (l1 ++ b :: a :: l2)) ->
Proper (@Permutation A ==> Basics.impl) P.
#[export]
Instance Permutation_cons A :
Proper (Logic.eq ==> @Permutation A ==> @Permutation A) (@cons A).
Section Permutation_properties.
Variable A B:Type.
Implicit Types a : A.
Implicit Types l m : list A.
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).
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').
#[export] Instance Permutation_app' :
Proper (@Permutation A ==> @Permutation A ==> @Permutation A) (@app A).
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).
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).
Global Instance Permutation_Exists (P : A -> Prop) :
Proper ((@Permutation A) ==> Basics.impl) (Exists P).
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).
Lemma Permutation_repeat x n l :
Permutation l (repeat x n) -> l = repeat x n.
Lemma Permutation_incl_cons_inv_r (l1 l2 : list A) a : incl l1 (a :: l2) ->
exists n l3, Permutation l1 (repeat a n ++ l3) /\ incl l3 l2.
Lemma Permutation_pigeonhole l1 l2 : incl l1 l2 -> length l2 < length l1 ->
exists a l3, Permutation l1 (a :: a :: l3).
Lemma Permutation_pigeonhole_rel (R : B -> A -> Prop) (l1 : list B) l2 :
Forall (fun b => Exists (R b) l2) l1 ->
length l2 < length l1 ->
exists b b' (l3 : list B), Permutation l1 (b :: b' :: l3) /\ exists a, In a l2 /\ R b a /\ R b' a.
Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}.
Lemma Permutation_count_occ l1 l2 :
Permutation l1 l2 <-> forall x, count_occ eq_dec l1 x = count_occ eq_dec l2 x.
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).
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).
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
Let adapt f n :=
let m := f (S n) in if le_lt_dec m (f 0) then m else pred m.
Local Definition adapt_injective f : Injective f -> Injective (adapt f).
Local Definition adapt_ok a l1 l2 f : Injective f -> length l1 = f 0 ->
forall n, nth_error (l1++a::l2) (f (S n)) = nth_error (l1++l2) (adapt f n).
Lemma Permutation_nth_error l l' :
Permutation l l' <->
(length l = length l' /\
exists f:nat->nat,
Injective f /\ forall n, nth_error l' n = nth_error l (f n)).
Lemma Permutation_nth_error_bis l l' :
Permutation l l' <->
exists f:nat->nat,
Injective f /\
bFun (length l) f /\
(forall n, nth_error l' n = nth_error l (f n)).
Lemma Permutation_nth l l' d :
Permutation l l' <->
(let n := length l in
length l' = n /\
exists f:nat->nat,
bFun n f /\
bInjective n f /\
(forall x, x < n -> nth x l' d = nth (f x) l d)).
End Permutation_alt.
#[global]
Instance Permutation_list_sum : Proper (@Permutation nat ==> eq) list_sum | 10.
#[global]
Instance Permutation_list_max : Proper (@Permutation nat ==> eq) list_max | 10.
Section Permutation_transp.
Variable A:Type.
Permutation definition based on transpositions for induction with fixed length
Inductive Permutation_transp : list A -> list A -> Prop :=
| perm_t_refl : forall l, Permutation_transp l l
| perm_t_swap : forall x y l1 l2, Permutation_transp (l1 ++ y :: x :: l2) (l1 ++ x :: y :: l2)
| perm_t_trans l l' l'' :
Permutation_transp l l' -> Permutation_transp l' l'' -> Permutation_transp l l''.
Instance Permutation_transp_sym : Symmetric Permutation_transp.
Global Instance Permutation_transp_equiv : Equivalence Permutation_transp | 100.
Lemma Permutation_transp_cons : forall (x : A) l1 l2,
Permutation_transp l1 l2 -> Permutation_transp (x :: l1) (x :: l2).
Lemma Permutation_Permutation_transp : forall l1 l2 : list A,
Permutation l1 l2 <-> Permutation_transp l1 l2.
Lemma Permutation_ind_transp : forall P : list A -> list A -> Prop,
(forall l, P l l) ->
(forall x y l1 l2, P (l1 ++ y :: x :: l2) (l1 ++ x :: y :: l2)) ->
(forall l l' l'',
Permutation l l' -> P l l' -> Permutation l' l'' -> P l' l'' -> P l l'') ->
forall l1 l2, Permutation l1 l2 -> P l1 l2.
End Permutation_transp.