From d5bd62a0be614b6f55f061d6e6cdef97d52cc19e Mon Sep 17 00:00:00 2001 From: msozeau Date: Wed, 28 Jul 2010 17:15:21 +0000 Subject: 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 --- theories/Sorting/Heap.v | 49 +++++++++++++++++++++++++------------------------ 1 file changed, 25 insertions(+), 24 deletions(-) (limited to 'theories/Sorting') 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 *) -- cgit v1.2.3