saved_prop.v 1.3 KB
 Robbert Krebbers committed Feb 13, 2016 1 2 3 4 5 6 7 8 9 10 11 12 ``````From algebra Require Export agree. From program_logic Require Export ghost_ownership. Import uPred. Class SavedPropInG Λ Σ (i : gid) := saved_prop_inG :> InG Λ Σ i (agreeRA (laterC (iPreProp Λ (globalF Σ)))). Definition saved_prop_own {Λ Σ} (i : gid) `{SavedPropInG Λ Σ i} (γ : gname) (P : iPropG Λ Σ) : iPropG Λ Σ := own i γ (to_agree (Next (iProp_unfold P))). Instance: Params (@saved_prop_own) 5. `````` Robbert Krebbers committed Feb 13, 2016 13 ``````Section saved_prop. `````` Robbert Krebbers committed Feb 13, 2016 14 15 16 17 `````` Context `{SavedPropInG Λ Σ SPI}. Implicit Types P Q : iPropG Λ Σ. Implicit Types γ : gname. `````` 18 `````` Lemma saved_prop_alloc_strong N P (G : gset gname) : `````` Robbert Krebbers committed Feb 14, 2016 19 `````` True ⊑ pvs N N (∃ γ, ■ (γ ∉ G) ∧ saved_prop_own SPI γ P). `````` 20 21 `````` Proof. by apply own_alloc_strong. Qed. `````` Robbert Krebbers committed Feb 13, 2016 22 23 24 25 `````` Lemma saved_prop_alloc N P : True ⊑ pvs N N (∃ γ, saved_prop_own SPI γ P). Proof. by apply own_alloc. Qed. `````` Robbert Krebbers committed Feb 14, 2016 26 `````` Lemma saved_prop_agree γ P Q : `````` Robbert Krebbers committed Feb 13, 2016 27 28 29 30 31 32 33 34 `````` (saved_prop_own SPI γ P ★ saved_prop_own SPI γ Q) ⊑ ▷ (P ↔ Q). Proof. rewrite /saved_prop_own -own_op own_valid agree_validI. rewrite agree_equivI later_equivI /=; apply later_mono. rewrite -{2}(iProp_fold_unfold P) -{2}(iProp_fold_unfold Q). apply (eq_rewrite (iProp_unfold P) (iProp_unfold Q) (λ Q' : iPreProp Λ _, iProp_fold (iProp_unfold P) ↔ iProp_fold Q')%I); solve_ne || auto with I. Qed. `````` Robbert Krebbers committed Feb 13, 2016 35 ``End saved_prop.``