Imported Upstream version 8.4dfsgupstream/8.4dfsg

8 files changed, 281 insertions, 108 deletions

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index ecadddbc..69475a6f 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Le Gt Minus Bool.
+Require Import Le Gt Minus Bool Setoid.
 
 Set Implicit Arguments.
 
@@ -546,30 +546,21 @@ Section Elts.
     end.
 
   (** Compatibility of count_occ with operations on list *)
-  Theorem count_occ_In : forall (l : list A) (x : A), In x l <-> count_occ l x > 0.
+  Theorem count_occ_In (l : list A) (x : A) : In x l <-> count_occ l x > 0.
   Proof.
-    induction l as [|y l].
-    simpl; intros; split; [destruct 1 | apply gt_irrefl].
-    simpl. intro x; destruct (eq_dec y x) as [Heq|Hneq].
-    rewrite Heq; intuition.
-    pose (IHl x). intuition.
+    induction l as [|y l]; simpl.
+    - split; [destruct 1 | apply gt_irrefl].
+    - destruct eq_dec as [->|Hneq]; rewrite IHl; intuition.
   Qed.
 
-  Theorem count_occ_inv_nil : forall (l : list A), (forall x:A, count_occ l x = 0) <-> l = [].
+  Theorem count_occ_inv_nil (l : list A) :
+    (forall x:A, count_occ l x = 0) <-> l = [].
   Proof.
     split.
-    (* Case -> *)
-    induction l as [|x l].
-    trivial.
-    intro H.
-    elim (O_S (count_occ l x)).
-    apply sym_eq.
-    generalize (H x).
-    simpl. destruct (eq_dec x x) as [|HF].
-    trivial.
-    elim HF; reflexivity.
-    (* Case <- *)
-    intro H; rewrite H; simpl; reflexivity.
+    - induction l as [|x l]; trivial.
+      intros H. specialize (H x). simpl in H.
+      destruct eq_dec as [_|NEQ]; [discriminate|now elim NEQ].
+    - now intros ->.
   Qed.
 
   Lemma count_occ_nil : forall (x : A), count_occ [] x = 0.
@@ -754,22 +745,11 @@ Section ListOps.
 
   Hypothesis eq_dec : forall (x y : A), {x = y}+{x <> y}.
 
