summaryrefslogtreecommitdiff
path: root/theories/Sorting
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-08-06 16:15:08 -0400
committerGravatar Stephane Glondu <steph@glondu.net>2010-08-06 16:17:55 -0400
commitf18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 (patch)
treec413c5bb42d20daf5307634ae6402526bb994fd6 /theories/Sorting
parentb9f47391f7f259c24119d1de0a87839e2cc5e80c (diff)
Imported Upstream version 8.3~rc1+dfsgupstream/8.3.rc1.dfsg
Diffstat (limited to 'theories/Sorting')
-rw-r--r--theories/Sorting/Heap.v51
-rw-r--r--theories/Sorting/Mergesort.v2
-rw-r--r--theories/Sorting/PermutEq.v2
-rw-r--r--theories/Sorting/PermutSetoid.v2
-rw-r--r--theories/Sorting/Permutation.v2
-rw-r--r--theories/Sorting/Sorted.v2
-rw-r--r--theories/Sorting/Sorting.v2
7 files changed, 32 insertions, 31 deletions
diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v
index 2e463120..eb53f061 100644
--- a/theories/Sorting/Heap.v
+++ b/theories/Sorting/Heap.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Heap.v 13346 2010-07-28 17:17:32Z msozeau $ i*)
(** This file is deprecated, for a tree on list, use [Mergesort.v]. *)
@@ -136,45 +136,46 @@ Section defs.
(munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2)) ->
(forall a, HdRel leA a l1 -> HdRel leA a l2 -> HdRel leA a l) ->
merge_lem l1 l2.
-
+ Require Import Morphisms.
+
+ Instance: Equivalence (@meq A).
+ Proof. constructor; auto with datatypes. red. apply meq_trans. Defined.
+
+ Instance: Proper (@meq A ++> @meq _ ++> @meq _) (@munion A).
+ Proof. intros x y H x' y' H'. now apply meq_congr. Qed.
+
Lemma merge :
forall l1:list A, Sorted leA l1 ->
forall l2:list A, Sorted leA l2 -> merge_lem l1 l2.
Proof.
- simple induction 1; intros.
+ fix 1; intros; destruct l1.
apply merge_exist with l2; auto with datatypes.
- elim H2; intros.
- apply merge_exist with (a :: l); simpl in |- *; auto using cons_sort with datatypes.
+ rename l1 into l.
+ revert l2 H0. fix 1. intros.
+ destruct l2 as [|a0 l0].
+ apply merge_exist with (a :: l); simpl; auto with datatypes.
elim (leA_dec a a0); intros.
(* 1 (leA a a0) *)
- cut (merge_lem l (a0 :: l0)); auto using cons_sort with datatypes.
- intros [l3 l3sorted l3contents Hrec].
- apply merge_exist with (a :: l3); simpl in |- *;
+ apply Sorted_inv in H. destruct H.
+ destruct (merge l H (a0 :: l0) H0).
+ apply merge_exist with (a :: l1). clear merge merge0.
auto using cons_sort, cons_leA with datatypes.
- apply meq_trans with
- (munion (singletonBag a)
- (munion (list_contents _ eqA_dec l)
- (list_contents _ eqA_dec (a0 :: l0)))).
- apply meq_right; trivial with datatypes.
- apply meq_sym; apply munion_ass.
- intros; apply cons_leA.
+ simpl. rewrite m. now rewrite munion_ass.
+ intros. apply cons_leA.
apply (@HdRel_inv _ leA) with l; trivial with datatypes.
(* 2 (leA a0 a) *)
- elim X0; simpl in |- *; intros.
- apply merge_exist with (a0 :: l3); simpl in |- *;
+ apply Sorted_inv in H0. destruct H0.
+ destruct (merge0 l0 H0). clear merge merge0.
+ apply merge_exist with (a0 :: l1);
auto using cons_sort, cons_leA with datatypes.
- apply meq_trans with
- (munion (singletonBag a0)
- (munion (munion (singletonBag a) (list_contents _ eqA_dec l))
- (list_contents _ eqA_dec l0))).
- apply meq_right; trivial with datatypes.
- apply munion_perm_left.
- intros; apply cons_leA; apply HdRel_inv with (l:=l0); trivial with datatypes.
+ simpl; rewrite m. simpl. setoid_rewrite munion_ass at 1. rewrite munion_comm.
+ repeat rewrite munion_ass. setoid_rewrite munion_comm at 3. reflexivity.
+ intros. apply cons_leA.
+ apply (@HdRel_inv _ leA) with l0; trivial with datatypes.
Qed.
-
(** ** From trees to multisets *)
(** contents of a tree as a multiset *)
diff --git a/theories/Sorting/Mergesort.v b/theories/Sorting/Mergesort.v
index f52a24b4..e576db2b 100644
--- a/theories/Sorting/Mergesort.v
+++ b/theories/Sorting/Mergesort.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Mergesort.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
(** A modular implementation of mergesort (the complexity is O(n.log n) in
the length of the list) *)
diff --git a/theories/Sorting/PermutEq.v b/theories/Sorting/PermutEq.v
index 1388df6a..00a09051 100644
--- a/theories/Sorting/PermutEq.v
+++ b/theories/Sorting/PermutEq.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: PermutEq.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
Require Import Relations Setoid SetoidList List Multiset PermutSetoid Permutation.
diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v
index f5f91887..e47e2b84 100644
--- a/theories/Sorting/PermutSetoid.v
+++ b/theories/Sorting/PermutSetoid.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: PermutSetoid.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
Require Import Omega Relations Multiset SetoidList.
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
index f88c29cb..1e145f57 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Permutation.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
(*********************************************************************)
(** ** List permutations as a composition of adjacent transpositions *)
diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v
index 7d75d60a..ab399d40 100644
--- a/theories/Sorting/Sorted.v
+++ b/theories/Sorting/Sorted.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Sorted.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
(* Made by Hugo Herbelin *)
diff --git a/theories/Sorting/Sorting.v b/theories/Sorting/Sorting.v
index 85d89441..860e0517 100644
--- a/theories/Sorting/Sorting.v
+++ b/theories/Sorting/Sorting.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Sorting.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
Require Export Sorted.
Require Export Mergesort.