Make saved props have discardable fractions

CHANGELOG.md

@@ -65,6 +65,10 @@ lemma.
   with later credits (suffix `_lc`) and without later credits (suffix `_no_lc`).
   The lemmas without later credits still generate credits, but they cannot be used
   in any meaningful way. The lemma `step_fupdN_soundness_gen` is generic over this choice.
+* Add discardable fractions `dfrac` to `saved_anything_own`, `saved_prop_own`,
+  and `saved_pred_own`, so they can be updated. The previous persistent versions
+  can be recovered with the fraction `DfracDiscarded`. Allocation lemmas now take
+  a `dq` parameter to define the initial fraction.
 
 **Changes in `program_logic`:**
 

iris/base_logic/algebra.v

 From iris.algebra Require Import cmra view auth agree csum list excl gmap.
-From iris.algebra.lib Require Import excl_auth gmap_view.
+From iris.algebra.lib Require Import excl_auth gmap_view dfrac_agree.
 From iris.base_logic Require Import bi derived.
 From iris.prelude Require Import options.
 
@@ -12,6 +12,7 @@ Context {M : ucmra}.
 (* Force implicit argument M *)
 Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P Q).
 Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
+Notation "⊢ Q" := (bi_entails (PROP:=uPredI M) True Q).
 
 Lemma prod_validI {A B : cmra} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
 Proof. by uPred.unseal. Qed.
@@ -94,6 +95,21 @@ Section agree.
   Lemma agree_validI x y : ✓ (x ⋅ y) ⊢ x ≡ y.
   Proof. uPred.unseal; split=> r n _ ?; by apply: agree_op_invN. Qed.
 
+  Lemma to_agree_validI a : ⊢ ✓ to_agree a.
+  Proof. uPred.unseal; done. Qed.
+  Lemma to_agree_op_validI a b : ✓ (to_agree a ⋅ to_agree b) ⊣⊢ a ≡ b.
+  Proof.
+    apply bi.entails_anti_sym.
+    - rewrite agree_validI. by rewrite agree_equivI.
+    - pose (Ψ := (λ x : A, ✓ (to_agree a ⋅ to_agree x) : uPred M)%I).
+      assert (NonExpansive Ψ) as ? by solve_proper.
+      rewrite (internal_eq_rewrite a b Ψ).
+      eapply bi.impl_elim; first reflexivity.
+      etrans; first apply bi.True_intro.
+      subst Ψ; simpl.
+      rewrite agree_idemp. apply to_agree_validI.
+  Qed.
+
   Lemma to_agree_uninjI x : ✓ x ⊢ ∃ a, to_agree a ≡ x.
   Proof. uPred.unseal. split=> n y _. exact: to_agree_uninjN. Qed.
 End agree.
@@ -239,6 +255,36 @@ Section excl_auth.
   Qed.
 End excl_auth.
 
+Section dfrac_agree.
+  Context {A : ofe}.
+  Implicit Types a b : A.
+
+  Lemma dfrac_agree_validI dq a : ✓ (to_dfrac_agree dq a) ⊣⊢ ⌜✓ dq⌝.
+  Proof.
+    rewrite prod_validI /= uPred.discrete_valid. apply bi.entails_anti_sym.
+    - by rewrite bi.and_elim_l.
+    - apply bi.and_intro; first done. etrans; last apply to_agree_validI.
+      apply bi.True_intro.
+  Qed.
+
+  Lemma dfrac_agree_validI_2 dq1 dq2 a b :
+    ✓ (to_dfrac_agree dq1 a ⋅ to_dfrac_agree dq2 b) ⊣⊢ ⌜✓ (dq1 ⋅ dq2)⌝ ∧ (a ≡ b).
+  Proof.
+    rewrite prod_validI /= uPred.discrete_valid to_agree_op_validI //.
+  Qed.
+
+  Lemma frac_agree_validI q a : ✓ (to_frac_agree q a) ⊣⊢ ⌜(q ≤ 1)%Qp⌝.
+  Proof.
+    rewrite dfrac_agree_validI dfrac_valid_own //.
+  Qed.
+
+  Lemma frac_agree_validI_2 q1 q2 a b :
+    ✓ (to_frac_agree q1 a ⋅ to_frac_agree q2 b) ⊣⊢ ⌜(q1 + q2 ≤ 1)%Qp⌝ ∧ (a ≡ b).
+  Proof.
+    rewrite dfrac_agree_validI_2 dfrac_valid_own //.
+  Qed.
+End dfrac_agree.
+
 Section gmap_view.
   Context {K : Type} `{Countable K} {V : ofe}.
   Implicit Types (m : gmap K V) (k : K) (dq : dfrac) (v : V).

iris/base_logic/lib/saved_prop.v

 From stdpp Require Import gmap.
-From iris.algebra Require Import agree.
+From iris.algebra Require Import dfrac_agree.
 From iris.proofmode Require Import proofmode.
 From iris.base_logic Require Export own.
+From iris.bi Require Import fractional.
 From iris.prelude Require Import options.
 Import uPred.
 
@@ -9,57 +10,104 @@ Import uPred.
    saved whatever-you-like. *)
 
 Class savedAnythingG (Σ : gFunctors) (F : oFunctor) := SavedAnythingG {
-  saved_anything_inG : inG Σ (agreeR (oFunctor_apply F (iPropO Σ)));
+  saved_anything_inG : inG Σ (dfrac_agreeR (oFunctor_apply F (iPropO Σ)));
   saved_anything_contractive : oFunctorContractive F (* NOT an instance to avoid cycles with [subG_savedAnythingΣ]. *)
 }.
 Local Existing Instance saved_anything_inG.
 
 Definition savedAnythingΣ (F : oFunctor) `{!oFunctorContractive F} : gFunctors :=
