From iris.heap_lang Require Export proofmode notation. From iris.algebra Require Import frac. From iris_c.lib Require Import locking_heap. From iris.proofmode Require Import modalities classes. Section U. Context `{heapG Σ, locking_heapG Σ}. (** * Unlocking modality *) Definition U_def (P : iProp Σ) : iProp Σ := (∃ ls : gmultiset (cloc * (frac * val)), ([∗ mset] x ∈ ls, x.1 ↦C[LLvl]{x.2.1} x.2.2) ∗ (([∗ mset] 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. 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". 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]". rewrite U_eq. iDestruct "HP" as (ls1) "[HP1 HP2]". iDestruct "HQ" as (ls2) "[HQ1 HQ2]". iExists (ls1 ∪ ls2). iFrame "HP1 HQ1". iIntros "[HP1 HQ1]". iSplitL "HP1 HP2". - by iApply "HP2". - by iApply "HQ2". 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_unlock l q v : l ↦C[LLvl]{q} v ⊢ U (l ↦C{q} v). Proof. iIntros "Hl". rewrite U_eq. iExists {[ (l,(q,v)) ]}. rewrite !big_sepMS_singleton /=. auto with iFrame. 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] i↦x ∈ l, U (Φ i x)) ⊢ U ([∗ list] i↦x ∈ 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. Global Instance into_unlock_id P : IntoUnlock P P | 10. Proof. apply U_intro. Qed. Global Instance into_unlock_unlock l q v x : IntoUnlock (l ↦C[x]{q} v)%I (l ↦C{q} v)%I | 0. Proof. destruct x. apply U_unlock. apply U_intro. Qed. Lemma modality_U_mixin : modality_mixin U MIEnvId (MIEnvTransform IntoUnlock). Proof. split; simpl; eauto using bi.equiv_entails_sym, U_intro, U_mono, U_sep_2 with typeclass_instances. Qed. Definition modality_U := Modality _ modality_U_mixin. Global Instance from_modal_later P : FromModal modality_U (U P) (U P) P. Proof. by rewrite /FromModal. Qed. End U. Hint Extern 1 (environments.envs_entails _ (U _)) => iModIntro.