isolate instances about Permutation and PermutationA which may slow rewrite

 After discovering a rewrite in Ergo that takes a loooong time due
 to a bad interaction with the instances of Permutation and PermutationA :

 - PermutationA is now in a separate file SetoidPermutation
 - File Permutation.v isn't Require'd by SetoidList anymore
   nor MergeSort.v, just the definitions in Sorted.v
 - Attempt to put a priority on these instances.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15584 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 135 insertions, 120 deletions

diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 6ad232b5f..0f21c082b 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -411,6 +411,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Lists/List.v
     theories/Lists/ListSet.v
     theories/Lists/SetoidList.v
+    theories/Lists/SetoidPermutation.v
     theories/Lists/Streams.v
     theories/Lists/StreamMemo.v
     theories/Lists/ListTactics.v
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index f6eab8649..7d3c383c1 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -7,7 +7,7 @@
 (***********************************************************************)
 
 Require Export List.
-Require Export Sorting.
+Require Export Sorted.
 Require Export Setoid Basics Morphisms.
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -908,118 +908,6 @@ Qed.
 
 End Find.
 
-(** Permutations of list modulo a setoid equality. *)
-(** Section contributed by Robbert Krebbers (Nijmegen University). *)
-
-Section Permutation.
-Context {A : Type} (eqA : relation A) (e : Equivalence eqA).
-
-Inductive PermutationA : list A -> list A -> Prop :=
-  | permA_nil: PermutationA nil nil
-  | permA_skip x₁ x₂ l₁ l₂ :
-     eqA x₁ x₂ -> PermutationA l₁ l₂ -> PermutationA (x₁ :: l₁) (x₂ :: l₂)
-  | permA_swap x y l : PermutationA (y :: x :: l) (x :: y :: l)
-  | permA_trans l₁ l₂ l₃ :
-     PermutationA l₁ l₂ -> PermutationA l₂ l₃ -> PermutationA l₁ l₃.
-Local Hint Constructors PermutationA.
-
-Global Instance: Equivalence PermutationA.
-Proof.
- constructor.
- - intro l. induction l; intuition.
- - intros l₁ l₂. induction 1; eauto. apply permA_skip; intuition.
- - exact permA_trans.
-Qed.
-
-Global Instance PermutationA_cons :
-  Proper (eqA ==> PermutationA ==> PermutationA) (@cons A).
-Proof.
- repeat intro. now apply permA_skip.
-Qed.
-
-Lemma PermutationA_app_head l₁ l₂ l :
-  PermutationA l₁ l₂ -> PermutationA (l ++ l₁) (l ++ l₂).
-Proof.
- induction l; trivial; intros. apply permA_skip; intuition.
-Qed.
-
-Global Instance PermutationA_app :
-  Proper (PermutationA ==> PermutationA ==> PermutationA) (@app A).
-Proof.
- intros l₁ l₂ Pl k₁ k₂ Pk.
- induction Pl.
- - easy.
- - now apply permA_skip.
- - etransitivity.
-   * rewrite <-!app_comm_cons. now apply permA_swap.
-   * rewrite !app_comm_cons. now apply PermutationA_app_head.
- - do 2 (etransitivity; try eassumption).
-   apply PermutationA_app_head. now symmetry.
-Qed.
-
-Lemma PermutationA_app_tail l₁ l₂ l :
-  PermutationA l₁ l₂ -> PermutationA (l₁ ++ l) (l₂ ++ l).
-Proof.
- intros E. now rewrite E.
-Qed.
-
-Lemma PermutationA_cons_append l x :
-  PermutationA (x :: l) (l ++ x :: nil).
-Proof.
- induction l.
- - easy.
- - simpl. rewrite <-IHl. intuition.
-Qed.
-
-Lemma PermutationA_app_comm l₁ l₂ :
-  PermutationA (l₁ ++ l₂) (l₂ ++ l₁).
-Proof.
- induction l₁.
- - now rewrite app_nil_r.
- - rewrite <-app_comm_cons, IHl₁, app_comm_cons.
-   now rewrite PermutationA_cons_append, <-app_assoc.
-Qed.
-
-Lemma PermutationA_cons_app l l₁ l₂ x :
-  PermutationA l (l₁ ++ l₂) -> PermutationA (x :: l) (l₁ ++ x :: l₂).
-Proof.
- intros E. rewrite E.
- now rewrite app_comm_cons, PermutationA_cons_append, <-app_assoc.
-Qed.
-
-Lemma PermutationA_middle l₁ l₂ x :
-  PermutationA (x :: l₁ ++ l₂) (l₁ ++ x :: l₂).
-Proof.
- now apply PermutationA_cons_app.
-Qed.
-
-Lemma PermutationA_equivlistA l₁ l₂ :
-  PermutationA l₁ l₂ -> equivlistA eqA l₁ l₂.
-Proof.
- induction 1.
- - reflexivity.
- - now apply equivlistA_cons_proper.
- - now apply equivlistA_permute_heads.
- - etransitivity; eassumption.
-Qed.
-
-Lemma NoDupA_equivlistA_PermutationA l₁ l₂ :
-  NoDupA eqA l₁ -> NoDupA eqA l₂ ->
-   equivlistA eqA l₁ l₂ -> PermutationA l₁ l₂.
-Proof.
-  intros Pl₁. revert l₂. induction Pl₁ as [|x l₁ E1].
-  - intros l₂ _ H₂. symmetry in H₂. now rewrite (equivlistA_nil_eq eqA).
-  - intros l₂ Pl₂ E2.
-    destruct (@InA_split _ eqA l₂ x) as [l₂h [y [l₂t [E3 ?]]]].
-    { rewrite <-E2. intuition. }
-    subst. transitivity (y :: l₁); [intuition |].
-    apply PermutationA_cons_app, IHPl₁.
-    now apply NoDupA_split with y.
-    apply equivlistA_NoDupA_split with x y; intuition.
-Qed.
-
-End Permutation.
-
 (** Compatibility aliases. [Proper] is rather to be used directly now.*)
 
 Definition compat_bool {A} (eqA:A->A->Prop)(f:A->bool) :=
