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, 44 insertions, 0 deletions

diff --git a/LocallySorted.v b/LocallySorted.v
new file mode 100644
index 000000000..8f6264134
--- /dev/null
+++ b/LocallySorted.v
@@ -0,0 +1,44 @@
+Require Import List Program.Syntax.
+
+Variable A:Type.
+Variable le:A->A->Prop.
+Infix "<=" := le.
+
+(*
+if of_sumbool H then _ else _
+if H then _ else _
+*)
+
+Inductive locally_sorted : list A -> Prop :=
+| nil_locally_sorted : locally_sorted []
+| cons1_locally_sorted a : locally_sorted [a]
+| consn_locally_sorted a b l : locally_sorted (b::l) -> a <= b -> locally_sorted (a::b::l).
+
+Inductive lelist (a:A) : list A -> Prop :=
+    | nil_le : lelist a nil
+    | cons_le : forall (b:A) (l:list A), le a b -> lelist a (b :: l).
+
+Inductive sort : list A -> Prop :=
+    | nil_sort : sort nil
+    | cons_sort :
+      forall (a:A) (l:list A), sort l -> lelist a l -> sort (a :: l).
+
+Goal forall l, sort l -> locally_sorted l.
+induction l.
+  constructor.
+  inversion 1; subst.
+  destruct l; constructor.
+  apply IHl; trivial.
+  inversion H3; auto.
+Qed.
+
+Goal forall l, lelist
+
+Goal forall l, locally_sorted l -> sort l.
+induction 1; constructor.
+  constructor.
+  constructor.
+  assumption.
+  inversion IHlocally_sorted; subst.
+
+