From 877ff8482ba084a85ac3613ee11fc388d9a7698d Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Tue, 9 Feb 2016 23:00:23 +0100 Subject: [PATCH] Notation for = in uPred_scope. --- algebra/upred.v | 1 + heap_lang/lifting.v | 6 +++--- heap_lang/tests.v | 4 ++-- 3 files changed, 6 insertions(+), 5 deletions(-) diff --git a/algebra/upred.v b/algebra/upred.v index e07d358d..146d71c6 100644 --- a/algebra/upred.v +++ b/algebra/upred.v @@ -209,6 +209,7 @@ Arguments uPred_entails _ _%I _%I. Notation "P ⊑ Q" := (uPred_entails P%I Q%I) (at level 70) : C_scope. Notation "(⊑)" := uPred_entails (only parsing) : C_scope. Notation "■ φ" := (uPred_const φ%type) (at level 20) : uPred_scope. +Notation "x = y" := (uPred_const (x%type = y%type)) : uPred_scope. Notation "'False'" := (uPred_const False) : uPred_scope. Notation "'True'" := (uPred_const True) : uPred_scope. Infix "∧" := uPred_and : uPred_scope. diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v index 64236156..8bbf0350 100644 --- a/heap_lang/lifting.v +++ b/heap_lang/lifting.v @@ -22,7 +22,7 @@ Proof. apply weakestpre.wp_bind. Qed. (** Base axioms for core primitives of the language: Stateful reductions. *) Lemma wp_alloc_pst E σ e v Q : to_val e = Some v → - (ownP σ ★ ▷ (∀ l, ■(σ !! l = None) ∧ ownP (<[l:=v]>σ) -★ Q (LocV l))) + (ownP σ ★ ▷ (∀ l, σ !! l = None ∧ ownP (<[l:=v]>σ) -★ Q (LocV l))) ⊑ wp E (Alloc e) Q. Proof. (* TODO RJ: This works around ssreflect bug #22. *) @@ -48,7 +48,7 @@ Qed. Lemma wp_store_pst E σ l e v v' Q : to_val e = Some v → σ !! l = Some v' → - (ownP σ ★ ▷ (ownP (<[l:=v]>σ) -★ Q \$ LitV LitUnit)) ⊑ wp E (Store (Loc l) e) Q. + (ownP σ ★ ▷ (ownP (<[l:=v]>σ) -★ Q (LitV LitUnit))) ⊑ wp E (Store (Loc l) e) Q. Proof. intros. rewrite -(wp_lift_atomic_det_step σ (LitV LitUnit) (<[l:=v]>σ) None) ?right_id //; last by intros; inv_step; eauto. @@ -73,7 +73,7 @@ Qed. (** Base axioms for core primitives of the language: Stateless reductions *) Lemma wp_fork E e : - ▷ wp (Σ:=Σ) coPset_all e (λ _, True) ⊑ wp E (Fork e) (λ v, ■(v = LitV LitUnit)). + ▷ wp (Σ:=Σ) coPset_all e (λ _, True) ⊑ wp E (Fork e) (λ v, v = LitV LitUnit). Proof. rewrite -(wp_lift_pure_det_step (Fork e) (Lit LitUnit) (Some e)) //=; last by intros; inv_step; eauto. diff --git a/heap_lang/tests.v b/heap_lang/tests.v index 317277cc..fff9f45f 100644 --- a/heap_lang/tests.v +++ b/heap_lang/tests.v @@ -28,7 +28,7 @@ Module LiftingTests. Definition e : expr := let: "x" := ref (Lit 1) in "x" <- !"x" + Lit 1; !"x". - Goal ∀ σ E, (ownP σ : iProp heap_lang Σ) ⊑ (wp E e (λ v, ■ (v = LitV 2))). + Goal ∀ σ E, ownP (Σ:=Σ) σ ⊑ wp E e (λ v, v = LitV 2). Proof. move=> σ E. rewrite /e. rewrite -wp_let /= -wp_alloc_pst //=. @@ -97,7 +97,7 @@ Module LiftingTests. Goal ∀ E, True ⊑ wp (Σ:=Σ) E (let: "x" := Pred (Lit 42) in Pred "x") - (λ v, ■ (v = LitV 40)). + (λ v, v = LitV 40). Proof. intros E. rewrite -wp_let. rewrite -Pred_spec -!later_intro /=. rewrite -Pred_spec -later_intro. by apply const_intro. -- GitLab