From 7d2f957dac4b9383fad090cf4eaec740dfacc191 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 10 Feb 2016 02:42:54 +0100
Subject: [PATCH] Remove Unshelve hack in ghost_ownership.

---
 algebra/cmra.v                  | 11 -----------
 program_logic/ghost_ownership.v | 26 ++++++++++++++++----------
 2 files changed, 16 insertions(+), 21 deletions(-)

diff --git a/algebra/cmra.v b/algebra/cmra.v
index 8861dbc82..75c088480 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -396,27 +396,16 @@ End cmra_monotone.
 (** * Transporting a CMRA equality *)
 Definition cmra_transport {A B : cmraT} (H : A = B) (x : A) : B :=
   eq_rect A id x _ H.
-Definition cmra_transport_back {A B : cmraT} (H : A = B) (x : B) : A :=
-  eq_rect B id x _ (eq_sym H).
 
 Section cmra_transport.
   Context {A B : cmraT} (H : A = B).
   Notation T := (cmra_transport H).
-  Notation T' := (cmra_transport_back H).
   Global Instance cmra_transport_ne n : Proper (dist n ==> dist n) T.
   Proof. by intros ???; destruct H. Qed.
   Global Instance cmra_transport_proper : Proper ((≡) ==> (≡)) T.
   Proof. by intros ???; destruct H. Qed.
-  Lemma cmra_transport_and_back x : T' (T x) = x.
-  Proof. by destruct H. Qed.
-  Lemma cmra_transport_back_and x : T (T' x) = x.
-  Proof. by destruct H. Qed.
   Lemma cmra_transport_op x y : T (x â‹… y) = T x â‹… T y.
   Proof. by destruct H. Qed.
-  Lemma cmra_transport_back_op_r y x : T (x â‹… T' y) = T x â‹… y.
-  Proof. by destruct H. Qed.
-  Lemma cmra_transport_back_op_l y x : T (T' x â‹… y) = x â‹… T y.
-  Proof. by destruct H. Qed.
   Lemma cmra_transport_unit x : T (unit x) = unit (T x).
   Proof. by destruct H. Qed.
   Lemma cmra_transport_validN n x : ✓{n} (T x) ↔ ✓{n} x.
diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index a1c60d307..421f05067 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -23,7 +23,7 @@ Section global.
 Context {Λ : language} {Σ : gid → iFunctor} (i : gid) `{!InG Λ Σ i A}.
 Implicit Types a : A.
 
-(* Properties of to_globalC *)
+(** * Properties of to_globalC *)
 Instance to_globalC_ne γ n : Proper (dist n ==> dist n) (to_globalC i γ).
 Proof. by intros a a' Ha; apply iprod_singleton_ne; rewrite Ha. Qed.
 Lemma to_globalC_validN n γ a : ✓{n} (to_globalC i γ a) ↔ ✓{n} a.
@@ -44,7 +44,19 @@ Qed.
 Instance to_globalC_timeless γ m : Timeless m → Timeless (to_globalC i γ m).
 Proof. rewrite /to_globalC; apply _. Qed.
 
-(* Properties of own *)
+(** * Transport empty *)
+Instance inG_empty `{Empty A} : Empty (Σ i (laterC (iPreProp Λ (globalC Σ)))) :=
+  cmra_transport inG ∅.
+Instance inG_empty_spec `{Empty A} :
+  CMRAIdentity A → CMRAIdentity (Σ i (laterC (iPreProp Λ (globalC Σ)))).
+Proof.
+  split.
+  * apply cmra_transport_valid, cmra_empty_valid.
+  * intros x; rewrite /empty /inG_empty; destruct inG. by rewrite left_id.
+  * apply _.
+Qed.
+
+(** * Properties of own *)
 Global Instance own_ne γ n : Proper (dist n ==> dist n) (own i γ).
 Proof. by intros m m' Hm; rewrite /own Hm. Qed.
 Global Instance own_proper γ : Proper ((≡) ==> (≡)) (own i γ) := ne_proper _.
@@ -91,17 +103,11 @@ Lemma own_updateP_empty `{Empty A, !CMRAIdentity A} E γ a P :
 Proof.
   intros Hemp.
   rewrite -(pvs_mono _ _ (∃ m, ■ (∃ a', m = to_globalC i γ a' ∧ P a') ∧ ownG m)%I).
-  * eapply pvs_ownG_updateP_empty, iprod_singleton_updateP_empty with (x:=i);
-      first by (eapply map_singleton_updateP_empty', cmra_transport_updateP', Hemp).
+  * eapply pvs_ownG_updateP_empty, iprod_singleton_updateP_empty;
+      first eapply map_singleton_updateP_empty', cmra_transport_updateP', Hemp.
     naive_solver.
   * apply exist_elim=>m; apply const_elim_l=>-[a' [-> HP]].
     rewrite -(exist_intro a'). by apply and_intro; [apply const_intro|].
-Unshelve.
-(* We have to prove that we actually follow the identity laws on the "other side". *)
-split.
-- apply cmra_transport_valid, cmra_empty_valid.
-- move=>b. by rewrite -cmra_transport_back_op_r left_id cmra_transport_back_and.
-- apply _. 
 Qed.
 
 Lemma own_update E γ a a' : a ~~> a' → own i γ a ⊑ pvs E E (own i γ a').
-- 
GitLab