diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-10-27 09:23:19 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-10-27 09:23:19 +0000 |
commit | b54721f58c2ecb65ce554d8b34f214d5121a2b0c (patch) | |
tree | 01bc71f3e5e6b1681dac76de97ab925e005cc2c4 /lib | |
parent | 63cc20f9ddb18bebae523c46438abdf2a4b140d4 (diff) |
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
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Heaps.v | 570 | ||||
-rw-r--r-- | lib/Lattice.v | 383 | ||||
-rw-r--r-- | lib/Maps.v | 24 |
3 files changed, 905 insertions, 72 deletions
diff --git a/lib/Heaps.v b/lib/Heaps.v new file mode 100644 index 0000000..a5c0d61 --- /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). + + diff --git a/lib/Lattice.v b/lib/Lattice.v index a185c43..c200fc8 100644 --- a/lib/Lattice.v +++ b/lib/Lattice.v @@ -35,12 +35,11 @@ Module Type SEMILATTICE. Variable ge: t -> t -> Prop. Hypothesis ge_refl: forall x y, eq x y -> ge x y. Hypothesis ge_trans: forall x y z, ge x y -> ge y z -> ge x z. - Hypothesis ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'. Variable bot: t. Hypothesis ge_bot: forall x, ge x bot. Variable lub: t -> t -> t. - Hypothesis lub_commut: forall x y, eq (lub x y) (lub y x). Hypothesis ge_lub_left: forall x y, ge (lub x y) x. + Hypothesis ge_lub_right: forall x y, ge (lub x y) y. End SEMILATTICE. @@ -57,6 +56,8 @@ End SEMILATTICE_WITH_TOP. (** * Semi-lattice over maps *) +Set Implicit Arguments. + (** Given a semi-lattice with top [L], the following functor implements a semi-lattice structure over finite maps from positive numbers to [L.t]. The default value for these maps is either [L.top] or [L.bot]. *) @@ -156,11 +157,6 @@ Proof. unfold ge; intros. apply L.ge_trans with (get p y); auto. Qed. -Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'. -Proof. - unfold eq,ge; intros. eapply L.ge_compat; eauto. -Qed. - Definition bot := Bot_except (PTree.empty L.t). Lemma get_bot: forall p, get p bot = L.bot. @@ -185,6 +181,232 @@ Proof. unfold ge; intros. rewrite get_top. apply L.ge_top. Qed. +(** A [combine] operation over the type [PTree.t L.t] that attempts + to share its result with its arguments. *) + +Section COMBINE. + +Variable f: option L.t -> option L.t -> option L.t. +Hypothesis f_none_none: f None None = None. + +Definition opt_eq (ox oy: option L.t) : Prop := + match ox, oy with + | None, None => True + | Some x, Some y => L.eq x y + | _, _ => False + end. + +Lemma opt_eq_refl: forall ox, opt_eq ox ox. +Proof. + intros. unfold opt_eq. destruct ox. apply L.eq_refl. auto. +Qed. + +Lemma opt_eq_sym: forall ox oy, opt_eq ox oy -> opt_eq oy ox. +Proof. + unfold opt_eq. destruct ox; destruct oy; auto. apply L.eq_sym. +Qed. + +Lemma opt_eq_trans: forall ox oy oz, opt_eq ox oy -> opt_eq oy oz -> opt_eq ox oz. +Proof. + unfold opt_eq. destruct ox; destruct oy; destruct oz; intuition. + eapply L.eq_trans; eauto. +Qed. + +Definition opt_beq (ox oy: option L.t) : bool := + match ox, oy with + | None, None => true + | Some x, Some y => L.beq x y + | _, _ => false + end. + +Lemma opt_beq_correct: + forall ox oy, opt_beq ox oy = true -> opt_eq ox oy. +Proof. + unfold opt_beq, opt_eq. destruct ox; destruct oy; try congruence. + intros. apply L.beq_correct; auto. + auto. +Qed. + +Definition tree_eq (m1 m2: PTree.t L.t) : Prop := + forall i, opt_eq (PTree.get i m1) (PTree.get i m2). + +Lemma tree_eq_refl: forall m, tree_eq m m. +Proof. intros; red; intros; apply opt_eq_refl. Qed. + +Lemma tree_eq_sym: forall m1 m2, tree_eq m1 m2 -> tree_eq m2 m1. +Proof. intros; red; intros; apply opt_eq_sym; auto. Qed. + +Lemma tree_eq_trans: forall m1 m2 m3, tree_eq m1 m2 -> tree_eq m2 m3 -> tree_eq m1 m3. +Proof. intros; red; intros; apply opt_eq_trans with (PTree.get i m2); auto. Qed. + +Lemma tree_eq_node: + forall l1 o1 r1 l2 o2 r2, + tree_eq l1 l2 -> tree_eq r1 r2 -> opt_eq o1 o2 -> + tree_eq (PTree.Node l1 o1 r1) (PTree.Node l2 o2 r2). +Proof. + intros; red; intros. destruct i; simpl; auto. +Qed. + +Lemma tree_eq_node': + forall l1 o1 r1 l2 o2 r2, + tree_eq l1 l2 -> tree_eq r1 r2 -> opt_eq o1 o2 -> + tree_eq (PTree.Node l1 o1 r1) (PTree.Node' l2 o2 r2). +Proof. + intros; red; intros. rewrite PTree.gnode'. apply tree_eq_node; auto. +Qed. + +Lemma tree_eq_node'': + forall l1 o1 r1 l2 o2 r2, + tree_eq l1 l2 -> tree_eq r1 r2 -> opt_eq o1 o2 -> + tree_eq (PTree.Node' l1 o1 r1) (PTree.Node' l2 o2 r2). +Proof. + intros; red; intros. repeat rewrite PTree.gnode'. apply tree_eq_node; auto. +Qed. + +Hint Resolve opt_beq_correct opt_eq_refl opt_eq_sym + tree_eq_refl tree_eq_sym + tree_eq_node tree_eq_node' tree_eq_node'' : combine. + +Inductive changed: Type := Unchanged | Changed (m: PTree.t L.t). + +Fixpoint combine_l (m : PTree.t L.t) {struct m} : changed := + match m with + | PTree.Leaf => + Unchanged + | PTree.Node l o r => + let o' := f o None in + match combine_l l, combine_l r with + | Unchanged, Unchanged => if opt_beq o' o then Unchanged else Changed (PTree.Node' l o' r) + | Unchanged, Changed r' => Changed (PTree.Node' l o' r') + | Changed l', Unchanged => Changed (PTree.Node' l' o' r) + | Changed l', Changed r' => Changed (PTree.Node' l' o' r') + end + end. + +Lemma combine_l_eq: + forall m, + tree_eq (match combine_l m with Unchanged => m | Changed m' => m' end) + (PTree.xcombine_l f m). +Proof. + induction m; simpl. + auto with combine. + destruct (combine_l m1) as [ | l']; destruct (combine_l m2) as [ | r']; + auto with combine. + case_eq (opt_beq (f o None) o); auto with combine. +Qed. + +Fixpoint combine_r (m : PTree.t L.t) {struct m} : changed := + match m with + | PTree.Leaf => + Unchanged + | PTree.Node l o r => + let o' := f None o in + match combine_r l, combine_r r with + | Unchanged, Unchanged => if opt_beq o' o then Unchanged else Changed (PTree.Node' l o' r) + | Unchanged, Changed r' => Changed (PTree.Node' l o' r') + | Changed l', Unchanged => Changed (PTree.Node' l' o' r) + | Changed l', Changed r' => Changed (PTree.Node' l' o' r') + end + end. + +Lemma combine_r_eq: + forall m, + tree_eq (match combine_r m with Unchanged => m | Changed m' => m' end) + (PTree.xcombine_r f m). +Proof. + induction m; simpl. + auto with combine. + destruct (combine_r m1) as [ | l']; destruct (combine_r m2) as [ | r']; + auto with combine. + case_eq (opt_beq (f None o) o); auto with combine. +Qed. + +Inductive changed2 : Type := + | Same + | Same1 + | Same2 + | CC(m: PTree.t L.t). + +Fixpoint xcombine (m1 m2 : PTree.t L.t) {struct m1} : changed2 := + match m1, m2 with + | PTree.Leaf, PTree.Leaf => + Same + | PTree.Leaf, _ => + match combine_r m2 with + | Unchanged => Same2 + | Changed m => CC m + end + | _, PTree.Leaf => + match combine_l m1 with + | Unchanged => Same1 + | Changed m => CC m + end + | PTree.Node l1 o1 r1, PTree.Node l2 o2 r2 => + let o := f o1 o2 in + match xcombine l1 l2, xcombine r1 r2 with + | Same, Same => + match opt_beq o o1, opt_beq o o2 with + | true, true => Same + | true, false => Same1 + | false, true => Same2 + | false, false => CC(PTree.Node' l1 o r1) + end + | Same1, Same | Same, Same1 | Same1, Same1 => + if opt_beq o o1 then Same1 else CC(PTree.Node' l1 o r1) + | Same2, Same | Same, Same2 | Same2, Same2 => + if opt_beq o o2 then Same2 else CC(PTree.Node' l2 o r2) + | Same1, Same2 => CC(PTree.Node' l1 o r2) + | (Same|Same1), CC r => CC(PTree.Node' l1 o r) + | Same2, Same1 => CC(PTree.Node' l2 o r1) + | Same2, CC r => CC(PTree.Node' l2 o r) + | CC l, (Same|Same1) => CC(PTree.Node' l o r1) + | CC l, Same2 => CC(PTree.Node' l o r2) + | CC l, CC r => CC(PTree.Node' l o r) + end + end. + +Lemma xcombine_eq: + forall m1 m2, + match xcombine m1 m2 with + | Same => tree_eq m1 (PTree.combine f m1 m2) /\ tree_eq m2 (PTree.combine f m1 m2) + | Same1 => tree_eq m1 (PTree.combine f m1 m2) + | Same2 => tree_eq m2 (PTree.combine f m1 m2) + | CC m => tree_eq m (PTree.combine f m1 m2) + end. +Proof. +Opaque combine_l combine_r PTree.xcombine_l PTree.xcombine_r. + induction m1; destruct m2; simpl. + split; apply tree_eq_refl. + generalize (combine_r_eq (PTree.Node m2_1 o m2_2)). + destruct (combine_r (PTree.Node m2_1 o m2_2)); auto. + generalize (combine_l_eq (PTree.Node m1_1 o m1_2)). + destruct (combine_l (PTree.Node m1_1 o m1_2)); auto. + generalize (IHm1_1 m2_1) (IHm1_2 m2_2). + destruct (xcombine m1_1 m2_1); + destruct (xcombine m1_2 m2_2); auto with combine; + intuition; case_eq (opt_beq (f o o0) o); case_eq (opt_beq (f o o0) o0); auto with combine. +Qed. + +Definition combine (m1 m2: PTree.t L.t) : PTree.t L.t := + match xcombine m1 m2 with + | Same|Same1 => m1 + | Same2 => m2 + | CC m => m + end. + +Lemma gcombine: + forall m1 m2 i, opt_eq (PTree.get i (combine m1 m2)) (f (PTree.get i m1) (PTree.get i m2)). +Proof. + intros. + assert (tree_eq (combine m1 m2) (PTree.combine f m1 m2)). + unfold combine. + generalize (xcombine_eq m1 m2). + destruct (xcombine m1 m2); tauto. + eapply opt_eq_trans. apply H. rewrite PTree.gcombine; auto. apply opt_eq_refl. +Qed. + +End COMBINE. + Definition opt_lub (x y: L.t) : option L.t := let z := L.lub x y in if L.beq z L.top then None else Some z. @@ -193,7 +415,7 @@ Definition lub (x y: t) : t := match x, y with | Bot_except m, Bot_except n => Bot_except - (PTree.combine + (combine (fun a b => match a, b with | Some u, Some v => Some (L.lub u v) @@ -203,7 +425,7 @@ Definition lub (x y: t) : t := m n) | Bot_except m, Top_except n => Top_except - (PTree.combine + (combine (fun a b => match a, b with | Some u, Some v => opt_lub u v @@ -213,7 +435,7 @@ Definition lub (x y: t) : t := m n) | Top_except m, Bot_except n => Top_except - (PTree.combine + (combine (fun a b => match a, b with | Some u, Some v => opt_lub u v @@ -223,7 +445,7 @@ Definition lub (x y: t) : t := m n) | Top_except m, Top_except n => Top_except - (PTree.combine + (combine (fun a b => match a, b with | Some u, Some v => opt_lub u v @@ -232,29 +454,26 @@ Definition lub (x y: t) : t := m n) end. -Lemma lub_commut: - forall x y, eq (lub x y) (lub y x). +Lemma gcombine_top: + forall f t1 t2 p, + f None None = None -> + L.eq (get p (Top_except (combine f t1 t2))) + (match f t1!p t2!p with Some x => x | None => L.top end). Proof. - intros x y p. - assert (forall u v, - L.eq (match opt_lub u v with - | Some x => x - | None => L.top end) - (match opt_lub v u with - | Some x => x - | None => L.top - end)). - intros. unfold opt_lub. - case_eq (L.beq (L.lub u v) L.top); - case_eq (L.beq (L.lub v u) L.top); intros. - apply L.eq_refl. - eapply L.eq_trans. apply L.eq_sym. apply L.beq_correct; eauto. apply L.lub_commut. - eapply L.eq_trans. apply L.lub_commut. apply L.beq_correct; auto. - apply L.lub_commut. - destruct x; destruct y; simpl; - repeat rewrite PTree.gcombine; auto; - destruct t0!p; destruct t1!p; - auto; apply L.eq_refl || apply L.lub_commut. + intros. simpl. generalize (gcombine f H t1 t2 p). unfold opt_eq. + destruct ((combine f t1 t2)!p); destruct (f t1!p t2!p). + auto. contradiction. contradiction. intros; apply L.eq_refl. +Qed. + +Lemma gcombine_bot: + forall f t1 t2 p, + f None None = None -> + L.eq (get p (Bot_except (combine f t1 t2))) + (match f t1!p t2!p with Some x => x | None => L.bot end). +Proof. + intros. simpl. generalize (gcombine f H t1 t2 p). unfold opt_eq. + destruct ((combine f t1 t2)!p); destruct (f t1!p t2!p). + auto. contradiction. contradiction. intros; apply L.eq_refl. Qed. Lemma ge_lub_left: @@ -265,31 +484,70 @@ Proof. intros; unfold opt_lub. case_eq (L.beq (L.lub u v) L.top); intros. apply L.ge_top. apply L.ge_lub_left. - unfold ge, get, lub; intros; destruct x; destruct y. + unfold ge, lub; intros. destruct x; destruct y. - rewrite PTree.gcombine; auto. - destruct t0!p; destruct t1!p. + eapply L.ge_trans. apply L.ge_refl. apply gcombine_bot. auto. + simpl. destruct t0!p; destruct t1!p. apply L.ge_lub_left. apply L.ge_refl. apply L.eq_refl. apply L.ge_bot. apply L.ge_refl. apply L.eq_refl. - rewrite PTree.gcombine; auto. - destruct t0!p; destruct t1!p. + eapply L.ge_trans. apply L.ge_refl. apply gcombine_top. auto. + simpl. destruct t0!p; destruct t1!p. auto. apply L.ge_top. apply L.ge_bot. apply L.ge_top. - rewrite PTree.gcombine; auto. - destruct t0!p; destruct t1!p. + eapply L.ge_trans. apply L.ge_refl. apply gcombine_top. auto. + simpl. destruct t0!p; destruct t1!p. + auto. + apply L.ge_refl. apply L.eq_refl. + apply L.ge_top. + apply L.ge_top. + + eapply L.ge_trans. apply L.ge_refl. apply gcombine_top. auto. + simpl. destruct t0!p; destruct t1!p. + auto. + apply L.ge_top. + apply L.ge_top. + apply L.ge_top. +Qed. + +Lemma ge_lub_right: + forall x y, ge (lub x y) y. +Proof. + assert (forall u v, + L.ge (match opt_lub u v with Some x => x | None => L.top end) v). + intros; unfold opt_lub. + case_eq (L.beq (L.lub u v) L.top); intros. apply L.ge_top. apply L.ge_lub_right. + + unfold ge, lub; intros. destruct x; destruct y. + + eapply L.ge_trans. apply L.ge_refl. apply gcombine_bot. auto. + simpl. destruct t0!p; destruct t1!p. + apply L.ge_lub_right. + apply L.ge_bot. + apply L.ge_refl. apply L.eq_refl. + apply L.ge_refl. apply L.eq_refl. + + eapply L.ge_trans. apply L.ge_refl. apply gcombine_top. auto. + simpl. destruct t0!p; destruct t1!p. auto. + apply L.ge_top. apply L.ge_refl. apply L.eq_refl. apply L.ge_top. + + eapply L.ge_trans. apply L.ge_refl. apply gcombine_top. auto. + simpl. destruct t0!p; destruct t1!p. + auto. + apply L.ge_bot. + apply L.ge_top. apply L.ge_top. - rewrite PTree.gcombine; auto. - destruct t0!p; destruct t1!p. + eapply L.ge_trans. apply L.ge_refl. apply gcombine_top. auto. + simpl. destruct t0!p; destruct t1!p. auto. apply L.ge_top. apply L.ge_top. @@ -303,7 +561,7 @@ End LPMap. (** Given a set [S: FSetInterface.S], the following functor implements a semi-lattice over these sets, ordered by inclusion. *) -Module LFSet (S: FSetInterface.S) <: SEMILATTICE. +Module LFSet (S: FSetInterface.WS) <: SEMILATTICE. Definition t := S.t. @@ -323,10 +581,6 @@ Module LFSet (S: FSetInterface.S) <: SEMILATTICE. Proof. unfold ge, S.Subset; intros. eauto. Qed. - Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'. - Proof. - unfold ge, eq, S.Subset, S.Equal; intros. firstorder. - Qed. Definition bot: t := S.empty. Lemma ge_bot: forall x, ge x bot. @@ -335,18 +589,17 @@ Module LFSet (S: FSetInterface.S) <: SEMILATTICE. Qed. Definition lub: t -> t -> t := S.union. - Lemma lub_commut: forall x y, eq (lub x y) (lub y x). - Proof. - unfold lub, eq, S.Equal; intros. split; intro. - destruct (S.union_1 H). apply S.union_3; auto. apply S.union_2; auto. - destruct (S.union_1 H). apply S.union_3; auto. apply S.union_2; auto. - Qed. Lemma ge_lub_left: forall x y, ge (lub x y) x. Proof. unfold lub, ge, S.Subset; intros. apply S.union_2; auto. Qed. + Lemma ge_lub_right: forall x y, ge (lub x y) y. + Proof. + unfold lub, ge, S.Subset; intros. apply S.union_3; auto. + Qed. + End LFSet. (** * Flat semi-lattice *) @@ -403,11 +656,6 @@ Proof. transitivity t1; auto. Qed. -Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'. -Proof. - unfold eq; intros; congruence. -Qed. - Definition bot: t := Bot. Lemma ge_bot: forall x, ge x bot. @@ -431,13 +679,13 @@ Definition lub (x y: t) : t := | Inj a, Inj b => if X.eq a b then Inj a else Top end. -Lemma lub_commut: forall x y, eq (lub x y) (lub y x). +Lemma ge_lub_left: forall x y, ge (lub x y) x. Proof. - unfold eq; destruct x; destruct y; simpl; auto. - case (X.eq t0 t1); case (X.eq t1 t0); intros; congruence. + destruct x; destruct y; simpl; auto. + case (X.eq t0 t1); simpl; auto. Qed. -Lemma ge_lub_left: forall x y, ge (lub x y) x. +Lemma ge_lub_right: forall x y, ge (lub x y) y. Proof. destruct x; destruct y; simpl; auto. case (X.eq t0 t1); simpl; auto. @@ -472,11 +720,6 @@ Proof. unfold ge; tauto. Qed. Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. Proof. unfold ge; intuition congruence. Qed. -Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'. -Proof. - unfold eq; intros; congruence. -Qed. - Definition bot := false. Lemma ge_bot: forall x, ge x bot. @@ -489,10 +732,10 @@ Proof. unfold ge, top; tauto. Qed. Definition lub (x y: t) := x || y. -Lemma lub_commut: forall x y, eq (lub x y) (lub y x). -Proof. intros; unfold eq, lub. apply orb_comm. Qed. - Lemma ge_lub_left: forall x y, ge (lub x y) x. Proof. destruct x; destruct y; compute; tauto. Qed. +Lemma ge_lub_right: forall x y, ge (lub x y) y. +Proof. destruct x; destruct y; compute; tauto. Qed. + End LBoolean. @@ -98,6 +98,13 @@ Module Type TREE. forall (A B: Type) (f: elt -> A -> B) (i: elt) (m: t A), get i (map f m) = option_map (f i) (get i m). + (** Same as [map], but the function does not receive the [elt] argument. *) + Variable map1: + forall (A B: Type), (A -> B) -> t A -> t B. + Hypothesis gmap1: + forall (A B: Type) (f: A -> B) (i: elt) (m: t A), + get i (map1 f m) = option_map f (get i m). + (** Applying a function pairwise to all data of two trees. *) Variable combine: forall (A: Type), (option A -> option A -> option A) -> t A -> t A -> t A. @@ -492,6 +499,19 @@ Module PTree <: TREE. rewrite append_neutral_l; auto. Qed. + Fixpoint map1 (A B: Type) (f: A -> B) (m: t A) {struct m} : t B := + match m with + | Leaf => Leaf + | Node l o r => Node (map1 f l) (option_map f o) (map1 f r) + end. + + Theorem gmap1: + forall (A B: Type) (f: A -> B) (i: elt) (m: t A), + get i (map1 f m) = option_map f (get i m). + Proof. + induction i; intros; destruct m; simpl; auto. + Qed. + Definition Node' (A: Type) (l: t A) (x: option A) (r: t A): t A := match l, x, r with | Leaf, None, Leaf => Leaf @@ -1091,13 +1111,13 @@ Module PMap <: MAP. Qed. Definition map (A B : Type) (f : A -> B) (m : t A) : t B := - (f (fst m), PTree.map (fun _ => f) (snd m)). + (f (fst m), PTree.map1 f (snd m)). Theorem gmap: forall (A B: Type) (f: A -> B) (i: positive) (m: t A), get i (map f m) = f(get i m). Proof. - intros. unfold map. unfold get. simpl. rewrite PTree.gmap. + intros. unfold map. unfold get. simpl. rewrite PTree.gmap1. unfold option_map. destruct (PTree.get i (snd m)); auto. Qed. |