From fc6fdaa180c559082eb71060974ab3505c631919 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 4 Oct 2020 11:38:01 +0200
Subject: [PATCH] Put isomorphism `iProp` to `iPreProp` into `own`
 construction.

---
 theories/base_logic/lib/boxes.v      |  10 +-
 theories/base_logic/lib/own.v        | 193 ++++++++++++++++++---------
 theories/base_logic/lib/saved_prop.v |  12 +-
 theories/base_logic/lib/wsat.v       |  10 +-
 4 files changed, 143 insertions(+), 82 deletions(-)

diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index c9c7bfef4..a186d80b6 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -8,7 +8,7 @@ Import uPred.
 Class boxG Σ :=
   boxG_inG :> inG Σ (prodR
     (excl_authR boolO)
-    (optionR (agreeR (laterO (iPrePropO Σ))))).
+    (optionR (agreeR (laterO (iPropO Σ))))).
 
 Definition boxΣ : gFunctors := #[ GFunctor (excl_authR boolO *
                                             optionRF (agreeRF (▶ ∙)) ) ].
@@ -25,7 +25,7 @@ Section box_defs.
     own γ (a, None).
 
   Definition box_own_prop (γ : slice_name) (P : iProp Σ) : iProp Σ :=
-    own γ (ε, Some (to_agree (Next (iProp_unfold P)))).
+    own γ (ε, Some (to_agree (Next P))).
 
   Definition slice_inv (γ : slice_name) (P : iProp Σ) : iProp Σ :=
     ∃ b, box_own_auth γ (●E b) ∗ if b then P else True.
@@ -93,9 +93,7 @@ Lemma box_own_agree γ Q1 Q2 :
   box_own_prop γ Q1 ∗ box_own_prop γ Q2 ⊢ ▷ (Q1 ≡ Q2).
 Proof.
   rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_r.
-  rewrite option_validI /= agree_validI agree_equivI later_equivI /=.
-  iIntros "#HQ". iNext. rewrite -{2}(iProp_fold_unfold Q1).
-  iRewrite "HQ". by rewrite iProp_fold_unfold.
+  by rewrite option_validI /= agree_validI agree_equivI later_equivI /=.
 Qed.
 
 Lemma box_alloc : ⊢ box N ∅ True.
@@ -109,7 +107,7 @@ Lemma slice_insert_empty E q f Q P :
 Proof.
   iDestruct 1 as (Φ) "[#HeqP Hf]".
   iMod (own_alloc_cofinite (●E false ⋅ ◯E false,
-    Some (to_agree (Next (iProp_unfold Q)))) (dom _ f))
+    Some (to_agree (Next Q))) (dom _ f))
     as (γ) "[Hdom Hγ]"; first by (split; [apply auth_both_valid_discrete|]).
   rewrite pair_split. iDestruct "Hγ" as "[[Hγ Hγ'] #HγQ]".
   iDestruct "Hdom" as % ?%not_elem_of_dom.
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 74d39b9ad..ee1f44d5c 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -8,16 +8,20 @@ Import uPred.
 individual CMRAs instead of (lists of) CMRA *functors*. This additional class is
 needed because Coq is otherwise unable to solve type class constraints due to
 higher-order unification problems. *)
-Class inG (Σ : gFunctors) (A : cmraT) :=
-  InG { inG_id : gid Σ; inG_prf :
-    A = rFunctor_apply (gFunctors_lookup Σ inG_id) (iPrePropO Σ)}.
+Class inG (Σ : gFunctors) (A : cmraT) := InG {
+  inG_id : gid Σ;
+  inG_apply := rFunctor_apply (gFunctors_lookup Σ inG_id);
+  inG_prf : A = inG_apply (iPropO Σ) _;
+}.
 Arguments inG_id {_ _} _.
+Arguments inG_apply {_ _} _ _ {_}.
+
 (** We use the mode [-] for [Σ] since there is always a unique [Σ]. We use the
 mode [!] for [A] since we can have multiple [inG]s for different [A]s, so we do
 not want Coq to pick one arbitrarily. *)
 Hint Mode inG - ! : typeclass_instances.
 
