Commit 672dff6d authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Use proper notations in saved_prop.

parent efc8fb86
...@@ -25,26 +25,24 @@ Section one_shot. ...@@ -25,26 +25,24 @@ Section one_shot.
Global Instance ne_shot_own_persistent γ x : PersistentP (one_shot_own γ x). Global Instance ne_shot_own_persistent γ x : PersistentP (one_shot_own γ x).
Proof. rewrite /one_shot_own; apply _. Qed. Proof. rewrite /one_shot_own; apply _. Qed.
Lemma one_shot_alloc_strong N (G : gset gname) : Lemma one_shot_alloc_strong E (G : gset gname) :
True pvs N N ( γ, (γ G) one_shot_pending γ). True |={E}=> γ, (γ G) one_shot_pending γ.
Proof. by apply own_alloc_strong. Qed. Proof. by apply own_alloc_strong. Qed.
Lemma one_shot_alloc N : True pvs N N ( γ, one_shot_pending γ). Lemma one_shot_alloc E : True |={E}=> γ, one_shot_pending γ.
Proof. by apply own_alloc. Qed. Proof. by apply own_alloc. Qed.
Lemma one_shot_init N γ x : Lemma one_shot_init E γ x : one_shot_pending γ |={E}=> one_shot_own γ x.
one_shot_pending γ pvs N N (one_shot_own γ x).
Proof. by apply own_update, one_shot_update_shoot. Qed. Proof. by apply own_update, one_shot_update_shoot. Qed.
Lemma one_shot_alloc_init N x : True pvs N N ( γ, one_shot_own γ x). Lemma one_shot_alloc_init E x : True |={E}=> γ, one_shot_own γ x.
Proof. Proof.
rewrite (one_shot_alloc N). apply pvs_strip_pvs. rewrite (one_shot_alloc E). apply pvs_strip_pvs.
apply exist_elim=>γ. rewrite -(exist_intro γ). apply exist_elim=>γ. rewrite -(exist_intro γ).
apply one_shot_init. apply one_shot_init.
Qed. Qed.
Lemma one_shot_agree γ x y : Lemma one_shot_agree γ x y : (one_shot_own γ x one_shot_own γ y) (x y).
(one_shot_own γ x one_shot_own γ y) (x y).
Proof. Proof.
rewrite -own_op own_valid one_shot_validI /= agree_validI. rewrite -own_op own_valid one_shot_validI /= agree_validI.
rewrite agree_equivI later_equivI. rewrite agree_equivI later_equivI.
......
...@@ -23,11 +23,11 @@ Section saved_prop. ...@@ -23,11 +23,11 @@ Section saved_prop.
Global Instance saved_prop_persistent γ x : PersistentP (saved_prop_own γ x). Global Instance saved_prop_persistent γ x : PersistentP (saved_prop_own γ x).
Proof. rewrite /saved_prop_own; apply _. Qed. Proof. rewrite /saved_prop_own; apply _. Qed.
Lemma saved_prop_alloc_strong N x (G : gset gname) : Lemma saved_prop_alloc_strong E x (G : gset gname) :
True pvs N N ( γ, (γ G) saved_prop_own γ x). True |={E}=> γ, (γ G) saved_prop_own γ x.
Proof. by apply own_alloc_strong. Qed. Proof. by apply own_alloc_strong. Qed.
Lemma saved_prop_alloc N x : True pvs N N ( γ, saved_prop_own γ x). Lemma saved_prop_alloc E x : True |={E}=> γ, saved_prop_own γ x.
Proof. by apply own_alloc. Qed. Proof. by apply own_alloc. Qed.
Lemma saved_prop_agree γ x y : Lemma saved_prop_agree γ x y :
......
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