From 2ae43be7b9d4118335c9d2cef6e098f9b9f807fe Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 9 Feb 2006 14:55:48 +0000 Subject: Initial import of compcert git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Lattice.v | 331 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 331 insertions(+) create mode 100644 lib/Lattice.v (limited to 'lib/Lattice.v') diff --git a/lib/Lattice.v b/lib/Lattice.v new file mode 100644 index 00000000..7adcffba --- /dev/null +++ b/lib/Lattice.v @@ -0,0 +1,331 @@ +(** Constructions of semi-lattices. *) + +Require Import Coqlib. +Require Import Maps. + +(** * Signatures of semi-lattices *) + +(** A semi-lattice is a type [t] equipped with a decidable equality [eq], + a partial order [ge], a smallest element [bot], and an upper + bound operation [lub]. Note that we do not demand that [lub] computes + the least upper bound. *) + +Module Type SEMILATTICE. + + Variable t: Set. + Variable eq: forall (x y: t), {x=y} + {x<>y}. + Variable ge: t -> t -> Prop. + Hypothesis ge_refl: forall x, ge x x. + Hypothesis ge_trans: forall x y z, ge x y -> ge y z -> ge x z. + Variable bot: t. + Hypothesis ge_bot: forall x, ge x bot. + Variable lub: t -> t -> t. + Hypothesis lub_commut: forall x y, lub x y = lub y x. + Hypothesis ge_lub_left: forall x y, ge (lub x y) x. + +End SEMILATTICE. + +(** A semi-lattice ``with top'' is similar, but also has a greatest + element [top]. *) + +Module Type SEMILATTICE_WITH_TOP. + + Variable t: Set. + Variable eq: forall (x y: t), {x=y} + {x<>y}. + Variable ge: t -> t -> Prop. + Hypothesis ge_refl: forall x, ge x x. + Hypothesis ge_trans: forall x y z, ge x y -> ge y z -> ge x z. + Variable bot: t. + Hypothesis ge_bot: forall x, ge x bot. + Variable top: t. + Hypothesis ge_top: forall x, ge top x. + Variable lub: t -> t -> t. + Hypothesis lub_commut: forall x y, lub x y = lub y x. + Hypothesis ge_lub_left: forall x y, ge (lub x y) x. + +End SEMILATTICE_WITH_TOP. + +(** * Semi-lattice over maps *) + +(** 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]. *) + +Module LPMap(L: SEMILATTICE_WITH_TOP) <: SEMILATTICE_WITH_TOP. + +Inductive t_ : Set := + | Bot_except: PTree.t L.t -> t_ + | Top_except: PTree.t L.t -> t_. + +Definition t: Set := t_. + +Lemma eq: forall (x y: t), {x=y} + {x<>y}. +Proof. + assert (forall m1 m2: PTree.t L.t, {m1=m2} + {m1<>m2}). + apply PTree.eq. exact L.eq. + decide equality. +Qed. + +Definition get (p: positive) (x: t) : L.t := + match x with + | Bot_except m => + match m!p with None => L.bot | Some x => x end + | 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_except m => + Bot_except (PTree.set p v m) + | Top_except m => + Top_except (PTree.set p v m) + end. + +Lemma gss: + forall p v x, + get p (set p v x) = v. +Proof. + intros. destruct x; simpl; rewrite PTree.gss; auto. +Qed. + +Lemma gso: + forall p q v x, + p <> q -> get p (set q v x) = get p x. +Proof. + intros. destruct x; simpl; rewrite PTree.gso; auto. +Qed. + +Definition ge (x y: t) : Prop := + forall p, L.ge (get p x) (get p y). + +Lemma ge_refl: forall x, ge x x. +Proof. + unfold ge; intros. apply L.ge_refl. +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_except (PTree.empty L.t). + +Lemma get_bot: forall p, get p bot = L.bot. +Proof. + unfold bot; intros; simpl. rewrite PTree.gempty. 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. + +Definition lub (x y: t) : t := + match x, y with + | Bot_except m, Bot_except n => + Bot_except + (PTree.combine + (fun a b => + match a, b with + | Some u, Some v => Some (L.lub u v) + | None, _ => b + | _, None => a + end) + m n) + | Bot_except m, Top_except n => + Top_except + (PTree.combine + (fun a b => + match a, b with + | Some u, Some v => Some (L.lub u v) + | None, _ => b + | _, None => None + end) + m n) + | Top_except m, Bot_except n => + Top_except + (PTree.combine + (fun a b => + match a, b with + | Some u, Some v => Some (L.lub u v) + | None, _ => None + | _, None => a + end) + m n) + | Top_except m, Top_except n => + Top_except + (PTree.combine + (fun a b => + match a, b with + | Some u, Some v => Some (L.lub u v) + | _, _ => None + end) + m n) + end. + +Lemma lub_commut: + forall x y, lub x y = lub y x. +Proof. + destruct x; destruct y; unfold lub; decEq; + apply PTree.combine_commut; intros; + (destruct i; destruct j; auto; decEq; apply L.lub_commut). +Qed. + +Lemma ge_lub_left: + forall x y, ge (lub x y) x. +Proof. + unfold ge, get, lub; intros; destruct x; destruct y. + + rewrite PTree.gcombine. + destruct t0!p. destruct t1!p. apply L.ge_lub_left. + apply L.ge_refl. destruct t1!p. apply L.ge_bot. apply L.ge_refl. + auto. + + rewrite PTree.gcombine. + destruct t0!p. destruct t1!p. apply L.ge_lub_left. + apply L.ge_top. destruct t1!p. apply L.ge_bot. apply L.ge_bot. + auto. + + rewrite PTree.gcombine. + destruct t0!p. destruct t1!p. apply L.ge_lub_left. + apply L.ge_refl. apply L.ge_refl. auto. + + rewrite PTree.gcombine. + destruct t0!p. destruct t1!p. apply L.ge_lub_left. + apply L.ge_top. apply L.ge_refl. + auto. +Qed. + +End LPMap. + +(** * Flat semi-lattice *) + +(** Given a type with decidable equality [X], the following functor + returns a semi-lattice structure over [X.t] complemented with + a top and a bottom element. The ordering is the flat ordering + [Bot < Inj x < Top]. *) + +Module LFlat(X: EQUALITY_TYPE) <: SEMILATTICE_WITH_TOP. + +Inductive t_ : Set := + | Bot: t_ + | Inj: X.t -> t_ + | Top: t_. + +Definition t : Set := t_. + +Lemma eq: forall (x y: t), {x=y} + {x<>y}. +Proof. + decide equality. apply X.eq. +Qed. + +Definition ge (x y: t) : Prop := + match x, y with + | Top, _ => True + | _, Bot => True + | Inj a, Inj b => a = b + | _, _ => False + end. + +Lemma ge_refl: forall x, ge x x. +Proof. + unfold ge; destruct x; auto. +Qed. + +Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. +Proof. + unfold ge; destruct x; destruct y; try destruct z; intuition. + transitivity t1; auto. +Qed. + +Definition bot: t := Bot. + +Lemma ge_bot: forall x, ge x bot. +Proof. + destruct x; simpl; auto. +Qed. + +Definition top: t := Top. + +Lemma ge_top: forall x, ge top x. +Proof. + destruct x; simpl; auto. +Qed. + +Definition lub (x y: t) : t := + match x, y with + | Bot, _ => y + | _, Bot => x + | Top, _ => Top + | _, Top => Top + | Inj a, Inj b => if X.eq a b then Inj a else Top + end. + +Lemma lub_commut: forall x y, lub x y = lub y x. +Proof. + destruct x; destruct y; simpl; auto. + case (X.eq t0 t1); case (X.eq t1 t0); intros; congruence. +Qed. + +Lemma ge_lub_left: forall x y, ge (lub x y) x. +Proof. + destruct x; destruct y; simpl; auto. + case (X.eq t0 t1); simpl; auto. +Qed. + +End LFlat. + +(** * Boolean semi-lattice *) + +(** This semi-lattice has only two elements, [bot] and [top], trivially + ordered. *) + +Module LBoolean <: SEMILATTICE_WITH_TOP. + +Definition t := bool. + +Lemma eq: forall (x y: t), {x=y} + {x<>y}. +Proof. decide equality. Qed. + +Definition ge (x y: t) : Prop := x = y \/ x = true. + +Lemma ge_refl: forall x, ge x x. +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. + +Definition bot := false. + +Lemma ge_bot: forall x, ge x bot. +Proof. destruct x; compute; tauto. Qed. + +Definition top := true. + +Lemma ge_top: forall x, ge top x. +Proof. unfold ge, top; tauto. Qed. + +Definition lub (x y: t) := x || y. + +Lemma lub_commut: forall x y, lub x y = lub y x. +Proof. intros; unfold 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. + +End LBoolean. + + -- cgit