Require Import List Setoid.

Set Implicit Arguments.

Local Notation "[ ]" := nil.
Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..).

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.

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.


Local Hint Resolve perm_swap perm_trans.
Local Hint Resolve Permutation_sym Permutation_trans.


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

Add Parametric Morphism A (a:A) : (cons a)
  with signature @Permutation A ==> @Permutation A
  as Permutation_cons.

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

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.