From 950db182d54378f4eb3a10b4bd67ee3850ba3652 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 15 Nov 2017 17:21:32 +0100
Subject: [PATCH] Show that `saved_prop` and `saved_pred` are contractive.

---
 theories/base_logic/lib/saved_prop.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index 73a957514..d7c76c2a5 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -63,6 +63,10 @@ Notation savedPropΣ := (savedAnythingΣ (▶ ∙)).
 Definition saved_prop_own `{savedPropG Σ} (γ : gname) (P: iProp Σ) :=
   saved_anything_own (F := ▶ ∙) γ (Next P).
 
+Instance saved_prop_own_contractive `{savedPropG Σ} γ :
+  Contractive (saved_prop_own γ).
+Proof. rewrite /saved_prop_own. solve_contractive. Qed.
+
 Lemma saved_prop_alloc_strong `{savedPropG Σ} (G : gset gname) (P: iProp Σ) :
   (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ saved_prop_own γ P)%I.
 Proof. iApply saved_anything_alloc_strong. Qed.
@@ -84,6 +88,12 @@ Notation savedPredΣ A := (savedAnythingΣ (constCF A -n> ▶ ∙)).
 Definition saved_pred_own `{savedPredG Σ A} (γ : gname) (Φ : A -n> iProp Σ) :=
   saved_anything_own (F := A -n> ▶ ∙) γ (CofeMor Next ◎ Φ).
 
+Instance saved_pred_own_contractive `{savedPredG Σ A} γ : Contractive (saved_pred_own γ).
+Proof.
+  intros n Φ Φ' HΦ. rewrite /saved_pred_own /saved_anything_own /=.
+  do 3 f_equiv. intros x. rewrite /=. by f_contractive.
+Qed.
+
 Lemma saved_pred_alloc_strong `{savedPredG Σ A} (G : gset gname) (Φ : A -n> iProp Σ) :
   (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ saved_pred_own γ Φ)%I.
 Proof. iApply saved_anything_alloc_strong. Qed.
-- 
GitLab