Require Import List Setoid Compare_dec Morphisms FinFun.
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.

Theorem Permutation_nil : forall (l : list A), Permutation [] l -> l = [].

Theorem Permutation_nil_cons : forall (l : list A) (x : A),
 ~ Permutation nil (x::l).

Theorem Permutation_refl : forall l : list A, Permutation l l.

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.

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.


Instance Permutation_Equivalence A : Equivalence (@Permutation A) | 10 := {
  Equivalence_Reflexive := @Permutation_refl A ;
  Equivalence_Symmetric := @Permutation_sym A ;
  Equivalence_Transitive := @Permutation_trans A }.

Instance Permutation_cons A :
 Proper (Logic.eq ==> @Permutation A ==> @Permutation A) (@cons A) | 10.

Section Permutation_properties.

Variable A:Type.

Implicit Types a b : A.
Implicit Types l m : list A.

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.

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.

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.

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_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 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 -> 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.

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.

Let adapt f n :=
 let m := f (S n) in if le_lt_dec m (f 0) then m else pred m.

Let adapt_injective f : Injective f -> Injective (adapt f).

Let 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.