diff --git a/theories/Lists/SetoidPermutation.v b/theories/Lists/SetoidPermutation.v
new file mode 100644
index 000000000..b0657b63a
--- /dev/null
+++ b/theories/Lists/SetoidPermutation.v
@@ -0,0 +1,125 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+Require Import SetoidList.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** Permutations of list modulo a setoid equality. *)
+
+(** Contribution by Robbert Krebbers (Nijmegen University). *)
+
+Section Permutation.
+Context {A : Type} (eqA : relation A) (e : Equivalence eqA).
+
+Inductive PermutationA : list A -> list A -> Prop :=
+  | permA_nil: PermutationA nil nil
+  | permA_skip x₁ x₂ l₁ l₂ :
+     eqA x₁ x₂ -> PermutationA l₁ l₂ -> PermutationA (x₁ :: l₁) (x₂ :: l₂)
+  | permA_swap x y l : PermutationA (y :: x :: l) (x :: y :: l)
+  | permA_trans l₁ l₂ l₃ :
+     PermutationA l₁ l₂ -> PermutationA l₂ l₃ -> PermutationA l₁ l₃.
+Local Hint Constructors PermutationA.
+
+Global Instance: Equivalence PermutationA.
+Proof.
+ constructor.
+ - intro l. induction l; intuition.
+ - intros l₁ l₂. induction 1; eauto. apply permA_skip; intuition.
+ - exact permA_trans.
+Qed.
+
+Global Instance PermutationA_cons :
+  Proper (eqA ==> PermutationA ==> PermutationA) (@cons A).
+Proof.
+ repeat intro. now apply permA_skip.
+Qed.
+
+Lemma PermutationA_app_head l₁ l₂ l :
+  PermutationA l₁ l₂ -> PermutationA (l ++ l₁) (l ++ l₂).
+Proof.
+ induction l; trivial; intros. apply permA_skip; intuition.
+Qed.
+
+Global Instance PermutationA_app :
+  Proper (PermutationA ==> PermutationA ==> PermutationA) (@app A).
+Proof.
+ intros l₁ l₂ Pl k₁ k₂ Pk.
+ induction Pl.
+ - easy.
+ - now apply permA_skip.
+ - etransitivity.
+   * rewrite <-!app_comm_cons. now apply permA_swap.
+   * rewrite !app_comm_cons. now apply PermutationA_app_head.
+ - do 2 (etransitivity; try eassumption).
+   apply PermutationA_app_head. now symmetry.
+Qed.
+
+Lemma PermutationA_app_tail l₁ l₂ l :
+  PermutationA l₁ l₂ -> PermutationA (l₁ ++ l) (l₂ ++ l).
+Proof.
+ intros E. now rewrite E.
+Qed.
+
+Lemma PermutationA_cons_append l x :
+  PermutationA (x :: l) (l ++ x :: nil).
+Proof.
+ induction l.
+ - easy.
+ - simpl. rewrite <-IHl. intuition.
+Qed.
+
+Lemma PermutationA_app_comm l₁ l₂ :
+  PermutationA (l₁ ++ l₂) (l₂ ++ l₁).
+Proof.
+ induction l₁.
+ - now rewrite app_nil_r.
+ - rewrite <-app_comm_cons, IHl₁, app_comm_cons.
+   now rewrite PermutationA_cons_append, <-app_assoc.
+Qed.
+
+Lemma PermutationA_cons_app l l₁ l₂ x :
+  PermutationA l (l₁ ++ l₂) -> PermutationA (x :: l) (l₁ ++ x :: l₂).
+Proof.
+ intros E. rewrite E.
+ now rewrite app_comm_cons, PermutationA_cons_append, <-app_assoc.
+Qed.
+
+Lemma PermutationA_middle l₁ l₂ x :
+  PermutationA (x :: l₁ ++ l₂) (l₁ ++ x :: l₂).
+Proof.
+ now apply PermutationA_cons_app.
+Qed.
+
+Lemma PermutationA_equivlistA l₁ l₂ :
+  PermutationA l₁ l₂ -> equivlistA eqA l₁ l₂.
+Proof.
+ induction 1.
+ - reflexivity.
+ - now apply equivlistA_cons_proper.
+ - now apply equivlistA_permute_heads.
+ - etransitivity; eassumption.
+Qed.
+
+Lemma NoDupA_equivlistA_PermutationA l₁ l₂ :
+  NoDupA eqA l₁ -> NoDupA eqA l₂ ->
+   equivlistA eqA l₁ l₂ -> PermutationA l₁ l₂.
+Proof.
+  intros Pl₁. revert l₂. induction Pl₁ as [|x l₁ E1].
+  - intros l₂ _ H₂. symmetry in H₂. now rewrite (equivlistA_nil_eq eqA).
+  - intros l₂ Pl₂ E2.
+    destruct (@InA_split _ eqA l₂ x) as [l₂h [y [l₂t [E3 ?]]]].
+    { rewrite <-E2. intuition. }
+    subst. transitivity (y :: l₁); [intuition |].
+    apply PermutationA_cons_app, IHPl₁.
+    now apply NoDupA_split with y.
+    apply equivlistA_NoDupA_split with x y; intuition.
+Qed.
+
+End Permutation.
diff --git a/theories/Lists/vo.itarget b/theories/Lists/vo.itarget
index adcfba495..04994f593 100644
--- a/theories/Lists/vo.itarget
+++ b/theories/Lists/vo.itarget
@@ -2,5 +2,6 @@ ListSet.vo
 ListTactics.vo
 List.vo
 SetoidList.vo
