aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-07-28 17:15:21 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-07-28 17:15:21 +0000
commitd5bd62a0be614b6f55f061d6e6cdef97d52cc19e (patch)
treeb7399c274f04e8757697d80da8d884fbf540192d
parent4b2155f4deb67bcee70a27e9217bef884408142a (diff)
Rewrite Heap merging so that it extracts to an O(n log n) definition.
Fixes bug #2047. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13345 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--theories/Sorting/Heap.v49
1 files changed, 25 insertions, 24 deletions
diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v
index c28422e02..60bb50cec 100644
--- a/theories/Sorting/Heap.v
+++ b/theories/Sorting/Heap.v
@@ -134,45 +134,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 *)