Commit 18cce8d0 authored by Ralf Jung's avatar Ralf Jung

prove open_close also for wp

parent a64118a2
Require Export algebra.base prelude.countable prelude.co_pset.
Require Import program_logic.ownership.
Require Export program_logic.pviewshifts.
Require Export program_logic.pviewshifts program_logic.weakestpre.
Import uPred.
Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of.
......@@ -69,6 +69,7 @@ Proof. by rewrite always_always. Qed.
any more. But that's okay; all this means is that sugar like the atomic
triples will have to prove its own version of the open_close rule
by unfolding `inv`. *)
(* TODO Can we prove something that helps for both open_close lemmas? *)
Lemma pvs_open_close E N P Q R :
nclose N E
P (inv N R (R - pvs (E nclose N) (E nclose N) (R Q)))%I
......@@ -77,22 +78,38 @@ Proof.
move=>HN -> {P}.
rewrite /inv and_exist_r. apply exist_elim=>i.
rewrite -associative. apply const_elim_l=>HiN.
rewrite -(pvs_trans3 E (E {[encode i]})) //; last by solve_elem_of+.
(* Add this to the local context, so that solve_elem_of finds it. *)
assert ({[encode i]} nclose N) by eauto.
rewrite always_and_sep_l' (always_sep_dup' (ownI _ _)).
rewrite {1}pvs_openI !pvs_frame_r.
(* TODO is there a common pattern here in the way we combine pvs_trans
and pvs_mask_frame_mono? *)
rewrite -(pvs_trans E (E {[ encode i ]}));
last by solve_elem_of. (* FIXME: Shouldn't eauto work, since I added a Hint Extern? *)
apply pvs_mask_frame_mono; [solve_elem_of..|].
apply pvs_mask_frame_mono ; [solve_elem_of..|].
rewrite (commutative _ (R)%I) -associative wand_elim_r pvs_frame_l.
rewrite -(pvs_trans _ (E {[ encode i ]}) E); last by solve_elem_of.
apply pvs_mask_frame_mono; [solve_elem_of..|].
rewrite associative -always_and_sep_l' pvs_closeI pvs_frame_r left_id.
apply pvs_mask_frame'; solve_elem_of.
Qed.
Lemma wp_open_close E e N P (Q : val Λ iProp Λ Σ) R :
atomic e nclose N E
P (inv N R (R - wp (E nclose N) e (λ v, R Q v)))%I
P wp E e Q.
Proof.
move=>He HN -> {P}.
rewrite /inv and_exist_r. apply exist_elim=>i.
rewrite -associative. apply const_elim_l=>HiN.
rewrite -(wp_atomic E (E {[encode i]})) //; last by solve_elem_of+.
(* Add this to the local context, so that solve_elem_of finds it. *)
assert ({[encode i]} nclose N) by eauto.
rewrite always_and_sep_l' (always_sep_dup' (ownI _ _)).
rewrite {1}pvs_openI !pvs_frame_r.
apply pvs_mask_frame_mono; [solve_elem_of..|].
rewrite (commutative _ (R)%I) -associative wand_elim_r wp_frame_l.
apply wp_mask_frame_mono; [solve_elem_of..|]=>v.
rewrite associative -always_and_sep_l' pvs_closeI pvs_frame_r left_id.
apply pvs_mask_frame'; solve_elem_of.
Qed.
Lemma pvs_alloc N P : P pvs N N (inv N P).
Proof.
rewrite /inv (pvs_allocI N); first done.
......
......@@ -158,6 +158,12 @@ Lemma pvs_mask_frame_mono E1 E1' E2 E2' P Q :
P Q pvs E1' E2' P pvs E1 E2 Q.
Proof. intros HE1 HE2 HEE ->. by apply pvs_mask_frame'. Qed.
Lemma pvs_trans3 E1 E2 Q :
E2 E1 pvs E1 E2 (pvs E2 E2 (pvs E2 E1 Q)) pvs E1 E1 Q.
Proof.
move=>HE. rewrite !pvs_trans; first done; solve_elem_of.
Qed.
Lemma pvs_mask_weaken E1 E2 P : E1 E2 pvs E1 E1 P pvs E2 E2 P.
Proof.
intros. apply pvs_mask_frame'; solve_elem_of.
......
......@@ -186,6 +186,13 @@ Lemma wp_value' E Q e v : to_val e = Some v → Q v ⊑ wp E e Q.
Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value. Qed.
Lemma wp_frame_l E e Q R : (R wp E e Q) wp E e (λ v, R Q v).
Proof. setoid_rewrite (commutative _ R); apply wp_frame_r. Qed.
Lemma wp_mask_frame_mono E E' e (P Q : val Λ iProp Λ Σ) :
E' E
( v, P v Q v) wp E' e P wp E e Q.
Proof.
intros HE HPQ. rewrite wp_mask_weaken; last eexact HE.
by apply wp_mono.
Qed.
Lemma wp_frame_later_l E e Q R :
to_val e = None ( R wp E e Q) wp E e (λ v, R Q v).
Proof.
......
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