New notion of local updates.

_CoqProject

@@ -78,7 +78,6 @@ program_logic/ectxi_language.v
 program_logic/ectx_lifting.v
 program_logic/ghost_ownership.v
 program_logic/saved_prop.v
-program_logic/auth.v
 program_logic/sts.v
 program_logic/namespaces.v
 program_logic/boxes.v

algebra/auth.v

@@ -200,26 +200,20 @@ Proof. by rewrite /op /auth_op /= left_id. Qed.
 Lemma auth_auth_valid a : ✓ a → ✓ (● a).
 Proof. intros; split; simpl; auto using ucmra_unit_leastN. Qed.
 
-Lemma auth_update a af b :
-  a ~l~> b @ Some af → ● (a ⋅ af) ⋅ ◯ a ~~> ● (b ⋅ af) ⋅ ◯ b.
+Lemma auth_update a b a' b' :
+  (a,b) ~l~> (a',b') → ● a ⋅ ◯ b ~~> ● a' ⋅ ◯ b'.
 Proof.
-  intros [Hab Hab']; apply cmra_total_update.
-  move=> n [[[?|]|] bf1] // =>-[[bf2 Ha] ?]; do 2 red; simpl in *.
-  move: Ha; rewrite !left_id=> Hm; split; auto.
-  exists bf2. rewrite -assoc.
-  apply (Hab' _ (Some _)); auto. by rewrite /= assoc.
+  intros Hup; apply cmra_total_update.
+  move=> n [[[?|]|] bf1] // [[bf2 Ha] ?]; do 2 red; simpl in *.
+  move: Ha; rewrite !left_id -assoc=> Ha.
+  destruct (Hup n (Some (bf1 ⋅ bf2))); auto.
+  split; last done. exists bf2. by rewrite -assoc.
 Qed.
 
-Lemma auth_update_no_frame a b : a ~l~> b @ Some ∅ → ● a ⋅ ◯ a ~~> ● b ⋅ ◯ b.
-Proof.
-  intros. rewrite -{1}(right_id _ _ a) -{1}(right_id _ _ b).
-  by apply auth_update.
-Qed.
-Lemma auth_update_no_frag af b : ∅ ~l~> b @ Some af → ● af ~~> ● (b ⋅ af) ⋅ ◯ b.
-Proof.
-  intros. rewrite -{1}(left_id _ _ af) -{1}(right_id _ _ (● _)).
-  by apply auth_update.
-Qed.
+Lemma auth_update_alloc a a' b' : (a,∅) ~l~> (a',b') → ● a ~~> ● a' ⋅ ◯ b'.
+Proof. intros. rewrite -(right_id _ _ (● a)). by apply auth_update. Qed.
+Lemma auth_update_dealloc a b a' : (a,b) ~l~> (a',∅) → ● a ⋅ ◯ b ~~> ● a'.
+Proof. intros. rewrite -(right_id _ _ (● a')). by apply auth_update. Qed.
 End cmra.
 
 Arguments authR : clear implicits.

algebra/coPset.v

@@ -48,11 +48,11 @@ Section coPset.
   Lemma coPset_update X Y : X ~~> Y.
   Proof. done. Qed.
 
-  Lemma coPset_local_update X Y mXf : X ⊆ Y → X ~l~> Y @ mXf.
+  Lemma coPset_local_update X Y X' : X ⊆ X' → (X,Y) ~l~> (X',X').
   Proof.
     intros (Z&->&?)%subseteq_disjoint_union_L.
-    intros; apply local_update_total; split; [done|]; simpl.
-    intros mZ _. rewrite !coPset_opM=> HX. by rewrite (comm_L _ X) -!assoc_L HX.
+    rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->.
+    split. done. rewrite coPset_op_union. set_solver.
   Qed.
 End coPset.
 

algebra/csum.v

@@ -300,31 +300,22 @@ Proof. eauto using csum_updateP_l. Qed.
 Lemma csum_updateP'_r (P : B → Prop) b :
   b ~~>: P → Cinr b ~~>: λ m', ∃ b', m' = Cinr b' ∧ P b'.
 Proof. eauto using csum_updateP_r. Qed.
-Lemma csum_local_update_l (a1 a2 : A) af :
-  (∀ af', af = Cinl <$> af' → a1 ~l~> a2 @ af') → Cinl a1 ~l~> Cinl a2 @ af.
+
+Lemma csum_local_update_l (a1 a2 a1' a2' : A) :
+  (a1,a2) ~l~> (a1',a2') → (Cinl a1,Cinl a2) ~l~> (Cinl a1',Cinl a2').
 Proof.
-  intros Ha. split; destruct af as [[af'| |]|]=>//=.
-  - by eapply (Ha (Some af')).
-  - by eapply (Ha None).
-  - destruct (Ha (Some af') (reflexivity _)) as [_ Ha'].
-    intros n [[mz|mz|]|] ?; inversion 1; subst; constructor.
-    by apply (Ha' n (Some mz)). by apply (Ha' n None).
-  - destruct (Ha None (reflexivity _)) as [_ Ha'].
-    intros n [[mz|mz|]|] ?; inversion 1; subst; constructor.
-    by apply (Ha' n (Some mz)). by apply (Ha' n None).
+  intros Hup n mf ? Ha1; simpl in *.
+  destruct (Hup n (mf ≫= maybe Cinl)); auto.
+  { by destruct mf as [[]|]; inversion_clear Ha1. }
+  split. done. by destruct mf as [[]|]; inversion_clear Ha1; constructor.
 Qed.
-Lemma csum_local_update_r (b1 b2 : B) bf :
-  (∀ bf', bf = Cinr <$> bf' → b1 ~l~> b2 @ bf') → Cinr b1 ~l~> Cinr b2 @ bf.
+Lemma csum_local_update_r (b1 b2 b1' b2' : B) :
+  (b1,b2) ~l~> (b1',b2') → (Cinr b1,Cinr b2) ~l~> (Cinr b1',Cinr b2').
 Proof.
-  intros Hb. split; destruct bf as [[|bf'|]|]=>//=.
-  - by eapply (Hb (Some bf')).
-  - by eapply (Hb None).
-  - destruct (Hb (Some bf') (reflexivity _)) as [_ Hb'].
-    intros n [[mz|mz|]|] ?; inversion 1; subst; constructor.
-    by apply (Hb' n (Some mz)). by apply (Hb' n None).
-  - destruct (Hb None (reflexivity _)) as [_ Hb'].
-    intros n [[mz|mz|]|] ?; inversion 1; subst; constructor.
-    by apply (Hb' n (Some mz)). by apply (Hb' n None).
+  intros Hup n mf ? Ha1; simpl in *.
+  destruct (Hup n (mf ≫= maybe Cinr)); auto.
+  { by destruct mf as [[]|]; inversion_clear Ha1. }
+  split. done. by destruct mf as [[]|]; inversion_clear Ha1; constructor.
 Qed.
 End cmra.
 

algebra/gmap.v

@@ -378,50 +378,63 @@ Section freshness.
   Qed.
 End freshness.
 
-Lemma insert_local_update m i x y mf :
-  x ~l~> y @ mf ≫= (!! i) → <[i:=x]>m ~l~> <[i:=y]>m @ mf.
+Lemma alloc_local_update m1 m2 i x :
+  m1 !! i = None → ✓ x → (m1,m2) ~l~> (<[i:=x]>m1, <[i:=x]>m2).
 Proof.
-  intros [Hxy Hxy']; split.
-  - intros n Hm j. move: (Hm j). destruct (decide (i = j)); subst.
-    + rewrite !lookup_opM !lookup_insert !Some_op_opM. apply Hxy.
-    + by rewrite !lookup_opM !lookup_insert_ne.
-  - intros n mf' Hm Hm' j. move: (Hm j) (Hm' j).
-    destruct (decide (i = j)); subst.
-    + rewrite !lookup_opM !lookup_insert !Some_op_opM !inj_iff. apply Hxy'.
-    + by rewrite !lookup_opM !lookup_insert_ne.
-Qed.
-
-Lemma singleton_local_update i x y mf :
-  x ~l~> y @ mf ≫= (!! i) → {[ i := x ]} ~l~> {[ i := y ]} @ mf.
-Proof. apply insert_local_update. Qed.
-
-Lemma alloc_singleton_local_update m i x mf :
-  (m ⋅? mf) !! i = None → ✓ x → m ~l~> <[i:=x]> m @ mf.
+  rewrite cmra_valid_validN=> Hi ?.
+  apply local_update_unital=> n mf Hmv Hm; simpl in *.
+  split; auto using insert_validN.
+  intros j; destruct (decide (i = j)) as [->|].
+  - move: (Hm j); rewrite Hi symmetry_iff dist_None lookup_op op_None=>-[_ Hj].
+    by rewrite lookup_op !lookup_insert Hj.
+  - rewrite Hm lookup_insert_ne // !lookup_op lookup_insert_ne //.
+Qed.
+
+Lemma alloc_singleton_local_update m i x :
+  m !! i = None → ✓ x → (m,∅) ~l~> (<[i:=x]>m, {[ i:=x ]}).
+Proof. apply alloc_local_update. Qed.
+
+Lemma insert_local_update m1 m2 i x y x' y' :
+  m1 !! i = Some x → m2 !! i = Some y →
+  (x, y) ~l~> (x', y') →
+  (m1, m2) ~l~> (<[i:=x']>m1, <[i:=y']>m2).
 Proof.
-  rewrite lookup_opM op_None=> -[Hi Hif] ?.
-  rewrite insert_singleton_op // comm. apply alloc_local_update.
-  intros n Hm j. move: (Hm j). destruct (decide (i = j)); subst.
-  - intros _; rewrite !lookup_opM lookup_op !lookup_singleton Hif Hi.
-    by apply cmra_valid_validN.
-  - by rewrite !lookup_opM lookup_op !lookup_singleton_ne // right_id.
+  intros Hi1 Hi2 Hup; apply local_update_unital=> n mf Hmv Hm; simpl in *.
+  destruct (Hup n (mf !! i)) as [? Hx']; simpl in *.
+  { move: (Hmv i). by rewrite Hi1. }
+  { move: (Hm i). by rewrite lookup_op Hi1 Hi2 Some_op_opM (inj_iff Some). }
+  split; auto using insert_validN.
+  rewrite Hm Hx'=> j; destruct (decide (i = j)) as [->|].
+  - by rewrite lookup_insert lookup_op lookup_insert Some_op_opM.
+  - by rewrite lookup_insert_ne // !lookup_op lookup_insert_ne.
+Qed.
+
+Lemma singleton_local_update m i x y x' y' :
+  m !! i = Some x →
+  (x, y) ~l~> (x', y') →
+  (m, {[ i := y ]}) ~l~> (<[i:=x']>m, {[ i := y' ]}).
+Proof.
+  intros. rewrite /singletonM /map_singleton -(insert_insert ∅ i y' y).
+  eapply insert_local_update; eauto using lookup_insert.
 Qed.
 
-Lemma alloc_unit_singleton_local_update i x mf :
-  mf ≫= (!! i) = None → ✓ x → (∅:gmap K A) ~l~> {[ i := x ]} @ mf.
+Lemma delete_local_update m1 m2 i x `{!Exclusive x} :
+  m2 !! i = Some x → (m1, m2) ~l~> (delete i m1, delete i m2).
 Proof.
-  intros Hi; apply alloc_singleton_local_update. by rewrite lookup_opM Hi.
+  intros Hi. apply local_update_unital=> n mf Hmv Hm; simpl in *.
+  split; auto using delete_validN.
+  rewrite Hm=> j; destruct (decide (i = j)) as [<-|].
+  - rewrite lookup_op !lookup_delete left_id symmetry_iff dist_None.
+    apply eq_None_not_Some=> -[y Hi'].
+    move: (Hmv i). rewrite Hm lookup_op Hi Hi' -Some_op. by apply exclusiveN_l.
+  - by rewrite lookup_op !lookup_delete_ne // lookup_op. 
 Qed.
 
-Lemma delete_local_update m i x `{!Exclusive x} mf :
-  m !! i = Some x → m ~l~> delete i m @ mf.
+Lemma delete_singleton_local_update m i x `{!Exclusive x} :
+  (m, {[ i := x ]}) ~l~> (delete i m, ∅).
 Proof.
-  intros Hx; split; [intros n; apply delete_update|].
-  intros n mf' Hm Hm' j. move: (Hm j) (Hm' j).
-  destruct (decide (i = j)); subst.
-  + rewrite !lookup_opM !lookup_delete Hx=> ? Hj.
-    rewrite (exclusiveN_Some_l n x (mf ≫= lookup j)) //.
-    by rewrite (exclusiveN_Some_l n x (mf' ≫= lookup j)) -?Hj.
-  + by rewrite !lookup_opM !lookup_delete_ne.
+  rewrite -(delete_singleton i x).
+  eapply delete_local_update; eauto using lookup_singleton.
 Qed.
 End properties.
 

algebra/gset.v

@@ -47,16 +47,15 @@ Section gset.
   Lemma gset_update X Y : X ~~> Y.
   Proof. done. Qed.
 
-  Lemma gset_local_update X Y mXf : X ⊆ Y → X ~l~> Y @ mXf.
+  Lemma gset_local_update X Y X' : X ⊆ X' → (X,Y) ~l~> (X',X').
   Proof.
     intros (Z&->&?)%subseteq_disjoint_union_L.
-    intros; apply local_update_total; split; [done|]; simpl.
-    intros mZ _. rewrite !gset_opM=> HX. by rewrite (comm_L _ X) -!assoc_L HX.
+    rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->.
+    split. done. rewrite gset_op_union. set_solver.
   Qed.
 
   Global Instance gset_persistent X : Persistent X.
   Proof. by apply persistent_total; rewrite gset_core_self. Qed.
-
 End gset.
 
 Arguments gsetR _ {_ _}.
@@ -72,6 +71,8 @@ Arguments GSetBot {_ _ _}.
 Section gset_disj.
   Context `{Countable K}.
   Arguments op _ _ !_ !_ /.
+  Arguments cmra_op _ !_ !_ /.
+  Arguments ucmra_op _ !_ !_ /.
 
   Canonical Structure gset_disjC := leibnizC (gset_disj K).
 
@@ -174,35 +175,45 @@ Section gset_disj.
     Proof. eauto using gset_disj_alloc_empty_updateP. Qed.
   End fresh_updates.
 
-  Lemma gset_disj_dealloc_local_update X Y Xf :
-    GSet X ~l~> GSet (X ∖ Y) @ Some (GSet Xf).
+  Lemma gset_disj_dealloc_local_update X Y :
+    (GSet X, GSet Y) ~l~> (GSet (X ∖ Y), ∅).
+  Proof.
+    apply local_update_total_valid=> _ _ /gset_disj_included HYX.
+    rewrite local_update_unital_discrete=> -[Xf|] _ /leibniz_equiv_iff //=.
+    rewrite {1}/op /=. destruct (decide _) as [HXf|]; [intros[= ->]|done].
+    by rewrite difference_union_distr_l_L
+      difference_diag_L !left_id_L difference_disjoint_L.
+  Qed.
+  Lemma gset_disj_dealloc_empty_local_update X Z :
+    (GSet Z ⋅ GSet X, GSet Z) ~l~> (GSet X,∅).
   Proof.
-    apply local_update_total; split; simpl.
-    { rewrite !gset_disj_valid_op; set_solver. }
-    intros mZ ?%gset_disj_valid_op. rewrite gset_disj_union //.
-    destruct mZ as [[Z|]|]; simpl; try done.
-    - rewrite {1}/op {1}/cmra_op /=. destruct (decide _); simpl; try done.
-      intros [=]. do 2 f_equal. by apply union_cancel_l_L with X.
-    - intros [=]. assert (Xf = ∅) as -> by set_solver. by rewrite right_id.
+    apply local_update_total_valid=> /gset_disj_valid_op HZX _ _.
+    assert (X = (Z ∪ X) ∖ Z) as HX by set_solver.
+    rewrite gset_disj_union // {2}HX. apply gset_disj_dealloc_local_update.
   Qed.
-  Lemma gset_disj_dealloc_empty_local_update X Xf :
-    GSet X ~l~> GSet ∅ @ Some (GSet Xf).
+  Lemma gset_disj_dealloc_op_local_update X Y Z :
+    (GSet Z ⋅ GSet X, GSet Z ⋅ GSet Y) ~l~> (GSet X,GSet Y).
   Proof.
-    rewrite -(difference_diag_L X). apply gset_disj_dealloc_local_update.
+    rewrite -{2}(left_id ∅ _ (GSet Y)).
+    apply op_local_update_frame, gset_disj_dealloc_empty_local_update.
   Qed.
 
-  Lemma gset_disj_alloc_local_update X i Xf :
-    i ∉ X → i ∉ Xf → GSet X ~l~> GSet ({[i]} ∪ X) @ Some (GSet Xf).
+  Lemma gset_disj_alloc_op_local_update X Y Z :
+    Z ⊥ X → (GSet X,GSet Y) ~l~> (GSet Z ⋅ GSet X, GSet Z ⋅ GSet Y).
+  Proof.
+    intros. apply op_local_update_discrete. by rewrite gset_disj_valid_op.
+  Qed.
+  Lemma gset_disj_alloc_local_update X Y Z :
+    Z ⊥ X → (GSet X,GSet Y) ~l~> (GSet (Z ∪ X), GSet (Z ∪ Y)).
   Proof.
-    intros ??; apply local_update_total; split; simpl.
-    - rewrite !gset_disj_valid_op; set_solver.
-    - intros mZ ?%gset_disj_valid_op HXf.
-      rewrite -gset_disj_union -?assoc ?HXf ?cmra_opM_assoc; set_solver.
+    intros. apply local_update_total_valid=> _ _ /gset_disj_included ?.
+    rewrite -!gset_disj_union //; last set_solver.
+    auto using gset_disj_alloc_op_local_update.
   Qed.
-  Lemma gset_disj_alloc_empty_local_update i Xf :
-    i ∉ Xf → GSet ∅ ~l~> GSet {[i]} @ Some (GSet Xf).
+  Lemma gset_disj_alloc_empty_local_update X Z :
+    Z ⊥ X → (GSet X, GSet ∅) ~l~> (GSet (Z ∪ X), GSet Z).
   Proof.
-    intros. rewrite -(right_id_L _ _ {[i]}).
+    intros. rewrite -{2}(right_id_L _ union Z).
     apply gset_disj_alloc_local_update; set_solver.
   Qed.
 End gset_disj.

algebra/list.v

@@ -398,6 +398,7 @@ Section properties.
     rewrite !cmra_update_updateP=> ?; eauto using list_middle_updateP with subst.
   Qed.
 
+(* FIXME
   Lemma list_middle_local_update l1 l2 x y ml :
     x ~l~> y @ ml ≫= (!! length l1) →
     l1 ++ x :: l2 ~l~> l1 ++ y :: l2 @ ml.
@@ -421,6 +422,7 @@ Section properties.
   Lemma list_singleton_local_update i x y ml :
     x ~l~> y @ ml ≫= (!! i) → {[ i := x ]} ~l~> {[ i := y ]} @ ml.
   Proof. intros; apply list_middle_local_update. by rewrite replicate_length. Qed.
+*)
 End properties.
 
 (** Functor *)

algebra/local_updates.v

 From iris.algebra Require Export cmra.
 
 (** * Local updates *)
-Record local_update {A : cmraT} (mz : option A) (x y : A) := {
-  local_update_valid n : ✓{n} (x ⋅? mz) → ✓{n} (y ⋅? mz);
-  local_update_go n mz' :
-    ✓{n} (x ⋅? mz) → x ⋅? mz ≡{n}≡ x ⋅? mz' → y ⋅? mz ≡{n}≡ y ⋅? mz'
-}.
-Notation "x ~l~> y @ mz" := (local_update mz x y) (at level 70).
+Definition local_update {A : cmraT} (x y : A * A) := ∀ n mz,
+  ✓{n} x.1 → x.1 ≡{n}≡ x.2 ⋅? mz → ✓{n} y.1 ∧ y.1 ≡{n}≡ y.2 ⋅? mz.
 Instance: Params (@local_update) 1.
+Infix "~l~>" := local_update (at level 70).
 
 Section updates.
-Context {A : cmraT}.
-Implicit Types x y : A.
+  Context {A : cmraT}.
+  Implicit Types x y : A.
 
-Global Instance local_update_proper :
-  Proper ((≡) ==> (≡) ==> (≡) ==> iff) (@local_update A).
-Proof.
-  cut (Proper ((≡) ==> (≡) ==> (≡) ==> impl) (@local_update A)).
-  { intros Hproper; split; by apply Hproper. }
-  intros mz mz' Hmz x x' Hx y y' Hy [Hv Hup]; constructor; setoid_subst; auto.
-Qed.
+  Global Instance local_update_proper :
+    Proper ((≡) ==> (≡) ==> iff) (@local_update A).
+  Proof. unfold local_update. by repeat intro; setoid_subst. Qed.
 
-Global Instance local_update_preorder mz : PreOrder (@local_update A mz).
-Proof.
-  split.
-  - intros x; by split.
-  - intros x1 x2 x3 [??] [??]; split; eauto.
-Qed.
+  Global Instance local_update_preorder : PreOrder (@local_update A).
+  Proof. split; unfold local_update; red; naive_solver. Qed.
 
-Lemma exclusive_local_update `{!Exclusive x} y mz : ✓ y → x ~l~> y @ mz.
-Proof.
-  split; intros n.
-  - move=> /exclusiveN_opM ->. by apply cmra_valid_validN.
-  - intros mz' ? Hmz.
-    by rewrite (exclusiveN_opM n x mz) // (exclusiveN_opM n x mz') -?Hmz.
-Qed.
+  Lemma exclusive_local_update `{!Exclusive y} x x' : ✓ x' → (x,y) ~l~> (x',x').
+  Proof.
+    intros ? n mz Hxv Hx; simpl in *.
+    move: Hxv; rewrite Hx; move=> /exclusiveN_opM=> ->; split; auto.
+    by apply cmra_valid_validN.
+  Qed.
 
-Lemma op_local_update x1 x2 y mz :
-  x1 ~l~> x2 @ Some (y ⋅? mz) → x1 ⋅ y ~l~> x2 ⋅ y @ mz.
-Proof.
-  intros [Hv1 H1]; split.
-  - intros n. rewrite !cmra_opM_assoc. move=> /Hv1 /=; auto.
-  - intros n mz'. rewrite !cmra_opM_assoc. move=> Hv /(H1 _ (Some _) Hv) /=; auto.
-Qed.
+  Lemma op_local_update x y z :
+    (∀ n, ✓{n} x → ✓{n} (z ⋅ x)) → (x,y) ~l~> (z ⋅ x, z ⋅ y).
+  Proof.
+    intros Hv n mz Hxv Hx; simpl in *; split; [by auto|].
+    by rewrite Hx -cmra_opM_assoc.
+  Qed.
+  Lemma op_local_update_discrete `{!CMRADiscrete A} x y z :
+    (✓ x → ✓ (z ⋅ x)) → (x,y) ~l~> (z ⋅ x, z ⋅ y).
+  Proof.
+    intros; apply op_local_update=> n. by rewrite -!(cmra_discrete_valid_iff n).
+  Qed.
 
-Lemma alloc_local_update x y mz :
-  (∀ n, ✓{n} (x ⋅? mz) → ✓{n} (x ⋅ y ⋅? mz)) → x ~l~> x ⋅ y @ mz.
-Proof.
-  split; first done.
-  intros n mz' _. by rewrite !(comm _ x) !cmra_opM_assoc=> ->.
-Qed.
+  Lemma op_local_update_frame x y x' y' yf :
+    (x,y) ~l~> (x',y') → (x,y ⋅ yf) ~l~> (x', y' ⋅ yf).
+  Proof.
+    intros Hup n mz Hxv Hx; simpl in *.
+    destruct (Hup n (Some (yf ⋅? mz))); [done|by rewrite /= -cmra_opM_assoc|].
+    by rewrite cmra_opM_assoc.
+  Qed.
 
-Lemma local_update_total `{CMRADiscrete A} x y mz :
-  x ~l~> y @ mz ↔
-    (✓ (x ⋅? mz) → ✓ (y ⋅? mz)) ∧
-    (∀ mz', ✓ (x ⋅? mz) → x ⋅? mz ≡ x ⋅? mz' → y ⋅? mz ≡ y ⋅? mz').
-Proof.
-  split.
-  - destruct 1. split; intros until 0;
-      rewrite !(cmra_discrete_valid_iff 0) ?(timeless_iff 0); auto.
-  - intros [??]; split; intros until 0;
-      rewrite -!cmra_discrete_valid_iff -?timeless_iff; auto.
-Qed.
+  Lemma local_update_discrete `{!CMRADiscrete A} (x y x' y' : A) :
+    (x,y) ~l~> (x',y') ↔ ∀ mz, ✓ x → x ≡ y ⋅? mz → ✓ x' ∧ x' ≡ y' ⋅? mz.
+  Proof.
+    rewrite /local_update /=. setoid_rewrite <-cmra_discrete_valid_iff.
+    setoid_rewrite <-(λ n, timeless_iff n x).
+    setoid_rewrite <-(λ n, timeless_iff n x'). naive_solver eauto using 0.
+  Qed.
+
+  Lemma local_update_valid0 x y x' y' :
+    (✓{0} x → ✓{0} y → x ≡{0}≡ y ∨ y ≼{0} x → (x,y) ~l~> (x',y')) →
+    (x,y) ~l~> (x',y').
+  Proof.
+    intros Hup n mz Hmz Hz; simpl in *. apply Hup; auto.
+    - by apply (cmra_validN_le n); last lia.
+    - apply (cmra_validN_le n); last lia.
+      move: Hmz; rewrite Hz. destruct mz; simpl; eauto using cmra_validN_op_l.
+    - destruct mz as [z|].
+      + right. exists z. apply dist_le with n; auto with lia.
+      + left. apply dist_le with n; auto with lia.
+  Qed.
+  Lemma local_update_valid `{!CMRADiscrete A} x y x' y' :
+    (✓ x → ✓ y → x ≡ y ∨ y ≼ x → (x,y) ~l~> (x',y')) → (x,y) ~l~> (x',y').
+  Proof.
+    rewrite !(cmra_discrete_valid_iff 0)
+      (cmra_discrete_included_iff 0) (timeless_iff 0).
+    apply local_update_valid0.
+  Qed.
+
+  Lemma local_update_total_valid0 `{!CMRATotal A} x y x' y' :
+    (✓{0} x → ✓{0} y → y ≼{0} x → (x,y) ~l~> (x',y')) → (x,y) ~l~> (x',y').
+  Proof.
+    intros Hup. apply local_update_valid0=> ?? [Hx|?]; apply Hup; auto.
+    by rewrite Hx.
+  Qed.
+  Lemma local_update_total_valid `{!CMRATotal A, !CMRADiscrete A} x y x' y' :
+    (✓ x → ✓ y → y ≼ x → (x,y) ~l~> (x',y')) → (x,y) ~l~> (x',y').
+  Proof.
+    rewrite !(cmra_discrete_valid_iff 0) (cmra_discrete_included_iff 0).
+    apply local_update_total_valid0.
+  Qed.
 End updates.
 
+Section updates_unital.
+  Context {A : ucmraT}.
+  Implicit Types x y : A.
+
+  Lemma local_update_unital x y x' y' :
+    (x,y) ~l~> (x',y') ↔ ∀ n z,
+      ✓{n} x → x ≡{n}≡ y ⋅ z → ✓{n} x' ∧ x' ≡{n}≡ y' ⋅ z.
+  Proof.
+    split.
+    - intros Hup n z. apply (Hup _ (Some z)).
+    - intros Hup n [z|]; simpl; [by auto|].
+      rewrite -(right_id ∅ op y) -(right_id ∅ op y'). auto.
+  Qed.
+
+  Lemma local_update_unital_discrete `{!CMRADiscrete A} (x y x' y' : A) :
+    (x,y) ~l~> (x',y') ↔ ∀ z, ✓ x → x ≡ y ⋅ z → ✓ x' ∧ x' ≡ y' ⋅ z.
+  Proof.
+    rewrite local_update_discrete. split.
+    - intros Hup z. apply (Hup (Some z)).
+    - intros Hup [z|]; simpl; [by auto|].
+      rewrite -(right_id ∅ op y) -(right_id ∅ op y'). auto.
+  Qed.
+End updates_unital.
+
 (** * Product *)
-Lemma prod_local_update {A B : cmraT} (x y : A * B) mz :
-  x.1 ~l~> y.1 @ fst <$> mz → x.2 ~l~> y.2 @ snd <$> mz →
-  x ~l~> y @ mz.
+Lemma prod_local_update {A B : cmraT} (x y x' y' : A * B) :
+  (x.1,y.1) ~l~> (x'.1,y'.1) → (x.2,y.2) ~l~> (x'.2,y'.2) →
+  (x,y) ~l~> (x',y').
 Proof.
-  intros [Hv1 H1] [Hv2 H2]; split.
-  - intros n [??]; destruct mz; split; auto.
-  - intros n mz' [??] [??].
-    specialize (H1 n (fst <$> mz')); specialize (H2 n (snd <$> mz')).
-    destruct mz, mz'; split; naive_solver.
+  intros Hup1 Hup2 n mz [??] [??]; simpl in *.
+  destruct (Hup1 n (fst <$> mz)); [done|by destruct mz|].
+  destruct (Hup2 n (snd <$> mz)); [done|by destruct mz|].
+  by destruct mz.
 Qed.
 
+Lemma prod_local_update' {A B : cmraT} (x1 y1 x1' y1' : A) (x2 y2 x2' y2' : B) :
+  (x1,y1) ~l~> (x1',y1') → (x2,y2) ~l~> (x2',y2') →
+  ((x1,x2),(y1,y2)) ~l~> ((x1',x2'),(y1',y2')).
+Proof. intros. by apply prod_local_update. Qed.
+Lemma prod_local_update_1 {A B : cmraT} (x1 y1 x1' y1' : A) (x2 y2 : B) :
+  (x1,y1) ~l~> (x1',y1') → ((x1,x2),(y1,y2)) ~l~> ((x1',x2),(y1',y2)).
+Proof. intros. by apply prod_local_update. Qed.
+Lemma prod_local_update_2 {A B : cmraT} (x1 y1 : A) (x2 y2 x2' y2' : B) :
+  (x2,y2) ~l~> (x2',y2') → ((x1,x2),(y1,y2)) ~l~> ((x1,x2'),(y1,y2')).
+Proof. intros. by apply prod_local_update. Qed.
+
 (** * Option *)
-Lemma option_local_update {A : cmraT} (x y : A) mmz :
-  x ~l~> y @ mjoin mmz →
-  Some x ~l~> Some y @ mmz.
+Lemma option_local_update {A : cmraT} (x y x' y' : A) :
+  (x, y) ~l~> (x',y') →
+  (Some x, Some y) ~l~> (Some x', Some y').
 Proof.
-  intros [Hv H]; split; first destruct mmz as [[?|]|]; auto.
-  intros n mmz'. specialize (H n (mjoin mmz')).
-  destruct mmz as [[]|], mmz' as [[]|]; inversion_clear 2; constructor; auto.
+  intros Hup n mmz Hxv Hx; simpl in *.
+  destruct (Hup n (mjoin mmz)); first done.
+  { destruct mmz as [[?|]|]; inversion_clear Hx; auto. }
+  split; first done. destruct mmz as [[?|]|]; constructor; auto.
 Qed.
 
 (** * Natural numbers  *)
-Lemma nat_local_update (x y : nat) mz : x ~l~> y @ mz.
+Lemma nat_local_update (x y x' y' : nat) :
+  x + y' = x' + y → (x,y) ~l~> (x',y').
 Proof.
-  split; first done.
-  compute -[plus]; destruct mz as [z|]; intros n [z'|]; lia.
+  intros ??; apply local_update_unital_discrete=> z _.
+  compute -[minus plus]; lia.
 Qed.
 
-Lemma mnat_local_update (x y : mnat) mz : x ≤ y → x ~l~> y @ mz.
+Lemma mnat_local_update (x y x' : mnatUR) :
+  x ≤ x' → (x,y) ~l~> (x',x').
 Proof.
-  split; first done.
-  compute -[max]; destruct mz as [z|]; intros n [z'|]; lia.
+  intros ??; apply local_update_unital_discrete=> z _.
+  compute -[max]; lia.
 Qed.

algebra/updates.v

@@ -76,8 +76,7 @@ Lemma cmra_update_op x1 x2 y1 y2 : x1 ~~> y1 → x2 ~~> y2 → x1 ⋅ x2 ~~> y1
 Proof.
   rewrite !cmra_update_updateP; eauto using cmra_updateP_op with congruence.
 Qed.
-Lemma cmra_update_valid0 x y :
-  (✓{0} x → x ~~> y) → x ~~> y.
+Lemma cmra_update_valid0 x y : (✓{0} x → x ~~> y) → x ~~> y.
 Proof.
   intros H n mz Hmz. apply H, Hmz.
   apply (cmra_validN_le n); last lia.

heap_lang/adequacy.v

 From iris.program_logic Require Export weakestpre adequacy.
 From iris.heap_lang Require Export heap.
-From iris.program_logic Require Import auth ownership.
+From iris.algebra Require Import auth.
+From iris.program_logic Require Import ownership.
 From iris.heap_lang Require Import proofmode notation.
 From iris.proofmode Require Import tactics.
 
-Definition heapΣ : gFunctors := #[authΣ heapUR; irisΣ heap_lang].
+Class heapPreG Σ := HeapPreG {
+  heap_preG_iris :> irisPreG heap_lang Σ;
+  heap_preG_heap :> inG Σ (authR heapUR)
+}.
 
-Definition heap_adequacy Σ `{irisPreG heap_lang Σ, authG Σ heapUR} e σ φ :
+Definition heapΣ : gFunctors :=
+  #[irisΣ heap_lang; GFunctor (constRF (authR heapUR))].
+Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
+Proof. intros [? ?%subG_inG]%subG_inv. split; apply _. Qed.
+
+Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
   (∀ `{heapG Σ}, heap_ctx ⊢ WP e {{ v, ■ φ v }}) →
   adequate e σ φ.
 Proof.
   intros Hwp; eapply (wp_adequacy Σ); iIntros (?) "Hσ".
-  iVs (auth_alloc (ownP ∘ of_heap) heapN _ (to_heap σ) with "[Hσ]") as (γ) "[??]".
-  - auto using to_heap_valid.
-  - rewrite /= (from_to_heap σ); auto.
-  - iApply (Hwp (HeapG _ _ _ γ)). by rewrite /heap_ctx.
+  iVs (own_alloc (● to_heap σ)) as (γ) "Hh".
+  { apply (auth_auth_valid (to_heap _)), to_heap_valid. }
+  set (Hheap := HeapG _ _ _ γ).
+  iVs (inv_alloc heapN _ heap_inv with "[-]"); [iNext; iExists σ; by iFrame|].
+  iApply (Hwp _). by rewrite /heap_ctx.
 Qed.
\ No newline at end of file

heap_lang/heap.v

 From iris.heap_lang Require Export lifting.
-From iris.algebra Require Import upred_big_op gmap frac dec_agree.
+From iris.algebra Require Import auth gmap frac dec_agree.
 From iris.program_logic Require Export invariants ghost_ownership.
-From iris.program_logic Require Import ownership auth.
+From iris.program_logic Require Import ownership.
 From iris.proofmode Require Import tactics.
 Import uPred.
 (* TODO: The entire construction could be generalized to arbitrary languages that have
@@ -14,32 +14,24 @@ Definition heapUR : ucmraT := gmapUR loc (prodR fracR (dec_agreeR val)).
 (** The CMRA we need. *)
 Class heapG Σ := HeapG {
   heapG_iris_inG :> irisG heap_lang Σ;
-  heap_inG :> authG Σ heapUR;
+  heap_inG :> inG Σ (authR heapUR);
   heap_name : gname
 }.
 (** The Functor we need. *)
 Definition to_heap : state → heapUR := fmap (λ v, (1%Qp, DecAgree v)).
-Definition of_heap : heapUR → state := omap (maybe DecAgree ∘ snd).
 
 Section definitions.
   Context `{heapG Σ}.
 
   Definition heap_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
-    auth_own heap_name {[ l := (q, DecAgree v) ]}.
+    own heap_name (◯ {[ l := (q, DecAgree v) ]}).
   Definition heap_mapsto_aux : { x | x = @heap_mapsto_def }. by eexists. Qed.
   Definition heap_mapsto := proj1_sig heap_mapsto_aux.
   Definition heap_mapsto_eq : @heap_mapsto = @heap_mapsto_def :=
     proj2_sig heap_mapsto_aux.
 
-  Definition heap_inv (h : heapUR) : iProp Σ :=
-    ownP (of_heap h).
-  Definition heap_ctx : iProp Σ :=
-    auth_ctx heap_name heapN heap_inv.
-
-  Global Instance heap_inv_proper : Proper ((≡) ==> (⊣⊢)) heap_inv.
-  Proof. solve_proper. Qed.
-  Global Instance heap_ctx_persistent : PersistentP heap_ctx.
-  Proof. apply _. Qed.
+  Definition heap_inv : iProp Σ := (∃ σ, ownP σ ★ own heap_name (● to_heap σ))%I.
+  Definition heap_ctx : iProp Σ := inv heapN heap_inv.
 End definitions.
 
 Typeclasses Opaque heap_ctx heap_mapsto.
@@ -57,57 +49,38 @@ Section heap.
   Implicit Types h g : heapUR.
 
   (** Conversion to heaps and back *)
-  Global Instance of_heap_proper : Proper ((≡) ==> (=)) of_heap.
-  Proof. solve_proper. Qed.
-  Lemma from_to_heap σ : of_heap (to_heap σ) = σ.
-  Proof.
-    apply map_eq=>l. rewrite lookup_omap lookup_fmap. by case (σ !! l).
-  Qed.
   Lemma to_heap_valid σ : ✓ to_heap σ.
   Proof. intros l. rewrite lookup_fmap. by case (σ !! l). Qed.
-  Lemma of_heap_insert l v h :
-    of_heap (<[l:=(1%Qp, DecAgree v)]> h) = <[l:=v]> (of_heap h).
-  Proof. by rewrite /of_heap -(omap_insert _ _ _ (1%Qp, DecAgree v)). Qed.
-  Lemma of_heap_singleton_op l q v h :
-    ✓ ({[l := (q, DecAgree v)]} ⋅ h) →
-    of_heap ({[l := (q, DecAgree v)]} ⋅ h) = <[l:=v]> (of_heap h).
+  Lemma lookup_to_heap_None σ l : σ !! l = None → to_heap σ !! l = None.
+  Proof. by rewrite /to_heap lookup_fmap=> ->. Qed.
+  Lemma heap_singleton_included σ l q v :
+    {[l := (q, DecAgree v)]} ≼ to_heap σ → σ !! l = Some v.
   Proof.
-    intros Hv. apply map_eq=> l'; destruct (decide (l' = l)) as [->|].
-    - move: (Hv l). rewrite /of_heap lookup_insert
-        lookup_omap (lookup_op _ h) lookup_singleton.
-      case _:(h !! l)=>[[q' [v'|]]|] //=; last by move=> [??].
-      move=> [? /dec_agree_op_inv [->]]. by rewrite dec_agree_idemp.
-    - rewrite /of_heap lookup_insert_ne // !lookup_omap.
-      by rewrite (lookup_op _ h) lookup_singleton_ne // left_id_L.
+    rewrite singleton_included=> -[[q' av] [/leibniz_equiv_iff Hl Hqv]].
+    move: Hl. rewrite /to_heap lookup_fmap fmap_Some=> -[v' [Hl [??]]]; subst.
+    by move: Hqv=> /Some_pair_included_total_2 [_ /DecAgree_included ->].
   Qed.
-  Lemma to_heap_insert l v σ :
-    to_heap (<[l:=v]> σ) = <[l:=(1%Qp, DecAgree v)]> (to_heap σ).
-  Proof. by rewrite /to_heap -fmap_insert. Qed.
-  Lemma of_heap_None h l : ✓ h → of_heap h !! l = None → h !! l = None.
+  Lemma heap_singleton_included' σ l q v :
+    {[l := (q, DecAgree v)]} ≼ to_heap σ → to_heap σ !! l = Some (1%Qp,DecAgree v).
   Proof.
-    move=> /(_ l). rewrite /of_heap lookup_omap.
-    by case: (h !! l)=> [[q [v|]]|] //=; destruct 1; auto.
+    intros Hl%heap_singleton_included. by rewrite /to_heap lookup_fmap Hl.
   Qed.
-  Lemma heap_store_valid l h v1 v2 :
-    ✓ ({[l := (1%Qp, DecAgree v1)]} ⋅ h) →
-    ✓ ({[l := (1%Qp, DecAgree v2)]} ⋅ h).
-  Proof.
-    intros Hv l'; move: (Hv l'). destruct (decide (l' = l)) as [->|].
-    - rewrite !lookup_op !lookup_singleton.
-      by case: (h !! l)=> [x|] // /Some_valid/exclusive_l.
-    - by rewrite !lookup_op !lookup_singleton_ne.
-  Qed.
-  Hint Resolve heap_store_valid.
+  Lemma to_heap_insert l v σ :
+    to_heap (<[l:=v]> σ) = <[l:=(1%Qp, DecAgree v)]> (to_heap σ).
+  Proof. by rewrite /to_heap fmap_insert. Qed.
 
   Context `{heapG Σ}.
 
   (** General properties of mapsto *)
+  Global Instance heap_ctx_persistent : PersistentP heap_ctx.
+  Proof. rewrite /heap_ctx. apply _. Qed.
   Global Instance heap_mapsto_timeless l q v : TimelessP (l ↦{q} v).
   Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed.
 
   Lemma heap_mapsto_op_eq l q1 q2 v : l ↦{q1} v ★ l ↦{q2} v ⊣⊢ l ↦{q1+q2} v.
   Proof.
-    by rewrite heap_mapsto_eq -auth_own_op op_singleton pair_op dec_agree_idemp.
+    by rewrite heap_mapsto_eq
+      -own_op -auth_frag_op op_singleton pair_op dec_agree_idemp.
   Qed.
 
   Lemma heap_mapsto_op l q1 q2 v1 v2 :
@@ -115,11 +88,10 @@ Section heap.
   Proof.
     destruct (decide (v1 = v2)) as [->|].
     { by rewrite heap_mapsto_op_eq pure_equiv // left_id. }
-    rewrite heap_mapsto_eq -auth_own_op op_singleton pair_op dec_agree_ne //.
     apply (anti_symm (⊢)); last by apply pure_elim_l.
-    rewrite auth_own_valid gmap_validI (forall_elim l) lookup_singleton.
-    rewrite option_validI prod_validI !discrete_valid /=.
-    by apply pure_elim_r.
+    rewrite heap_mapsto_eq -own_op -auth_frag_op own_valid discrete_valid.
+    eapply pure_elim; [done|]=> /auth_own_valid /=.
+    rewrite op_singleton pair_op dec_agree_ne // singleton_valid. by intros [].
   Qed.
 
   Lemma heap_mapsto_op_1 l q1 q2 v1 v2 :
@@ -140,15 +112,14 @@ Section heap.
     heap_ctx ★ ▷ (∀ l, l ↦ v ={E}=★ Φ (LitV (LitLoc l))) ⊢ WP Alloc e @ E {{ Φ }}.
   Proof.
     iIntros (<-%of_to_val ?) "[#Hinv HΦ]". rewrite /heap_ctx.
-    iVs (auth_empty heap_name) as "Hh".
-    iVs (auth_open with "[Hh]") as (h) "[Hv [Hh Hclose]]"; eauto.
-    rewrite left_id_L /heap_inv. iDestruct "Hv" as %?.
-    iApply wp_alloc_pst. iFrame "Hh". iNext.
-    iIntros (l) "[% Hh] !==>".
-    iVs ("Hclose" $! {[ l := (1%Qp, DecAgree v) ]} with "[Hh]").
-    { rewrite -of_heap_insert -(insert_singleton_op h); last by apply of_heap_None.
-      iFrame "Hh". iPureIntro.
-      by apply alloc_unit_singleton_local_update; first apply of_heap_None. }
+    iInv heapN as (σ) ">[Hσ Hh] " "Hclose".
+    iApply wp_alloc_pst. iFrame "Hσ". iNext. iIntros (l) "[% Hσ] !==>".
+    iVs (own_update with "Hh") as "[Hh H]".
+    { apply auth_update_alloc,
+        (alloc_singleton_local_update _ l (1%Qp,DecAgree v));
+        by auto using lookup_to_heap_None. }
+    iVs ("Hclose" with "[Hσ Hh]") as "_".
+    { iNext. iExists (<[l:=v]> σ). rewrite to_heap_insert. by iFrame. }
     iApply "HΦ". by rewrite heap_mapsto_eq /heap_mapsto_def.
   Qed.
 
@@ -157,14 +128,13 @@ Section heap.
     heap_ctx ★ ▷ l ↦{q} v ★ ▷ (l ↦{q} v ={E}=★ Φ v)
     ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
   Proof.
-    iIntros (?) "[#Hinv [Hl HΦ]]".
+    iIntros (?) "[#Hinv [>Hl HΦ]]".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
-    iVs (auth_open with "[Hl]") as (h) "[% [Hl Hclose]]"; eauto.
-    rewrite /heap_inv.
-    iApply (wp_load_pst _ (<[l:=v]>(of_heap h)));first by rewrite lookup_insert.
-    rewrite of_heap_singleton_op //. iFrame "Hl".
-    iIntros "!> Hown !==>". iVs ("Hclose" with "* [Hown]").
-    { iSplit; first done. rewrite of_heap_singleton_op //. by iFrame. }
+    iInv heapN as (σ) ">[Hσ Hh] " "Hclose".
+    iDestruct (own_valid_2 with "[$Hh $Hl]") as %[??]%auth_valid_discrete_2.
+    iApply (wp_load_pst _ σ); first eauto using heap_singleton_included.
+    iIntros "{$Hσ} !> Hσ !==>". iVs ("Hclose" with "[Hσ Hh]") as "_".
+    { iNext. iExists σ. by iFrame. }
     by iApply "HΦ".
   Qed.
 
@@ -173,17 +143,18 @@ Section heap.
     heap_ctx ★ ▷ l ↦ v' ★ ▷ (l ↦ v ={E}=★ Φ (LitV LitUnit))
     ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
   Proof.
-    iIntros (<-%of_to_val ?) "[#Hinv [Hl HΦ]]".
+    iIntros (<-%of_to_val ?) "[#Hinv [>Hl HΦ]]".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
-    iVs (auth_open with "[Hl]") as (h) "[% [Hl Hclose]]"; eauto.
-    rewrite /heap_inv.
-    iApply (wp_store_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
-    rewrite insert_insert !of_heap_singleton_op; eauto. iFrame "Hl".
-    iIntros "!> Hl !==>".
-    iVs ("Hclose" $! {[l := (1%Qp, DecAgree v)]} with "[Hl]").
-    { iSplit.
-      - iPureIntro; by apply singleton_local_update, exclusive_local_update.
-      - rewrite of_heap_singleton_op //; eauto. }
+    iInv heapN as (σ) ">[Hσ Hh] " "Hclose".
+    iDestruct (own_valid_2 with "[$Hh $Hl]") as %[??]%auth_valid_discrete_2.
+    iApply (wp_store_pst _ σ); first eauto using heap_singleton_included.
+    iIntros "{$Hσ} !> Hσ !==>".
+    iVs (own_update_2 with "[$Hh $Hl]") as "[Hh Hl]".
+    { eapply auth_update, singleton_local_update,
+        (exclusive_local_update _ (1%Qp, DecAgree v)); last done.
+      by eapply heap_singleton_included'. }
+    iVs ("Hclose" with "[Hσ Hh]") as "_".
+    { iNext. iExists (<[l:=v]>σ). rewrite to_heap_insert. iFrame. }
     by iApply "HΦ".
   Qed.
 
@@ -192,14 +163,13 @@ Section heap.
     heap_ctx ★ ▷ l ↦{q} v' ★ ▷ (l ↦{q} v' ={E}=★ Φ (LitV (LitBool false)))
     ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
   Proof.
-    iIntros (<-%of_to_val <-%of_to_val ??) "[#Hh [Hl HΦ]]".
+    iIntros (<-%of_to_val <-%of_to_val ??) "[#Hinv [>Hl HΦ]]".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
-    iVs (auth_open with "[Hl]") as (h) "[% [Hl Hclose]]"; eauto.
-    rewrite /heap_inv.
-    iApply (wp_cas_fail_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
-    rewrite of_heap_singleton_op //. iFrame "Hl".
-    iIntros "!> Hown !==>". iVs ("Hclose" with "* [Hown]").
-    { iSplit; first done. rewrite of_heap_singleton_op //. by iFrame. }
+    iInv heapN as (σ) ">[Hσ Hh] " "Hclose".
+    iDestruct (own_valid_2 with "[$Hh $Hl]") as %[??]%auth_valid_discrete_2.
+    iApply (wp_cas_fail_pst _ σ); [eauto using heap_singleton_included|done|].
+    iIntros "{$Hσ} !> Hσ !==>". iVs ("Hclose" with "[Hσ Hh]") as "_".
+    { iNext. iExists σ. by iFrame. }
     by iApply "HΦ".
   Qed.
 
@@ -208,17 +178,18 @@ Section heap.
     heap_ctx ★ ▷ l ↦ v1 ★ ▷ (l ↦ v2 ={E}=★ Φ (LitV (LitBool true)))
     ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
   Proof.
-    iIntros (<-%of_to_val <-%of_to_val ?) "[#Hh [Hl HΦ]]".
+    iIntros (<-%of_to_val <-%of_to_val ?) "[#Hinv [>Hl HΦ]]".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
-    iVs (auth_open with "[Hl]") as (h) "[% [Hl Hclose]]"; eauto.
-    rewrite /heap_inv.
-    iApply (wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))); rewrite ?lookup_insert //.
-    rewrite insert_insert !of_heap_singleton_op; eauto. iFrame "Hl".
-    iIntros "!> Hl !==>".
-    iVs ("Hclose" $! {[l := (1%Qp, DecAgree v2)]} with "[Hl]").
-    { iSplit.
-      - iPureIntro; by apply singleton_local_update, exclusive_local_update.
-      - rewrite of_heap_singleton_op //; eauto. }
+    iInv heapN as (σ) ">[Hσ Hh] " "Hclose".
+    iDestruct (own_valid_2 with "[$Hh $Hl]") as %[??]%auth_valid_discrete_2.
+    iApply (wp_cas_suc_pst _ σ); first eauto using heap_singleton_included.
+    iIntros "{$Hσ} !> Hσ !==>".
+    iVs (own_update_2 with "[$Hh $Hl]") as "[Hh Hl]".
+    { eapply auth_update, singleton_local_update,
+        (exclusive_local_update _ (1%Qp, DecAgree v2)); last done.
+      by eapply heap_singleton_included'. }
+    iVs ("Hclose" with "[Hσ Hh]") as "_".
+    { iNext. iExists (<[l:=v2]>σ). rewrite to_heap_insert. iFrame. }
     by iApply "HΦ".
   Qed.
 End heap.

heap_lang/lib/counter.v

 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import tactics.
-From iris.program_logic Require Import auth.
+From iris.algebra Require Import auth.
 From iris.heap_lang Require Import proofmode notation.
 
 Definition newcounter : val := λ: <>, ref #0.
@@ -13,20 +13,21 @@ Definition read : val := λ: "l", !"l".
 Global Opaque newcounter inc get.
 
 (** The CMRA we need. *)
-Class counterG Σ := CounterG { counter_tokG :> authG Σ mnatUR }.
-Definition counterΣ : gFunctors := #[authΣ mnatUR].
+Class counterG Σ := CounterG { counter_tokG :> inG Σ (authR mnatUR) }.
+Definition counterΣ : gFunctors := #[GFunctor (constRF (authR mnatUR))].
 
 Instance subG_counterΣ {Σ} : subG counterΣ Σ → counterG Σ.
-Proof. intros [? _]%subG_inv. split; apply _. Qed.
+Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
 
 Section proof.
 Context `{!heapG Σ, !counterG Σ} (N : namespace).
 
-Definition counter_inv (l : loc) (n : mnat) : iProp Σ := (l ↦ #n)%I.
+Definition counter_inv (γ : gname) (l : loc) : iProp Σ :=
+  (∃ n, own γ (● (n : mnat)) ★ l ↦ #n)%I.
 
 Definition counter (l : loc) (n : nat) : iProp Σ :=
   (∃ γ, heapN ⊥ N ∧ heap_ctx ∧
-        auth_ctx γ N (counter_inv l) ∧ auth_own γ (n:mnat))%I.
+        inv N (counter_inv γ l) ∧ own γ (◯ (n : mnat)))%I.
 
 (** The main proofs. *)
 Global Instance counter_persistent l n : PersistentP (counter l n).
@@ -37,35 +38,33 @@ Lemma newcounter_spec (R : iProp Σ) Φ :
   heap_ctx ★ (∀ l, counter l 0 -★ Φ #l) ⊢ WP newcounter #() {{ Φ }}.
 Proof.
   iIntros (?) "[#Hh HΦ]". rewrite /newcounter /=. wp_seq. wp_alloc l as "Hl".
-  iVs (auth_alloc (counter_inv l) N _ (O:mnat) with "[Hl]")
-    as (γ) "[#? Hγ]"; try by auto.
+  iVs (own_alloc (● (O:mnat) ⋅ ◯ (O:mnat))) as (γ) "[Hγ Hγ']"; first done.
+  iVs (inv_alloc N _ (counter_inv γ l) with "[Hl Hγ]").
+  { iNext. iExists 0%nat. by iFrame. }
   iVsIntro. iApply "HΦ". rewrite /counter; eauto 10.
 Qed.
 
-Lemma inc_spec l j (Φ : val → iProp Σ) :
-  counter l j ★ (counter l (S j) -★ Φ #()) ⊢ WP inc #l {{ Φ }}.
+Lemma inc_spec l n (Φ : val → iProp Σ) :
+  counter l n ★ (counter l (S n) -★ Φ #()) ⊢ WP inc #l {{ Φ }}.
 Proof.
   iIntros "[Hl HΦ]". iLöb as "IH". wp_rec.
-  iDestruct "Hl" as (γ) "(% & #? & #Hγ & Hγf)".
-  wp_bind (! _)%E.
-  iVs (auth_open (counter_inv l) with "[Hγf]") as (j') "(% & Hl & Hclose)"; auto.
-  rewrite {2}/counter_inv.
-  wp_load. iVs ("Hclose" $! j with "[Hl]") as "Hγf"; eauto.
-  iVsIntro. wp_let; wp_op. wp_bind (CAS _ _ _).
-  iVs (auth_open (counter_inv l) with "[Hγf]") as (j'') "(% & Hl & Hclose)"; auto.
-  rewrite {2}/counter_inv.
-  destruct (decide (j `max` j'' = j `max` j')) as [Hj|Hj].
-  - wp_cas_suc; first (by do 3 f_equal).
-    iVs ("Hclose" $! (1 + j `max` j')%nat with "[Hl]") as "Hγf".
-    { iSplit; [iPureIntro|iNext].
-      { apply mnat_local_update. abstract lia. }
-      rewrite {2}/counter_inv !mnat_op_max (Nat.max_l (S _)); last abstract lia.
-      by rewrite Nat2Z.inj_succ -Z.add_1_l. }
-    iVsIntro. wp_if.
-    iVsIntro; iApply "HΦ"; iExists γ; repeat iSplit; eauto.
-    iApply (auth_own_mono with "Hγf"). apply mnat_included. abstract lia.
-  - wp_cas_fail; first (rewrite !mnat_op_max; by intros [= ?%Nat2Z.inj]).
-    iVs ("Hclose" $! j with "[Hl]") as "Hγf"; eauto.
+  iDestruct "Hl" as (γ) "(% & #? & #Hinv & Hγf)".
+  wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]" "Hclose".
+  wp_load. iVs ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
+  iVsIntro. wp_let. wp_op.
+  wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]" "Hclose".
+  destruct (decide (c' = c)) as [->|].
+  - iDestruct (own_valid_2 with "[$Hγ $Hγf]")
+      as %[?%mnat_included _]%auth_valid_discrete_2.
+    iVs (own_update_2 with "[$Hγ $Hγf]") as "[Hγ Hγf]".
+    { apply auth_update, (mnat_local_update _ _ (S c)); auto. } 
+    wp_cas_suc. iVs ("Hclose" with "[Hl Hγ]") as "_".
+    { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
+    iVsIntro. wp_if. iApply "HΦ"; iExists γ; repeat iSplit; eauto.
+    iApply (own_mono with "Hγf"). apply: auth_frag_mono.
+    by apply mnat_included, le_n_S.
+  - wp_cas_fail; first (by intros [= ?%Nat2Z.inj]).
+    iVs ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
     iVsIntro. wp_if. iApply ("IH" with "[Hγf] HΦ"). rewrite {3}/counter; eauto 10.
 Qed.
 
@@ -73,15 +72,13 @@ Lemma read_spec l j (Φ : val → iProp Σ) :
   counter l j ★ (∀ i, ■ (j ≤ i)%nat → counter l i -★ Φ #i)
   ⊢ WP read #l {{ Φ }}.
 Proof.
-  iIntros "[Hc HΦ]". iDestruct "Hc" as (γ) "(% & #? & #Hγ & Hγf)".
-  rewrite /read /=. wp_let.
-  iVs (auth_open (counter_inv l) with "[Hγf]") as (j') "(% & Hl & Hclose)"; auto.
-  wp_load.
-  iVs ("Hclose" $! (j `max` j') with "[Hl]") as "Hγf".
-  { iSplit; [iPureIntro|iNext].
-    { apply mnat_local_update; abstract lia. }
-    by rewrite !mnat_op_max -Nat.max_assoc Nat.max_idempotent. }
-  iVsIntro. rewrite !mnat_op_max.
-  iApply ("HΦ" with "[%]"); first abstract lia. rewrite /counter; eauto 10.
+  iIntros "[Hc HΦ]". iDestruct "Hc" as (γ) "(% & #? & #Hinv & Hγf)".
+  rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
+  iDestruct (own_valid_2 with "[$Hγ $Hγf]")
+    as %[?%mnat_included _]%auth_valid_discrete_2.
+  iVs (own_update_2 with "[$Hγ $Hγf]") as "[Hγ Hγf]".
+  { apply auth_update, (mnat_local_update _ _ c); auto. }
+  iVs ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
+  iApply ("HΦ" with "[%]"); rewrite /counter; eauto 10.
 Qed.
 End proof.

heap_lang/lib/ticket_lock.v

@@ -101,8 +101,7 @@ Section proof.
         iVsIntro. wp_let. wp_op=>[_|[]] //.
         wp_if. iVsIntro.
         iApply ("HΦ" with "[-HR] HR"). rewrite /locked; eauto.
-      + iExFalso. iCombine "Ht" "Haown" as "Haown".
-        iDestruct (own_valid with "Haown") as % [_ ?%gset_disj_valid_op].
+      + iDestruct (own_valid_2 with "[$Ht $Haown]") as % [_ ?%gset_disj_valid_op].
         set_solver.
     - iVs ("Hclose" with "[Hlo Hln Ha]").
       { iNext. iExists o, n. by iFrame. }
@@ -123,12 +122,10 @@ Section proof.
     iInv N as (o' n') "(>Hlo' & >Hln' & >Hauth & Haown)" "Hclose".
     destruct (decide (#n' = #n))%V as [[= ->%Nat2Z.inj] | Hneq].
     - wp_cas_suc.
-      iVs (own_update with "Hauth") as "Hauth".
-      { eapply (auth_update_no_frag _ (∅, _)), prod_local_update,
-          (gset_disj_alloc_empty_local_update n); [done|].
-        rewrite elem_of_seq_set. omega. }
-      rewrite pair_op left_id_L. iDestruct "Hauth" as "[Hauth Hofull]".
-      rewrite gset_disj_union; last by apply (seq_set_S_disjoint 0).
+      iVs (own_update with "Hauth") as "[Hauth Hofull]".
+      { eapply auth_update_alloc, prod_local_update_2.
+        eapply (gset_disj_alloc_empty_local_update _ {[ n ]}).
+        apply (seq_set_S_disjoint 0). }
       rewrite -(seq_set_S_union_L 0).
       iVs ("Hclose" with "[Hlo' Hln' Haown Hauth]") as "_".
       { iNext. iExists o', (S n).
@@ -137,7 +134,7 @@ Section proof.
       iApply (wait_loop_spec γ (#lo, #ln)).
       iFrame "HΦ". rewrite /issued; eauto 10.
     - wp_cas_fail.
-      iVs ("Hclose" with "[Hlo' Hln' Hauth Haown]").
+      iVs ("Hclose" with "[Hlo' Hln' Hauth Haown]") as "_".
       { iNext. iExists o', n'. by iFrame. }
       iVsIntro. wp_if. by iApply "IH".
   Qed.
@@ -151,28 +148,20 @@ Section proof.
     rewrite /release. wp_let. wp_proj. wp_proj. wp_bind (! _)%E.
     iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)" "Hclose".
     wp_load.
-    iAssert (o' = o)%I with "[#]" as "%"; subst.
-    { iCombine "Hγo" "Hauth" as "Hγo".
-      by iDestruct (own_valid with "Hγo") (* FIXME: this is horrible *)
-        as %[[[[?|] ?] [=]%leibniz_equiv_iff] ?]%auth_valid_discrete. }
+    iDestruct (own_valid_2 with "[$Hauth $Hγo]") as
+      %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_valid_discrete_2.
     iVs ("Hclose" with "[Hlo Hln Hauth Haown]") as "_".
     { iNext. iExists o, n. by iFrame. }
     iVsIntro. wp_op.
     iInv N as (o' n') "(>Hlo & >Hln & >Hauth & Haown)" "Hclose".
     wp_store.
-    iAssert (o' = o)%I with "[#]" as "%"; subst.
-    { iCombine "Hγo" "Hauth" as "Hγo".
-      by iDestruct (own_valid with "Hγo")
-        as %[[[[?|] ?] [=]%leibniz_equiv_iff] ?]%auth_valid_discrete. }
+    iDestruct (own_valid_2 with "[$Hauth $Hγo]") as
+      %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_valid_discrete_2.
     iDestruct "Haown" as "[[Hγo' _]|?]".
-    { iCombine "Hγo" "Hγo'" as "Hγo".
-      iDestruct (own_valid with "Hγo") as %[[] ?]. }
-    iCombine "Hauth" "Hγo" as "Hauth".
-    iVs (own_update with "Hauth") as "Hauth".
-    { rewrite pair_split_L. apply: (auth_update _ _ (Excl' (S o), _)). (* FIXME: apply is slow *)
-      apply prod_local_update, reflexivity; simpl.
-      by apply option_local_update, exclusive_local_update. }
-    rewrite -pair_split_L. iDestruct "Hauth" as "[Hauth Hγo]".
+    { iDestruct (own_valid_2 with "[$Hγo $Hγo']") as %[[] ?]. }
+    iVs (own_update_2 with "[$Hauth $Hγo]") as "[Hauth Hγo]".
+    { apply auth_update, prod_local_update_1.
+      by apply option_local_update, (exclusive_local_update _ (Excl (S o))). }
     iVs ("Hclose" with "[Hlo Hln Hauth Haown Hγo HR]") as "_"; last auto.
     iNext. iExists (S o), n'.
     rewrite Nat2Z.inj_succ -Z.add_1_r. iFrame. iLeft. by iFrame.

program_logic/auth.v

-From iris.program_logic Require Export invariants.
-From iris.algebra Require Export auth.
-From iris.algebra Require Import gmap.
-From iris.proofmode Require Import tactics.
-Import uPred.
-
-(* The CMRA we need. *)
-Class authG Σ (A : ucmraT) := AuthG {
-  auth_inG :> inG Σ (authR A);
-  auth_discrete :> CMRADiscrete A;
-}.
-Definition authΣ (A : ucmraT) : gFunctors := #[ GFunctor (constRF (authR A)) ].
-
-Instance subG_authΣ Σ A : subG (authΣ A) Σ → CMRADiscrete A → authG Σ A.
-Proof. intros ?%subG_inG ?. by split. Qed.
-
-Section definitions.
-  Context `{irisG Λ Σ, authG Σ A} (γ : gname).
-  Definition auth_own (a : A) : iProp Σ :=
-    own γ (◯ a).
-  Definition auth_inv (φ : A → iProp Σ) : iProp Σ :=
-    (∃ a, own γ (● a) ★ φ a)%I.
-  Definition auth_ctx (N : namespace) (φ : A → iProp Σ) : iProp Σ :=
-    inv N (auth_inv φ).
-
-  Global Instance auth_own_ne n : Proper (dist n ==> dist n) auth_own.
-  Proof. solve_proper. Qed.
-  Global Instance auth_own_proper : Proper ((≡) ==> (⊣⊢)) auth_own.
-  Proof. solve_proper. Qed.
-  Global Instance auth_own_timeless a : TimelessP (auth_own a).
-  Proof. apply _. Qed.
-  Global Instance auth_inv_ne n : 
-    Proper (pointwise_relation A (dist n) ==> dist n) (auth_inv).
-  Proof. solve_proper. Qed.
-  Global Instance auth_ctx_ne n N :
-    Proper (pointwise_relation A (dist n) ==> dist n) (auth_ctx N).
-  Proof. solve_proper. Qed.
-  Global Instance auth_ctx_persistent N φ : PersistentP (auth_ctx N φ).
-  Proof. apply _. Qed.
-End definitions.
-
-Typeclasses Opaque auth_own auth_ctx.
-Instance: Params (@auth_inv) 6.
-Instance: Params (@auth_own) 6.
-Instance: Params (@auth_ctx) 7.
-
-Section auth.
-  Context `{irisG Λ Σ, authG Σ A}.
-  Context (φ : A → iProp Σ) {φ_proper : Proper ((≡) ==> (⊣⊢)) φ}.
-  Implicit Types N : namespace.
-  Implicit Types P Q R : iProp Σ.
-  Implicit Types a b : A.
-  Implicit Types γ : gname.
-
-  Lemma auth_own_op γ a b : auth_own γ (a ⋅ b) ⊣⊢ auth_own γ a ★ auth_own γ b.
-  Proof. by rewrite /auth_own -own_op auth_frag_op. Qed.
-
-  Global Instance from_sep_own_authM γ a b :
-    FromSep (auth_own γ (a ⋅ b)) (auth_own γ a) (auth_own γ b) | 90.
-  Proof. by rewrite /FromSep auth_own_op. Qed.
-
-  Lemma auth_own_mono γ a b : a ≼ b → auth_own γ b ⊢ auth_own γ a.
-  Proof. intros [? ->]. by rewrite auth_own_op sep_elim_l. Qed.
-
-  Global Instance auth_own_persistent γ a :
-    Persistent a → PersistentP (auth_own γ a).
-  Proof. rewrite /auth_own. apply _. Qed.
-
-  Lemma auth_own_valid γ a : auth_own γ a ⊢ ✓ a.
-  Proof. by rewrite /auth_own own_valid auth_validI. Qed.
-
-  Lemma auth_alloc_strong N E a (G : gset gname) :
-    ✓ a → ▷ φ a ={E}=> ∃ γ, ■ (γ ∉ G) ∧ auth_ctx γ N φ ∧ auth_own γ a.
-  Proof.
-    iIntros (?) "Hφ". rewrite /auth_own /auth_ctx.
-    iVs (own_alloc_strong (Auth (Excl' a) a) G) as (γ) "[% Hγ]"; first done.
-    iRevert "Hγ"; rewrite auth_both_op; iIntros "[Hγ Hγ']".
-    iVs (inv_alloc N _ (auth_inv γ φ) with "[-Hγ']").
-    { iNext. iExists a. by iFrame. }
-    iVsIntro; iExists γ. iSplit; first by iPureIntro. by iFrame.
-  Qed.
-
-  Lemma auth_alloc N E a :
-    ✓ a → ▷ φ a ={E}=> ∃ γ, auth_ctx γ N φ ∧ auth_own γ a.
-  Proof.
-    iIntros (?) "Hφ".
-    iVs (auth_alloc_strong N E a ∅ with "Hφ") as (γ) "[_ ?]"; eauto.
-  Qed.
-
-  Lemma auth_empty γ : True =r=> auth_own γ ∅.
-  Proof. by rewrite /auth_own -own_empty. Qed.
-
-  Lemma auth_open E N γ a :
-    nclose N ⊆ E →
-    auth_ctx γ N φ ★ ▷ auth_own γ a ={E,E∖N}=> ∃ af,
-      ■ ✓ (a ⋅ af) ★ ▷ φ (a ⋅ af) ★ ∀ b,
-      ■ (a ~l~> b @ Some af) ★ ▷ φ (b ⋅ af) ={E∖N,E}=★ auth_own γ b.
-  Proof.
-    iIntros (?) "(#? & >Hγf)". rewrite /auth_ctx /auth_own.
-    iInv N as (a') "[>Hγ Hφ]" "Hclose". iCombine "Hγ" "Hγf" as "Hγ".
-    iDestruct (own_valid with "Hγ") as % [[af Ha'] ?]%auth_valid_discrete.
-    simpl in Ha'; rewrite ->(left_id _ _) in Ha'; setoid_subst.
-    iVsIntro. iExists af; iFrame "Hφ"; iSplit; first done.
-    iIntros (b) "[% Hφ]".
-    iVs (own_update with "Hγ") as "[Hγ Hγf]"; first eapply auth_update; eauto.
-    iVs ("Hclose" with "[Hφ Hγ]") as "_"; auto.
-    iNext. iExists (b ⋅ af). by iFrame.
-  Qed.
-End auth.

program_logic/boxes.v

@@ -65,10 +65,8 @@ Lemma box_own_auth_update γ b1 b2 b3 :
   box_own_auth γ (● Excl' b1) ★ box_own_auth γ (◯ Excl' b2)
   =r=> box_own_auth γ (● Excl' b3) ★ box_own_auth γ (◯ Excl' b3).
 Proof.
-  rewrite /box_own_prop -!own_op own_valid_l prod_validI; iIntros "[[Hb _] Hγ]".
-  iDestruct "Hb" as % [[[] [= ->]%leibniz_equiv] ?]%auth_valid_discrete.
-  iApply (own_update with "Hγ"); apply prod_update; simpl; last reflexivity.
-  by apply auth_update_no_frame, option_local_update, exclusive_local_update.
+  rewrite /box_own_auth -!own_op. apply own_update, prod_update; last done.
+  by apply auth_update, option_local_update, exclusive_local_update.
 Qed.
 
 Lemma box_own_agree γ Q1 Q2 :

program_logic/ownership.v

@@ -67,8 +67,8 @@ Proof.
 Qed.
 Lemma ownP_update σ1 σ2 : ownP_auth σ1 ★ ownP σ1 =r=> ownP_auth σ2 ★ ownP σ2.
 Proof.
-  rewrite /ownP -!own_op. by apply own_update, auth_update_no_frame,
-    option_local_update, exclusive_local_update.
+  rewrite /ownP -!own_op.
+  by apply own_update, auth_update, option_local_update, exclusive_local_update.
 Qed.
 
 (* Invariants *)
@@ -161,8 +161,8 @@ Proof.
       as (i & [? HIi%not_elem_of_dom]%not_elem_of_union & ?); eauto. }
   iDestruct "HE" as (X) "[Hi HE]"; iDestruct "Hi" as %(i & -> & HIi & ?).
   iVs (own_update with "Hw") as "[Hw HiP]".
-  { apply (auth_update_no_frag _ {[ i := invariant_unfold P ]}).
-    apply alloc_unit_singleton_local_update; last done.
+  { eapply auth_update_alloc,
+     (alloc_singleton_local_update _ i (invariant_unfold P)); last done.
     by rewrite /= lookup_fmap HIi. }
   iVsIntro; iExists i;  iSplit; [done|]. rewrite /ownI; iFrame "HiP".
   iExists (<[i:=P]>I); iSplitL "Hw".

tests/barrier_client.v

@@ -2,7 +2,6 @@ From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang.lib.barrier Require Import proof.
 From iris.heap_lang Require Import par.
-From iris.program_logic Require Import auth sts saved_prop hoare ownership.
 From iris.heap_lang Require Import adequacy proofmode.
 
 Definition worker (n : Z) : val :=