-  Lemma list_eq_dec :
-    forall l l':list A, {l = l'} + {l <> l'}.
-  Proof.
-    induction l as [| x l IHl]; destruct l' as [| y l'].
-    left; trivial.
-    right; apply nil_cons.
-    right; unfold not; intro HF; apply (nil_cons (sym_eq HF)).
-    destruct (eq_dec x y) as [xeqy|xneqy]; destruct (IHl l') as [leql'|lneql'];
-      try (right; unfold not; intro HF; injection HF; intros; contradiction).
-    rewrite xeqy; rewrite leql'; left; trivial.
-  Qed.
-
+  Lemma list_eq_dec : forall l l':list A, {l = l'} + {l <> l'}.
+  Proof. decide equality. Defined.
 
 End ListOps.
 
-
 (***************************************************)
 (** * Applying functions to the elements of a list *)
 (***************************************************)
diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v
index d67baf57..b846c48d 100644
--- a/theories/Lists/ListSet.v
+++ b/theories/Lists/ListSet.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -85,15 +85,15 @@ Section first_definitions.
   Lemma set_In_dec : forall (a:A) (x:set), {set_In a x} + {~ set_In a x}.
 
   Proof.
-    unfold set_In in |- *.
+    unfold set_In.
     (*** Realizer set_mem. Program_all. ***)
     simple induction x.
     auto.
     intros a0 x0 Ha0. case (Aeq_dec a a0); intro eq.
-    rewrite eq; simpl in |- *; auto with datatypes.
+    rewrite eq; simpl; auto with datatypes.
     elim Ha0.
     auto with datatypes.
-    right; simpl in |- *; unfold not in |- *; intros [Hc1| Hc2];
+    right; simpl; unfold not; intros [Hc1| Hc2];
      auto with datatypes.
   Qed.
 
@@ -102,7 +102,7 @@ Section first_definitions.
      (set_In a x -> P y) -> P z -> P (if set_mem a x then y else z).
 
   Proof.
-    simple induction x; simpl in |- *; intros.
+    simple induction x; simpl; intros.
     assumption.
     elim (Aeq_dec a a0); auto with datatypes.
   Qed.
@@ -113,11 +113,11 @@ Section first_definitions.
      (~ set_In a x -> P z) -> P (if set_mem a x then y else z).
 
   Proof.
-    simple induction x; simpl in |- *; intros.
-    apply H0; red in |- *; trivial.
+    simple induction x; simpl; intros.
+    apply H0; red; trivial.
     case (Aeq_dec a a0); auto with datatypes.
     intro; apply H; intros; auto.
-    apply H1; red in |- *; intro.
+    apply H1; red; intro.
     case H3; auto.
   Qed.
 
@@ -125,7 +125,7 @@ Section first_definitions.
   Lemma set_mem_correct1 :
    forall (a:A) (x:set), set_mem a x = true -> set_In a x.
   Proof.
-    simple induction x; simpl in |- *.
+    simple induction x; simpl.
     discriminate.
     intros a0 l; elim (Aeq_dec a a0); auto with datatypes.
   Qed.
@@ -133,7 +133,7 @@ Section first_definitions.
   Lemma set_mem_correct2 :
    forall (a:A) (x:set), set_In a x -> set_mem a x = true.
   Proof.
-    simple induction x; simpl in |- *.
+    simple induction x; simpl.
     intro Ha; elim Ha.
     intros a0 l; elim (Aeq_dec a a0); auto with datatypes.
     intros H1 H2 [H3| H4].
@@ -144,17 +144,17 @@ Section first_definitions.
   Lemma set_mem_complete1 :
    forall (a:A) (x:set), set_mem a x = false -> ~ set_In a x.
   Proof.
-    simple induction x; simpl in |- *.
+    simple induction x; simpl.
     tauto.
     intros a0 l; elim (Aeq_dec a a0).
     intros; discriminate H0.
-    unfold not in |- *; intros; elim H1; auto with datatypes.
+    unfold not; intros; elim H1; auto with datatypes.
   Qed.
 
   Lemma set_mem_complete2 :
    forall (a:A) (x:set), ~ set_In a x -> set_mem a x = false.
   Proof.
-    simple induction x; simpl in |- *.
+    simple induction x; simpl.
     tauto.
     intros a0 l; elim (Aeq_dec a a0).
     intros; elim H0; auto with datatypes.
@@ -165,7 +165,7 @@ Section first_definitions.
    forall (a b:A) (x:set), set_In a x -> set_In a (set_add b x).
 
   Proof.
-    unfold set_In in |- *; simple induction x; simpl in |- *.
+    unfold set_In; simple induction x; simpl.
     auto with datatypes.
     intros a0 l H [Ha0a| Hal].
     elim (Aeq_dec b a0); left; assumption.
@@ -176,11 +176,11 @@ Section first_definitions.
    forall (a b:A) (x:set), a = b -> set_In a (set_add b x).
 
   Proof.
-    unfold set_In in |- *; simple induction x; simpl in |- *.
+    unfold set_In; simple induction x; simpl.
     auto with datatypes.
     intros a0 l H Hab.
     elim (Aeq_dec b a0);
-     [ rewrite Hab; intro Hba0; rewrite Hba0; simpl in |- *;
+     [ rewrite Hab; intro Hba0; rewrite Hba0; simpl;
         auto with datatypes
      | auto with datatypes ].
   Qed.
@@ -198,13 +198,13 @@ Section first_definitions.
    forall (a b:A) (x:set), set_In a (set_add b x) -> a = b \/ set_In a x.
 
   Proof.
-    unfold set_In in |- *.
+    unfold set_In.
     simple induction x.
-    simpl in |- *; intros [H1| H2]; auto with datatypes.
-    simpl in |- *; do 3 intro.
+    simpl; intros [H1| H2]; auto with datatypes.
+    simpl; do 3 intro.
     elim (Aeq_dec b a0).
-    simpl in |- *; tauto.
-    simpl in |- *; intros; elim H0.
+    simpl; tauto.
+    simpl; intros; elim H0.
     trivial with datatypes.
     tauto.
     tauto.
@@ -220,7 +220,7 @@ Section first_definitions.
 
   Lemma set_add_not_empty : forall (a:A) (x:set), set_add a x <> empty_set.
   Proof.
-    simple induction x; simpl in |- *.
+    simple induction x; simpl.
     discriminate.
     intros; elim (Aeq_dec a a0); intros; discriminate.
   Qed.
@@ -229,13 +229,13 @@ Section first_definitions.
   Lemma set_union_intro1 :
    forall (a:A) (x y:set), set_In a x -> set_In a (set_union x y).
   Proof.
-    simple induction y; simpl in |- *; auto with datatypes.
+    simple induction y; simpl; auto with datatypes.
   Qed.
 
   Lemma set_union_intro2 :
    forall (a:A) (x y:set), set_In a y -> set_In a (set_union x y).
   Proof.
-    simple induction y; simpl in |- *.
+    simple induction y; simpl.
     tauto.
     intros; elim H0; auto with datatypes.
   Qed.
@@ -253,7 +253,7 @@ Section first_definitions.
    forall (a:A) (x y:set),
      set_In a (set_union x y) -> set_In a x \/ set_In a y.
   Proof.
-    simple induction y; simpl in |- *.
+    simple induction y; simpl.
     auto with datatypes.
     intros.
     generalize (set_add_elim _ _ _ H0).
@@ -280,11 +280,11 @@ Section first_definitions.
   Proof.
     simple induction x.
     auto with datatypes.
-    simpl in |- *; intros a0 l Hrec y [Ha0a| Hal] Hy.
-    simpl in |- *; rewrite Ha0a.
+    simpl; intros a0 l Hrec y [Ha0a| Hal] Hy.
+    simpl; rewrite Ha0a.
     generalize (set_mem_correct1 a y).
     generalize (set_mem_complete1 a y).
-    elim (set_mem a y); simpl in |- *; intros.
+    elim (set_mem a y); simpl; intros.
     auto with datatypes.
     absurd (set_In a y); auto with datatypes.
     elim (set_mem a0 y); [ right; auto with datatypes | auto with datatypes ].
@@ -295,9 +295,9 @@ Section first_definitions.
   Proof.
     simple induction x.
     auto with datatypes.
-    simpl in |- *; intros a0 l Hrec y.
+    simpl; intros a0 l Hrec y.
     generalize (set_mem_correct1 a0 y).
-    elim (set_mem a0 y); simpl in |- *; intros.
+    elim (set_mem a0 y); simpl; intros.
     elim H0; eauto with datatypes.
     eauto with datatypes.
   Qed.
@@ -306,10 +306,10 @@ Section first_definitions.
    forall (a:A) (x y:set), set_In a (set_inter x y) -> set_In a y.
   Proof.
     simple induction x.
-    simpl in |- *; tauto.
-    simpl in |- *; intros a0 l Hrec y.
+    simpl; tauto.
+    simpl; intros a0 l Hrec y.
     generalize (set_mem_correct1 a0 y).
-    elim (set_mem a0 y); simpl in |- *; intros.
+    elim (set_mem a0 y); simpl; intros.
     elim H0;
      [ intro Hr; rewrite <- Hr; eauto with datatypes | eauto with datatypes ].
     eauto with datatypes.
@@ -329,8 +329,8 @@ Section first_definitions.
      set_In a x -> ~ set_In a y -> set_In a (set_diff x y).
   Proof.
     simple induction x.
-    simpl in |- *; tauto.
-    simpl in |- *; intros a0 l Hrec y [Ha0a| Hal] Hay.
+    simpl; tauto.
+    simpl; intros a0 l Hrec y [Ha0a| Hal] Hay.
     rewrite Ha0a; generalize (set_mem_complete2 _ _ Hay).
     elim (set_mem a y);
      [ intro Habs; discriminate Habs | auto with datatypes ].
@@ -341,8 +341,8 @@ Section first_definitions.
    forall (a:A) (x y:set), set_In a (set_diff x y) -> set_In a x.
   Proof.
     simple induction x.
-    simpl in |- *; tauto.
-    simpl in |- *; intros a0 l Hrec y; elim (set_mem a0 y).
+    simpl; tauto.
+    simpl; intros a0 l Hrec y; elim (set_mem a0 y).
     eauto with datatypes.
     intro; generalize (set_add_elim _ _ _ H).
     intros [H1| H2]; eauto with datatypes.
@@ -350,7 +350,7 @@ Section first_definitions.
 
   Lemma set_diff_elim2 :
    forall (a:A) (x y:set), set_In a (set_diff x y) -> ~ set_In a y.
-  intros a x y; elim x; simpl in |- *.
+  intros a x y; elim x; simpl.
   intros; contradiction.
   intros a0 l Hrec.
   apply set_mem_ind2; auto.
@@ -359,7 +359,7 @@ Section first_definitions.
   Qed.
 
   Lemma set_diff_trivial : forall (a:A) (x:set), ~ set_In a (set_diff x x).
-  red in |- *; intros a x H.
+  red; intros a x H.
   apply (set_diff_elim2 _ _ _ H).
   apply (set_diff_elim1 _ _ _ H).
   Qed.
diff --git a/theories/Lists/ListTactics.v b/theories/Lists/ListTactics.v
index 3343aa6f..74336555 100644
--- a/theories/Lists/ListTactics.v
+++ b/theories/Lists/ListTactics.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -60,7 +60,7 @@ Ltac Find_at a l :=
    match l with
    | nil     => fail 100 "anomaly: Find_at"
    | a :: _  => eval compute in n
-   | _ :: ?l => find (Psucc n) l
+   | _ :: ?l => find (Pos.succ n) l
    end
  in find 1%positive l.
 
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index 97915055..0fd1693e 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.
@@ -199,7 +199,29 @@ Proof.
  rewrite <- In_rev; auto.
 Qed.
 
+(** Some more facts about InA *)
 
+Lemma InA_singleton x y : InA x (y::nil) <-> eqA x y.
+Proof.
+ rewrite InA_cons, InA_nil; tauto.
+Qed.
+
+Lemma InA_double_head x y l :
+ InA x (y :: y :: l) <-> InA x (y :: l).
+Proof.
+ rewrite !InA_cons; tauto.
+Qed.
+
+Lemma InA_permute_heads x y z l :
+ InA x (y :: z :: l) <-> InA x (z :: y :: l).
+Proof.
+ rewrite !InA_cons; tauto.
+Qed.
+
+Lemma InA_app_idem x l : InA x (l ++ l) <-> InA x l.
+Proof.
+ rewrite InA_app_iff; tauto.
+Qed.
 
 Section NoDupA.
 
@@ -270,7 +292,56 @@ Proof.
  eapply NoDupA_split; eauto.
 Qed.
 
-Lemma equivlistA_NoDupA_split : forall l l1 l2 x y, eqA x y ->
+Lemma NoDupA_singleton x : NoDupA (x::nil).
+Proof.
+ repeat constructor. inversion 1.
+Qed.
+
+End NoDupA.
+
+Section EquivlistA.
+
+Global Instance equivlistA_cons_proper:
+ Proper (eqA ==> equivlistA ==> equivlistA) (@cons A).
+Proof.
+ intros ? ? E1 ? ? E2 ?; now rewrite !InA_cons, E1, E2.
+Qed.
+
+Global Instance equivlistA_app_proper:
+ Proper (equivlistA ==> equivlistA ==> equivlistA) (@app A).
+Proof.
+ intros ? ? E1 ? ? E2 ?. now rewrite !InA_app_iff, E1, E2.
+Qed.
+
+Lemma equivlistA_cons_nil x l : ~ equivlistA (x :: l) nil.
+Proof.
+ intros E. now eapply InA_nil, E, InA_cons_hd.
+Qed.
+
+Lemma equivlistA_nil_eq l : equivlistA l nil -> l = nil.
+Proof.
+ destruct l.
+ - trivial.
+ - intros H. now apply equivlistA_cons_nil in H.
+Qed.
+
+Lemma equivlistA_double_head x l : equivlistA (x :: x :: l) (x :: l).
+Proof.
+ intro. apply InA_double_head.
+Qed.
+
+Lemma equivlistA_permute_heads x y l :
+ equivlistA (x :: y :: l) (y :: x :: l).
+Proof.
+ intro. apply InA_permute_heads.
+Qed.
+
+Lemma equivlistA_app_idem l : equivlistA (l ++ l) l.
+Proof.
+ intro. apply InA_app_idem.
+Qed.
+
+Lemma equivlistA_NoDupA_split l l1 l2 x y : eqA x y ->
  NoDupA (x::l) -> NoDupA (l1++y::l2) ->
  equivlistA (x::l) (l1++y::l2) -> equivlistA l (l1++l2).
 Proof.
@@ -290,9 +361,7 @@ Proof.
  rewrite <-H,<-EQN; auto.
 Qed.
 
-End NoDupA.
-
-
+End EquivlistA.
 
 Section Fold.
 
@@ -588,10 +657,9 @@ Proof.
 Qed.
 
 (** For compatibility, can be deduced from [InfA_compat] *)
-Lemma InfA_eqA :
- forall l x y, eqA x y -> InfA y l -> InfA x l.
+Lemma InfA_eqA l x y : eqA x y -> InfA y l -> InfA x l.
 Proof.
- intros l x y H; rewrite H; auto.
+ intros H; now rewrite H.
 Qed.
 Hint Immediate InfA_ltA InfA_eqA.
 
@@ -785,9 +853,11 @@ Qed.
 End Filter.
 End Type_with_equality.
 
-
 Hint Constructors InA eqlistA NoDupA sort lelistA.
 
+Arguments equivlistA_cons_nil {A} eqA {eqA_equiv} x l _.
+Arguments equivlistA_nil_eq {A} eqA {eqA_equiv} l _.
+
 Section Find.
 
 Variable A B : Type.
@@ -838,7 +908,6 @@ Qed.
 
 End Find.
 
-
 (** Compatibility aliases. [Proper] is rather to be used directly now.*)
 
 Definition compat_bool {A} (eqA:A->A->Prop)(f:A->bool) :=
@@ -852,4 +921,3 @@ Definition compat_P {A} (eqA:A->A->Prop)(P:A->Prop) :=
 
 Definition compat_op {A B} (eqA:A->A->Prop)(eqB:B->B->Prop)(f:A->B->B) :=
  Proper (eqA==>eqB==>eqB) f.
-
diff --git a/theories/Lists/SetoidPermutation.v b/theories/Lists/SetoidPermutation.v
new file mode 100644
index 00000000..b0657b63
--- /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/StreamMemo.v b/theories/Lists/StreamMemo.v
index 45490c62..67882cde 100644
--- a/theories/Lists/StreamMemo.v
+++ b/theories/Lists/StreamMemo.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -32,10 +32,10 @@ Fixpoint memo_get (n:nat) (l:Stream A) : A :=
 Theorem memo_get_correct: forall n, memo_get n memo_list = f n.
 Proof.
 assert (F1: forall n m, memo_get n (memo_make m) = f (n + m)).
-  induction n as [| n Hrec]; try (intros m; refine (refl_equal _)).
+{ induction n as [| n Hrec]; try (intros m; reflexivity).
   intros m; simpl; rewrite Hrec.
-  rewrite plus_n_Sm; auto.
-intros n; apply trans_equal with (f (n + 0)); try exact (F1 n 0).
+  rewrite plus_n_Sm; auto. }
+intros n; transitivity (f (n + 0)); try exact (F1 n 0).
 rewrite <- plus_n_O; auto.
 Qed.
 
@@ -57,11 +57,10 @@ Definition imemo_list := let f0 := f 0 in
 
 Theorem imemo_get_correct: forall n, memo_get n imemo_list = f n.
 Proof.
-assert (F1: forall n m,
-    memo_get n (imemo_make (f m)) = f (S (n + m))).
-  induction n as [| n Hrec]; try (intros m; exact (sym_equal (Hg_correct m))).
-  simpl; intros m; rewrite <- Hg_correct; rewrite Hrec; rewrite <- plus_n_Sm; auto.
-destruct n as [| n]; try apply refl_equal.
+assert (F1: forall n m, memo_get n (imemo_make (f m)) = f (S (n + m))).
+{ induction n as [| n Hrec]; try (intros m; exact (eq_sym (Hg_correct m))).
+  simpl; intros m; rewrite <- Hg_correct, Hrec, <- plus_n_Sm; auto. }
+destruct n as [| n]; try reflexivity.
 unfold imemo_list; simpl; rewrite F1.
 rewrite <- plus_n_O; auto.
 Qed.
@@ -82,7 +81,7 @@ Inductive memo_val: Type :=
 
 Fixpoint is_eq (n m : nat) : {n = m} + {True} :=
   match n, m return {n = m} + {True} with
-  | 0, 0 =>left True (refl_equal 0)
+  | 0, 0 =>left True (eq_refl 0)
   | 0, S m1 => right (0 = S m1) I
   | S n1, 0 => right (S n1 = 0) I
   | S n1, S m1 =>
@@ -98,7 +97,7 @@ match v with
     match is_eq n m with
     | left H =>
        match H in (eq _ y) return (A y -> A n) with
-        | refl_equal => fun v1 : A n => v1
+        | eq_refl => fun v1 : A n => v1
        end
     | right _ => fun _ : A m => f n
     end x
@@ -115,7 +114,7 @@ Proof.
 intros n; unfold dmemo_get, dmemo_list.
 rewrite (memo_get_correct memo_val mf n); simpl.
 case (is_eq n n); simpl; auto; intros e.
-assert (e = refl_equal n).
+assert (e = eq_refl n).
  apply eq_proofs_unicity.
  induction x as [| x Hx]; destruct y as [| y].
  left; auto.
@@ -144,7 +143,7 @@ Proof.
 intros n; unfold dmemo_get, dimemo_list.
 rewrite (imemo_get_correct memo_val mf mg); simpl.
 case (is_eq n n); simpl; auto; intros e.
-assert (e = refl_equal n).
+assert (e = eq_refl n).
  apply eq_proofs_unicity.
  induction x as [| x Hx]; destruct y as [| y].
  left; auto.
@@ -169,11 +168,11 @@ Open Scope Z_scope.
 Fixpoint tfact (n: nat) :=
   match n with
    | O => 1
-   | S n1 => Z_of_nat n * tfact n1
+   | S n1 => Z.of_nat n * tfact n1
   end.
 
 Definition lfact_list :=
-  dimemo_list _ tfact (fun n z => (Z_of_nat (S  n) * z)).
+  dimemo_list _ tfact (fun n z => (Z.of_nat (S  n) * z)).
 
 Definition lfact n := dmemo_get _ tfact n lfact_list.
 
diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v
index 7a6f38fc..e1122cf9 100644
--- a/theories/Lists/Streams.v
+++ b/theories/Lists/Streams.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -49,21 +49,21 @@ Qed.
 Lemma tl_nth_tl :
  forall (n:nat) (s:Stream), tl (Str_nth_tl n s) = Str_nth_tl n (tl s).
 Proof.
-  simple induction n; simpl in |- *; auto.
+  simple induction n; simpl; auto.
 Qed.
 Hint Resolve tl_nth_tl: datatypes v62.
 
 Lemma Str_nth_tl_plus :
  forall (n m:nat) (s:Stream),
    Str_nth_tl n (Str_nth_tl m s) = Str_nth_tl (n + m) s.
-simple induction n; simpl in |- *; intros; auto with datatypes.
+simple induction n; simpl; intros; auto with datatypes.
 rewrite <- H.
 rewrite tl_nth_tl; trivial with datatypes.
 Qed.
 
 Lemma Str_nth_plus :
  forall (n m:nat) (s:Stream), Str_nth n (Str_nth_tl m s) = Str_nth (n + m) s.
-intros; unfold Str_nth in |- *; rewrite Str_nth_tl_plus;
+intros; unfold Str_nth; rewrite Str_nth_tl_plus;
  trivial with datatypes.
 Qed.
 
@@ -89,7 +89,7 @@ Qed.
 
 Theorem sym_EqSt : forall s1 s2:Stream, EqSt s1 s2 -> EqSt s2 s1.
 coinduction Eq_sym.
-case H; intros; symmetry  in |- *; assumption.
+case H; intros; symmetry ; assumption.
 case H; intros; assumption.
 Qed.
 
@@ -110,10 +110,10 @@ Qed.
 
 Theorem eqst_ntheq :
  forall (n:nat) (s1 s2:Stream), EqSt s1 s2 -> Str_nth n s1 = Str_nth n s2.
-unfold Str_nth in |- *; simple induction n.
+unfold Str_nth; simple induction n.
 intros s1 s2 H; case H; trivial with datatypes.
 intros m hypind.
-simpl in |- *.
+simpl.
 intros s1 s2 H.
 apply hypind.
 case H; trivial with datatypes.
diff --git a/theories/Lists/vo.itarget b/theories/Lists/vo.itarget
index adcfba49..04994f59 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