From a34133c2cdc0e4f3066e58a7aeb58cc5c2c92e14 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Sun, 14 Feb 2016 22:01:06 +0100 Subject: [PATCH] More properties about auth_own. --- program_logic/auth.v | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/program_logic/auth.v b/program_logic/auth.v index a557cb5..6811f57 100644 --- a/program_logic/auth.v +++ b/program_logic/auth.v @@ -30,9 +30,16 @@ Section auth. Implicit Types a b : A. Implicit Types γ : gname. + Global Instance auth_own_ne n γ : + Proper (dist n ==> dist n) (auth_own AuthI γ). + Proof. by rewrite /auth_own=> a b ->. Qed. + Global Instance auth_own_proper γ : Proper ((≡) ==> (≡)) (auth_own AuthI γ). + Proof. by rewrite /auth_own=> a b ->. Qed. Lemma auto_own_op γ a b : auth_own AuthI γ (a ⋅ b) ≡ (auth_own AuthI γ a ★ auth_own AuthI γ b)%I. Proof. by rewrite /auth_own -own_op auth_frag_op. Qed. + Lemma auto_own_valid γ a : auth_own AuthI γ a ⊑ ✓ a. + Proof. by rewrite /auth_own own_valid auth_validI. Qed. Lemma auth_alloc N a : ✓ a → φ a ⊑ pvs N N (∃ γ, auth_ctx AuthI γ N φ ∧ auth_own AuthI γ a). -- GitLab