Skip to content
Snippets Groups Projects
Commit e88e2129 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents 5b0c6378 3d01a881
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
barrier/proof.v
+ 2
− 2
View file @ e88e2129
...@@ -325,7 +325,7 @@ Proof. ...@@ -325,7 +325,7 @@ Proof.
rewrite !wand_diag -!later_intro. solve_sep_entails. rewrite !wand_diag -!later_intro. solve_sep_entails.
Qed. Qed.
Lemma recv_strengthen l P1 P2 : Lemma recv_weaken l P1 P2 :
(P1 -★ P2) ⊑ (recv l P1 -★ recv l P2). (P1 -★ P2) ⊑ (recv l P1 -★ recv l P2).
Proof. Proof.
apply wand_intro_l. rewrite /recv. rewrite sep_exist_r. apply exist_mono=>γ. apply wand_intro_l. rewrite /recv. rewrite sep_exist_r. apply exist_mono=>γ.
...@@ -339,7 +339,7 @@ Qed. ...@@ -339,7 +339,7 @@ Qed.
Lemma recv_mono l P1 P2 : Lemma recv_mono l P1 P2 :
P1 ⊑ P2 → recv l P1 ⊑ recv l P2. P1 ⊑ P2 → recv l P1 ⊑ recv l P2.
Proof. Proof.
intros HP%entails_wand. apply wand_entails. rewrite HP. apply recv_strengthen. intros HP%entails_wand. apply wand_entails. rewrite HP. apply recv_weaken.
Qed. Qed.
End proof. End proof.
barrier/specification.v
+ 1
− 1
View file @ e88e2129
...@@ -29,6 +29,6 @@ Proof. ...@@ -29,6 +29,6 @@ Proof.
- intros l P. apply ht_alt. - intros l P. apply ht_alt.
by rewrite -(wait_spec heapN N l P) wand_diag right_id. by rewrite -(wait_spec heapN N l P) wand_diag right_id.
- intros l P Q. apply vs_alt. rewrite -(recv_split heapN N N l P Q) //. - intros l P Q. apply vs_alt. rewrite -(recv_split heapN N N l P Q) //.
- intros l P Q. apply recv_strengthen. - intros l P Q. apply recv_weaken.
Qed. Qed.
End spec. End spec.
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