Commit 950db182 authored by Robbert Krebbers's avatar Robbert Krebbers

Show that `saved_prop` and `saved_pred` are contractive.

parent 5d74ded9
......@@ -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 γ).
intros n Φ Φ' HΦ. rewrite /saved_pred_own /saved_anything_own /=.
do 3 f_equiv. intros x. rewrite /=. by f_contractive.
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.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment