From 9e8c1030e7fcd5a3b7904af2bcb151c80cdfda9e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 10 Dec 2018 12:21:45 +0100
Subject: [PATCH] =?UTF-8?q?New=20lemma=20`later=5Fown=20=CE=B3=20a=20:=20?=
 =?UTF-8?q?=E2=96=B7=20own=20=CE=B3=20a=20-=E2=88=97=20=E2=97=87=20(?=
 =?UTF-8?q?=E2=88=83=20b,=20own=20=CE=B3=20b=20=E2=88=A7=20=E2=96=B7=20(a?=
 =?UTF-8?q?=20=E2=89=A1=20b))`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This lemma is similar to `later_ownM`.
---
 theories/base_logic/lib/own.v | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)

diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index a9d78acb9..9f570de8b 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -110,6 +110,36 @@ Proof. rewrite !own_eq /own_def; apply _. Qed.
 Global Instance own_core_persistent γ a : CoreId a → Persistent (own γ a).
 Proof. rewrite !own_eq /own_def; apply _. Qed.
 
+Lemma later_own γ a : ▷ own γ a -∗ ◇ (∃ b, own γ b ∧ ▷ (a ≡ b)).
+Proof.
+  rewrite own_eq /own_def later_ownM. apply exist_elim=> r.
+  assert (NonExpansive (λ r : iResUR Σ, r (inG_id H) !! γ)).
+  { intros n r1 r2 Hr. f_equiv. by specialize (Hr (inG_id _)). }
+  rewrite (f_equiv (λ r : iResUR Σ, r (inG_id H) !! γ) _ r).
+  rewrite {1}/iRes_singleton ofe_fun_lookup_singleton lookup_singleton.
+  rewrite option_equivI. case Hb: (r (inG_id _) !! γ)=> [b|]; last first.
+  { by rewrite and_elim_r /sbi_except_0 -or_intro_l. }
+  rewrite -except_0_intro -(exist_intro (cmra_transport (eq_sym inG_prf) b)).
+  apply and_mono.
+  - rewrite /iRes_singleton. assert (∀ {A A' : cmraT} (Heq : A' = A) (a : A),
+      cmra_transport Heq (cmra_transport (eq_sym Heq) a) = a) as ->
+      by (by intros ?? ->).
+    apply ownM_mono=> /=.
+    exists (ofe_fun_insert (inG_id _) (delete γ (r (inG_id H))) r).
+    intros i'. rewrite ofe_fun_lookup_op.
+    destruct (decide (i' = inG_id _)) as [->|?].
+    + rewrite ofe_fun_lookup_insert ofe_fun_lookup_singleton.
+      intros γ'. rewrite lookup_op. destruct (decide (γ' = γ)) as [->|?].
+      * by rewrite lookup_singleton lookup_delete Hb.
+      * by rewrite lookup_singleton_ne // lookup_delete_ne // left_id.
+    + rewrite ofe_fun_lookup_insert_ne //.
+      by rewrite ofe_fun_lookup_singleton_ne // left_id.
+  - apply later_mono.
+    by assert (∀ {A A' : cmraT} (Heq : A' = A) (a' : A') (a : A),
+      cmra_transport Heq a' ≡ a ⊢@{iPropI Σ}
+        a' ≡ cmra_transport (eq_sym Heq) a) as -> by (by intros ?? ->).
+Qed.
+
 (** ** Allocation *)
 (* TODO: This also holds if we just have ✓ a at the current step-idx, as Iris
    assertion. However, the map_updateP_alloc does not suffice to show this. *)
-- 
GitLab