From b54721f58c2ecb65ce554d8b34f214d5121a2b0c Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 27 Oct 2010 09:23:19 +0000 Subject: Various algorithmic improvements that reduce compile times (thanks Alexandre Pilkiewicz): - Lattice: preserve sharing in "combine" operation - Kildall: use splay heaps (lib/Heaps.v) for node sets - RTLgen: add a "nop" before loops so that natural enumeration of nodes coincides with (reverse) postorder - Maps: add PTree.map1 operation, use it in RTL and LTL. - Driver: increase minor heap size git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1543 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Heaps.v | 570 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 570 insertions(+) create mode 100644 lib/Heaps.v (limited to 'lib/Heaps.v') diff --git a/lib/Heaps.v b/lib/Heaps.v new file mode 100644 index 00000000..a5c0d61b --- /dev/null +++ b/lib/Heaps.v @@ -0,0 +1,570 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** A heap data structure. *) + +(** The implementation uses splay heaps, following C. Okasaki, + "Purely functional data structures", section 5.4. + One difference: we eliminate duplicate elements. + (If an element is already in a heap, inserting it again does nothing.) +*) + +Require Import Coqlib. +Require Import FSets. +Require Import Ordered. + +Module SplayHeapSet(E: OrderedType). + +(** "Raw" implementation. The "is a binary search tree" invariant + is proved separately. *) + +Module R. + +Inductive heap: Type := + | Empty + | Node (l: heap) (x: E.t) (r: heap). + +Function partition (pivot: E.t) (h: heap) { struct h } : heap * heap := + match h with + | Empty => (Empty, Empty) + | Node a x b => + match E.compare x pivot with + | EQ _ => (a, b) + | LT _ => + match b with + | Empty => (h, Empty) + | Node b1 y b2 => + match E.compare y pivot with + | EQ _ => (Node a x b1, b2) + | LT _ => + let (small, big) := partition pivot b2 + in (Node (Node a x b1) y small, big) + | GT _ => + let (small, big) := partition pivot b1 + in (Node a x small, Node big y b2) + end + end + | GT _ => + match a with + | Empty => (Empty, h) + | Node a1 y a2 => + match E.compare y pivot with + | EQ _ => (a1, Node a2 x b) + | LT _ => + let (small, big) := partition pivot a2 + in (Node a1 y small, Node big x b) + | GT _ => + let (small, big) := partition pivot a1 + in (small, Node big y (Node a2 x b)) + end + end + end + end. + +Definition insert (x: E.t) (h: heap) : heap := + let (a, b) := partition x h in Node a x b. + +Fixpoint findMin (h: heap) : option E.t := + match h with + | Empty => None + | Node Empty x b => Some x + | Node a x b => findMin a + end. + +Function deleteMin (h: heap) : heap := + match h with + | Empty => Empty + | Node Empty x b => b + | Node (Node Empty x b) y c => Node b y c + | Node (Node a x b) y c => Node (deleteMin a) x (Node b y c) + end. + +Fixpoint findMax (h: heap) : option E.t := + match h with + | Empty => None + | Node a x Empty => Some x + | Node a x b => findMax b + end. + +Function deleteMax (h: heap) : heap := + match h with + | Empty => Empty + | Node b x Empty => b + | Node b x (Node c y Empty) => Node b x c + | Node a x (Node b y c) => Node (Node a x b) y (deleteMax c) + end. + +(** Specification *) + +Fixpoint In (x: E.t) (h: heap) : Prop := + match h with + | Empty => False + | Node a y b => In x a \/ E.eq x y \/ In x b + end. + +(** Invariants *) + +Fixpoint lt_heap (h: heap) (x: E.t) : Prop := + match h with + | Empty => True + | Node a y b => lt_heap a x /\ E.lt y x /\ lt_heap b x + end. + +Fixpoint gt_heap (h: heap) (x: E.t) : Prop := + match h with + | Empty => True + | Node a y b => gt_heap a x /\ E.lt x y /\ gt_heap b x + end. + +Fixpoint bst (h: heap) : Prop := + match h with + | Empty => True + | Node a x b => bst a /\ bst b /\ lt_heap a x /\ gt_heap b x + end. + +Definition le (x y: E.t) := E.eq x y \/ E.lt x y. + +Lemma le_lt_trans: + forall x1 x2 x3, le x1 x2 -> E.lt x2 x3 -> E.lt x1 x3. +Proof. + unfold le; intros; intuition. + destruct (E.compare x1 x3). + auto. + elim (@E.lt_not_eq x2 x3). auto. apply E.eq_trans with x1. apply E.eq_sym; auto. auto. + elim (@E.lt_not_eq x2 x1). eapply E.lt_trans; eauto. apply E.eq_sym; auto. + eapply E.lt_trans; eauto. +Qed. + +Lemma lt_le_trans: + forall x1 x2 x3, E.lt x1 x2 -> le x2 x3 -> E.lt x1 x3. +Proof. + unfold le; intros; intuition. + destruct (E.compare x1 x3). + auto. + elim (@E.lt_not_eq x1 x2). auto. apply E.eq_trans with x3. auto. apply E.eq_sym; auto. + elim (@E.lt_not_eq x3 x2). eapply E.lt_trans; eauto. apply E.eq_sym; auto. + eapply E.lt_trans; eauto. +Qed. + +Lemma le_trans: + forall x1 x2 x3, le x1 x2 -> le x2 x3 -> le x1 x3. +Proof. + intros. destruct H. destruct H0. red; left; eapply E.eq_trans; eauto. + red. right. eapply le_lt_trans; eauto. red; auto. + red. right. eapply lt_le_trans; eauto. +Qed. + +Lemma lt_heap_trans: + forall x y, le x y -> + forall h, lt_heap h x -> lt_heap h y. +Proof. + induction h; simpl; intros. + auto. + intuition. eapply lt_le_trans; eauto. +Qed. + +Lemma gt_heap_trans: + forall x y, le y x -> + forall h, gt_heap h x -> gt_heap h y. +Proof. + induction h; simpl; intros. + auto. + intuition. eapply le_lt_trans; eauto. +Qed. + +(** Properties of [partition] *) + +Lemma In_partition: + forall x pivot, ~E.eq x pivot -> + forall h, bst h -> (In x h <-> In x (fst (partition pivot h)) \/ In x (snd (partition pivot h))). +Proof. + intros x pivot NEQ h0. functional induction (partition pivot h0); simpl; intros. + tauto. + intuition. elim NEQ. eapply E.eq_trans; eauto. + intuition. + intuition. elim NEQ. eapply E.eq_trans; eauto. + rewrite e3 in IHp; simpl in IHp. intuition. + rewrite e3 in IHp; simpl in IHp. intuition. + intuition. + intuition. elim NEQ. eapply E.eq_trans; eauto. + rewrite e3 in IHp; simpl in IHp. intuition. + rewrite e3 in IHp; simpl in IHp. intuition. +Qed. + +Lemma partition_lt: + forall x pivot h, + lt_heap h x -> lt_heap (fst (partition pivot h)) x /\ lt_heap (snd (partition pivot h)) x. +Proof. + intros x pivot h0. functional induction (partition pivot h0); simpl. + tauto. + tauto. + tauto. + tauto. + rewrite e3 in IHp; simpl in IHp. tauto. + rewrite e3 in IHp; simpl in IHp. tauto. + tauto. + tauto. + rewrite e3 in IHp; simpl in IHp. tauto. + rewrite e3 in IHp; simpl in IHp. tauto. +Qed. + +Lemma partition_gt: + forall x pivot h, + gt_heap h x -> gt_heap (fst (partition pivot h)) x /\ gt_heap (snd (partition pivot h)) x. +Proof. + intros x pivot h0. functional induction (partition pivot h0); simpl. + tauto. + tauto. + tauto. + tauto. + rewrite e3 in IHp; simpl in IHp. tauto. + rewrite e3 in IHp; simpl in IHp. tauto. + tauto. + tauto. + rewrite e3 in IHp; simpl in IHp. tauto. + rewrite e3 in IHp; simpl in IHp. tauto. +Qed. + +Lemma partition_split: + forall pivot h, + bst h -> lt_heap (fst (partition pivot h)) pivot /\ gt_heap (snd (partition pivot h)) pivot. +Proof. + intros pivot h0. functional induction (partition pivot h0); simpl. + tauto. + intuition. eapply lt_heap_trans; eauto. red; auto. eapply gt_heap_trans; eauto. red; left; apply E.eq_sym; auto. + intuition. eapply lt_heap_trans; eauto. red; auto. + intuition. eapply lt_heap_trans; eauto. red; auto. + eapply lt_heap_trans; eauto. red; auto. + apply gt_heap_trans with y; auto. red. left; apply E.eq_sym; auto. + rewrite e3 in IHp; simpl in IHp. intuition. + eapply lt_heap_trans; eauto. red; auto. + eapply lt_heap_trans; eauto. red; auto. + rewrite e3 in IHp; simpl in IHp. intuition. + eapply lt_heap_trans; eauto. red; auto. + apply gt_heap_trans with y; eauto. red; auto. + intuition. eapply gt_heap_trans; eauto. red; auto. + intuition. apply lt_heap_trans with y; eauto. red; auto. + eapply gt_heap_trans; eauto. red; left; apply E.eq_sym; auto. + eapply gt_heap_trans; eauto. red; auto. + rewrite e3 in IHp; simpl in IHp. intuition. + apply lt_heap_trans with y; eauto. red; auto. + eapply gt_heap_trans; eauto. red; auto. + rewrite e3 in IHp; simpl in IHp. intuition. + apply gt_heap_trans with y; eauto. red; auto. + apply gt_heap_trans with x; eauto. red; auto. +Qed. + +Lemma partition_bst: + forall pivot h, + bst h -> + bst (fst (partition pivot h)) /\ bst (snd (partition pivot h)). +Proof. + intros pivot h0. functional induction (partition pivot h0); simpl. + tauto. + tauto. + tauto. + tauto. + rewrite e3 in IHp; simpl in IHp. intuition. + apply lt_heap_trans with x; auto. red; auto. + generalize (partition_gt y pivot b2 H7). rewrite e3; simpl. tauto. + rewrite e3 in IHp; simpl in IHp. intuition. + generalize (partition_gt x pivot b1 H3). rewrite e3; simpl. tauto. + generalize (partition_lt y pivot b1 H4). rewrite e3; simpl. tauto. + tauto. + tauto. + rewrite e3 in IHp; simpl in IHp. intuition. + generalize (partition_gt y pivot a2 H6). rewrite e3; simpl. tauto. + generalize (partition_lt x pivot a2 H8). rewrite e3; simpl. tauto. + rewrite e3 in IHp; simpl in IHp. intuition. + generalize (partition_lt y pivot a1 H3). rewrite e3; simpl. tauto. + apply gt_heap_trans with x; auto. red. auto. +Qed. + +(** Properties of [insert] *) + +Lemma insert_bst: + forall x h, bst h -> bst (insert x h). +Proof. + intros. + unfold insert. case_eq (partition x h). intros a b EQ; simpl. + generalize (partition_bst x h H). + generalize (partition_split x h H). + rewrite EQ; simpl. tauto. +Qed. + +Lemma In_insert: + forall x h y, bst h -> (In y (insert x h) <-> E.eq y x \/ In y h). +Proof. + intros. unfold insert. + case_eq (partition x h). intros a b EQ; simpl. + assert (E.eq y x \/ ~E.eq y x). + destruct (E.compare y x); auto. + right; red; intros. elim (E.lt_not_eq l). apply E.eq_sym; auto. + destruct H0. + tauto. + generalize (In_partition y x H0 h H). rewrite EQ; simpl. tauto. +Qed. + +(** Properties of [findMin] and [deleteMin] *) + +Lemma deleteMin_lt: + forall x h, lt_heap h x -> lt_heap (deleteMin h) x. +Proof. + intros x h0. functional induction (deleteMin h0); simpl; intros. + auto. + tauto. + tauto. + intuition. +Qed. + +Lemma deleteMin_bst: + forall h, bst h -> bst (deleteMin h). +Proof. + intros h0. functional induction (deleteMin h0); simpl; intros. + auto. + tauto. + tauto. + intuition. + apply deleteMin_lt; auto. + apply gt_heap_trans with y; auto. red; auto. +Qed. + +Lemma In_deleteMin: + forall y x h, + findMin h = Some x -> + (In y h <-> E.eq y x \/ In y (deleteMin h)). +Proof. + intros y x h0. functional induction (deleteMin h0); simpl; intros. + congruence. + inv H. tauto. + inv H. tauto. + destruct a. contradiction. tauto. +Qed. + +Lemma gt_heap_In: + forall x y h, gt_heap h x -> In y h -> E.lt x y. +Proof. + induction h; simpl; intros. + contradiction. + intuition. apply lt_le_trans with x0; auto. red. left. apply E.eq_sym; auto. +Qed. + +Lemma findMin_min: + forall x h, findMin h = Some x -> bst h -> forall y, In y h -> le x y. +Proof. + induction h; simpl; intros. + contradiction. + destruct h1. + inv H. simpl in *. intuition. + red; left; apply E.eq_sym; auto. + red; right. eapply gt_heap_In; eauto. + assert (le x x1). + apply IHh1; auto. tauto. simpl. right; left; apply E.eq_refl. + intuition. + apply le_trans with x1. auto. apply le_trans with x0. simpl in H4. red; tauto. + red; left; apply E.eq_sym; auto. + apply le_trans with x1. auto. apply le_trans with x0. simpl in H4. red; tauto. + red; right. eapply gt_heap_In; eauto. +Qed. + +Lemma findMin_empty: + forall h, h <> Empty -> findMin h <> None. +Proof. + induction h; simpl; intros. + congruence. + destruct h1. congruence. apply IHh1. congruence. +Qed. + +(** Properties of [findMax] and [deleteMax]. *) + +Lemma deleteMax_gt: + forall x h, gt_heap h x -> gt_heap (deleteMax h) x. +Proof. + intros x h0. functional induction (deleteMax h0); simpl; intros. + auto. + tauto. + tauto. + intuition. +Qed. + +Lemma deleteMax_bst: + forall h, bst h -> bst (deleteMax h). +Proof. + intros h0. functional induction (deleteMax h0); simpl; intros. + auto. + tauto. + tauto. + intuition. + apply lt_heap_trans with x; auto. red; auto. + apply deleteMax_gt; auto. +Qed. + +Lemma In_deleteMax: + forall y x h, + findMax h = Some x -> + (In y h <-> E.eq y x \/ In y (deleteMax h)). +Proof. + intros y x h0. functional induction (deleteMax h0); simpl; intros. + congruence. + inv H. tauto. + inv H. tauto. + destruct c. contradiction. tauto. +Qed. + +Lemma lt_heap_In: + forall x y h, lt_heap h x -> In y h -> E.lt y x. +Proof. + induction h; simpl; intros. + contradiction. + intuition. apply le_lt_trans with x0; auto. red. left. apply E.eq_sym; auto. +Qed. + +Lemma findMax_max: + forall x h, findMax h = Some x -> bst h -> forall y, In y h -> le y x. +Proof. + induction h; simpl; intros. + contradiction. + destruct h2. + inv H. simpl in *. intuition. + red; right. eapply lt_heap_In; eauto. + red; left. auto. + assert (le x1 x). + apply IHh2; auto. tauto. simpl. right; left; apply E.eq_refl. + intuition. + apply le_trans with x1; auto. apply le_trans with x0. + red; right. eapply lt_heap_In; eauto. + simpl in H6. red; tauto. + apply le_trans with x1; auto. apply le_trans with x0. + red; auto. + simpl in H6. red; tauto. +Qed. + +Lemma findMax_empty: + forall h, h <> Empty -> findMax h <> None. +Proof. + induction h; simpl; intros. + congruence. + destruct h2. congruence. apply IHh2. congruence. +Qed. + +End R. + +(** Wrapping in a dependent type *) + +Definition t := { h: R.heap | R.bst h }. + +(** Operations *) + +Program Definition empty : t := R.Empty. + +Program Definition insert (x: E.t) (h: t) : t := R.insert x h. +Next Obligation. apply R.insert_bst. apply proj2_sig. Qed. + +Program Definition findMin (h: t) : option E.t := R.findMin h. + +Program Definition deleteMin (h: t) : t := R.deleteMin h. +Next Obligation. apply R.deleteMin_bst. apply proj2_sig. Qed. + +Program Definition findMax (h: t) : option E.t := R.findMax h. + +Program Definition deleteMax (h: t) : t := R.deleteMax h. +Next Obligation. apply R.deleteMax_bst. apply proj2_sig. Qed. + +(** Membership (for specification) *) + +Program Definition In (x: E.t) (h: t) : Prop := R.In x h. + +(** Properties of [empty] *) + +Lemma In_empty: forall x, ~In x empty. +Proof. + intros; red; intros. + red in H. simpl in H. tauto. +Qed. + +(** Properties of [insert] *) + +Lemma In_insert: + forall x h y, + In y (insert x h) <-> E.eq y x \/ In y h. +Proof. + intros. unfold In, insert; simpl. apply R.In_insert. apply proj2_sig. +Qed. + +(** Properties of [findMin] *) + +Lemma findMin_empty: + forall h y, findMin h = None -> ~In y h. +Proof. + unfold findMin, In; intros; simpl. + destruct (proj1_sig h). + simpl. tauto. + exploit R.findMin_empty; eauto. congruence. +Qed. + +Lemma findMin_min: + forall h x y, findMin h = Some x -> In y h -> E.eq x y \/ E.lt x y. +Proof. + unfold findMin, In; simpl. intros. + change (R.le x y). eapply R.findMin_min; eauto. apply proj2_sig. +Qed. + +(** Properties of [deleteMin]. *) + +Lemma In_deleteMin: + forall h x y, + findMin h = Some x -> + (In y h <-> E.eq y x \/ In y (deleteMin h)). +Proof. + unfold findMin, In; simpl; intros. + apply R.In_deleteMin. auto. +Qed. + +(** Properties of [findMax] *) + +Lemma findMax_empty: + forall h y, findMax h = None -> ~In y h. +Proof. + unfold findMax, In; intros; simpl. + destruct (proj1_sig h). + simpl. tauto. + exploit R.findMax_empty; eauto. congruence. +Qed. + +Lemma findMax_max: + forall h x y, findMax h = Some x -> In y h -> E.eq y x \/ E.lt y x. +Proof. + unfold findMax, In; simpl. intros. + change (R.le y x). eapply R.findMax_max; eauto. apply proj2_sig. +Qed. + +(** Properties of [deleteMax]. *) + +Lemma In_deleteMax: + forall h x y, + findMax h = Some x -> + (In y h <-> E.eq y x \/ In y (deleteMax h)). +Proof. + unfold findMax, In; simpl; intros. + apply R.In_deleteMax. auto. +Qed. + +End SplayHeapSet. + +(** Instantiation over type [positive] *) + +Module PHeap := SplayHeapSet(OrderedPositive). + + -- cgit