saved_prop: provide convenience definitions for common instances

theories/base_logic/lib/saved_prop.v

 From iris.base_logic Require Export own.
 From iris.algebra Require Import agree.
 From stdpp Require Import gmap.
+From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 Import uPred.
 
-Class savedPropG (Σ : gFunctors) (F : cFunctor) :=
-  saved_prop_inG :> inG Σ (agreeR (F (iPreProp Σ))).
-Definition savedPropΣ (F : cFunctor) `{!cFunctorContractive F} : gFunctors :=
+(* "Saved anything" -- this can give you saved propositions, saved predicates,
+   saved whatever-you-like. *)
+
+Class savedAnythingG (Σ : gFunctors) (F : cFunctor) :=
+  saved_anything_inG :> inG Σ (agreeR (F (iPreProp Σ))).
+Definition savedAnythingΣ (F : cFunctor) `{!cFunctorContractive F} : gFunctors :=
   #[ GFunctor (agreeRF F) ].
 
-Instance subG_savedPropΣ {Σ F} `{!cFunctorContractive F} :
-  subG (savedPropΣ F) Σ → savedPropG Σ F.
+Instance subG_savedAnythingΣ {Σ F} `{!cFunctorContractive F} :
+  subG (savedAnythingΣ F) Σ → savedAnythingG Σ F.
 Proof. solve_inG. Qed.
 
-Definition saved_prop_own `{savedPropG Σ F}
+Definition saved_anything_own `{savedAnythingG Σ F}
     (γ : gname) (x : F (iProp Σ)) : iProp Σ :=
   own γ (to_agree $ (cFunctor_map F (iProp_fold, iProp_unfold) x)).
-Typeclasses Opaque saved_prop_own.
-Instance: Params (@saved_prop_own) 3.
+Typeclasses Opaque saved_anything_own.
+Instance: Params (@saved_anything_own) 3.
 
-Section saved_prop.
-  Context `{savedPropG Σ F}.
+Section saved_anything.
+  Context `{savedAnythingG Σ F}.
   Implicit Types x y : F (iProp Σ).
   Implicit Types γ : gname.
 
-  Global Instance saved_prop_persistent γ x : Persistent (saved_prop_own γ x).
-  Proof. rewrite /saved_prop_own; apply _. Qed.
+  Global Instance saved_prop_persistent γ x : Persistent (saved_anything_own γ x).
+  Proof. rewrite /saved_anything_own; apply _. Qed.
 
-  Lemma saved_prop_alloc_strong x (G : gset gname) :
-    (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ saved_prop_own γ x)%I.
+  Lemma saved_anything_alloc_strong x (G : gset gname) :
+    (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ saved_anything_own γ x)%I.
   Proof. by apply own_alloc_strong. Qed.
 
-  Lemma saved_prop_alloc x : (|==> ∃ γ, saved_prop_own γ x)%I.
+  Lemma saved_anything_alloc x : (|==> ∃ γ, saved_anything_own γ x)%I.
   Proof. by apply own_alloc. Qed.
 
-  Lemma saved_prop_agree γ x y :
-    saved_prop_own γ x -∗ saved_prop_own γ y -∗ x ≡ y.
+  Lemma saved_anything_agree γ x y :
+    saved_anything_own γ x -∗ saved_anything_own γ y -∗ x ≡ y.
   Proof.
+    (* TODO: Use the proof mode. *)
     apply wand_intro_r.
     rewrite -own_op own_valid agree_validI agree_equivI.
     set (G1 := cFunctor_map F (iProp_fold, iProp_unfold)).
@@ -46,4 +51,43 @@ Section saved_prop.
       apply (ne_proper (cFunctor_map F)); split=>?; apply iProp_fold_unfold. }
     rewrite -{2}[x]help -{2}[y]help. apply f_equiv, _.
   Qed.
-End saved_prop.
+End saved_anything.
+
+(** Provide specialized versions of this for convenience. **)
+
+(* Saved propositions. *)
+Notation savedPropG Σ := (savedAnythingG Σ (▶ ∙)).
+Notation savedPropΣ := (savedAnythingΣ (▶ ∙)).
+
+Definition saved_prop_own `{savedPropG Σ} (γ : gname) (P: iProp Σ) :=
+  saved_anything_own (F := ▶ ∙) γ (Next P).
+
+Lemma saved_prop_alloc `{savedPropG Σ} (P: iProp Σ) :
+  (|==> ∃ γ, saved_prop_own γ P)%I.
+Proof. iApply saved_anything_alloc. Qed.
+
+Lemma saved_prop_agree `{savedPropG Σ} γ P Q :
+  saved_prop_own γ P -∗ saved_prop_own γ Q -∗ ▷ (P ≡ Q).
+Proof.
+  iIntros "HP HQ". iApply later_equivI. iApply (saved_anything_agree with "HP HQ").
+Qed.
+
+(* Saved predicates. *)
+Notation savedPredG Σ A := (savedAnythingG Σ (constCF A -n> ▶ ∙)).
+Notation savedPredΣ A := (savedAnythingΣ (constCF A -n> ▶ ∙)).
+
+Definition saved_pred_own `{savedPredG Σ A} (γ : gname) (f: A -n> iProp Σ) :=
+  saved_anything_own (F := A -n> ▶ ∙) γ (CofeMor Next ◎ f).
+
+Lemma saved_pred_alloc `{savedPredG Σ A} (f: A -n> iProp Σ) :
+  (|==> ∃ γ, saved_pred_own γ f)%I.
+Proof. iApply saved_anything_alloc. Qed.
+
+Lemma saved_pred_agree `{savedPredG Σ A} γ f g :
+  saved_pred_own γ f -∗ saved_pred_own γ g -∗ ∀ x, ▷ (f x ≡ g x).
+Proof.
+  iIntros "Hx Hy *". unfold saved_pred_own. iApply later_equivI.
+  iDestruct (ofe_morC_equivI (CofeMor Next ◎ f) (CofeMor Next ◎ g)) as "[FE _]".
+  simpl. iApply ("FE" with "[-]").
+  iApply (saved_anything_agree with "Hx Hy").
+Qed.