generalize savedProp to let the user control the position of the type-level later

theories/base_logic/lib/saved_prop.v

@@ -5,16 +5,17 @@ Set Default Proof Using "Type".
 Import uPred.
 
 Class savedPropG (Σ : gFunctors) (F : cFunctor) :=
-  saved_prop_inG :> inG Σ (agreeR (laterC (F (iPreProp Σ)))).
-Definition savedPropΣ (F : cFunctor) : gFunctors :=
-  #[ GFunctor (agreeRF (▶ F)) ].
+  saved_prop_inG :> inG Σ (agreeR (F (iPreProp Σ))).
+Definition savedPropΣ (F : cFunctor) `{!cFunctorContractive F} : gFunctors :=
+  #[ GFunctor (agreeRF F) ].
 
-Instance subG_savedPropΣ  {Σ F} : subG (savedPropΣ F) Σ → savedPropG Σ F.
+Instance subG_savedPropΣ {Σ F} `{!cFunctorContractive F} :
+  subG (savedPropΣ F) Σ → savedPropG Σ F.
 Proof. solve_inG. Qed.
 
 Definition saved_prop_own `{savedPropG Σ F}
     (γ : gname) (x : F (iProp Σ)) : iProp Σ :=
-  own γ (to_agree $ Next (cFunctor_map F (iProp_fold, iProp_unfold) x)).
+  own γ (to_agree $ (cFunctor_map F (iProp_fold, iProp_unfold) x)).
 Typeclasses Opaque saved_prop_own.
 Instance: Params (@saved_prop_own) 3.
 
@@ -34,15 +35,15 @@ Section saved_prop.
   Proof. by apply own_alloc. Qed.
 
   Lemma saved_prop_agree γ x y :
-    saved_prop_own γ x -∗ saved_prop_own γ y -∗ ▷ (x ≡ y).
+    saved_prop_own γ x -∗ saved_prop_own γ y -∗ x ≡ y.
   Proof.
     apply wand_intro_r.
-    rewrite -own_op own_valid agree_validI agree_equivI later_equivI.
+    rewrite -own_op own_valid agree_validI agree_equivI.
     set (G1 := cFunctor_map F (iProp_fold, iProp_unfold)).
     set (G2 := cFunctor_map F (@iProp_unfold Σ, @iProp_fold Σ)).
     assert (∀ z, G2 (G1 z) ≡ z) as help.
     { intros z. rewrite /G1 /G2 -cFunctor_compose -{2}[z]cFunctor_id.
       apply (ne_proper (cFunctor_map F)); split=>?; apply iProp_fold_unfold. }
-    rewrite -{2}[x]help -{2}[y]help. apply later_mono, f_equiv, _.
+    rewrite -{2}[x]help -{2}[y]help. apply f_equiv, _.
   Qed.
 End saved_prop.