From 82511560abb3070022b1527db74379dce2bd3a4c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 5 Feb 2016 20:25:11 +0100
Subject: [PATCH] show that we always own something

---
 program_logic/upred.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/program_logic/upred.v b/program_logic/upred.v
index 9c7735c70..7bafefba9 100644
--- a/program_logic/upred.v
+++ b/program_logic/upred.v
@@ -786,7 +786,7 @@ Proof. intros; rewrite -always_and_sep_l; auto. Qed.
 Lemma always_entails_r P Q : (P ⊑ □ Q) → P ⊑ (P ★ □ Q).
 Proof. intros; rewrite -always_and_sep_r; auto. Qed.
 
-(* Own *)
+(* Own and valid *)
 Lemma own_op (a1 a2 : M) :
   uPred_own (a1 ⋅ a2) ≡ (uPred_own a1 ★ uPred_own a2)%I.
 Proof.
@@ -805,6 +805,8 @@ Proof.
 Qed.
 Lemma always_own (a : M) : unit a ≡ a → (□ uPred_own a)%I ≡ uPred_own a.
 Proof. by intros <-; rewrite always_own_unit. Qed.
+Lemma own_something : True ⊑ ∃ a, uPred_own a.
+Proof. intros x [|n] ??; [done|]. by exists x; simpl. Qed.
 Lemma own_empty `{Empty M, !CMRAIdentity M} : True ⊑ uPred_own ∅.
 Proof. intros x [|n] ??; [done|]. by  exists x; rewrite (left_id _ _). Qed.
 Lemma own_valid (a : M) : uPred_own a ⊑ (✓ a).
-- 
GitLab