-Lemma subG_inG Σ (F : gFunctor) : subG F Σ → inG Σ (rFunctor_apply F (iPrePropO Σ)).
+Lemma subG_inG Σ (F : gFunctor) : subG F Σ → inG Σ (rFunctor_apply F (iPropO Σ)).
 Proof. move=> /(_ 0%fin) /= [j ->]. by exists j. Qed.
 
 (** This tactic solves the usual obligations "subG ? Σ → {in,?}G ? Σ" *)
@@ -51,8 +55,16 @@ Ltac solve_inG :=
   split; (assumption || by apply _).
 
 (** * Definition of the connective [own] *)
+Definition inG_unfold {Σ A} {i : inG Σ A} :
+    inG_apply i (iPropO Σ) -n> inG_apply i (iPrePropO Σ) :=
+  rFunctor_map _ (iProp_fold, iProp_unfold).
+Definition inG_fold {Σ A} {i : inG Σ A} :
+    inG_apply i (iPrePropO Σ) -n> inG_apply i (iPropO Σ) :=
+  rFunctor_map _ (iProp_unfold, iProp_fold).
+
 Definition iRes_singleton {Σ A} {i : inG Σ A} (γ : gname) (a : A) : iResUR Σ :=
-  discrete_fun_singleton (inG_id i) {[ γ := cmra_transport inG_prf a ]}.
+  discrete_fun_singleton (inG_id i)
+    {[ γ := inG_unfold (cmra_transport inG_prf a) ]}.
 Instance: Params (@iRes_singleton) 4 := {}.
 
 Definition own_def `{!inG Σ A} (γ : gname) (a : A) : iProp Σ :=
@@ -65,17 +77,83 @@ Instance: Params (@own) 4 := {}.
 
 (** * Properties about ghost ownership *)
 Section global.
-Context `{Hin: !inG Σ A}.
+Context `{i : !inG Σ A}.
 Implicit Types a : A.
 
 (** ** Properties of [iRes_singleton] *)
-Global Instance iRes_singleton_ne γ :
-  NonExpansive (@iRes_singleton Σ A _ γ).
+Lemma inG_unfold_fold (x : inG_apply i (iPrePropO Σ)) : inG_unfold (inG_fold x) ≡ x.
+Proof.
+  rewrite /inG_unfold /inG_fold -rFunctor_map_compose -{2}[x]rFunctor_map_id.
+  apply (ne_proper (rFunctor_map _)); split=> ?; apply iProp_unfold_fold.
+Qed.
+Lemma inG_fold_unfold (x : inG_apply i (iPropO Σ)) : inG_fold (inG_unfold x) ≡ x.
+Proof.
+  rewrite /inG_unfold /inG_fold -rFunctor_map_compose -{2}[x]rFunctor_map_id.
+  apply (ne_proper (rFunctor_map _)); split=> ?; apply iProp_fold_unfold.
+Qed.
+
+Global Instance iRes_singleton_ne γ : NonExpansive (@iRes_singleton Σ A _ γ).
 Proof. by intros n a a' Ha; apply discrete_fun_singleton_ne; rewrite Ha. Qed.
+Lemma iRes_singleton_validI γ a : ✓ (iRes_singleton γ a) ⊢@{iPropI Σ} ✓ a.
+Proof.
+  rewrite /iRes_singleton.
+  rewrite discrete_fun_validI (forall_elim (inG_id i)) discrete_fun_lookup_singleton.
+  rewrite gmap_validI (forall_elim γ) lookup_singleton option_validI.
+  trans (✓ cmra_transport inG_prf a : iProp Σ)%I; last by destruct inG_prf.
+  apply valid_entails.
+  move=> n /(cmra_morphism_validN inG_fold). by rewrite inG_fold_unfold.
+Qed.
 Lemma iRes_singleton_op γ a1 a2 :
   iRes_singleton γ (a1 ⋅ a2) ≡ iRes_singleton γ a1 ⋅ iRes_singleton γ a2.
 Proof.
-  rewrite /iRes_singleton discrete_fun_singleton_op singleton_op -cmra_transport_op //.
+  rewrite /iRes_singleton discrete_fun_singleton_op singleton_op cmra_transport_op.
+  f_equiv. apply: singletonM_proper. apply (cmra_morphism_op _).
+Qed.
+
+Global Instance iRes_singleton_discrete γ a :
+  Discrete a → Discrete (iRes_singleton γ a).
+Proof.
+  intros ?. rewrite /iRes_singleton.
+  apply discrete_fun_singleton_discrete, gmap_singleton_discrete; [apply _|].
+  intros x Hx. assert (cmra_transport inG_prf a ≡ inG_fold x) as Ha.
+  { apply (discrete _). by rewrite -Hx inG_fold_unfold. }
+  by rewrite Ha inG_unfold_fold.
+Qed.
+Global Instance iRes_singleton_core_id γ a :
+  CoreId a → CoreId (iRes_singleton γ a).
+Proof.
+  intros. apply discrete_fun_singleton_core_id, gmap_singleton_core_id.
+  by rewrite /CoreId -cmra_morphism_pcore core_id.
+Qed.
+
+Lemma later_internal_eq_iRes_singleton γ a r :
+  ▷ (r ≡ iRes_singleton γ a) ⊢@{iPropI Σ}
+  ◇ ∃ b r', r ≡ iRes_singleton γ b ⋅ r' ∧ ▷ (a ≡ b).
+Proof.
+  assert (NonExpansive (λ r : iResUR Σ, r (inG_id i) !! γ)).
+  { intros n r1 r2 Hr. f_equiv. by specialize (Hr (inG_id i)). }
+  rewrite (f_equivI (λ r : iResUR Σ, r (inG_id i) !! γ) r).
+  rewrite {1}/iRes_singleton discrete_fun_lookup_singleton lookup_singleton.
+  rewrite option_equivI. case Hb: (r (inG_id _) !! γ)=> [b|]; last first.
+  { by rewrite /bi_except_0 -or_intro_l. }
+  rewrite -except_0_intro.
+  rewrite -(exist_intro (cmra_transport (eq_sym inG_prf) (inG_fold b))).
+  rewrite -(exist_intro (discrete_fun_insert (inG_id _) (delete γ (r (inG_id i))) r)).
+  apply and_intro.
+  - apply equiv_internal_eq. rewrite /iRes_singleton.
+    rewrite cmra_transport_trans eq_trans_sym_inv_l /=.
+    intros i'. rewrite discrete_fun_lookup_op.
+    destruct (decide (i' = inG_id i)) as [->|?].
+    + rewrite discrete_fun_lookup_insert discrete_fun_lookup_singleton.
+      intros γ'. rewrite lookup_op. destruct (decide (γ' = γ)) as [->|?].
+      * by rewrite lookup_singleton lookup_delete Hb inG_unfold_fold.
+      * by rewrite lookup_singleton_ne // lookup_delete_ne // left_id.
+    + rewrite discrete_fun_lookup_insert_ne //.
+      by rewrite discrete_fun_lookup_singleton_ne // left_id.
+  - apply later_mono. rewrite (f_equivI inG_fold) inG_fold_unfold.
+    apply: (internal_eq_rewrite' _ _ (λ b, a ≡ cmra_transport (eq_sym inG_prf) b)%I);
+      [solve_proper|apply internal_eq_sym|].
+    rewrite cmra_transport_trans eq_trans_sym_inv_r /=. apply internal_eq_refl.
 Qed.
 
 (** ** Properties of [own] *)
@@ -93,13 +171,7 @@ Global Instance own_mono' γ : Proper (flip (≼) ==> (⊢)) (@own Σ A _ γ).
 Proof. intros a1 a2. apply own_mono. Qed.
 
 Lemma own_valid γ a : own γ a ⊢ ✓ a.
-Proof.
-  rewrite !own_eq /own_def ownM_valid /iRes_singleton.
-  rewrite discrete_fun_validI (forall_elim (inG_id Hin)) discrete_fun_lookup_singleton.
-  rewrite gmap_validI (forall_elim γ) lookup_singleton option_validI.
-  (* implicit arguments differ a bit *)
-  by trans (✓ cmra_transport inG_prf a : iProp Σ)%I; last destruct inG_prf.
-Qed.
+Proof. by rewrite !own_eq /own_def ownM_valid iRes_singleton_validI. Qed.
 Lemma own_valid_2 γ a1 a2 : own γ a1 -∗ own γ a2 -∗ ✓ (a1 ⋅ a2).
 Proof. apply wand_intro_r. by rewrite -own_op own_valid. Qed.
 Lemma own_valid_3 γ a1 a2 a3 : own γ a1 -∗ own γ a2 -∗ own γ a3 -∗ ✓ (a1 ⋅ a2 ⋅ a3).
@@ -110,38 +182,22 @@ Lemma own_valid_l γ a : own γ a ⊢ ✓ a ∗ own γ a.
 Proof. by rewrite comm -own_valid_r. Qed.
 
 Global Instance own_timeless γ a : Discrete a → Timeless (own γ a).
-Proof. rewrite !own_eq /own_def; apply _. Qed.
+Proof. rewrite !own_eq /own_def. apply _. Qed.
 Global Instance own_core_persistent γ a : CoreId a → Persistent (own γ a).
 Proof. rewrite !own_eq /own_def; apply _. Qed.
 
-Lemma later_own γ a : ▷ own γ a -∗ ◇ (∃ b, own γ b ∧ ▷ (a ≡ b)).
+Lemma later_own γ a : ▷ own γ a -∗ ◇ ∃ b, own γ b ∧ ▷ (a ≡ b).
 Proof.
   rewrite own_eq /own_def later_ownM. apply exist_elim=> r.
-  assert (NonExpansive (λ r : iResUR Σ, r (inG_id Hin) !! γ)).
-  { intros n r1 r2 Hr. f_equiv. by specialize (Hr (inG_id Hin)). }
-  rewrite (f_equivI (λ r : iResUR Σ, r (inG_id Hin) !! γ) _ r).
-  rewrite {1}/iRes_singleton discrete_fun_lookup_singleton lookup_singleton.
-  rewrite option_equivI. case Hb: (r (inG_id _) !! γ)=> [b|]; last first.
-  { by rewrite and_elim_r /bi_except_0 -or_intro_l. }
-  rewrite -except_0_intro -(exist_intro (cmra_transport (eq_sym inG_prf) b)).
-  apply and_mono.
-  - rewrite /iRes_singleton. assert (∀ {A A' : cmraT} (Heq : A' = A) (a : A),
-      cmra_transport Heq (cmra_transport (eq_sym Heq) a) = a) as ->
-      by (by intros ?? ->).
-    apply ownM_mono=> /=.
-    exists (discrete_fun_insert (inG_id _) (delete γ (r (inG_id Hin))) r).
-    intros i'. rewrite discrete_fun_lookup_op.
-    destruct (decide (i' = inG_id Hin)) as [->|?].
-    + rewrite discrete_fun_lookup_insert discrete_fun_lookup_singleton.
-      intros γ'. rewrite lookup_op. destruct (decide (γ' = γ)) as [->|?].
-      * by rewrite lookup_singleton lookup_delete Hb.
-      * by rewrite lookup_singleton_ne // lookup_delete_ne // left_id.
-    + rewrite discrete_fun_lookup_insert_ne //.
-      by rewrite discrete_fun_lookup_singleton_ne // left_id.
-  - apply later_mono.
-    by assert (∀ {A A' : cmraT} (Heq : A' = A) (a' : A') (a : A),
-      cmra_transport Heq a' ≡ a ⊢@{iPropI Σ}
-        a' ≡ cmra_transport (eq_sym Heq) a) as -> by (by intros ?? ->).
+  assert (NonExpansive (λ r : iResUR Σ, r (inG_id i) !! γ)).
+  { intros n r1 r2 Hr. f_equiv. by specialize (Hr (inG_id i)). }
+  rewrite internal_eq_sym later_internal_eq_iRes_singleton.
+  rewrite (except_0_intro (uPred_ownM r)) -except_0_and. f_equiv.
+  rewrite and_exist_l. f_equiv=> b. rewrite and_exist_l. apply exist_elim=> r'.
+  rewrite assoc. apply and_mono_l.
+  etrans; [|apply ownM_mono, (cmra_included_l _ r')].
+  eapply (internal_eq_rewrite' _ _ uPred_ownM _); [apply and_elim_r|].
+  apply and_elim_l.
 Qed.
 
 (** ** Allocation *)
@@ -152,13 +208,16 @@ Lemma own_alloc_strong_dep (f : gname → A) (P : gname → Prop) :
   (∀ γ, P γ → ✓ (f γ)) →
   ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ own γ (f γ).
 Proof.
-  intros HP Ha.
+  intros HPinf Hf.
   rewrite -(bupd_mono (∃ m, ⌜∃ γ, P γ ∧ m = iRes_singleton γ (f γ)⌝ ∧ uPred_ownM m)%I).
   - rewrite /bi_emp_valid (ownM_unit emp).
-    eapply bupd_ownM_updateP, (discrete_fun_singleton_updateP_empty (inG_id Hin)).
-    + eapply alloc_updateP_strong_dep'; first done.
-      intros i _ ?. eapply cmra_transport_valid, Ha. done.
-    + naive_solver.
+    apply bupd_ownM_updateP, (discrete_fun_singleton_updateP_empty _ (λ m, ∃ γ,
+      m = {[ γ := inG_unfold (cmra_transport inG_prf (f γ)) ]} ∧ P γ));
+      [|naive_solver].
+    apply (alloc_updateP_strong_dep _ P _ (λ γ,
+      inG_unfold (cmra_transport inG_prf (f γ)))); [done| |naive_solver].
+    intros γ _ ?.
+    by apply (cmra_morphism_valid inG_unfold), cmra_transport_valid, Hf.
   - apply exist_elim=>m; apply pure_elim_l=>-[γ [Hfresh ->]].
     by rewrite !own_eq /own_def -(exist_intro γ) pure_True // left_id.
 Qed.
@@ -168,8 +227,8 @@ Proof.
   intros Ha.
   apply (own_alloc_strong_dep f (λ γ, γ ∉ G))=> //.
   apply (pred_infinite_set (C:=gset gname)).
-  intros E. set (i := fresh (G ∪ E)).
-  exists i. apply not_elem_of_union, is_fresh.
+  intros E. set (γ := fresh (G ∪ E)).
+  exists γ. apply not_elem_of_union, is_fresh.
 Qed.
 Lemma own_alloc_dep (f : gname → A) :
   (∀ γ, ✓ (f γ)) → ⊢ |==> ∃ γ, own γ (f γ).
@@ -191,14 +250,22 @@ Proof. intros Ha. eapply own_alloc_dep with (f := λ _, a); eauto. Qed.
 (** ** Frame preserving updates *)
 Lemma own_updateP P γ a : a ~~>: P → own γ a ==∗ ∃ a', ⌜P a'⌝ ∗ own γ a'.
 Proof.
-  intros Ha. rewrite !own_eq.
-  rewrite -(bupd_mono (∃ m, ⌜∃ a', m = iRes_singleton γ a' ∧ P a'⌝ ∧ uPred_ownM m)%I).
-  - eapply bupd_ownM_updateP, discrete_fun_singleton_updateP;
-      first by (eapply singleton_updateP', cmra_transport_updateP', Ha).
-    naive_solver.
-  - apply exist_elim=>m; apply pure_elim_l=>-[a' [-> HP]].
+  intros Hupd. rewrite !own_eq.
+  rewrite -(bupd_mono (∃ m,
+    ⌜ ∃ a', m = iRes_singleton γ a' ∧ P a' ⌝ ∧ uPred_ownM m)%I).
+  - apply bupd_ownM_updateP, (discrete_fun_singleton_updateP _ (λ m, ∃ x,
+      m = {[ γ := x ]} ∧ ∃ x',
+      x = inG_unfold x' ∧ ∃ a',
+      x' = cmra_transport inG_prf a' ∧ P a')); [|naive_solver].
+    apply singleton_updateP', (iso_cmra_updateP' inG_fold).
+    { apply inG_unfold_fold. }
+    { apply (cmra_morphism_op _). }
+    { intros n x. split; [|apply (cmra_morphism_validN _)].
+      move=> /(cmra_morphism_validN inG_fold). by rewrite inG_fold_unfold. }
+    by apply cmra_transport_updateP'.
+  - apply exist_elim=> m; apply pure_elim_l=> -[a' [-> HP]].
     rewrite -(exist_intro a'). rewrite -persistent_and_sep.
-      by apply and_intro; [apply pure_intro|].
+    by apply and_intro; [apply pure_intro|].
 Qed.
 
 Lemma own_update γ a a' : a ~~> a' → own γ a ==∗ own γ a'.
@@ -224,13 +291,16 @@ Arguments own_update {_ _} [_] _ _ _ _.
 Arguments own_update_2 {_ _} [_] _ _ _ _ _.
 Arguments own_update_3 {_ _} [_] _ _ _ _ _ _.
 
-Lemma own_unit A `{!inG Σ (A:ucmraT)} γ : ⊢ |==> own γ (ε:A).
+Lemma own_unit A `{i : !inG Σ (A:ucmraT)} γ : ⊢ |==> own γ (ε:A).
 Proof.
   rewrite /bi_emp_valid (ownM_unit emp) !own_eq /own_def.
   apply bupd_ownM_update, discrete_fun_singleton_update_empty.
-  apply (alloc_unit_singleton_update (cmra_transport inG_prf ε)); last done.
-  - apply cmra_transport_valid, ucmra_unit_valid.
-  - intros x; destruct inG_prf. by rewrite left_id.
+  apply (alloc_unit_singleton_update (inG_unfold (cmra_transport inG_prf ε))).
+  - apply (cmra_morphism_valid _), cmra_transport_valid, ucmra_unit_valid.
+  - intros x. rewrite -(inG_unfold_fold x) -(cmra_morphism_op inG_unfold).
+    f_equiv. generalize (inG_fold x)=> x'.
+    destruct inG_prf=> /=. by rewrite left_id.
+  - done.
 Qed.
 
 (** Big op class instances *)
@@ -258,7 +328,6 @@ Section big_op_instances.
     own γ ([^op mset] x ∈ X, g x) ⊣⊢ [∗ mset] x ∈ X, own γ (g x).
   Proof. apply (big_opMS_commute1 _). Qed.
 
-
   Global Instance own_cmra_sep_entails_homomorphism :
     MonoidHomomorphism op uPred_sep (⊢) (own γ).
   Proof.
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index d0e61c488..586725300 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -9,7 +9,7 @@ Import uPred.
    saved whatever-you-like. *)
 
 Class savedAnythingG (Σ : gFunctors) (F : oFunctor) := SavedAnythingG {
-  saved_anything_inG :> inG Σ (agreeR (oFunctor_apply F (iPrePropO Σ)));
+  saved_anything_inG :> inG Σ (agreeR (oFunctor_apply F (iPropO Σ)));
   saved_anything_contractive : oFunctorContractive F (* NOT an instance to avoid cycles with [subG_savedAnythingΣ]. *)
 }.
 Definition savedAnythingΣ (F : oFunctor) `{!oFunctorContractive F} : gFunctors :=
