More properties about auth_own.

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).