From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- lib/Lattice.v | 76 +++++++++++++++++++++++++++++------------------------------ 1 file changed, 38 insertions(+), 38 deletions(-) (limited to 'lib/Lattice.v') diff --git a/lib/Lattice.v b/lib/Lattice.v index 5a941a13..352b4479 100644 --- a/lib/Lattice.v +++ b/lib/Lattice.v @@ -27,7 +27,7 @@ Local Unset Case Analysis Schemes. (** * Signatures of semi-lattices *) (** A semi-lattice is a type [t] equipped with an equivalence relation [eq], - a boolean equivalence test [beq], a partial order [ge], a smallest element + a boolean equivalence test [beq], 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. *) @@ -86,9 +86,9 @@ Lemma gsspec: forall p v x q, L.eq (get q (set p v x)) (if peq q p then v else get q x). Proof. - intros. unfold set, get. + intros. unfold set, get. destruct (L.beq v L.bot) eqn:EBOT. - rewrite PTree.grspec. unfold PTree.elt_eq. destruct (peq q p). + 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. @@ -117,7 +117,7 @@ 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. unfold beq; intros; red; intros. unfold get. - rewrite PTree.beq_correct in H. specialize (H p). + 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. @@ -165,17 +165,17 @@ Definition opt_eq (ox oy: option L.t) : Prop := Lemma opt_eq_refl: forall ox, opt_eq ox ox. Proof. - intros. unfold opt_eq. destruct ox. apply L.eq_refl. auto. + 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. + 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. + unfold opt_eq. destruct ox; destruct oy; destruct oz; intuition. eapply L.eq_trans; eauto. Qed. @@ -189,8 +189,8 @@ Definition opt_beq (ox oy: option L.t) : bool := 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. + unfold opt_beq, opt_eq. destruct ox; destruct oy; try congruence. + intros. apply L.beq_correct; auto. auto. Qed. @@ -206,7 +206,7 @@ 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: +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). @@ -214,23 +214,23 @@ Proof. intros; red; intros. destruct i; simpl; auto. Qed. -Lemma tree_eq_node': +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. + intros; red; intros. rewrite PTree.gnode'. apply tree_eq_node; auto. Qed. -Lemma tree_eq_node'': +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. + intros; red; intros. repeat rewrite PTree.gnode'. apply tree_eq_node; auto. Qed. -Hint Resolve opt_beq_correct opt_eq_refl opt_eq_sym +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. @@ -296,7 +296,7 @@ Inductive changed2 : Type := Fixpoint xcombine (m1 m2 : PTree.t L.t) {struct m1} : changed2 := match m1, m2 with - | PTree.Leaf, PTree.Leaf => + | PTree.Leaf, PTree.Leaf => Same | PTree.Leaf, _ => match combine_r m2 with @@ -333,7 +333,7 @@ Fixpoint xcombine (m1 m2 : PTree.t L.t) {struct m1} : changed2 := end. Lemma xcombine_eq: - forall m1 m2, + 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) @@ -348,7 +348,7 @@ Opaque combine_l combine_r PTree.xcombine_l PTree.xcombine_r. 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). + 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. @@ -390,7 +390,7 @@ Lemma gcombine_bot: 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. + 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. @@ -398,9 +398,9 @@ Qed. Lemma ge_lub_left: forall x y, ge (lub x y) x. Proof. - unfold ge, lub; intros. + unfold ge, lub; intros. eapply L.ge_trans. apply L.ge_refl. apply gcombine_bot; auto. - unfold get. destruct x!p. destruct y!p. + 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. @@ -409,9 +409,9 @@ Qed. Lemma ge_lub_right: forall x y, ge (lub x y) y. Proof. - unfold ge, lub; intros. + unfold ge, lub; intros. eapply L.ge_trans. apply L.ge_refl. apply gcombine_bot; auto. - unfold get. destruct y!p. destruct x!p. + 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. @@ -451,11 +451,11 @@ Lemma gsspec: 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. + 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). + 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. @@ -561,7 +561,7 @@ Lemma gcombine_top: 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 (LM.gcombine f H t1 t2 p). unfold LM.opt_eq. + 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. @@ -574,10 +574,10 @@ Proof. rewrite get_bot. apply L.ge_bot. apply L.ge_refl. apply L.eq_refl. eapply L.ge_trans. apply L.ge_refl. apply gcombine_top; auto. - unfold get. destruct t0!p. destruct t1!p. + unfold get. destruct t0!p. destruct t1!p. unfold opt_lub. destruct (L.beq (L.lub t2 t3) L.top) eqn:E. - apply L.ge_top. apply L.ge_lub_left. - apply L.ge_top. + apply L.ge_top. apply L.ge_lub_left. + apply L.ge_top. apply L.ge_top. Qed. @@ -589,10 +589,10 @@ Proof. apply L.ge_refl. apply L.eq_refl. rewrite get_bot. apply L.ge_bot. eapply L.ge_trans. apply L.ge_refl. apply gcombine_top; auto. - unfold get. destruct t0!p; destruct t1!p. + unfold get. destruct t0!p; destruct t1!p. unfold opt_lub. destruct (L.beq (L.lub t2 t3) L.top) eqn:E. - apply L.ge_top. apply L.ge_lub_right. - apply L.ge_top. + apply L.ge_top. apply L.ge_lub_right. + apply L.ge_top. apply L.ge_top. apply L.ge_top. Qed. @@ -618,7 +618,7 @@ Module LFSet (S: FSetInterface.WS) <: SEMILATTICE. Definition ge (x y: t) := S.Subset y x. Lemma ge_refl: forall x y, eq x y -> ge x y. Proof. - unfold eq, ge, S.Equal, S.Subset; intros. firstorder. + unfold eq, ge, S.Equal, S.Subset; intros. firstorder. Qed. Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. Proof. @@ -635,12 +635,12 @@ Module LFSet (S: FSetInterface.WS) <: SEMILATTICE. Lemma ge_lub_left: forall x y, ge (lub x y) x. Proof. - unfold lub, ge, S.Subset; intros. apply S.union_2; auto. + 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. + unfold lub, ge, S.Subset; intros. apply S.union_3; auto. Qed. End LFSet. @@ -650,7 +650,7 @@ End LFSet. (** 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]. *) + [Bot < Inj x < Top]. *) Module LFlat(X: EQUALITY_TYPE) <: SEMILATTICE_WITH_TOP. @@ -735,7 +735,7 @@ Proof. Qed. End LFlat. - + (** * Boolean semi-lattice *) (** This semi-lattice has only two elements, [bot] and [top], trivially -- cgit