+SetoidPermutation.vo
 StreamMemo.vo
 Streams.vo
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
index fdfcd394a..eb769b77d 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -85,7 +85,7 @@ Instance Permutation_Equivalence A : Equivalence (@Permutation A) | 10 := {
   Equivalence_Transitive := @Permutation_trans A }.
 
 Instance Permutation_cons A :
- Proper (Logic.eq ==> @Permutation A ==> @Permutation A) (@cons A).
+ Proper (Logic.eq ==> @Permutation A ==> @Permutation A) (@cons A) | 10.
 Proof.
   repeat intro; subst; auto using perm_skip.
 Qed.
@@ -106,7 +106,7 @@ Proof.
 Qed.
 
 Global Instance Permutation_in' :
- Proper (Logic.eq ==> @Permutation A ==> iff) (@In A).
+ Proper (Logic.eq ==> @Permutation A ==> iff) (@In A) | 10.
 Proof.
   repeat red; intros; subst; eauto using Permutation_in.
 Qed.
@@ -138,7 +138,7 @@ Proof.
 Qed.
 
 Global Instance Permutation_app' :
- Proper (@Permutation A ==> @Permutation A ==> @Permutation A) (@app A).
+ Proper (@Permutation A ==> @Permutation A ==> @Permutation A) (@app A) | 10.
 Proof.
   repeat intro; now apply Permutation_app.
 Qed.
@@ -187,7 +187,7 @@ Proof.
 Qed.
 
 Global Instance Permutation_rev' :
- Proper (@Permutation A ==> @Permutation A) (@rev A).
+ Proper (@Permutation A ==> @Permutation A) (@rev A) | 10.
 Proof.
   repeat intro; now rewrite <- 2 Permutation_rev.
 Qed.
@@ -199,7 +199,7 @@ Proof.
 Qed.
 
 Global Instance Permutation_length' :
- Proper (@Permutation A ==> Logic.eq) (@length A).
+ Proper (@Permutation A ==> Logic.eq) (@length A) | 10.
 Proof.
   exact Permutation_length.
 Qed.
@@ -407,7 +407,7 @@ Proof.
 Qed.
 
 Global Instance Permutation_NoDup' :
- Proper (@Permutation A ==> iff) (@NoDup A).
+ Proper (@Permutation A ==> iff) (@NoDup A) | 10.
 Proof.
   repeat red; eauto using Permutation_NoDup.
 Qed.
@@ -426,7 +426,7 @@ Proof.
 Qed.
 
 Global Instance Permutation_map' :
-  Proper (@Permutation A ==> @Permutation B) (map f).
+  Proper (@Permutation A ==> @Permutation B) (map f) | 10.
 Proof.
   exact Permutation_map.
 Qed.