Addition of mergesort + cleaning of the Sorting library

- New (modular) mergesort purely using structural recursion
- Move of the (complex) notion of permutation up to setoid equality
  formerly defined in Permutation.v to file PermutSetoid.v
- Re-use of the file Permutation.v for making the canonical notion
  of permutation that was in List.v more visible
- New file Sorted.v that contains two definitions of sorted:
  "Sorted" is a renaming of "sort" that was defined in file
  Sorting.v and "StronglySorted" is the intuitive notion of sorted
  (there is also LocallySorted which is a variant of Sorted)
- File Sorting.v is replaced by a call to the main Require of the directory
- The merge function whose specification rely on counting elements is moved
  to Heap.v and both are stamped deprecated (the sort defined in
  Heap.v has complexity n^2 in worst case)
- Added some new naming conventions
- Removed uselessly-maximal implicit arguments of Forall2 predicate

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

1 files changed, 11 insertions, 1 deletions

diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v
index 75b9f2efa..7216ae335 100644
--- a/theories/Sets/Multiset.v
+++ b/theories/Sets/Multiset.v
@@ -10,7 +10,7 @@
 
 (* G. Huet 1-9-95 *)
 
-Require Import Permut.
+Require Import Permut Setoid.
 
 Set Implicit Arguments.
 
@@ -18,6 +18,7 @@ Section multiset_defs.
 
   Variable A : Type.
   Variable eqA : A -> A -> Prop.
+  Hypothesis eqA_equiv : Equivalence eqA.
   Hypothesis Aeq_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
 
   Inductive multiset : Type :=
@@ -167,6 +168,15 @@ Section multiset_defs.
     apply multiset_twist2.
   Qed.
 
+  (** SingletonBag *)
+
+  Lemma meq_singleton : forall a a',
+    eqA a a' -> meq (SingletonBag a) (SingletonBag a').
+  Proof.
+    intros; red; simpl; intro a0.
+    destruct (Aeq_dec a a0) as [Ha|Ha]; rewrite H in Ha;
+      decide (Aeq_dec a' a0) with Ha; reflexivity.
+  Qed.
 
 (*i theory of minter to do similarly
 Require Min.