-  #[ GFunctor (agreeRF F) ].
+  #[ GFunctor (dfrac_agreeRF F) ].
 
 Global Instance subG_savedAnythingΣ {Σ F} `{!oFunctorContractive F} :
   subG (savedAnythingΣ F) Σ → savedAnythingG Σ F.
 Proof. solve_inG. Qed.
 
 Definition saved_anything_own `{!savedAnythingG Σ F}
-    (γ : gname) (x : oFunctor_apply F (iPropO Σ)) : iProp Σ :=
-  own γ (to_agree x).
+    (γ : gname) (dq : dfrac) (x : oFunctor_apply F (iPropO Σ)) : iProp Σ :=
+  own γ (to_dfrac_agree dq x).
 Typeclasses Opaque saved_anything_own.
 Global Instance: Params (@saved_anything_own) 4 := {}.
 
 Section saved_anything.
   Context `{!savedAnythingG Σ F}.
   Implicit Types x y : oFunctor_apply F (iPropO Σ).
-  Implicit Types γ : gname.
+  Implicit Types (γ : gname) (dq : dfrac).
 
-  Global Instance saved_anything_persistent γ x :
-    Persistent (saved_anything_own γ x).
+  Global Instance saved_anything_discarded_persistent γ x :
+    Persistent (saved_anything_own γ DfracDiscarded x).
   Proof. rewrite /saved_anything_own; apply _. Qed.
 
-  Global Instance saved_anything_ne γ : NonExpansive (saved_anything_own γ).
+  Global Instance saved_anything_ne γ dq : NonExpansive (saved_anything_own γ dq).
   Proof. solve_proper. Qed.
-  Global Instance saved_anything_proper γ : Proper ((≡) ==> (≡)) (saved_anything_own γ).
+  Global Instance saved_anything_proper γ dq : Proper ((≡) ==> (≡)) (saved_anything_own γ dq).
   Proof. solve_proper. Qed.
 
-  Lemma saved_anything_alloc_strong x (I : gname → Prop) :
+  Global Instance saved_anything_fractional γ x : Fractional (λ q, saved_anything_own γ (DfracOwn q) x).
+  Proof. intros q1 q2. rewrite /saved_anything_own -own_op -dfrac_agree_op //. Qed.
+  Global Instance saved_anything_as_fractional γ x q :
+    AsFractional (saved_anything_own γ (DfracOwn q) x) (λ q, saved_anything_own γ (DfracOwn q) x) q.
+  Proof. split; [done|]. apply _. Qed.
+
+  (** Allocation *)
+  Lemma saved_anything_alloc_strong x (I : gname → Prop) dq :
+    ✓ dq →
     pred_infinite I →
-    ⊢ |==> ∃ γ, ⌜I γ⌝ ∗ saved_anything_own γ x.
-  Proof. intros ?. by apply own_alloc_strong. Qed.
+    ⊢ |==> ∃ γ, ⌜I γ⌝ ∗ saved_anything_own γ dq x.
+  Proof. intros ??. by apply own_alloc_strong. Qed.
 
-  Lemma saved_anything_alloc_cofinite x (G : gset gname) :
-    ⊢ |==> ∃ γ, ⌜γ ∉ G⌝ ∗ saved_anything_own γ x.
-  Proof. by apply own_alloc_cofinite. Qed.
+  Lemma saved_anything_alloc_cofinite x (G : gset gname) dq :
+    ✓ dq →
+    ⊢ |==> ∃ γ, ⌜γ ∉ G⌝ ∗ saved_anything_own γ dq x.
+  Proof. intros ?. by apply own_alloc_cofinite. Qed.
 
-  Lemma saved_anything_alloc x : ⊢ |==> ∃ γ, saved_anything_own γ x.
-  Proof. by apply own_alloc. Qed.
+  Lemma saved_anything_alloc x dq :
+    ✓ dq →
+    ⊢ |==> ∃ γ, saved_anything_own γ dq x.
+  Proof. intros ?. by apply own_alloc. Qed.
 
-  Lemma saved_anything_agree γ x y :
-    saved_anything_own γ x -∗ saved_anything_own γ y -∗ x ≡ y.
+  (** Validity *)
+  Lemma saved_anything_valid γ dq x :
+    saved_anything_own γ dq x -∗ ⌜✓ dq⌝.
+  Proof.
+    rewrite /saved_anything_own own_valid dfrac_agree_validI //.
+  Qed.
+  Lemma saved_anything_valid_2 γ dq1 dq2 x y :
+    saved_anything_own γ dq1 x -∗ saved_anything_own γ dq2 y -∗ ⌜✓ (dq1 ⋅ dq2)⌝ ∗ x ≡ y.
   Proof.
     iIntros "Hx Hy". rewrite /saved_anything_own.
     iDestruct (own_valid_2 with "Hx Hy") as "Hv".
-    by rewrite agree_validI agree_equivI.
+    rewrite dfrac_agree_validI_2. iDestruct "Hv" as "[$ $]".
+  Qed.
+  Lemma saved_anything_agree γ dq1 dq2 x y :
+    saved_anything_own γ dq1 x -∗ saved_anything_own γ dq2 y -∗ x ≡ y.
+  Proof. iIntros "Hx Hy". iPoseProof (saved_anything_valid_2 with "Hx Hy") as "[_ $]". Qed.
+
+  (** Make an element read-only. *)
+  Lemma saved_anything_persist γ dq v :
+    saved_anything_own γ dq v ==∗ saved_anything_own γ DfracDiscarded v.
+  Proof.
+    iApply own_update. apply dfrac_agree_persist.
+  Qed.
+
+  (** Updates *)
+  Lemma saved_anything_update y γ x :
+    saved_anything_own γ (DfracOwn 1) x ==∗ saved_anything_own γ (DfracOwn 1) y.
+  Proof.
+    iApply own_update. apply cmra_update_exclusive. done.
   Qed.
+  Lemma saved_anything_update_2 y γ q1 q2 x1 x2 :
+    (q1 + q2 = 1)%Qp →
+    saved_anything_own γ (DfracOwn q1) x1 -∗ saved_anything_own γ (DfracOwn q2) x2 ==∗ saved_anything_own γ (DfracOwn q1) y ∗ saved_anything_own γ (DfracOwn q2) y.
+  Proof.
+    intros Hq. rewrite -own_op. iApply own_update_2.
+    apply dfrac_agree_update_2.
+    rewrite dfrac_op_own Hq //.
+  Qed.
+  Lemma saved_anything_update_halves y γ x1 x2 :
+    saved_anything_own γ (DfracOwn (1/2)) x1 -∗
+    saved_anything_own γ (DfracOwn (1/2)) x2 ==∗
+    saved_anything_own γ (DfracOwn (1/2)) y ∗ saved_anything_own γ (DfracOwn (1/2)) y.
+  Proof. iApply saved_anything_update_2. apply Qp_half_half. Qed.
 End saved_anything.
 
 (** Provide specialized versions of this for convenience. **)
@@ -68,64 +116,152 @@ End saved_anything.
 Notation savedPropG Σ := (savedAnythingG Σ (▶ ∙)).
 Notation savedPropΣ := (savedAnythingΣ (▶ ∙)).
 
-Definition saved_prop_own `{!savedPropG Σ} (γ : gname) (P: iProp Σ) :=
-  saved_anything_own (F := ▶ ∙) γ (Next P).
+Section saved_prop.
+  Context `{!savedPropG Σ}.
+
+  Definition saved_prop_own (γ : gname) (dq : dfrac) (P: iProp Σ) :=
+    saved_anything_own (F := ▶ ∙) γ dq (Next P).
+
+  Global Instance saved_prop_own_contractive γ dq :
+    Contractive (saved_prop_own γ dq).
+  Proof. solve_contractive. Qed.
+
+  Global Instance saved_prop_discarded_persistent γ P :
+    Persistent (saved_prop_own γ DfracDiscarded P).
+  Proof. apply _. Qed.
+
+  Global Instance saved_prop_fractional γ P : Fractional (λ q, saved_prop_own γ (DfracOwn q) P).
+  Proof. apply _. Qed.
+  Global Instance saved_prop_as_fractional γ P q :
+    AsFractional (saved_prop_own γ (DfracOwn q) P) (λ q, saved_prop_own γ (DfracOwn q) P) q.
+  Proof. apply _. Qed.
+
+  (** Allocation *)
+  Lemma saved_prop_alloc_strong (I : gname → Prop) (P: iProp Σ) dq :
+    ✓ dq →
+    pred_infinite I →
+    ⊢ |==> ∃ γ, ⌜I γ⌝ ∗ saved_prop_own γ dq P.
+  Proof. intros ??. by apply saved_anything_alloc_strong. Qed.
 
-Global Instance saved_prop_own_contractive `{!savedPropG Σ} γ :
-  Contractive (saved_prop_own γ).
-Proof. solve_contractive. Qed.
+  Lemma saved_prop_alloc_cofinite (G : gset gname) (P: iProp Σ) dq :
+    ✓ dq →
+    ⊢ |==> ∃ γ, ⌜γ ∉ G⌝ ∗ saved_prop_own γ dq P.
+  Proof. by apply saved_anything_alloc_cofinite. Qed.
 