@@ -21,7 +21,7 @@ Proof. solve_inG. Qed.
 
 Definition saved_anything_own `{!savedAnythingG Σ F}
     (γ : gname) (x : oFunctor_apply F (iPropO Σ)) : iProp Σ :=
-  own γ (to_agree $ (oFunctor_map F (iProp_fold, iProp_unfold) x)).
+  own γ (to_agree x).
 Typeclasses Opaque saved_anything_own.
 Instance: Params (@saved_anything_own) 4 := {}.
 
@@ -56,13 +56,7 @@ Section saved_anything.
   Proof.
     iIntros "Hx Hy". rewrite /saved_anything_own.
     iDestruct (own_valid_2 with "Hx Hy") as "Hv".
-    rewrite agree_validI agree_equivI.
-    set (G1 := oFunctor_map F (iProp_fold, iProp_unfold)).
-    set (G2 := oFunctor_map F (@iProp_unfold Σ, @iProp_fold Σ)).
-    assert (∀ z, G2 (G1 z) ≡ z) as help.
-    { intros z. rewrite /G1 /G2 -oFunctor_map_compose -{2}[z]oFunctor_map_id.
-      apply (ne_proper (oFunctor_map F)); split=>?; apply iProp_fold_unfold. }
-    rewrite -{2}[x]help -{2}[y]help. by iApply f_equivI.
+    by rewrite agree_validI agree_equivI.
   Qed.
 End saved_anything.
 
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index b665b0562..e30f3a194 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -9,7 +9,7 @@ exception of what's in the [invG] module. The module [invG] is thus exported in
 [fancy_updates], which [wsat] is only imported. *)
 Module invG.
   Class invG (Σ : gFunctors) : Set := WsatG {
-    inv_inG :> inG Σ (authR (gmapUR positive (agreeR (laterO (iPrePropO Σ)))));
+    inv_inG :> inG Σ (authR (gmapUR positive (agreeR (laterO (iPropO Σ)))));
     enabled_inG :> inG Σ coPset_disjR;
     disabled_inG :> inG Σ (gset_disjR positive);
     invariant_name : gname;
@@ -23,7 +23,7 @@ Module invG.
       GFunctor (gset_disjUR positive)].
 
   Class invPreG (Σ : gFunctors) : Set := WsatPreG {
-    inv_inPreG :> inG Σ (authR (gmapUR positive (agreeR (laterO (iPrePropO Σ)))));
+    inv_inPreG :> inG Σ (authR (gmapUR positive (agreeR (laterO (iPropO Σ)))));
     enabled_inPreG :> inG Σ coPset_disjR;
     disabled_inPreG :> inG Σ (gset_disjR positive);
   }.
@@ -33,8 +33,8 @@ Module invG.
 End invG.
 Import invG.
 
-Definition invariant_unfold {Σ} (P : iProp Σ) : agree (later (iPrePropO Σ)) :=
-  to_agree (Next (iProp_unfold P)).
+Definition invariant_unfold {Σ} (P : iProp Σ) : agree (later (iProp Σ)) :=
+  to_agree (Next P).
 Definition ownI `{!invG Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
   own invariant_name (â—¯ {[ i := invariant_unfold P ]}).
 Arguments ownI {_ _} _ _%I.
@@ -121,7 +121,7 @@ Proof.
     iRewrite "HI" in "HvI". rewrite uPred.option_validI agree_validI.
     iRewrite -"HvI" in "HI". by rewrite agree_idemp. }
   rewrite /invariant_unfold.
-  by rewrite agree_equivI later_equivI iProp_unfold_equivI.
+  by rewrite agree_equivI later_equivI.
 Qed.
 
 Lemma ownI_open i P : wsat ∗ ownI i P ∗ ownE {[i]} ⊢ wsat ∗ ▷ P ∗ ownD {[i]}.
-- 
GitLab