U.v 3.34 KB
 Dan Frumin committed Apr 27, 2018 1 2 ``````From iris.heap_lang Require Export proofmode notation. From iris.algebra Require Import frac. `````` Dan Frumin committed May 28, 2018 3 ``````From iris_c.lib Require Import locking_heap. `````` Robbert Krebbers committed May 03, 2018 4 ``````From iris.proofmode Require Import modalities classes. `````` Dan Frumin committed Apr 27, 2018 5 `````` `````` Robbert Krebbers committed Jun 19, 2018 6 ``````Section U. `````` Dan Frumin committed May 28, 2018 7 `````` Context `{heapG Σ, locking_heapG Σ}. `````` Dan Frumin committed Apr 27, 2018 8 9 `````` (** * Unlocking modality *) `````` Robbert Krebbers committed Nov 15, 2018 10 `````` Definition U_def (P : iProp Σ) : iProp Σ := `````` Robbert Krebbers committed Jan 26, 2019 11 12 13 `````` (∃ 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. `````` Robbert Krebbers committed Nov 15, 2018 14 15 16 `````` Definition U_aux : seal (@U_def). by eexists. Qed. Definition U := unseal U_aux. Definition U_eq : @U = @U_def := seal_eq U_aux. `````` Dan Frumin committed Apr 27, 2018 17 `````` `````` Robbert Krebbers committed Nov 15, 2018 18 19 20 21 22 23 24 25 `````` 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. `````` Dan Frumin committed Apr 27, 2018 26 27 `````` Lemma U_intro P : P ⊢ U P. `````` Robbert Krebbers committed Jan 26, 2019 28 `````` Proof. iIntros "HP". rewrite U_eq. iExists ∅. eauto. Qed. `````` Dan Frumin committed Apr 27, 2018 29 `````` `````` Dan Frumin committed May 24, 2018 30 `````` (** [U] behaves like an applicative functor aka "lax functor with a strength" *) `````` Robbert Krebbers committed May 03, 2018 31 `````` Lemma U_sep_2 P Q : U P ∗ U Q ⊢ U (P ∗ Q). `````` Dan Frumin committed Apr 27, 2018 32 `````` Proof. `````` Robbert Krebbers committed Nov 15, 2018 33 `````` iIntros "[HP HQ]". rewrite U_eq. `````` Dan Frumin committed Apr 27, 2018 34 35 `````` iDestruct "HP" as (ls1) "[HP1 HP2]". iDestruct "HQ" as (ls2) "[HQ1 HQ2]". `````` Robbert Krebbers committed Jan 26, 2019 36 `````` iExists (ls1 ∪ ls2). iFrame "HP1 HQ1". `````` Dan Frumin committed Apr 27, 2018 37 38 39 40 41 `````` iIntros "[HP1 HQ1]". iSplitL "HP1 HP2". - by iApply "HP2". - by iApply "HQ2". Qed. `````` Dan Frumin committed May 24, 2018 42 43 44 `````` Lemma U_stength P Q : P ∗ U Q ⊢ U (P ∗ Q). Proof. by rewrite {1}(U_intro P) U_sep_2. Qed. `````` Robbert Krebbers committed Jun 19, 2018 45 `````` Lemma U_unlock l q v : l ↦C[LLvl]{q} v ⊢ U (l ↦C{q} v). `````` Dan Frumin committed Apr 27, 2018 46 `````` Proof. `````` Robbert Krebbers committed Jan 26, 2019 47 48 `````` iIntros "Hl". rewrite U_eq. iExists {[ (l,(q,v)) ]}. rewrite !big_sepMS_singleton /=. auto with iFrame. `````` Dan Frumin committed Apr 27, 2018 49 50 `````` Qed. `````` Robbert Krebbers committed Nov 15, 2018 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 `````` (* 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. `````` Robbert Krebbers committed May 03, 2018 69 70 71 72 73 `````` 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. `````` Robbert Krebbers committed Nov 11, 2018 74 75 76 `````` 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. `````` Robbert Krebbers committed May 03, 2018 77 78 79 80 81 82 83 84 85 86 87 `````` 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. `````` Robbert Krebbers committed Jun 19, 2018 88 ``````End U. `````` Robbert Krebbers committed Jun 28, 2018 89 `````` `````` Dan Frumin committed Jun 29, 2018 90 ``Hint Extern 1 (environments.envs_entails _ (U _)) => iModIntro.``