Commit 877ff848 authored by Robbert Krebbers's avatar Robbert Krebbers

Notation for = in uPred_scope.

parent 6646e43c
...@@ -209,6 +209,7 @@ Arguments uPred_entails _ _%I _%I. ...@@ -209,6 +209,7 @@ Arguments uPred_entails _ _%I _%I.
Notation "P ⊑ Q" := (uPred_entails P%I Q%I) (at level 70) : C_scope. Notation "P ⊑ Q" := (uPred_entails P%I Q%I) (at level 70) : C_scope.
Notation "(⊑)" := uPred_entails (only parsing) : C_scope. Notation "(⊑)" := uPred_entails (only parsing) : C_scope.
Notation "■ φ" := (uPred_const φ%type) (at level 20) : uPred_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 "'False'" := (uPred_const False) : uPred_scope.
Notation "'True'" := (uPred_const True) : uPred_scope. Notation "'True'" := (uPred_const True) : uPred_scope.
Infix "∧" := uPred_and : uPred_scope. Infix "∧" := uPred_and : uPred_scope.
......
...@@ -22,7 +22,7 @@ Proof. apply weakestpre.wp_bind. Qed. ...@@ -22,7 +22,7 @@ Proof. apply weakestpre.wp_bind. Qed.
(** Base axioms for core primitives of the language: Stateful reductions. *) (** Base axioms for core primitives of the language: Stateful reductions. *)
Lemma wp_alloc_pst E σ e v Q : Lemma wp_alloc_pst E σ e v Q :
to_val e = Some v 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. wp E (Alloc e) Q.
Proof. Proof.
(* TODO RJ: This works around ssreflect bug #22. *) (* TODO RJ: This works around ssreflect bug #22. *)
...@@ -48,7 +48,7 @@ Qed. ...@@ -48,7 +48,7 @@ Qed.
Lemma wp_store_pst E σ l e v v' Q : Lemma wp_store_pst E σ l e v v' Q :
to_val e = Some v σ !! l = Some v' 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. Proof.
intros. rewrite -(wp_lift_atomic_det_step σ (LitV LitUnit) (<[l:=v]>σ) None) intros. rewrite -(wp_lift_atomic_det_step σ (LitV LitUnit) (<[l:=v]>σ) None)
?right_id //; last by intros; inv_step; eauto. ?right_id //; last by intros; inv_step; eauto.
...@@ -73,7 +73,7 @@ Qed. ...@@ -73,7 +73,7 @@ Qed.
(** Base axioms for core primitives of the language: Stateless reductions *) (** Base axioms for core primitives of the language: Stateless reductions *)
Lemma wp_fork E e : 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. Proof.
rewrite -(wp_lift_pure_det_step (Fork e) (Lit LitUnit) (Some e)) //=; rewrite -(wp_lift_pure_det_step (Fork e) (Lit LitUnit) (Some e)) //=;
last by intros; inv_step; eauto. last by intros; inv_step; eauto.
......
...@@ -28,7 +28,7 @@ Module LiftingTests. ...@@ -28,7 +28,7 @@ Module LiftingTests.
Definition e : expr := Definition e : expr :=
let: "x" := ref (Lit 1) in "x" <- !"x" + Lit 1; !"x". 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. Proof.
move=> σ E. rewrite /e. move=> σ E. rewrite /e.
rewrite -wp_let /= -wp_alloc_pst //=. rewrite -wp_let /= -wp_alloc_pst //=.
...@@ -97,7 +97,7 @@ Module LiftingTests. ...@@ -97,7 +97,7 @@ Module LiftingTests.
Goal E, Goal E,
True wp (Σ:=Σ) E (let: "x" := Pred (Lit 42) in Pred "x") True wp (Σ:=Σ) E (let: "x" := Pred (Lit 42) in Pred "x")
(λ v, (v = LitV 40)). (λ v, v = LitV 40).
Proof. Proof.
intros E. rewrite -wp_let. rewrite -Pred_spec -!later_intro /=. intros E. rewrite -wp_let. rewrite -Pred_spec -!later_intro /=.
rewrite -Pred_spec -later_intro. by apply const_intro. rewrite -Pred_spec -later_intro. by apply const_intro.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment