Commit b92e8df1 authored by Zhen Zhang's avatar Zhen Zhang
Browse files

Add weakest-pre version atomic_triple

parent 6edb53e7
From iris.program_logic Require Export hoare weakestpre. From iris.program_logic Require Export hoare weakestpre pviewshifts ownership.
From iris.program_logic Require Export pviewshifts.
From iris.program_logic Require Import ownership.
From iris.algebra Require Import upred_big_op. From iris.algebra Require Import upred_big_op.
From iris.prelude Require Export coPset. From iris.prelude Require Export coPset.
From iris.proofmode Require Import tactics pviewshifts weakestpre. From iris.proofmode Require Import tactics pviewshifts weakestpre.
Import uPred. Import uPred.
Section atomic. Section atomic.
Context `{irisG Λ Σ}. Context `{irisG Λ Σ} {A: Type}.
(* <x, α> e @ E_i, E_o <v, β x v> *)
Definition atomic_triple {A: Type} (* logically atomic triple: <x, α> e @ E_i, E_o <v, β x v> *)
Definition atomic_triple
(α: A iProp Σ) (α: A iProp Σ)
(β: A val _ iProp Σ) (β: A val _ iProp Σ)
(Ei Eo: coPset) (Ei Eo: coPset)
...@@ -20,14 +19,32 @@ Section atomic. ...@@ -20,14 +19,32 @@ Section atomic.
( v, β x v ={Ei, Eo}= Q x v)) ( v, β x v ={Ei, Eo}= Q x v))
) - {{ P }} e @ {{ v, ( x: A, Q x v) }})%I. ) - {{ P }} e @ {{ v, ( x: A, Q x v) }})%I.
Arguments atomic_triple {_} _ _ _ _ _. (* Weakest-pre version of the above one. Also weaker in some sense *)
Definition atomic_triple_wp
(α: A iProp Σ)
(β: A val _ iProp Σ)
(Ei Eo: coPset)
(e: expr _) : iProp Σ :=
( P Q, (P ={Eo, Ei}=> x,
α x
((α x ={Ei, Eo}= P)
( v, β x v ={Ei, Eo}= Q x v))
) - P - WP e @ {{ v, ( x, Q x v) }})%I.
Lemma atomic_triple_weaken α β Ei Eo e:
atomic_triple α β Ei Eo e atomic_triple_wp α β Ei Eo e.
Proof.
iIntros "H". iIntros (P Q) "Hvs Hp".
by iApply ("H" $! P Q with "Hvs").
Qed.
Arguments atomic_triple {_} _ _ _ _.
End atomic. End atomic.
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang proofmode notation.
From iris.proofmode Require Import invariants tactics. From iris.proofmode Require Import invariants.
From iris.heap_lang Require Import proofmode notation.
Section demo. Section incr.
Context `{!heapG Σ} (N : namespace). Context `{!heapG Σ} (N : namespace).
Definition incr: val := Definition incr: val :=
...@@ -74,7 +91,7 @@ Section demo. ...@@ -74,7 +91,7 @@ Section demo.
iVs ("Hvs'" with "[Hl]") as "HP"; first by iFrame. iVs ("Hvs'" with "[Hl]") as "HP"; first by iFrame.
iVsIntro. wp_if. by iApply "IH". iVsIntro. wp_if. by iApply "IH".
Qed. Qed.
End demo. End incr.
From iris.heap_lang.lib Require Import par. From iris.heap_lang.lib Require Import par.
......
Supports Markdown
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