From 4dacd90f2b7a32e75625297ffdd2ef9070a11662 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 17 Feb 2016 10:46:48 +0100
Subject: [PATCH] establish that saved propositions are AlwaysStable

---
 program_logic/ghost_ownership.v | 4 ++++
 program_logic/ownership.v       | 4 ++++
 program_logic/saved_prop.v      | 6 ++++++
 3 files changed, 14 insertions(+)

diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index 62578f262..dda7000ce 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -70,6 +70,8 @@ Global Instance own_mono γ : Proper (flip (≼) ==> (⊑)) (own γ).
 Proof. move=>a b [c H]. rewrite H own_op. eauto with I. Qed.
 Lemma always_own_unit γ a : (□ own γ (unit a))%I ≡ own γ (unit a).
 Proof. by rewrite /own -to_globalF_unit always_ownG_unit. Qed.
+Lemma always_own γ a : unit a ≡ a → (□ own γ a)%I ≡ own γ a.
+Proof. by intros <-; rewrite always_own_unit. Qed.
 Lemma own_valid γ a : own γ a ⊑ ✓ a.
 Proof.
   rewrite /own ownG_valid /to_globalF.
@@ -83,6 +85,8 @@ Lemma own_valid_l γ a : own γ a ⊑ (✓ a ★ own γ a).
 Proof. by rewrite comm -own_valid_r. Qed.
 Global Instance own_timeless γ a : Timeless a → TimelessP (own γ a).
 Proof. unfold own; apply _. Qed.
+Global Instance own_unit_always_stable γ a : AlwaysStable (own γ (unit a)).
+Proof. by rewrite /AlwaysStable always_own_unit. Qed.
 
 (* 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. *)
diff --git a/program_logic/ownership.v b/program_logic/ownership.v
index 2f96898b7..7a971a817 100644
--- a/program_logic/ownership.v
+++ b/program_logic/ownership.v
@@ -57,6 +57,8 @@ Proof.
   apply uPred.always_ownM.
   by rewrite Res_unit !cmra_unit_empty -{2}(cmra_unit_idemp m).
 Qed.
+Lemma always_ownG m : unit m ≡ m → (□ ownG m)%I ≡ ownG m.
+Proof. by intros <-; rewrite always_ownG_unit. Qed.
 Lemma ownG_valid m : ownG m ⊑ ✓ m.
 Proof.
   rewrite /ownG uPred.ownM_valid res_validI /= option_validI; auto with I.
@@ -65,6 +67,8 @@ Lemma ownG_valid_r m : ownG m ⊑ (ownG m ★ ✓ m).
 Proof. apply (uPred.always_entails_r _ _), ownG_valid. Qed.
 Global Instance ownG_timeless m : Timeless m → TimelessP (ownG m).
 Proof. rewrite /ownG; apply _. Qed.
+Global Instance ownG_unit_always_stable m : AlwaysStable (ownG (unit m)).
+Proof. by rewrite /AlwaysStable always_ownG_unit. Qed.
 
 (* inversion lemmas *)
 Lemma ownI_spec r n i P :
diff --git a/program_logic/saved_prop.v b/program_logic/saved_prop.v
index e313311c2..c6697b393 100644
--- a/program_logic/saved_prop.v
+++ b/program_logic/saved_prop.v
@@ -15,6 +15,12 @@ Section saved_prop.
   Implicit Types P Q : iPropG Λ Σ.
   Implicit Types γ : gname.
 
+  Global Instance : ∀ P, AlwaysStable (saved_prop_own γ P).
+  Proof.
+    intros. rewrite /AlwaysStable /saved_prop_own.
+    rewrite always_own; done.
+  Qed.
+
   Lemma saved_prop_alloc_strong N P (G : gset gname) :
     True ⊑ pvs N N (∃ γ, ■ (γ ∉ G) ∧ saved_prop_own γ P).
   Proof. by apply own_alloc_strong. Qed.
-- 
GitLab