Commit 40b27d98 authored by Robbert Krebbers's avatar Robbert Krebbers

Seal off U.

parent 46b315e0
......@@ -386,7 +386,7 @@ Section proofs.
iApply awp_atomic_env. iIntros (env) "Henv $". iApply wp_fupd.
iDestruct "Henv" as (X σ _) "[Hlocks Hσ]".
wp_lam. wp_apply (mset_clear_spec with "Hlocks"); iIntros "Hlocks".
iDestruct "H" as (us) "[Hus H]".
rewrite U_eq. iDestruct "H" as (us) "[Hus H]".
iInduction us as [|[ul [uq uv]] us] "IH" forall (σ); simpl.
- iModIntro. iSplitR "H".
+ iExists , σ. by iFrame.
......
......@@ -7,25 +7,30 @@ Section U.
Context `{heapG Σ, locking_heapG Σ}.
(** * Unlocking modality *)
Definition U (P : iProp Σ) : iProp Σ :=
Definition U_def (P : iProp Σ) : iProp Σ :=
( ls : list (cloc * (frac * val)),
([ list] x ls, x.1 C[LLvl]{x.2.1} x.2.2)
(([ list] x ls, x.1 C{x.2.1} x.2.2) - P))%I.
Definition U_aux : seal (@U_def). by eexists. Qed.
Definition U := unseal U_aux.
Definition U_eq : @U = @U_def := seal_eq U_aux.
Lemma U_mono P Q : (P Q) U P U Q.
Proof.
intros HPQ.
unfold U. iDestruct 1 as (ls) "[Hls HP]".
iExists ls. iFrame. iIntros "Hls". iApply HPQ. by iApply "HP".
Qed.
Global Instance U_ne : NonExpansive U.
Proof. rewrite U_eq. solve_proper. Qed.
Global Instance U_proper : Proper (() ==> ()) U.
Proof. rewrite U_eq. solve_proper. Qed.
Global Instance U_mono' : Proper (() ==> ()) U.
Proof. rewrite U_eq. solve_proper. Qed.
Global Instance U_flip_mono' : Proper (flip () ==> flip ()) U.
Proof. rewrite U_eq. solve_proper. Qed.
Lemma U_intro P : P U P.
Proof. iIntros "HP". iExists []. eauto. Qed.
Proof. iIntros "HP". rewrite U_eq. iExists []. eauto. Qed.
(** [U] behaves like an applicative functor aka "lax functor with a strength" *)
Lemma U_sep_2 P Q : U P U Q U (P Q).
Proof.
iIntros "[HP HQ]".
iIntros "[HP HQ]". rewrite U_eq.
iDestruct "HP" as (ls1) "[HP1 HP2]".
iDestruct "HQ" as (ls2) "[HQ1 HQ2]".
iExists (ls1 ++ ls2). iFrame.
......@@ -34,31 +39,32 @@ Section U.
- by iApply "HQ2".
Qed.
Global Instance U_monoid_morphism : MonoidHomomorphism bi_sep bi_sep (flip ()) U.
Proof. split. split; try apply _. solve_proper. apply U_sep_2. apply U_intro. Qed.
Lemma U_big_sepL {A} (l : list A) Φ :
(([ list] ix l, U (Φ i x)) U ([ list] ix l, Φ i x))%I.
Proof. apply big_opL_commute, _. Qed.
Lemma U_stength P Q : P U Q U (P Q).
Proof. by rewrite {1}(U_intro P) U_sep_2. Qed.
Lemma U_applicative P Q : U (P - Q) U P - U Q.
Proof.
iDestruct 1 as (ls1) "[HPQ1 HPQ2]".
iDestruct 1 as (ls2) "[HP1 HP2]".
iExists (ls1++ls2). rewrite !big_sepL_app. iFrame.
iIntros "[HPQ1 HP1]".
iApply ("HPQ2" with "HPQ1").
iApply ("HP2" with "HP1").
Qed.
Lemma U_unlock l q v : l C[LLvl]{q} v U (l C{q} v).
Proof.
iIntros "Hl". iExists [(l,(q,v))]. iIntros "/= {$Hl} [$ _]".
iIntros "Hl". rewrite U_eq. iExists [(l,(q,v))]. iIntros "/= {$Hl} [$ _]".
Qed.
(* Derived properties *)
Lemma U_mono P Q : (P Q) U P U Q.
Proof. by intros ->. Qed.
Lemma U_applicative P Q : U (P - Q) U P - U Q.
Proof. apply bi.wand_intro_l. by rewrite U_sep_2 bi.wand_elim_r. Qed.
Global Instance U_monoid_morphism : MonoidHomomorphism bi_sep bi_sep (flip ()) U.
Proof. split; [split|]; try apply _. apply U_sep_2. apply U_intro. Qed.
Lemma U_big_sepL {A} (l : list A) Φ :
(([ list] ix l, U (Φ i x)) U ([ list] ix l, Φ i x))%I.
Proof. apply big_opL_commute, _. Qed.
(* Proof mode stuff *)
Global Instance frame_U p R P Q : Frame p R P Q Frame p R (U P) (U Q).
Proof. rewrite /Frame=> HRQ. by rewrite U_stength HRQ. Qed.
Class IntoUnlock (P Q : iProp Σ) := into_unlock : P U Q.
Global Instance into_unlock_intro P : IntoUnlock (U P) P.
Proof. rewrite /IntoUnlock. reflexivity. Qed.
......
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