From f698148f6aee01a207ce5ddd4bebf19da2108bff Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sun, 13 Dec 2009 21:23:17 +0000
Subject: 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
---
 LocallySorted.v | 44 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 44 insertions(+)
 create mode 100644 LocallySorted.v

(limited to 'LocallySorted.v')

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.
+
+
-- 
cgit v1.2.3