-Lemma saved_prop_alloc_strong `{!savedPropG Σ} (I : gname → Prop) (P: iProp Σ) :
-  pred_infinite I →
-  ⊢ |==> ∃ γ, ⌜I γ⌝ ∗ saved_prop_own γ P.
-Proof. iIntros (?). by iApply saved_anything_alloc_strong. Qed.
+  Lemma saved_prop_alloc (P : iProp Σ) dq :
+    ✓ dq →
+    ⊢ |==> ∃ γ, saved_prop_own γ dq P.
+  Proof. apply saved_anything_alloc. Qed.
 
-Lemma saved_prop_alloc_cofinite `{!savedPropG Σ} (G : gset gname) (P: iProp Σ) :
-  ⊢ |==> ∃ γ, ⌜γ ∉ G⌝ ∗ saved_prop_own γ P.
-Proof. iApply saved_anything_alloc_cofinite. Qed.
+  (** Validity *)
+  Lemma saved_prop_valid γ dq P :
+    saved_prop_own γ dq P -∗ ⌜✓ dq⌝.
+  Proof. apply saved_anything_valid. Qed.
+  Lemma saved_prop_valid_2 γ dq1 dq2 P Q :
+    saved_prop_own γ dq1 P -∗ saved_prop_own γ dq2 Q -∗ ⌜✓ (dq1 ⋅ dq2)⌝ ∗ ▷ (P ≡ Q).
+  Proof.
+    iIntros "HP HQ".
+    iPoseProof (saved_anything_valid_2 (F := ▶ ∙) with "HP HQ") as "($ & Hag)".
+    by iApply later_equivI.
+  Qed.
+  Lemma saved_prop_agree γ dq1 dq2 P Q :
+    saved_prop_own γ dq1 P -∗ saved_prop_own γ dq2 Q -∗ ▷ (P ≡ Q).
+  Proof. iIntros "HP HQ". iPoseProof (saved_prop_valid_2 with "HP HQ") as "[_ $]". Qed.
 
