diff options
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Camlcoq.ml | 10 | ||||
-rw-r--r-- | lib/Integers.v | 13 | ||||
-rw-r--r-- | lib/IntvSets.v | 410 | ||||
-rw-r--r-- | lib/Lattice.v | 235 |
4 files changed, 615 insertions, 53 deletions
diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml index 929b61e3..ca48341d 100644 --- a/lib/Camlcoq.ml +++ b/lib/Camlcoq.ml @@ -363,6 +363,16 @@ let time3 name fn arg1 arg2 arg3 = add_to_timer name (Unix.gettimeofday() -. start); raise x +let time4 name fn arg1 arg2 arg3 arg4 = + let start = Unix.gettimeofday() in + try + let res = fn arg1 arg2 arg3 arg4 in + add_to_timer name (Unix.gettimeofday() -. start); + res + with x -> + add_to_timer name (Unix.gettimeofday() -. start); + raise x + let print_timers () = Hashtbl.iter (fun name time -> Printf.printf "%-20s %.3f\n" name time) diff --git a/lib/Integers.v b/lib/Integers.v index cbbf28c7..d85007b4 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -2454,6 +2454,19 @@ Proof. generalize wordsize_pos; generalize wordsize_max_unsigned; omega. Qed. +Theorem ror_rol_neg: + forall x y, (zwordsize | modulus) -> ror x y = rol x (neg y). +Proof. + intros. apply same_bits_eq; intros. + rewrite bits_ror by auto. rewrite bits_rol by auto. + f_equal. apply eqmod_mod_eq. omega. + apply eqmod_trans with (i - (- unsigned y)). + apply eqmod_refl2; omega. + apply eqmod_sub. apply eqmod_refl. + apply eqmod_divides with modulus. + apply eqm_unsigned_repr. auto. +Qed. + Theorem or_ror: forall x y z, ltu y iwordsize = true -> diff --git a/lib/IntvSets.v b/lib/IntvSets.v new file mode 100644 index 00000000..9f1a895f --- /dev/null +++ b/lib/IntvSets.v @@ -0,0 +1,410 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** Finite sets of integer intervals *) + +Require Import Coqlib. + +Module ISet. + +(** "Raw", non-dependent implementation. A set of intervals is a + list of nonempty semi-open intervals [(lo, hi)], + sorted in increasing order of the low bound, + and with no overlap nor adjacency between elements. + In particular, if the list contains [(lo1, hi1)] followed by [(lo2, hi2)], + we have [lo1 < hi1 < lo2 < hi2]. *) + +Module R. + +Inductive t : Type := Nil | Cons (lo hi: Z) (tl: t). + +Fixpoint In (x: Z) (s: t) := + match s with + | Nil => False + | Cons l h s' => l <= x < h \/ In x s' + end. + +Inductive ok: t -> Prop := + | ok_nil: ok Nil + | ok_cons: forall l h s + (BOUNDS: l < h) + (BELOW: forall x, In x s -> h < x) + (OK: ok s), + ok (Cons l h s). + +Fixpoint mem (x: Z) (s: t) : bool := + match s with + | Nil => false + | Cons l h s' => if zlt x h then zle l x else mem x s' + end. + +Lemma mem_In: + forall x s, ok s -> (mem x s = true <-> In x s). +Proof. + induction 1; simpl. +- intuition congruence. +- destruct (zlt x h). ++ destruct (zle l x); simpl. + * tauto. + * split; intros. congruence. + exfalso. destruct H0. omega. exploit BELOW; eauto. omega. ++ rewrite IHok. intuition. +Qed. + +Fixpoint contains (L H: Z) (s: t) : bool := + match s with + | Nil => false + | Cons l h s' => (zle H h && zle l L) || contains L H s' + end. + +Lemma contains_In: + forall l0 h0, l0 < h0 -> forall s, ok s -> + (contains l0 h0 s = true <-> (forall x, l0 <= x < h0 -> In x s)). +Proof. + induction 2; simpl. +- intuition. elim (H0 l0); omega. +- destruct (zle h0 h); simpl. + destruct (zle l l0); simpl. + intuition. + rewrite IHok. intuition. destruct (H3 x); auto. exfalso. + destruct (H3 l0). omega. omega. exploit BELOW; eauto. omega. + rewrite IHok. intuition. destruct (H3 x); auto. exfalso. + destruct (H3 h). omega. omega. exploit BELOW; eauto. omega. +Qed. + +Fixpoint add (L H: Z) (s: t) {struct s} : t := + match s with + | Nil => Cons L H Nil + | Cons l h s' => + if zlt h L then Cons l h (add L H s') + else if zlt H l then Cons L H s + else add (Z.min l L) (Z.max h H) s' + end. + +Lemma In_add: + forall x s, ok s -> forall l0 h0, (In x (add l0 h0 s) <-> l0 <= x < h0 \/ In x s). +Proof. + induction 1; simpl; intros. + tauto. + destruct (zlt h l0). + simpl. rewrite IHok. tauto. + destruct (zlt h0 l). + simpl. tauto. + rewrite IHok. intuition. + assert (l0 <= x < h0 \/ l <= x < h) by xomega. tauto. + left; xomega. + left; xomega. +Qed. + +Lemma add_ok: + forall s, ok s -> forall l0 h0, l0 < h0 -> ok (add l0 h0 s). +Proof. + induction 1; simpl; intros. + constructor. auto. intros. inv H0. constructor. + destruct (zlt h l0). + constructor; auto. intros. rewrite In_add in H1; auto. + destruct H1. omega. auto. + destruct (zlt h0 l). + constructor. auto. simpl; intros. destruct H1. omega. exploit BELOW; eauto. omega. + constructor. omega. auto. auto. + apply IHok. xomega. +Qed. + +Fixpoint remove (L H: Z) (s: t) {struct s} : t := + match s with + | Nil => Nil + | Cons l h s' => + if zlt h L then Cons l h (remove L H s') + else if zlt H l then s + else if zlt l L then + if zlt H h then Cons l L (Cons H h s') else Cons l L (remove L H s') + else + if zlt H h then Cons H h s' else remove L H s' + end. + +Lemma In_remove: + forall x l0 h0 s, ok s -> + (In x (remove l0 h0 s) <-> ~(l0 <= x < h0) /\ In x s). +Proof. + induction 1; simpl. + tauto. + destruct (zlt h l0). + simpl. rewrite IHok. intuition omega. + destruct (zlt h0 l). + simpl. intuition. exploit BELOW; eauto. omega. + destruct (zlt l l0). + destruct (zlt h0 h); simpl. clear IHok. split. + intros [A | [A | A]]. + split. omega. left; omega. + split. omega. left; omega. + split. exploit BELOW; eauto. omega. auto. + intros [A [B | B]]. + destruct (zlt x l0). left; omega. right; left; omega. + auto. + intuition omega. + destruct (zlt h0 h); simpl. + intuition. exploit BELOW; eauto. omega. + rewrite IHok. intuition. omegaContradiction. +Qed. + +Lemma remove_ok: + forall l0 h0, l0 < h0 -> forall s, ok s -> ok (remove l0 h0 s). +Proof. + induction 2; simpl. + constructor. + destruct (zlt h l0). + constructor; auto. intros; apply BELOW. rewrite In_remove in H1; tauto. + destruct (zlt h0 l). + constructor; auto. + destruct (zlt l l0). + destruct (zlt h0 h). + constructor. omega. intros. inv H1. omega. exploit BELOW; eauto. omega. + constructor. omega. auto. auto. + constructor; auto. intros. rewrite In_remove in H1 by auto. destruct H1. exploit BELOW; eauto. omega. + destruct (zlt h0 h). + constructor; auto. + auto. +Qed. + +Fixpoint inter (s1 s2: t) {struct s1} : t := + let fix intr (s2: t) : t := + match s1, s2 with + | Nil, _ => Nil + | _, Nil => Nil + | Cons l1 h1 s1', Cons l2 h2 s2' => + if zle h1 l2 then inter s1' s2 + else if zle h2 l1 then intr s2' + else if zle l1 l2 then + if zle h2 h1 then Cons l2 h2 (intr s2') else Cons l2 h1 (inter s1' s2) + else + if zle h1 h2 then Cons l1 h1 (inter s1' s2) else Cons l1 h2 (intr s2') + end + in intr s2. + +Lemma In_inter: + forall x s1, ok s1 -> forall s2, ok s2 -> + (In x (inter s1 s2) <-> In x s1 /\ In x s2). +Proof. + induction 1. + simpl. induction 1; simpl. tauto. tauto. + assert (ok (Cons l h s)) by (constructor; auto). + induction 1; simpl. + tauto. + assert (ok (Cons l0 h0 s0)) by (constructor; auto). + destruct (zle h l0). + rewrite IHok; auto. simpl. intuition. omegaContradiction. + exploit BELOW0; eauto. intros. omegaContradiction. + destruct (zle h0 l). + simpl in IHok0; rewrite IHok0. intuition. omegaContradiction. + exploit BELOW; eauto. intros; omegaContradiction. + destruct (zle l l0). + destruct (zle h0 h). + simpl. simpl in IHok0; rewrite IHok0. intuition. + simpl. rewrite IHok; auto. simpl. intuition. exploit BELOW0; eauto. intros; omegaContradiction. + destruct (zle h h0). + simpl. rewrite IHok; auto. simpl. intuition. + simpl. simpl in IHok0; rewrite IHok0. intuition. + exploit BELOW; eauto. intros; omegaContradiction. +Qed. + +Lemma inter_ok: + forall s1, ok s1 -> forall s2, ok s2 -> ok (inter s1 s2). +Proof. + induction 1. + intros; simpl. destruct s2; constructor. + assert (ok (Cons l h s)). constructor; auto. + induction 1; simpl. + constructor. + assert (ok (Cons l0 h0 s0)). constructor; auto. + destruct (zle h l0). + auto. + destruct (zle h0 l). + auto. + destruct (zle l l0). + destruct (zle h0 h). + constructor; auto. intros. + assert (In x (inter (Cons l h s) s0)) by exact H3. + rewrite In_inter in H4; auto. apply BELOW0. tauto. + constructor. omega. intros. rewrite In_inter in H3; auto. apply BELOW. tauto. + auto. + destruct (zle h h0). + constructor. omega. intros. rewrite In_inter in H3; auto. apply BELOW. tauto. + auto. + constructor. omega. intros. + assert (In x (inter (Cons l h s) s0)) by exact H3. + rewrite In_inter in H4; auto. apply BELOW0. tauto. + auto. +Qed. + +Fixpoint union (s1 s2: t) : t := + match s1, s2 with + | Nil, _ => s2 + | _, Nil => s1 + | Cons l1 h1 s1', Cons l2 h2 s2' => add l1 h1 (add l2 h2 (union s1' s2')) + end. + +Lemma In_ok_union: + forall s1, ok s1 -> forall s2, ok s2 -> + ok (union s1 s2) /\ (forall x, In x s1 \/ In x s2 <-> In x (union s1 s2)). +Proof. + induction 1; destruct 1; simpl. + split. constructor. tauto. + split. constructor; auto. tauto. + split. constructor; auto. tauto. + destruct (IHok s0) as [A B]; auto. + split. apply add_ok; auto. apply add_ok; auto. + intros. rewrite In_add. rewrite In_add. rewrite <- B. tauto. auto. apply add_ok; auto. +Qed. + +Fixpoint beq (s1 s2: t) : bool := + match s1, s2 with + | Nil, Nil => true + | Cons l1 h1 t1, Cons l2 h2 t2 => zeq l1 l2 && zeq h1 h2 && beq t1 t2 + | _, _ => false + end. + +Lemma beq_spec: + forall s1, ok s1 -> forall s2, ok s2 -> + (beq s1 s2 = true <-> (forall x, In x s1 <-> In x s2)). +Proof. + induction 1; destruct 1; simpl. +- tauto. +- split; intros. discriminate. exfalso. apply (H0 l). left; omega. +- split; intros. discriminate. exfalso. apply (H0 l). left; omega. +- split; intros. ++ InvBooleans. subst. rewrite IHok in H3 by auto. rewrite H3. tauto. ++ destruct (zeq l l0). destruct (zeq h h0). simpl. subst. + apply IHok. auto. intros; split; intros. + destruct (proj1 (H1 x)); auto. exfalso. exploit BELOW; eauto. omega. + destruct (proj2 (H1 x)); auto. exfalso. exploit BELOW0; eauto. omega. + exfalso. subst l0. destruct (zlt h h0). + destruct (proj2 (H1 h)). left; omega. omega. exploit BELOW; eauto. omega. + destruct (proj1 (H1 h0)). left; omega. omega. exploit BELOW0; eauto. omega. + exfalso. destruct (zlt l l0). + destruct (proj1 (H1 l)). left; omega. omega. exploit BELOW0; eauto. omega. + destruct (proj2 (H1 l0)). left; omega. omega. exploit BELOW; eauto. omega. +Qed. + +End R. + +(** Exported interface, wrapping the [ok] invariant in a dependent type. *) + +Definition t := { r: R.t | R.ok r }. + +Program Definition In (x: Z) (s: t) := R.In x s. + +Program Definition empty : t := R.Nil. +Next Obligation. constructor. Qed. + +Theorem In_empty: forall x, ~(In x empty). +Proof. + unfold In; intros; simpl. tauto. +Qed. + +Program Definition interval (l h: Z) : t := + if zlt l h then R.Cons l h R.Nil else R.Nil. +Next Obligation. + constructor; auto. simpl; tauto. constructor. +Qed. +Next Obligation. + constructor. +Qed. + +Theorem In_interval: forall x l h, In x (interval l h) <-> l <= x < h. +Proof. + intros. unfold In, interval; destruct (zlt l h); simpl. + intuition. + intuition. +Qed. + +Program Definition add (l h: Z) (s: t) : t := + if zlt l h then R.add l h s else s. +Next Obligation. + apply R.add_ok. apply proj2_sig. auto. +Qed. + +Theorem In_add: forall x l h s, In x (add l h s) <-> l <= x < h \/ In x s. +Proof. + unfold add, In; intros. + destruct (zlt l h). + simpl. apply R.In_add. apply proj2_sig. + intuition. omegaContradiction. +Qed. + +Program Definition remove (l h: Z) (s: t) : t := + if zlt l h then R.remove l h s else s. +Next Obligation. + apply R.remove_ok. auto. apply proj2_sig. +Qed. + +Theorem In_remove: forall x l h s, In x (remove l h s) <-> ~(l <= x < h) /\ In x s. +Proof. + unfold remove, In; intros. + destruct (zlt l h). + simpl. apply R.In_remove. apply proj2_sig. + intuition. +Qed. + +Program Definition inter (s1 s2: t) : t := R.inter s1 s2. +Next Obligation. apply R.inter_ok; apply proj2_sig. Qed. + +Theorem In_inter: forall x s1 s2, In x (inter s1 s2) <-> In x s1 /\ In x s2. +Proof. + unfold inter, In; intros; simpl. apply R.In_inter; apply proj2_sig. +Qed. + +Program Definition union (s1 s2: t) : t := R.union s1 s2. +Next Obligation. + destruct (R.In_ok_union _ (proj2_sig s1) _ (proj2_sig s2)). auto. +Qed. + +Theorem In_union: forall x s1 s2, In x (union s1 s2) <-> In x s1 \/ In x s2. +Proof. + unfold union, In; intros; simpl. + destruct (R.In_ok_union _ (proj2_sig s1) _ (proj2_sig s2)). + generalize (H0 x); tauto. +Qed. + +Program Definition mem (x: Z) (s: t) := R.mem x s. + +Theorem mem_spec: forall x s, mem x s = true <-> In x s. +Proof. + unfold mem, In; intros. apply R.mem_In. apply proj2_sig. +Qed. + +Program Definition contains (l h: Z) (s: t) := + if zlt l h then R.contains l h s else true. + +Theorem contains_spec: + forall l h s, contains l h s = true <-> (forall x, l <= x < h -> In x s). +Proof. + unfold contains, In; intros. destruct (zlt l h). + apply R.contains_In. auto. apply proj2_sig. + split; intros. omegaContradiction. auto. +Qed. + +Program Definition beq (s1 s2: t) : bool := R.beq s1 s2. + +Theorem beq_spec: + forall s1 s2, beq s1 s2 = true <-> (forall x, In x s1 <-> In x s2). +Proof. + unfold mem, In; intros. apply R.beq_spec; apply proj2_sig. +Qed. + +End ISet. + + + + diff --git a/lib/Lattice.v b/lib/Lattice.v index cb28b5b9..5a941a13 100644 --- a/lib/Lattice.v +++ b/lib/Lattice.v @@ -66,42 +66,28 @@ End SEMILATTICE_WITH_TOP. Set Implicit Arguments. -(** Given a semi-lattice with top [L], the following functor implements +(** Given a semi-lattice (without 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]. *) - -Module LPMap(L: SEMILATTICE_WITH_TOP) <: SEMILATTICE_WITH_TOP. + The default value for these maps is [L.bot]. Bottom elements are not smashed. *) -Inductive t' : Type := - | Bot: t' - | Top_except: PTree.t L.t -> t'. +Module LPMap1(L: SEMILATTICE) <: SEMILATTICE. -Definition t: Type := t'. +Definition t := PTree.t L.t. Definition get (p: positive) (x: t) : L.t := - match x with - | Bot => L.bot - | Top_except m => match m!p with None => L.top | Some x => x end - end. + match x!p with None => L.bot | Some x => x end. Definition set (p: positive) (v: L.t) (x: t) : t := - match x with - | Bot => Bot - | Top_except m => - if L.beq v L.bot - then Bot - else Top_except (if L.beq v L.top then PTree.remove p m else PTree.set p v m) - end. + if L.beq v L.bot + then PTree.remove p x + else PTree.set p v x. Lemma gsspec: forall p v x q, - x <> Bot -> ~L.eq v L.bot -> L.eq (get q (set p v x)) (if peq q p then v else get q x). Proof. - intros. unfold set. destruct x. congruence. - destruct (L.beq v L.bot) eqn:EBOT. - elim H0. apply L.beq_correct; auto. - destruct (L.beq v L.top) eqn:ETOP; simpl. + intros. unfold set, get. + destruct (L.beq v L.bot) eqn:EBOT. rewrite PTree.grspec. unfold PTree.elt_eq. destruct (peq q p). apply L.eq_sym. apply L.beq_correct; auto. apply L.eq_refl. @@ -126,20 +112,13 @@ Proof. unfold eq; intros. eapply L.eq_trans; eauto. Qed. -Definition beq (x y: t) : bool := - match x, y with - | Bot, Bot => true - | Top_except m, Top_except n => PTree.beq L.beq m n - | _, _ => false - end. +Definition beq (x y: t) : bool := PTree.beq L.beq x y. Lemma beq_correct: forall x y, beq x y = true -> eq x y. Proof. - destruct x; destruct y; simpl; intro; try congruence. - apply eq_refl. - red; intro; simpl. - rewrite PTree.beq_correct in H. generalize (H p). - destruct (t0!p); destruct (t1!p); intuition. + unfold beq; intros; red; intros. unfold get. + rewrite PTree.beq_correct in H. specialize (H p). + destruct (x!p); destruct (y!p); intuition. apply L.beq_correct; auto. apply L.eq_refl. Qed. @@ -157,11 +136,11 @@ Proof. unfold ge; intros. apply L.ge_trans with (get p y); auto. Qed. -Definition bot := Bot. +Definition bot : t := PTree.empty _. Lemma get_bot: forall p, get p bot = L.bot. Proof. - unfold bot; intros; simpl. auto. + unfold bot, get; intros; simpl. rewrite PTree.gempty. auto. Qed. Lemma ge_bot: forall x, ge x bot. @@ -169,18 +148,6 @@ Proof. unfold ge; intros. rewrite get_bot. apply L.ge_bot. Qed. -Definition top := Top_except (PTree.empty L.t). - -Lemma get_top: forall p, get p top = L.top. -Proof. - unfold top; intros; simpl. rewrite PTree.gempty. auto. -Qed. - -Lemma ge_top: forall x, ge top x. -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. *) @@ -407,6 +374,168 @@ Qed. End COMBINE. +Definition lub (x y: t) : t := + combine + (fun a b => + match a, b with + | Some u, Some v => Some (L.lub u v) + | None, _ => b + | _, None => a + end) + x y. + +Lemma gcombine_bot: + forall f t1 t2 p, + f None None = None -> + L.eq (get p (combine f t1 t2)) + (match f t1!p t2!p with Some x => x | None => L.bot end). +Proof. + intros. unfold get. 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: + forall x y, ge (lub x y) x. +Proof. + unfold ge, lub; intros. + eapply L.ge_trans. apply L.ge_refl. apply gcombine_bot; auto. + unfold get. destruct x!p. destruct y!p. + apply L.ge_lub_left. + apply L.ge_refl. apply L.eq_refl. + apply L.ge_bot. +Qed. + +Lemma ge_lub_right: + forall x y, ge (lub x y) y. +Proof. + unfold ge, lub; intros. + eapply L.ge_trans. apply L.ge_refl. apply gcombine_bot; auto. + unfold get. destruct y!p. destruct x!p. + apply L.ge_lub_right. + apply L.ge_refl. apply L.eq_refl. + apply L.ge_bot. +Qed. + +End LPMap1. + +(** Given a semi-lattice with top [L], the following functor implements + a semi-lattice-with-top structure over finite maps from positive numbers to [L.t]. + The default value for these maps is [L.top]. Bottom elements are smashed. *) + +Module LPMap(L: SEMILATTICE_WITH_TOP) <: SEMILATTICE_WITH_TOP. + +Inductive t' : Type := + | Bot: t' + | Top_except: PTree.t L.t -> t'. + +Definition t: Type := t'. + +Definition get (p: positive) (x: t) : L.t := + match x with + | Bot => L.bot + | Top_except m => match m!p with None => L.top | Some x => x end + end. + +Definition set (p: positive) (v: L.t) (x: t) : t := + match x with + | Bot => Bot + | Top_except m => + if L.beq v L.bot + then Bot + else Top_except (if L.beq v L.top then PTree.remove p m else PTree.set p v m) + end. + +Lemma gsspec: + forall p v x q, + x <> Bot -> ~L.eq v L.bot -> + L.eq (get q (set p v x)) (if peq q p then v else get q x). +Proof. + intros. unfold set. destruct x. congruence. + destruct (L.beq v L.bot) eqn:EBOT. + elim H0. apply L.beq_correct; auto. + destruct (L.beq v L.top) eqn:ETOP; simpl. + rewrite PTree.grspec. unfold PTree.elt_eq. destruct (peq q p). + apply L.eq_sym. apply L.beq_correct; auto. + apply L.eq_refl. + rewrite PTree.gsspec. destruct (peq q p); apply L.eq_refl. +Qed. + +Definition eq (x y: t) : Prop := + forall p, L.eq (get p x) (get p y). + +Lemma eq_refl: forall x, eq x x. +Proof. + unfold eq; intros. apply L.eq_refl. +Qed. + +Lemma eq_sym: forall x y, eq x y -> eq y x. +Proof. + unfold eq; intros. apply L.eq_sym; auto. +Qed. + +Lemma eq_trans: forall x y z, eq x y -> eq y z -> eq x z. +Proof. + unfold eq; intros. eapply L.eq_trans; eauto. +Qed. + +Definition beq (x y: t) : bool := + match x, y with + | Bot, Bot => true + | Top_except m, Top_except n => PTree.beq L.beq m n + | _, _ => false + end. + +Lemma beq_correct: forall x y, beq x y = true -> eq x y. +Proof. + destruct x; destruct y; simpl; intro; try congruence. + apply eq_refl. + red; intro; simpl. + rewrite PTree.beq_correct in H. generalize (H p). + destruct (t0!p); destruct (t1!p); intuition. + apply L.beq_correct; auto. + apply L.eq_refl. +Qed. + +Definition ge (x y: t) : Prop := + forall p, L.ge (get p x) (get p y). + +Lemma ge_refl: forall x y, eq x y -> ge x y. +Proof. + unfold ge, eq; intros. apply L.ge_refl. auto. +Qed. + +Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. +Proof. + unfold ge; intros. apply L.ge_trans with (get p y); auto. +Qed. + +Definition bot := Bot. + +Lemma get_bot: forall p, get p bot = L.bot. +Proof. + unfold bot; intros; simpl. auto. +Qed. + +Lemma ge_bot: forall x, ge x bot. +Proof. + unfold ge; intros. rewrite get_bot. apply L.ge_bot. +Qed. + +Definition top := Top_except (PTree.empty L.t). + +Lemma get_top: forall p, get p top = L.top. +Proof. + unfold top; intros; simpl. rewrite PTree.gempty. auto. +Qed. + +Lemma ge_top: forall x, ge top x. +Proof. + unfold ge; intros. rewrite get_top. apply L.ge_top. +Qed. + +Module LM := LPMap1(L). + 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. @@ -417,7 +546,7 @@ Definition lub (x y: t) : t := | _, Bot => x | Top_except m, Top_except n => Top_except - (combine + (LM.combine (fun a b => match a, b with | Some u, Some v => opt_lub u v @@ -429,11 +558,11 @@ Definition lub (x y: t) : t := Lemma gcombine_top: forall f t1 t2 p, f None None = None -> - L.eq (get p (Top_except (combine f t1 t2))) + L.eq (get p (Top_except (LM.combine f t1 t2))) (match f t1!p t2!p with Some x => x | None => L.top 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). + intros. simpl. generalize (LM.gcombine f H t1 t2 p). unfold LM.opt_eq. + destruct ((LM.combine f t1 t2)!p); destruct (f t1!p t2!p). auto. contradiction. contradiction. intros; apply L.eq_refl. Qed. |