-Lemma saved_prop_alloc `{!savedPropG Σ} (P: iProp Σ) :
-  ⊢ |==> ∃ γ, saved_prop_own γ P.
-Proof. iApply saved_anything_alloc. Qed.
+  (** Make an element read-only. *)
+  Lemma saved_prop_persist γ dq P :
+    saved_prop_own γ dq P ==∗ saved_prop_own γ DfracDiscarded P.
+  Proof. apply saved_anything_persist. 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 (F := ▶ ∙) with "HP HQ").
-Qed.
+  (** Updates *)
+  Lemma saved_prop_update Q γ P :
+    saved_prop_own γ (DfracOwn 1) P ==∗ saved_prop_own γ (DfracOwn 1) Q.
+  Proof. apply saved_anything_update. Qed.
+  Lemma saved_prop_update_2 Q γ q1 q2 P1 P2 :
+    (q1 + q2 = 1)%Qp →
+    saved_prop_own γ (DfracOwn q1) P1 -∗ saved_prop_own γ (DfracOwn q2) P2 ==∗ saved_prop_own γ (DfracOwn q1) Q ∗ saved_prop_own γ (DfracOwn q2) Q.
+  Proof. apply saved_anything_update_2. Qed.
+  Lemma saved_prop_update_halves Q γ P1 P2 :
+    saved_prop_own γ (DfracOwn (1/2)) P1 -∗
+    saved_prop_own γ (DfracOwn (1/2)) P2 ==∗
+    saved_prop_own γ (DfracOwn (1/2)) Q ∗ saved_prop_own γ (DfracOwn (1/2)) Q.
+  Proof. apply saved_anything_update_halves. Qed.
+End saved_prop.
 
 (* Saved predicates. *)
 Notation savedPredG Σ A := (savedAnythingG Σ (A -d> ▶ ∙)).
 Notation savedPredΣ A := (savedAnythingΣ (A -d> ▶ ∙)).
 
-Definition saved_pred_own `{!savedPredG Σ A} (γ : gname) (Φ : A → iProp Σ) :=
-  saved_anything_own (F := A -d> ▶ ∙) γ (Next ∘ Φ).
-
-Global Instance saved_pred_own_contractive `{!savedPredG Σ A} γ :
-  Contractive (saved_pred_own γ : (A -d> iPropO Σ) → iProp Σ).
-Proof.
-  solve_proper_core ltac:(fun _ => first [ intros ?; progress simpl | by auto | f_contractive | f_equiv ]).
-Qed.
-
-Lemma saved_pred_alloc_strong `{!savedPredG Σ A} (I : gname → Prop) (Φ : A → iProp Σ) :
-  pred_infinite I →
-  ⊢ |==> ∃ γ, ⌜I γ⌝ ∗ saved_pred_own γ Φ.
-Proof. iIntros (?). by iApply saved_anything_alloc_strong. Qed.
-
-Lemma saved_pred_alloc_cofinite `{!savedPredG Σ A} (G : gset gname) (Φ : A → iProp Σ) :
-  ⊢ |==> ∃ γ, ⌜γ ∉ G⌝ ∗ saved_pred_own γ Φ.
-Proof. iApply saved_anything_alloc_cofinite. Qed.
-
-Lemma saved_pred_alloc `{!savedPredG Σ A} (Φ : A → iProp Σ) :
-  ⊢ |==> ∃ γ, saved_pred_own γ Φ.
-Proof. iApply saved_anything_alloc. Qed.
-
-(* We put the `x` on the outside to make this lemma easier to apply. *)
-Lemma saved_pred_agree `{!savedPredG Σ A} γ Φ Ψ x :
-  saved_pred_own γ Φ -∗ saved_pred_own γ Ψ -∗ ▷ (Φ x ≡ Ψ x).
-Proof.
-  unfold saved_pred_own. iIntros "#HΦ #HΨ /=". iApply later_equivI.
-  iDestruct (saved_anything_agree (F := A -d> ▶ ∙) with "HΦ HΨ") as "Heq".
-  by iDestruct (discrete_fun_equivI with "Heq") as "?".
-Qed.
+Section saved_pred.
+  Context `{!savedPredG Σ A}.
+
+  Definition saved_pred_own (γ : gname) (dq : dfrac) (Φ : A → iProp Σ) :=
+    saved_anything_own (F := A -d> ▶ ∙) γ dq (Next ∘ Φ).
+
+  Global Instance saved_pred_own_contractive `{!savedPredG Σ A} γ dq :
+    Contractive (saved_pred_own γ dq : (A -d> iPropO Σ) → iProp Σ).
+  Proof.
+    solve_proper_core ltac:(fun _ => first [ intros ?; progress simpl | by auto | f_contractive | f_equiv ]).
+  Qed.
+
+  Global Instance saved_pred_discarded_persistent γ Φ :
+    Persistent (saved_pred_own γ DfracDiscarded Φ).
+  Proof. apply _. Qed.
+
+  Global Instance saved_pred_fractional γ Φ : Fractional (λ q, saved_pred_own γ (DfracOwn q) Φ).
+  Proof. apply _. Qed.
+  Global Instance saved_pred_as_fractional γ Φ q :
+    AsFractional (saved_pred_own γ (DfracOwn q) Φ) (λ q, saved_pred_own γ (DfracOwn q) Φ) q.
+  Proof. apply _. Qed.
+
+  (** Allocation *)
+  Lemma saved_pred_alloc_strong (I : gname → Prop) (Φ : A → iProp Σ) dq :
+    ✓ dq →
+    pred_infinite I →
+    ⊢ |==> ∃ γ, ⌜I γ⌝ ∗ saved_pred_own γ dq Φ.
+  Proof. intros ??. by apply saved_anything_alloc_strong. Qed.
+
+  Lemma saved_pred_alloc_cofinite (G : gset gname) (Φ : A → iProp Σ) dq :
+    ✓ dq →
+    ⊢ |==> ∃ γ, ⌜γ ∉ G⌝ ∗ saved_pred_own γ dq Φ.
+  Proof. by apply saved_anything_alloc_cofinite. Qed.
+
+  Lemma saved_pred_alloc (Φ : A → iProp Σ) dq :
+    ✓ dq →
+    ⊢ |==> ∃ γ, saved_pred_own γ dq Φ.
+  Proof. apply saved_anything_alloc. Qed.
+
+  (** Validity *)
+  Lemma saved_pred_valid γ dq Φ :
+    saved_pred_own γ dq Φ -∗ ⌜✓ dq⌝.
+  Proof. apply saved_anything_valid. Qed.
+  Lemma saved_pred_valid_2 γ dq1 dq2 Φ Ψ x :
+    saved_pred_own γ dq1 Φ -∗ saved_pred_own γ dq2 Ψ -∗ ⌜✓ (dq1 ⋅ dq2)⌝ ∗ ▷ (Φ x ≡ Ψ x).
+  Proof.
+    iIntros "HΦ HΨ".
+    iPoseProof (saved_anything_valid_2 (F := A -d> ▶ ∙) with "HΦ HΨ") as "($ & Hag)".
+    iApply later_equivI. by iApply (discrete_fun_equivI with "Hag").
+  Qed.
+  Lemma saved_pred_agree γ dq1 dq2 Φ Ψ x :
+    saved_pred_own γ dq1 Φ -∗ saved_pred_own γ dq2 Ψ -∗ ▷ (Φ x ≡ Ψ x).
+  Proof. iIntros "HΦ HΨ". iPoseProof (saved_pred_valid_2 with "HΦ HΨ") as "[_ $]". Qed.
+
+  (** Make an element read-only. *)
+  Lemma saved_pred_persist γ dq Φ :
+    saved_pred_own γ dq Φ ==∗ saved_pred_own γ DfracDiscarded Φ.
+  Proof. apply saved_anything_persist. Qed.
+
+  (** Updates *)
+  Lemma saved_pred_update Ψ γ Φ :
+    saved_pred_own γ (DfracOwn 1) Φ ==∗ saved_pred_own γ (DfracOwn 1) Ψ.
+  Proof. apply saved_anything_update. Qed.
+  Lemma saved_pred_update_2 Ψ γ q1 q2 Φ1 Φ2 :
+    (q1 + q2 = 1)%Qp →
+    saved_pred_own γ (DfracOwn q1) Φ1 -∗ saved_pred_own γ (DfracOwn q2) Φ2 ==∗ saved_pred_own γ (DfracOwn q1) Ψ ∗ saved_pred_own γ (DfracOwn q2) Ψ.
+  Proof. apply saved_anything_update_2. Qed.
+  Lemma saved_pred_update_halves Ψ γ Φ1 Φ2 :
+    saved_pred_own γ (DfracOwn (1/2)) Φ1 -∗
+    saved_pred_own γ (DfracOwn (1/2)) Φ2 ==∗
+    saved_pred_own γ (DfracOwn (1/2)) Ψ ∗ saved_pred_own γ (DfracOwn (1/2)) Ψ.
+  Proof. apply saved_anything_update_halves. Qed.
+End saved_pred.