iris/algebra/dfrac.v

@@ -32,7 +32,18 @@ Inductive dfrac :=
   | DfracDiscarded : dfrac
   | DfracBoth : Qp → dfrac.
 
+(* This notation is intended to be used as a component in other notations that
+   include discardable fractions. The notation provides shorthands for the
+   constructors and the commonly used full fraction. For an example
+   demonstrating how this can be used see the notation in [gen_heap.v]. *)
+Declare Custom Entry dfrac.
+Notation "{ dq }" := (dq) (in custom dfrac at level 1, dq constr).
+Notation "□" := DfracDiscarded (in custom dfrac).
+Notation "{# q }" := (DfracOwn q) (in custom dfrac at level 1, q constr).
+Notation "" := (DfracOwn 1) (in custom dfrac).
+
 Section dfrac.
+  Context {SI : sidx}.
   Canonical Structure dfracO := leibnizO dfrac.
 
   Implicit Types p q : Qp.
@@ -80,7 +91,7 @@ Section dfrac.
     end.
 
   (** When elements are combined, ownership is added together and knowledge of
-     discarded fractions is combined with the max operation. *)
+     discarded fractions is preserved. *)
   Local Instance dfrac_op_instance : Op dfrac := λ dq dp,
     match dq, dp with
     | DfracOwn q, DfracOwn q' => DfracOwn (q + q')
@@ -94,6 +105,14 @@ Section dfrac.
     | DfracBoth q, DfracBoth q' => DfracBoth (q + q')
     end.
 
+  Lemma dfrac_valid dq :
+    ✓ dq ↔ match dq with
+           | DfracOwn q => q ≤ 1
+           | DfracDiscarded => True
+           | DfracBoth q => q < 1
+           end%Qp.
+  Proof. done. Qed.
+
   Lemma dfrac_op_own q p : DfracOwn p ⋅ DfracOwn q = DfracOwn (p + q).
   Proof. done. Qed.
 
@@ -103,7 +122,7 @@ Section dfrac.
 
   Lemma dfrac_own_included q p : DfracOwn q ≼ DfracOwn p ↔ (q < p)%Qp.
   Proof.
-    rewrite Qp_lt_sum. split.
+    rewrite Qp.lt_sum. split.
     - rewrite /included /op /dfrac_op_instance. intros [[o| |?] [= ->]]. by exists o.
     - intros [o ->]. exists (DfracOwn o). by rewrite dfrac_op_own.
   Qed.
@@ -120,18 +139,18 @@ Section dfrac.
     - intros [?| |?] [?| |?] [?| |?];
         rewrite /op /dfrac_op_instance 1?assoc_L 1?assoc_L; done.
     - intros [?| |?] [?| |?];
-        rewrite /op /dfrac_op_instance 1?(comm_L Qp_add); done.
+        rewrite /op /dfrac_op_instance 1?(comm_L Qp.add); done.
     - intros [?| |?] dq; rewrite /pcore /dfrac_pcore_instance; intros [= <-];
         rewrite /op /dfrac_op_instance; done.
     - intros [?| |?] ? [= <-]; done.
     - intros [?| |?] [?| |?] ? [[?| |?] [=]] [= <-]; eexists _; split; try done;
         apply dfrac_discarded_included.
     - intros [q| |q] [q'| |q']; rewrite /op /dfrac_op_instance /valid /dfrac_valid_instance //.
-      + intros. trans (q + q')%Qp; [|done]. apply Qp_le_add_l.
-      + apply Qp_lt_le_incl.
-      + intros. trans (q + q')%Qp; [|by apply Qp_lt_le_incl]. apply Qp_le_add_l.
-      + intros. trans (q + q')%Qp; [|done]. apply Qp_lt_add_l.
-      + intros. trans (q + q')%Qp; [|done]. apply Qp_lt_add_l.
+      + intros. trans (q + q')%Qp; [|done]. apply Qp.le_add_l.
+      + apply Qp.lt_le_incl.
+      + intros. trans (q + q')%Qp; [|by apply Qp.lt_le_incl]. apply Qp.le_add_l.
+      + intros. trans (q + q')%Qp; [|done]. apply Qp.lt_add_l.
+      + intros. trans (q + q')%Qp; [|done]. apply Qp.lt_add_l.
   Qed.
   Canonical Structure dfracR := discreteR dfrac dfrac_ra_mixin.
 
@@ -142,36 +161,38 @@ Section dfrac.
   Proof.
     intros [q| |q];
       rewrite /op /cmra_op -cmra_discrete_valid_iff /valid /cmra_valid //=.
-    - apply Qp_not_add_le_l.
-    - move=> /Qp_lt_le_incl. apply Qp_not_add_le_l.
+    - apply Qp.not_add_le_l.
+    - move=> /Qp.lt_le_incl. apply Qp.not_add_le_l.
   Qed.
 
   Global Instance dfrac_cancelable q : Cancelable (DfracOwn q).
   Proof.
     apply: discrete_cancelable.
     intros [q1| |q1][q2| |q2] _ [=]; simplify_eq/=; try done.
-    - by destruct (Qp_add_id_free q q2).
-    - by destruct (Qp_add_id_free q q1).
+    - by destruct (Qp.add_id_free q q2).
+    - by destruct (Qp.add_id_free q q1).
   Qed.
   Global Instance dfrac_own_id_free q : IdFree (DfracOwn q).
-  Proof. intros [q'| |q'] _ [=]. by apply (Qp_add_id_free q q'). Qed.
+  Proof. intros [q'| |q'] _ [=]. by apply (Qp.add_id_free q q'). Qed.
   Global Instance dfrac_discarded_core_id : CoreId DfracDiscarded.
   Proof. by constructor. Qed.
 
   Lemma dfrac_valid_own p : ✓ DfracOwn p ↔ (p ≤ 1)%Qp.
   Proof. done. Qed.
+  Lemma dfrac_valid_own_1 : ✓ DfracOwn 1.
+  Proof. done. Qed.
 
   Lemma dfrac_valid_own_r dq q : ✓ (dq ⋅ DfracOwn q) → (q < 1)%Qp.
   Proof.
     destruct dq as [q'| |q']; [|done|].
-    - apply Qp_lt_le_trans, Qp_lt_add_r.
-    - intro Hlt. etrans; last apply Hlt. apply Qp_lt_add_r.
+    - apply Qp.lt_le_trans, Qp.lt_add_r.
+    - intro Hlt. etrans; last apply Hlt. apply Qp.lt_add_r.
   Qed.
 
   Lemma dfrac_valid_own_l dq q : ✓ (DfracOwn q ⋅ dq) → (q < 1)%Qp.
-  Proof. rewrite comm. apply dfrac_valid_own_r. Qed.
+  Proof using SI. rewrite comm. apply dfrac_valid_own_r. Qed.
 
-  Lemma dfrac_valid_discarded p : ✓ DfracDiscarded.
+  Lemma dfrac_valid_discarded : ✓ DfracDiscarded.
   Proof. done. Qed.
 
   Lemma dfrac_valid_own_discarded q :
@@ -191,4 +212,21 @@ Section dfrac.
     - apply cmra_valid_op_r.
   Qed.
 
+  Lemma dfrac_undiscard_update : DfracDiscarded ~~>: λ k, ∃ q, k = DfracOwn q.
+  Proof.
+    apply cmra_discrete_updateP. intros [[q'| |q']|].
+    - intros [qd Hqd]%Qp.lt_sum. exists (DfracOwn (qd/2)%Qp).
+      split; first by eexists. apply dfrac_valid_own.
+      rewrite Hqd Qp.add_comm -Qp.add_le_mono_l.
+      by apply Qp.div_le.
+    - intros _. exists (DfracOwn (1/2)); split; first by eexists.
+      by apply dfrac_valid_own_discarded.
+    - intros [qd Hqd]%Qp.lt_sum. exists (DfracOwn (qd/2)%Qp).
+      split; first by eexists. rewrite /= /op /valid /cmra_op /cmra_valid /=.
+      rewrite Hqd Qp.add_comm -Qp.add_lt_mono_l.
+      by apply Qp.div_lt.
+    - intros _. exists (DfracOwn 1); split; first by eexists.
+      by apply dfrac_valid_own.
+  Qed.
+
 End dfrac.

iris/algebra/dyn_reservation_map.v

@@ -42,17 +42,19 @@ Global Instance: Params (@DynReservationMap) 1 := {}.
 Global Instance: Params (@dyn_reservation_map_data_proj) 1 := {}.
 Global Instance: Params (@dyn_reservation_map_token_proj) 1 := {}.
 
-Definition dyn_reservation_map_data {A : cmra} (k : positive) (a : A) : dyn_reservation_map A :=
+Definition dyn_reservation_map_data {SI : sidx} {A : cmra}
+    (k : positive) (a : A) : dyn_reservation_map A :=
   DynReservationMap {[ k := a ]} ε.
-Definition dyn_reservation_map_token {A : cmra} (E : coPset) : dyn_reservation_map A :=
+Definition dyn_reservation_map_token {SI : sidx} {A : cmra}
+    (E : coPset) : dyn_reservation_map A :=
   DynReservationMap ∅ (CoPset E).
-Global Instance: Params (@dyn_reservation_map_data) 2 := {}.
+Global Instance: Params (@dyn_reservation_map_data) 3 := {}.
 
 (** We consruct the OFE and CMRA structure via an isomorphism with
 [reservation_map]. *)
 
 Section ofe.
-  Context {A : ofe}.
+  Context {SI : sidx} {A : ofe}.
   Implicit Types x y : dyn_reservation_map A.
 
   Local Definition to_reservation_map x : reservation_map A :=
@@ -89,29 +91,31 @@ Section ofe.
 
   Global Instance DynReservationMap_discrete a b :
     Discrete a → Discrete b → Discrete (DynReservationMap a b).
-  Proof. intros ?? [??] [??]; split; unfold_leibniz; by eapply discrete. Qed.
+  Proof. intros ?? [??] [??]; split; unfold_leibniz; by eapply discrete_0. Qed.
   Global Instance dyn_reservation_map_ofe_discrete :
     OfeDiscrete A → OfeDiscrete dyn_reservation_mapO.
   Proof. intros ? [??]; apply _. Qed.
 End ofe.
 
-Global Arguments dyn_reservation_mapO : clear implicits.
+Global Arguments dyn_reservation_mapO {_} _.
 
 Section cmra.
-  Context {A : cmra}.
+  Context {SI : sidx} {A : cmra}.
   Implicit Types a b : A.
   Implicit Types x y : dyn_reservation_map A.
   Implicit Types k : positive.
 
-  Global Instance dyn_reservation_map_data_ne i : NonExpansive (@dyn_reservation_map_data A i).
+  Global Instance dyn_reservation_map_data_ne i :
+    NonExpansive (@dyn_reservation_map_data SI A i).
   Proof. intros ? ???. rewrite /dyn_reservation_map_data. solve_proper. Qed.
   Global Instance dyn_reservation_map_data_proper N :
-    Proper ((≡) ==> (≡)) (@dyn_reservation_map_data A N).
+    Proper ((≡) ==> (≡)) (@dyn_reservation_map_data SI A N).
   Proof. solve_proper. Qed.
   Global Instance dyn_reservation_map_data_discrete N a :
     Discrete a → Discrete (dyn_reservation_map_data N a).
   Proof. intros. apply DynReservationMap_discrete; apply _. Qed.
-  Global Instance dyn_reservation_map_token_discrete E : Discrete (@dyn_reservation_map_token A E).
+  Global Instance dyn_reservation_map_token_discrete E :
+    Discrete (@dyn_reservation_map_token SI A E).
   Proof. intros. apply DynReservationMap_discrete; apply _. Qed.
 
   Local Instance dyn_reservation_map_valid_instance : Valid (dyn_reservation_map A) := λ x,
@@ -120,7 +124,7 @@ Section cmra.
       ✓ (dyn_reservation_map_data_proj x) ∧ set_infinite (⊤ ∖ E) ∧
       (* dom (dyn_reservation_map_data_proj x) ⊥ E *)
       (∀ i, dyn_reservation_map_data_proj x !! i = None ∨ i ∉ E)
-    | CoPsetBot => False
+    | CoPsetInvalid => False
     end.
   Global Arguments dyn_reservation_map_valid_instance !_ /.
   Local Instance dyn_reservation_map_validN_instance : ValidN (dyn_reservation_map A) := λ n x,
@@ -129,7 +133,7 @@ Section cmra.
       ✓{n} (dyn_reservation_map_data_proj x) ∧ set_infinite (⊤ ∖ E) ∧
       (* dom (dyn_reservation_map_data_proj x) ⊥ E *)
       (∀ i, dyn_reservation_map_data_proj x !! i = None ∨ i ∉ E)
-    | CoPsetBot => False
+    | CoPsetInvalid => False
     end.
   Global Arguments dyn_reservation_map_validN_instance !_ /.
   Local Instance dyn_reservation_map_pcore_instance : PCore (dyn_reservation_map A) := λ x,
@@ -144,7 +148,7 @@ Section cmra.
                    ✓ (dyn_reservation_map_data_proj x) ∧ set_infinite (⊤ ∖ E) ∧
                    (* dom (dyn_reservation_map_data_proj x) ⊥ E *)
                    ∀ i, dyn_reservation_map_data_proj x !! i = None ∨ i ∉ E
-                 | CoPsetBot => False
+                 | CoPsetInvalid => False
                  end := eq_refl _.
   Definition dyn_reservation_map_validN_eq :
     validN = λ n x, match dyn_reservation_map_token_proj x with
@@ -152,7 +156,7 @@ Section cmra.
                       ✓{n} (dyn_reservation_map_data_proj x) ∧ set_infinite (⊤ ∖ E) ∧
                       (* dom (dyn_reservation_map_data_proj x) ⊥ E *)
                       ∀ i, dyn_reservation_map_data_proj x !! i = None ∨ i ∉ E
-                    | CoPsetBot => False
+                    | CoPsetInvalid => False
                     end := eq_refl _.
 
   Lemma dyn_reservation_map_included x y :
@@ -171,17 +175,18 @@ Section cmra.
 
   Lemma dyn_reservation_map_cmra_mixin : CmraMixin (dyn_reservation_map A).
   Proof.
-    apply (iso_cmra_mixin_restrict from_reservation_map to_reservation_map); try done.
+    apply (iso_cmra_mixin_restrict_validity from_reservation_map to_reservation_map); try done.
     - intros n [m [E|]];
         rewrite dyn_reservation_map_validN_eq reservation_map_validN_eq /=;
         naive_solver.
     - intros n [m1 [E1|]] [m2 [E2|]] [Hm ?]=> // -[?[??]]; split; simplify_eq/=.
       + by rewrite -Hm.
       + split; first done. intros i. by rewrite -(dist_None n) -Hm dist_None.
-    - intros [m [E|]]; rewrite dyn_reservation_map_valid_eq dyn_reservation_map_validN_eq /=
-        ?cmra_valid_validN; naive_solver eauto using O.
-    - intros n [m [E|]]; rewrite dyn_reservation_map_validN_eq /=;
-        naive_solver eauto using cmra_validN_S.
+    - pose 0ᵢ.
+      intros [m [E|]]; rewrite dyn_reservation_map_valid_eq
+        dyn_reservation_map_validN_eq /= ?cmra_valid_validN; naive_solver.
+    - intros n m [r [E|]]; rewrite dyn_reservation_map_validN_eq /=;
+        naive_solver eauto using cmra_validN_le.
     - intros n [m1 [E1|]] [m2 [E2|]]=> //=; rewrite dyn_reservation_map_validN_eq /=.
       rewrite {1}/op /cmra_op /=. case_decide; last done.
       intros [Hm [Hinf Hdisj]]; split; first by eauto using cmra_validN_op_l.
@@ -238,11 +243,13 @@ Section cmra.
   Lemma dyn_reservation_map_data_op k a b :
     dyn_reservation_map_data k (a ⋅ b) = dyn_reservation_map_data k a ⋅ dyn_reservation_map_data k b.
   Proof.
-      by rewrite {2}/op /dyn_reservation_map_op_instance /dyn_reservation_map_data /= singleton_op left_id_L.
+    by rewrite {2}/op /dyn_reservation_map_op_instance
+      /dyn_reservation_map_data /= singleton_op left_id_L.
   Qed.
+
   Lemma dyn_reservation_map_data_mono k a b :
     a ≼ b → dyn_reservation_map_data k a ≼ dyn_reservation_map_data k b.
-  Proof. intros [c ->]. rewrite dyn_reservation_map_data_op. apply cmra_included_l. Qed.
+  Proof. intros [c ->]. by rewrite dyn_reservation_map_data_op. Qed.
   Global Instance dyn_reservation_map_data_is_op k a b1 b2 :
     IsOp a b1 b2 →
     IsOp' (dyn_reservation_map_data k a) (dyn_reservation_map_data k b1) (dyn_reservation_map_data k b2).
@@ -282,10 +289,10 @@ Section cmra.
     intros [Hmap [Hinf Hdisj]].
     (* Pick a fresh set disjoint from the existing tokens [Ef] and map [mf],
        such that both that set [E1] and the remainder [E2] are infinite. *)
-    edestruct (coPset_split_infinite (⊤ ∖ (Ef ∪ dom coPset mf))) as
+    edestruct (coPset_split_infinite (⊤ ∖ (Ef ∪ (gset_to_coPset $ dom mf)))) as
         (E1 & E2 & HEunion & HEdisj & HE1inf & HE2inf).
-    { rewrite -difference_difference_L.
-        by apply difference_infinite, dom_finite. }
+    { rewrite -difference_difference_l_L.
+      by apply difference_infinite, gset_to_coPset_finite. }
     exists (dyn_reservation_map_token E1).
     split; first by apply HQ. clear HQ.
     rewrite dyn_reservation_map_validN_eq /=.
@@ -294,20 +301,20 @@ Section cmra.
     - eapply set_infinite_subseteq, HE2inf. set_solver.
     - intros i. rewrite left_id_L. destruct (Hdisj i) as [?|Hi]; first by left.
       destruct (mf !! i) as [p|] eqn:Hp; last by left.
-      apply (elem_of_dom_2 (D:=coPset)) in Hp. right. set_solver.
+      apply elem_of_dom_2, elem_of_gset_to_coPset in Hp. right. set_solver.
   Qed.
   Lemma dyn_reservation_map_reserve' :
-    ε ~~>: (λ x, ∃ E, set_infinite E ∧ x = dyn_reservation_map_token E).
+    ε ~~>: λ x, ∃ E, set_infinite E ∧ x = dyn_reservation_map_token E.
   Proof. eauto using dyn_reservation_map_reserve. Qed.
 
   Lemma dyn_reservation_map_alloc E k a :
     k ∈ E → ✓ a → dyn_reservation_map_token E ~~> dyn_reservation_map_data k a.
   Proof.
     intros ??. apply cmra_total_update=> n [mf [Ef|]] //.
-    rewrite dyn_reservation_map_validN_eq /= {1}/op /cmra_op /=. case_decide; last done.
-    rewrite left_id_L {1}left_id. intros [Hmf [Hinf Hdisj]]; split; last split.
+    rewrite dyn_reservation_map_validN_eq /= {1}/op {1}/cmra_op /=.
+    case_decide; last done.
+    rewrite !left_id_L. intros [Hmf [Hinf Hdisj]]; split; last split.
     - destruct (Hdisj k) as [Hmfi|]; last set_solver.
-      move: Hmfi. rewrite lookup_op lookup_empty left_id_L=> Hmfi.
       intros j. rewrite lookup_op.
       destruct (decide (k = j)) as [<-|].
       + rewrite Hmfi lookup_singleton right_id_L. by apply cmra_valid_validN.
@@ -315,8 +322,7 @@ Section cmra.
     - eapply set_infinite_subseteq, Hinf. set_solver.
     - intros j. destruct (decide (k = j)); first set_solver.
       rewrite lookup_op lookup_singleton_ne //.
-      destruct (Hdisj j) as [Hmfi|?]; last set_solver.
-      move: Hmfi. rewrite lookup_op lookup_empty; auto.
+      destruct (Hdisj j) as [Hmfi|?]; last set_solver. rewrite Hmfi; auto.
   Qed.
   Lemma dyn_reservation_map_updateP P (Q : dyn_reservation_map A → Prop) k a :
     a ~~>: P →
@@ -346,5 +352,5 @@ Section cmra.
   Qed.
 End cmra.
 
-Global Arguments dyn_reservation_mapR : clear implicits.
-Global Arguments dyn_reservation_mapUR : clear implicits.
+Global Arguments dyn_reservation_mapR {_} _.
+Global Arguments dyn_reservation_mapUR {_} _.

iris/algebra/excl.v

 From iris.algebra Require Export cmra.
 From iris.prelude Require Import options.
 
-Local Arguments validN _ _ _ !_ /.
+Local Arguments validN _ _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 
 Inductive excl (A : Type) :=
   | Excl : A → excl A
-  | ExclBot : excl A.
+  | ExclInvalid : excl A.
 Global Arguments Excl {_} _.
-Global Arguments ExclBot {_}.
+Global Arguments ExclInvalid {_}.
 
 Global Instance: Params (@Excl) 1 := {}.
-Global Instance: Params (@ExclBot) 1 := {}.
+Global Instance: Params (@ExclInvalid) 1 := {}.
 
 Notation excl' A := (option (excl A)).
 Notation Excl' x := (Some (Excl x)).
-Notation ExclBot' := (Some ExclBot).
+Notation ExclInvalid' := (Some ExclInvalid).
 
 Global Instance maybe_Excl {A} : Maybe (@Excl A) := λ x,
   match x with Excl a => Some a | _ => None end.
 
 Section excl.
-Context {A : ofe}.
+Context {SI : sidx} {A : ofe}.
 Implicit Types a b : A.
 Implicit Types x y : excl A.
 
 (* Cofe *)
 Inductive excl_equiv : Equiv (excl A) :=
   | Excl_equiv a b : a ≡ b → Excl a ≡ Excl b
-  | ExclBot_equiv : ExclBot ≡ ExclBot.
+  | ExclInvalid_equiv : ExclInvalid ≡ ExclInvalid.
 Local Existing Instance excl_equiv.
 Inductive excl_dist : Dist (excl A) :=
   | Excl_dist a b n : a ≡{n}≡ b → Excl a ≡{n}≡ Excl b
-  | ExclBot_dist n : ExclBot ≡{n}≡ ExclBot.
+  | ExclInvalid_dist n : ExclInvalid ≡{n}≡ ExclInvalid.
 Local Existing Instance excl_dist.
 
 Global Instance Excl_ne : NonExpansive (@Excl A).
@@ -54,36 +54,36 @@ Canonical Structure exclO : ofe := Ofe (excl A) excl_ofe_mixin.
 
 Global Instance excl_cofe `{!Cofe A} : Cofe exclO.
 Proof.
-  apply (iso_cofe (from_option Excl ExclBot) (maybe Excl)).
+  apply (iso_cofe (from_option Excl ExclInvalid) (maybe Excl)).
   - by intros n [a|] [b|]; split; inversion_clear 1; constructor.
   - by intros []; constructor.
 Qed.
 
 Global Instance excl_ofe_discrete : OfeDiscrete A → OfeDiscrete exclO.
-Proof. by inversion_clear 2; constructor; apply (discrete _). Qed.
+Proof. by inversion_clear 2; constructor; apply (discrete_0 _). Qed.
 Global Instance excl_leibniz : LeibnizEquiv A → LeibnizEquiv (excl A).
 Proof. by destruct 2; f_equal; apply leibniz_equiv. Qed.
 
 Global Instance Excl_discrete a : Discrete a → Discrete (Excl a).
-Proof. by inversion_clear 2; constructor; apply (discrete _). Qed.
-Global Instance ExclBot_discrete : Discrete (@ExclBot A).
+Proof. by inversion_clear 2; constructor; apply (discrete_0 _). Qed.
+Global Instance ExclInvalid_discrete : Discrete (@ExclInvalid A).
 Proof. by inversion_clear 1; constructor. Qed.
 
 (* CMRA *)
 Local Instance excl_valid_instance : Valid (excl A) := λ x,
-  match x with Excl _ => True | ExclBot => False end.
+  match x with Excl _ => True | ExclInvalid => False end.
 Local Instance excl_validN_instance : ValidN (excl A) := λ n x,
-  match x with Excl _ => True | ExclBot => False end.
+  match x with Excl _ => True | ExclInvalid => False end.
 Local Instance excl_pcore_instance : PCore (excl A) := λ _, None.
-Local Instance excl_op_instance : Op (excl A) := λ x y, ExclBot.
+Local Instance excl_op_instance : Op (excl A) := λ x y, ExclInvalid.
 
 Lemma excl_cmra_mixin : CmraMixin (excl A).
 Proof.
   split; try discriminate.
-  - by intros n []; destruct 1; constructor.
+  - by intros [] n; destruct 1; constructor.
   - by destruct 1; intros ?.
-  - intros x; split; [done|]. by move=> /(_ 0).
-  - intros n [?|]; simpl; auto with lia.
+  - intros x; split; [done|]. by move=> /(_ 0ᵢ).
+  - intros n m [?|]; simpl; auto.
   - by intros [?|] [?|] [?|]; constructor.
   - by intros [?|] [?|]; constructor.
   - by intros n [?|] [?|].
@@ -94,6 +94,19 @@ Canonical Structure exclR := Cmra (excl A) excl_cmra_mixin.
 Global Instance excl_cmra_discrete : OfeDiscrete A → CmraDiscrete exclR.
 Proof. split; first apply _. by intros []. Qed.
 
+Lemma excl_included x y : x ≼ y ↔ y = ExclInvalid.
+Proof.
+  split.
+  - destruct x, y; intros [[] Hxy]; by inv Hxy.
+  - intros ->. by exists ExclInvalid.
+Qed.
+Lemma excl_includedN n x y : x ≼{n} y ↔ y = ExclInvalid.
+Proof.
+  split.
+  - destruct x, y; intros [[] Hxy]; by inv Hxy.
+  - intros ->. by exists ExclInvalid.
+Qed.
+
 (** Exclusive *)
 Global Instance excl_exclusive x : Exclusive x.
 Proof. by destruct x; intros n []. Qed.
@@ -112,51 +125,61 @@ Lemma Excl_included a b : Excl' a ≼ Excl' b ↔ a ≡ b.
 Proof.
   split; [|by intros ->]. by intros [[c|] Hb%(inj Some)]; inversion_clear Hb.
 Qed.
+Lemma ExclInvalid_included ea : ea ≼ ExclInvalid.
+Proof. by exists ExclInvalid. Qed.
 End excl.
 
-Global Arguments exclO : clear implicits.
-Global Arguments exclR : clear implicits.
+(* We use a [Hint Extern] with [apply:], instead of [Hint Immediate], to invoke
+  the new unification algorithm. The old unification algorithm sometimes gets
+  confused by going from [ucmra]'s to [cmra]'s and back. *)
+Global Hint Extern 0 (_ ≼ ExclInvalid) => apply: ExclInvalid_included : core.
+
+Global Arguments exclO {_} _.
+Global Arguments exclR {_} _.
 
 (* Functor *)
 Definition excl_map {A B} (f : A → B) (x : excl A) : excl B :=
-  match x with Excl a => Excl (f a) | ExclBot => ExclBot end.
+  match x with Excl a => Excl (f a) | ExclInvalid => ExclInvalid end.
 Lemma excl_map_id {A} (x : excl A) : excl_map id x = x.
 Proof. by destruct x. Qed.
 Lemma excl_map_compose {A B C} (f : A → B) (g : B → C) (x : excl A) :
   excl_map (g ∘ f) x = excl_map g (excl_map f x).
 Proof. by destruct x. Qed.
-Lemma excl_map_ext {A B : ofe} (f g : A → B) x :
+Lemma excl_map_ext {SI : sidx} {A B : ofe} (f g : A → B) x :
   (∀ x, f x ≡ g x) → excl_map f x ≡ excl_map g x.
 Proof. by destruct x; constructor. Qed.
-Global Instance excl_map_ne {A B : ofe} n :
+Global Instance excl_map_ne {SI : sidx} {A B : ofe} n :
   Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@excl_map A B).
 Proof. by intros f f' Hf; destruct 1; constructor; apply Hf. Qed.
-Global Instance excl_map_cmra_morphism {A B : ofe} (f : A → B) :
+Global Instance excl_map_cmra_morphism {SI : sidx} {A B : ofe} (f : A → B) :
   NonExpansive f → CmraMorphism (excl_map f).
 Proof. split; try done; try apply _. by intros n [a|]. Qed.
-Definition exclO_map {A B} (f : A -n> B) : exclO A -n> exclO B :=
+Definition exclO_map {SI : sidx} {A B} (f : A -n> B) : exclO A -n> exclO B :=
   OfeMor (excl_map f).
-Global Instance exclO_map_ne A B : NonExpansive (@exclO_map A B).
+Global Instance exclO_map_ne {SI : sidx} A B : NonExpansive (@exclO_map SI A B).
 Proof. by intros n f f' Hf []; constructor; apply Hf. Qed.
 
-Program Definition exclRF (F : oFunctor) : rFunctor := {|
+Program Definition exclRF {SI : sidx} (F : oFunctor) : rFunctor := {|
   rFunctor_car A _ B _ := (exclR (oFunctor_car F A B));
   rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := exclO_map (oFunctor_map F fg)
 |}.
 Next Obligation.
-  intros F A1 ? A2 ? B1 ? B2 ? n x1 x2 ??. by apply exclO_map_ne, oFunctor_map_ne.
+  intros ? F A1 ? A2 ? B1 ? B2 ? n x1 x2 ??.
+  by apply exclO_map_ne, oFunctor_map_ne.
 Qed.
 Next Obligation.
-  intros F A ? B ? x; simpl. rewrite -{2}(excl_map_id x).
+  intros ? F A ? B ? x; simpl. rewrite -{2}(excl_map_id x).
   apply excl_map_ext=>y. by rewrite oFunctor_map_id.
 Qed.
 Next Obligation.
-  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl. rewrite -excl_map_compose.
+  intros ? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl.
+  rewrite -excl_map_compose.
   apply excl_map_ext=>y; apply oFunctor_map_compose.
 Qed.
 
-Global Instance exclRF_contractive F :
+Global Instance exclRF_contractive {SI : sidx} F :
   oFunctorContractive F → rFunctorContractive (exclRF F).
 Proof.
-  intros A1 ? A2 ? B1 ? B2 ? n x1 x2 ??. by apply exclO_map_ne, oFunctor_map_contractive.
+  intros A1 ? A2 ? B1 ? B2 ? n x1 x2 ??.
+  by apply exclO_map_ne, oFunctor_map_contractive.
 Qed.

iris/algebra/frac.v

@@ -13,6 +13,7 @@ From iris.prelude Require Import options.
 Notation frac := Qp (only parsing).
 
 Section frac.
+  Context {SI : sidx}.
   Canonical Structure fracO := leibnizO frac.
 
   Local Instance frac_valid_instance : Valid frac := λ x, (x ≤ 1)%Qp.
@@ -21,35 +22,37 @@ Section frac.
 
   Lemma frac_valid p : ✓ p ↔ (p ≤ 1)%Qp.
   Proof. done. Qed.
+  Lemma frac_valid_1 : ✓ 1%Qp.
+  Proof. done. Qed.
   Lemma frac_op p q : p ⋅ q = (p + q)%Qp.
   Proof. done. Qed.
   Lemma frac_included p q : p ≼ q ↔ (p < q)%Qp.
-  Proof. by rewrite Qp_lt_sum. Qed.
+  Proof. by rewrite Qp.lt_sum. Qed.
 
   Corollary frac_included_weak p q : p ≼ q → (p ≤ q)%Qp.
-  Proof. rewrite frac_included. apply Qp_lt_le_incl. Qed.
+  Proof. rewrite frac_included. apply Qp.lt_le_incl. Qed.
 
   Definition frac_ra_mixin : RAMixin frac.
   Proof.
     split; try apply _; try done.
     intros p q. rewrite !frac_valid frac_op=> ?.
-    trans (p + q)%Qp; last done. apply Qp_le_add_l.
+    trans (p + q)%Qp; last done. apply Qp.le_add_l.
   Qed.
   Canonical Structure fracR := discreteR frac frac_ra_mixin.
 
   Global Instance frac_cmra_discrete : CmraDiscrete fracR.
   Proof. apply discrete_cmra_discrete. Qed.
   Global Instance frac_full_exclusive : Exclusive 1%Qp.
-  Proof. intros p. apply Qp_not_add_le_l. Qed.
+  Proof. intros p. apply Qp.not_add_le_l. Qed.
   Global Instance frac_cancelable (q : frac) : Cancelable q.
-  Proof. intros n p1 p2 _. apply (inj (Qp_add q)). Qed.
+  Proof. intros n p1 p2 _. apply (inj (Qp.add q)). Qed.
   Global Instance frac_id_free (q : frac) : IdFree q.
-  Proof. intros p _. apply Qp_add_id_free. Qed.
+  Proof. intros p _. apply Qp.add_id_free. Qed.
 
   (* This one has a higher precendence than [is_op_op] so we get a [+] instead
      of an [⋅]. *)
   Global Instance frac_is_op q1 q2 : IsOp (q1 + q2)%Qp q1 q2 | 10.
   Proof. done. Qed.
   Global Instance is_op_frac q : IsOp' q (q/2)%Qp (q/2)%Qp.
-  Proof. by rewrite /IsOp' /IsOp frac_op Qp_div_2. Qed.
+  Proof. by rewrite /IsOp' /IsOp frac_op Qp.div_2. Qed.
 End frac.

iris/algebra/functions.v

@@ -3,17 +3,17 @@ From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates.
 From iris.prelude Require Import options.
 
-Definition discrete_fun_insert `{EqDecision A} {B : A → ofe}
+Definition discrete_fun_insert {SI : sidx} `{!EqDecision A} {B : A → ofe}
     (x : A) (y : B x) (f : discrete_fun B) : discrete_fun B := λ x',
   match decide (x = x') with left H => eq_rect _ B y _ H | right _ => f x' end.
-Global Instance: Params (@discrete_fun_insert) 5 := {}.
+Global Instance: Params (@discrete_fun_insert) 6 := {}.
 
-Definition discrete_fun_singleton `{EqDecision A} {B : A → ucmra}
+Definition discrete_fun_singleton {SI : sidx} `{!EqDecision A} {B : A → ucmra}
   (x : A) (y : B x) : discrete_fun B := discrete_fun_insert x y ε.
-Global Instance: Params (@discrete_fun_singleton) 5 := {}.
+Global Instance: Params (@discrete_fun_singleton) 6 := {}.
 
 Section ofe.
-  Context `{Heqdec : EqDecision A} {B : A → ofe}.
+  Context {SI : sidx} `{!EqDecision A} {B : A → ofe}.
   Implicit Types x : A.
   Implicit Types f g : discrete_fun B.
 
@@ -52,7 +52,7 @@ Section ofe.
 End ofe.
 
 Section cmra.
-  Context `{EqDecision A} {B : A → ucmra}.
+  Context {SI : sidx} `{!EqDecision A} {B : A → ucmra}.
   Implicit Types x : A.
   Implicit Types f g : discrete_fun B.
 
@@ -86,13 +86,23 @@ Section cmra.
       rewrite ?discrete_fun_lookup_singleton ?discrete_fun_lookup_singleton_ne //.
     by apply ucmra_unit_validN.
   Qed.
+  Lemma discrete_fun_singleton_valid x (y : B x) : ✓ discrete_fun_singleton x y ↔ ✓ y.
+  Proof.
+    by rewrite !cmra_valid_validN; setoid_rewrite discrete_fun_singleton_validN.
+  Qed.
+
+  Lemma discrete_fun_singleton_unit x : discrete_fun_singleton x (ε : B x) ≡ ε.
+  Proof.
+    move=>x'; destruct (decide (x = x')) as [->|];
+      by rewrite ?discrete_fun_lookup_singleton ?discrete_fun_lookup_singleton_ne.
+  Qed.
 
   Lemma discrete_fun_singleton_core x (y : B x) :
     core (discrete_fun_singleton x y) ≡ discrete_fun_singleton x (core y).
   Proof.
     move=>x'; destruct (decide (x = x')) as [->|];
       by rewrite discrete_fun_lookup_core ?discrete_fun_lookup_singleton
-      ?discrete_fun_lookup_singleton_ne // (core_id_core ∅).
+      ?discrete_fun_lookup_singleton_ne // (core_id_core _).
   Qed.
 
   Global Instance discrete_fun_singleton_core_id x (y : B x) :
@@ -150,7 +160,7 @@ Section cmra.
     exists (discrete_fun_singleton x y2); split; [by apply HQ|].
     intros x'; destruct (decide (x' = x)) as [->|].
     - by rewrite discrete_fun_lookup_op discrete_fun_lookup_singleton.
-    - rewrite discrete_fun_lookup_op discrete_fun_lookup_singleton_ne //. apply Hg.
+    - rewrite discrete_fun_lookup_op discrete_fun_lookup_singleton_ne //; by apply Hg.
   Qed.
   Lemma discrete_fun_singleton_updateP_empty' x (P : B x → Prop) :
     ε ~~>: P → ε ~~>: λ g, ∃ y2, g = discrete_fun_singleton x y2 ∧ P y2.
@@ -161,4 +171,23 @@ Section cmra.
     rewrite !cmra_update_updateP;
       eauto using discrete_fun_singleton_updateP_empty with subst.
   Qed.
+
+  Lemma discrete_fun_updateP `{!Finite A} f P Q :
+    (∀ a, f a ~~>: P a) → (∀ f', (∀ a, P a (f' a)) → Q f') → f ~~>: Q.
+  Proof.
+    repeat setoid_rewrite cmra_total_updateP. intros Hf HP n h Hh.
+    destruct (finite_choice
+      (λ a y, P a y ∧ ✓{n} (y ⋅ (h a)))) as [f' Hf']; first naive_solver.
+    naive_solver.
+  Qed.
+  Lemma discrete_fun_updateP' `{!Finite A} f P :
+    (∀ a, f a ~~>: P a) → f ~~>: λ f', ∀ a, P a (f' a).
+  Proof. eauto using discrete_fun_updateP. Qed.
+
+  Lemma discrete_fun_update f g :
+    (∀ a, f a ~~> g a) → f ~~> g.
+  Proof.
+    repeat setoid_rewrite cmra_total_update.
+    intros Hfg n h Hh a. apply (Hfg a), Hh.
+  Qed.
 End cmra.

iris/algebra/gmap.v

 From stdpp Require Export list gmap.
 From iris.algebra Require Export list cmra.
+From iris.algebra Require Import gset.
 From iris.algebra Require Import updates local_updates proofmode_classes big_op.
 From iris.prelude Require Import options.
 
 Section ofe.
-Context `{Countable K} {A : ofe}.
+Context {SI : sidx} `{Countable K} {A : ofe}.
 Implicit Types m : gmap K A.
 Implicit Types i : K.
 
@@ -20,25 +21,46 @@ Proof.
     + by intros m k.
     + by intros m1 m2 ? k.
     + by intros m1 m2 m3 ?? k; trans (m2 !! k).
-  - by intros n m1 m2 ? k; apply dist_S.
+  - intros n n' m1 m2 ? k ?. by eapply dist_le.
 Qed.
 Canonical Structure gmapO : ofe := Ofe (gmap K A) gmap_ofe_mixin.
 
-Program Definition gmap_chain (c : chain gmapO)
-  (k : K) : chain (optionO A) := {| chain_car n := c n !! k |}.
-Next Obligation. by intros c k n i ?; apply (chain_cauchy c). Qed.
-Definition gmap_compl `{Cofe A} : Compl gmapO := λ c,
-  map_imap (λ i _, compl (gmap_chain c i)) (c 0).
-Global Program Instance gmap_cofe `{Cofe A} : Cofe gmapO :=
-  {| compl := gmap_compl |}.
+Program Definition gmap_chain (c : chain gmapO) (k : K) : chain (optionO A) :=
+  {| chain_car n :=  c n !! k |}.
+Next Obligation. intros c k n p Hp. by apply c. Qed.
+Program Definition gmap_bchain {n} (c : bchain gmapO n)
+    (k : K) : bchain (optionO A) n :=
+  {| bchain_car p Hp := c p Hp !! k |}.
+Next Obligation. intros n c k p γ Hpγ Hp Hγ; by apply c. Qed.
+
+Definition gmap_compl `{!Cofe A} : Compl gmapO := λ c,
+  map_imap (λ i _, compl (gmap_chain c i)) (c 0ᵢ).
+Definition gmap_lbcompl `{!Cofe A} : LBCompl gmapO := λ n Hn c,
+  map_imap (λ i _, lbcompl Hn (gmap_bchain c i)) (c _ (SIdx.limit_lt_0 _ Hn)).
+
+Global Program Instance gmap_cofe `{!Cofe A} : Cofe gmapO :=
+  {| compl := gmap_compl; lbcompl := gmap_lbcompl |}.
 Next Obligation.
-  intros ? n c k. rewrite /compl /gmap_compl map_lookup_imap.
-  feed inversion (λ H, chain_cauchy c 0 n H k);simplify_option_eq;auto with lia.
-  by rewrite conv_compl /=; apply reflexive_eq.
+  intros ? n c k. rewrite /gmap_compl map_lookup_imap.
+  oinversion (λ H, chain_cauchy c 0ᵢ n H k); simplify_option_eq;
+    [apply SIdx.le_0_l| |done].
+  rewrite conv_compl /=. by apply reflexive_eq.
+Qed.
+Next Obligation.
+  intros ? n Hn c p Hp k. rewrite /lbcompl /gmap_lbcompl.
+  rewrite map_lookup_imap.
+  oinversion (bchain_cauchy _ c _ p (SIdx.limit_lt_0 _ Hn) Hp _ k);
+    simplify_option_eq; [apply SIdx.le_0_l| |done].
+  rewrite (conv_lbcompl _ _ Hp) /=. by apply reflexive_eq.
+Qed.
+Next Obligation.
+  intros ? n Hn c1 c2 p Hc k. rewrite /gmap_lbcompl !map_lookup_imap.
+  oinversion (Hc _ (SIdx.limit_lt_0 _ Hn) k); simpl; eauto.
+  apply lbcompl_ne=> ??. apply Hc.
 Qed.
 
 Global Instance gmap_ofe_discrete : OfeDiscrete A → OfeDiscrete gmapO.
-Proof. intros ? m m' ? i. by apply (discrete _). Qed.
+Proof. intros ? m m' ? i. by apply (discrete_0 _). Qed.
 (* why doesn't this go automatic? *)
 Global Instance gmapO_leibniz: LeibnizEquiv A → LeibnizEquiv gmapO.
 Proof. intros; change (LeibnizEquiv (gmap K A)); apply _. Qed.
@@ -77,9 +99,9 @@ Qed.
 Global Instance gmap_lookup_discrete m i : Discrete m → Discrete (m !! i).
 Proof.
   intros ? [x|] Hx; [|by symmetry; apply: discrete].
-  assert (m ≡{0}≡ <[i:=x]> m)
+  assert (m ≡{0ᵢ}≡ <[i:=x]> m)
     by (by symmetry in Hx; inversion Hx; ofe_subst; rewrite insert_id).
-  by rewrite (discrete m (<[i:=x]>m)) // lookup_insert.
+  by rewrite (discrete_0 m (<[i:=x]>m)) // lookup_insert.
 Qed.
 Global Instance gmap_insert_discrete m i x :
   Discrete x → Discrete m → Discrete (<[i:=x]>m).
@@ -89,42 +111,46 @@ Proof.
   by apply: discrete; rewrite -Hm lookup_insert_ne.
 Qed.
 Global Instance gmap_singleton_discrete i x :
-  Discrete x → Discrete ({[ i := x ]} : gmap K A) := _.
+  Discrete x → Discrete ({[ i := x ]} : gmap K A).
+Proof. rewrite /singletonM /map_singleton. apply _. Qed.
 Lemma insert_idN n m i x :
   m !! i ≡{n}≡ Some x → <[i:=x]>m ≡{n}≡ m.
 Proof. intros (y'&?&->)%dist_Some_inv_r'. by rewrite insert_id. Qed.
 
-(** Internalized properties *)
+Global Instance gmap_dom_ne n :
+  Proper ((≡{n}@{gmap K A}≡) ==> (=)) dom.
+Proof. intros m1 m2 Hm. apply set_eq=> k. by rewrite !elem_of_dom Hm. Qed.
 End ofe.
 
-Global Instance map_seq_ne {A : ofe} start :
+Global Instance map_seq_ne {SI : sidx} {A : ofe} start :
   NonExpansive (map_seq (M:=gmap nat A) start).
 Proof.
   intros n l1 l2 Hl. revert start.
   induction Hl; intros; simpl; repeat (done || f_equiv).
 Qed.
 
-Global Arguments gmapO _ {_ _} _.
+Global Arguments gmapO {_} _ {_ _} _.
 
-(** Non-expansiveness of higher-order map functions and big-ops *)
-Global Instance merge_ne `{Countable K} {A B C : ofe} n :
-  Proper (((dist (A:=option A) n) ==> (dist (A:=option B) n) ==> (dist (A:=option C) n)) ==>
-   (dist n) ==> (dist n) ==> (dist n)) (merge (M:=gmap K)).
+Global Instance merge_ne {SI : sidx} `{Countable K} {A B C : ofe} n :
+  Proper ((dist (A:=option A) n ==> dist (A:=option B) n ==> dist (A:=option C) n) ==>
+          dist n ==> dist n ==> (≡{n}@{gmap K C}≡)) merge.
 Proof.
   intros ?? Hf ?? Hm1 ?? Hm2 i. rewrite !lookup_merge.
   destruct (Hm1 i), (Hm2 i); try apply Hf; by constructor.
 Qed.
-Global Instance union_with_proper `{Countable K} {A : ofe} n :
-  Proper (((dist n) ==> (dist n) ==> (dist n)) ==>
-          (dist n) ==> (dist n) ==>(dist n)) (union_with (M:=gmap K A)).
+Global Instance union_with_ne {SI : sidx} `{Countable K} {A : ofe} n :
+  Proper ((dist n ==> dist n ==> dist n) ==>
+          dist n ==> dist n ==> dist n) (union_with (M:=gmap K A)).
 Proof.
   intros ?? Hf ?? Hm1 ?? Hm2 i; apply (merge_ne _ _); auto.
   by do 2 destruct 1; first [apply Hf | constructor].
 Qed.
-Global Instance map_fmap_proper `{Countable K} {A B : ofe} (f : A → B) n :
-  Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (fmap (M:=gmap K) f).
+Global Instance map_fmap_ne {SI : sidx} `{Countable K} {A B : ofe} (f : A → B) n :
+  Proper (dist n ==> dist n) f →
+  Proper (dist n ==> (≡{n}@{gmap K B}≡)) (fmap f).
 Proof. intros ? m m' ? k; rewrite !lookup_fmap. by repeat f_equiv. Qed.
-Global Instance map_zip_with_proper `{Countable K} {A B C : ofe} (f : A → B → C) n :
+Global Instance map_zip_with_ne {SI : sidx}
+    `{Countable K} {A B C : ofe} (f : A → B → C) n :
   Proper (dist n ==> dist n ==> dist n) f →
   Proper (dist n ==> dist n ==> dist n) (map_zip_with (M:=gmap K) f).
 Proof.
@@ -132,7 +158,33 @@ Proof.
   destruct 1; destruct 1; repeat f_equiv; constructor || done.
 Qed.
 
-Lemma big_opM_ne_2 `{Monoid M o} `{Countable K} {A : ofe} (f g : K → A → M) m1 m2 n :
+Global Instance gmap_union_ne {SI : sidx} `{Countable K} {A : ofe} :
+  NonExpansive2 (union (A:=gmap K A)).
+Proof. intros n. apply union_with_ne. by constructor. Qed.
+Global Instance gmap_disjoint_ne {SI : sidx} `{Countable K} {A : ofe} n :
+  Proper (dist n ==> dist n ==> iff) (map_disjoint (M:=gmap K) (A:=A)).
+Proof.
+  intros m1 m1' Hm1 m2 m2' Hm2; split;
+    intros Hm i; specialize (Hm i); by destruct (Hm1 i), (Hm2 i).
+Qed.
+
+Lemma gmap_union_dist_eq {SI : sidx} `{Countable K} {A : ofe}
+    (m m1 m2 : gmap K A) n :
+  m ≡{n}≡ m1 ∪ m2 ↔ ∃ m1' m2', m = m1' ∪ m2' ∧ m1' ≡{n}≡ m1 ∧ m2' ≡{n}≡ m2.
+Proof.
+  split; last first.
+  { by intros (m1'&m2'&->&<-&<-). }
+  intros Hm.
+  exists (filter (λ '(l,_), is_Some (m1 !! l)) m),
+    (m2 ∩ m1 ∪ filter (λ '(l,_), is_Some (m2 !! l)) m).
+  split_and!; [apply map_eq|..]; intros k; move: (Hm k);
+    rewrite ?lookup_union ?lookup_intersection !map_lookup_filter;
+    case _ : (m !! k)=> [x|] /=; case _ : (m1 !! k)=> [x1|] /=;
+      case _ : (m2 !! k)=> [x2|] /=; by inversion 1.
+Qed.
+
+Lemma big_opM_ne_2 {SI : sidx} {M: ofe} {o: M → M → M}
+    `{!Monoid o} `{Countable K} {A : ofe} (f g : K → A → M) m1 m2 n :
   m1 ≡{n}≡ m2 →
   (∀ k y1 y2,
     m1 !! k = Some y1 → m2 !! k = Some y2 → y1 ≡{n}≡ y2 → f k y1 ≡{n}≡ g k y2) →
@@ -147,7 +199,7 @@ Qed.
 
 (* CMRA *)
 Section cmra.
-Context `{Countable K} {A : cmra}.
+Context {SI : sidx} `{Countable K} {A : cmra}.
 Implicit Types m : gmap K A.
 
 Local Instance gmap_unit_instance : Unit (gmap K A) := (∅ : gmap K A).
@@ -207,7 +259,7 @@ Proof.
   - intros m; split.
     + by intros ? n i; apply cmra_valid_validN.
     + intros Hm i; apply cmra_valid_validN=> n; apply Hm.
-  - intros n m Hm i; apply cmra_validN_S, Hm.
+  - intros n m Hm i ? ?; eauto using cmra_validN_le.
   - by intros m1 m2 m3 i; rewrite !lookup_op assoc.
   - by intros m1 m2 i; rewrite !lookup_op comm.
   - intros m i. by rewrite lookup_op lookup_core cmra_core_l.
@@ -241,13 +293,18 @@ Proof.
 Qed.
 Canonical Structure gmapUR := Ucmra (gmap K A) gmap_ucmra_mixin.
 
+Global Instance gmap_op_empty_l_L : LeftId (=@{gmap K A}) ∅ op.
+Proof. apply _. Qed.
+Global Instance gmap_op_empty_r : RightId (=@{gmap K A}) ∅ op.
+Proof. apply _. Qed.
+
 End cmra.
 
-Global Arguments gmapR _ {_ _} _.
-Global Arguments gmapUR _ {_ _} _.
+Global Arguments gmapR {_} _ {_ _} _.
+Global Arguments gmapUR {_} _ {_ _} _.
 
 Section properties.
-Context `{Countable K} {A : cmra}.
+Context {SI : sidx} `{Countable K} {A : cmra}.
 Implicit Types m : gmap K A.
 Implicit Types i : K.
 Implicit Types x y : A.
@@ -311,11 +368,15 @@ Global Instance singleton_is_op i a a1 a2 :
   IsOp a a1 a2 → IsOp' ({[ i := a ]} : gmap K A) {[ i := a1 ]} {[ i := a2 ]}.
 Proof. rewrite /IsOp' /IsOp=> ->. by rewrite -singleton_op. Qed.
 
-Global Instance gmap_core_id m : (∀ x : A, CoreId x) → CoreId m.
+Lemma gmap_core_id m : (∀ i x, m !! i = Some x → CoreId x) → CoreId m.
 Proof.
-  intros; apply core_id_total=> i.
-  rewrite lookup_core. apply (core_id_core _).
+  intros Hcore; apply core_id_total=> i.
+  rewrite lookup_core. destruct (m !! i) as [x|] eqn:Hix; rewrite Hix; [|done].
+  by eapply Hcore.
 Qed.
+Global Instance gmap_core_id' m : (∀ x : A, CoreId x) → CoreId m.
+Proof. auto using gmap_core_id. Qed.
+
 Global Instance gmap_singleton_core_id i (x : A) :
   CoreId x → CoreId {[ i := x ]}.
 Proof. intros. by apply core_id_total, singleton_core'. Qed.
@@ -338,8 +399,7 @@ Lemma singleton_included_l m i x :
 Proof.
   split.
   - move=> [m' /(_ i)]; rewrite lookup_op lookup_singleton.
-    exists (x ⋅? m' !! i). rewrite -Some_op_opM.
-    split; first done. apply cmra_included_l.
+    exists (x ⋅? m' !! i). by rewrite -Some_op_opM.
   - intros (y&Hi&[mz Hy]). exists (partial_alter (λ _, mz) i m).
     intros j; destruct (decide (i = j)) as [->|].
     + by rewrite lookup_op lookup_singleton lookup_partial_alter Hi.
@@ -353,16 +413,18 @@ Proof.
   intros (y&?&->%(Some_included_exclusive _)); eauto using lookup_valid_Some.
 Qed.
 Lemma singleton_included i x y :
-  {[ i := x ]} ≼ ({[ i := y ]} : gmap K A) ↔ x ≡ y ∨ x ≼ y.
+  {[ i := x ]} ≼ ({[ i := y ]} : gmap K A) ↔ Some x ≼ Some y.
 Proof.
   rewrite singleton_included_l. split.
-  - intros (y'&Hi&?). rewrite lookup_insert in Hi.
-    apply Some_included. by rewrite Hi.
-  - intros ?. exists y. by rewrite lookup_insert Some_included.
+  - intros (y'&Hi&?). rewrite lookup_insert in Hi. by rewrite Hi.
+  - intros ?. exists y. by rewrite lookup_insert.
 Qed.
-Lemma singleton_mono i x y :
+Lemma singleton_included_total `{!CmraTotal A}  i x y :
+  {[ i := x ]} ≼ ({[ i := y ]} : gmap K A) ↔ x ≼ y.
+Proof. rewrite singleton_included Some_included_total. done. Qed.
+Lemma singleton_included_mono i x y :
   x ≼ y → {[ i := x ]} ≼ ({[ i := y ]} : gmap K A).
-Proof. intros Hincl. apply singleton_included. right. done. Qed.
+Proof. intros Hincl. apply singleton_included, Some_included_mono. done. Qed.
 
 Global Instance singleton_cancelable i x :
   Cancelable (Some x) → Cancelable {[ i := x ]}.
@@ -418,13 +480,31 @@ Proof.
   - move: (Hm j). by rewrite !lookup_op lookup_delete_ne.
 Qed.
 
-Lemma dom_op m1 m2 : dom (gset K) (m1 ⋅ m2) = dom _ m1 ∪ dom _ m2.
+Lemma gmap_op_union m1 m2 : m1 ##ₘ m2 → m1 ⋅ m2 = m1 ∪ m2.
+Proof.
+  intros Hm. apply map_eq=> k. specialize (Hm k).
+  rewrite lookup_op lookup_union. by destruct (m1 !! k), (m2 !! k).
+Qed.
+
+Lemma gmap_op_valid0_disjoint m1 m2 :
+  ✓{0ᵢ} (m1 ⋅ m2) → (∀ k x, m1 !! k = Some x → Exclusive x) → m1 ##ₘ m2.
+Proof.
+  unfold Exclusive. intros Hvalid Hexcl k.
+  specialize (Hvalid k). rewrite lookup_op in Hvalid. specialize (Hexcl k).
+  destruct (m1 !! k), (m2 !! k); [|done..].
+  rewrite -Some_op Some_validN in Hvalid. naive_solver.
+Qed.
+Lemma gmap_op_valid_disjoint m1 m2 :
+  ✓ (m1 ⋅ m2) → (∀ k x, m1 !! k = Some x → Exclusive x) → m1 ##ₘ m2.
+Proof. move=> /cmra_valid_validN /(_ 0ᵢ). apply gmap_op_valid0_disjoint. Qed.
+
+Lemma dom_op m1 m2 : dom (m1 ⋅ m2) = dom m1 ∪ dom m2.
 Proof.
   apply set_eq=> i; rewrite elem_of_union !elem_of_dom.
   unfold is_Some; setoid_rewrite lookup_op.
   destruct (m1 !! i), (m2 !! i); naive_solver.
 Qed.
-Lemma dom_included m1 m2 : m1 ≼ m2 → dom (gset K) m1 ⊆ dom _ m2.
+Lemma dom_included m1 m2 : m1 ≼ m2 → dom m1 ⊆ dom m2.
 Proof.
   rewrite lookup_included=>? i; rewrite !elem_of_dom. by apply is_Some_included.
 Qed.
@@ -439,15 +519,14 @@ Section freshness.
   Proof.
     move=> /(pred_infinite_set I (C:=gset K)) HP ? HQ.
     apply cmra_total_updateP. intros n mf Hm.
-    destruct (HP (dom (gset K) (m ⋅ mf))) as [i [Hi1 Hi2]].
+    destruct (HP (dom (m ⋅ mf))) as [i [Hi1 Hi2]].
     assert (m !! i = None).
-    { eapply (not_elem_of_dom (D:=gset K)). revert Hi2.
+    { eapply not_elem_of_dom. revert Hi2.
       rewrite dom_op not_elem_of_union. naive_solver. }
     exists (<[i:=f i]>m); split.
     - by apply HQ.
     - rewrite insert_singleton_op //.
-      rewrite -assoc -insert_singleton_op;
-        last by eapply (not_elem_of_dom (D:=gset K)).
+      rewrite -assoc -insert_singleton_op; last by eapply not_elem_of_dom.
     apply insert_validN; [apply cmra_valid_validN|]; auto.
   Qed.
   Lemma alloc_updateP_strong (Q : gmap K A → Prop) (I : K → Prop) m x :
@@ -516,16 +595,21 @@ Proof.
     eauto using alloc_unit_singleton_updateP with subst.
 Qed.
 
+Lemma gmap_local_update m1 m2 m1' m2' :
+  (∀ i, (m1 !! i, m2 !! i) ~l~> (m1' !! i, m2' !! i)) →
+  (m1, m2) ~l~> (m1', m2').
+Proof.
+  intros Hupd. apply local_update_unital=> n mf Hmv Hm.
+  apply forall_and_distr=> i. rewrite lookup_op -cmra_opM_fmap_Some.
+  apply Hupd; simpl; first done. by rewrite Hm lookup_op cmra_opM_fmap_Some.
+Qed.
+
 Lemma alloc_local_update m1 m2 i x :
   m1 !! i = None → ✓ x → (m1,m2) ~l~> (<[i:=x]>m1, <[i:=x]>m2).
 Proof.
-  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 //.
+  intros Hi ?. apply gmap_local_update=> j.
+  destruct (decide (i = j)) as [->|]; last by rewrite !lookup_insert_ne.
+  rewrite !lookup_insert Hi. by apply alloc_option_local_update.
 Qed.
 
 Lemma alloc_singleton_local_update m i x :
@@ -537,24 +621,20 @@ Lemma insert_local_update m1 m2 i x y x' y' :
   (x, y) ~l~> (x', y') →
   (m1, m2) ~l~> (<[i:=x']>m1, <[i:=y']>m2).
 Proof.
-  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.
+  intros Hi1 Hi2 Hup. apply gmap_local_update=> j.
+  destruct (decide (i = j)) as [->|]; last by rewrite !lookup_insert_ne.
+  rewrite !lookup_insert Hi1 Hi2. by apply option_local_update.
 Qed.
 
 Lemma singleton_local_update_any m i y x' y' :
   (∀ x, 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).
-  apply local_update_total_valid0=>_ _ /singleton_includedN_l [x0 [/dist_Some_inv_r Hlk0 _]].
-  edestruct Hlk0 as [x [Hlk _]]; [done..|].
-  eapply insert_local_update; [|eapply lookup_insert|]; eauto.
+  intros. apply gmap_local_update=> j.
+  destruct (decide (i = j)) as [->|]; last by rewrite !lookup_insert_ne.
+  rewrite !lookup_singleton lookup_insert.
+  destruct (m !! j); first by eauto using option_local_update.
+  apply local_update_total_valid0=> _ _ /option_includedN; naive_solver.
 Qed.
 
 Lemma singleton_local_update m i x y x' y' :
@@ -569,13 +649,9 @@ Qed.
 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 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.
+  intros Hi. apply gmap_local_update=> j.
+  destruct (decide (i = j)) as [->|]; last by rewrite !lookup_delete_ne.
+  rewrite !lookup_delete Hi. by apply delete_option_local_update.
 Qed.
 
 Lemma delete_singleton_local_update m i x `{!Exclusive x} :
@@ -589,12 +665,9 @@ Lemma delete_local_update_cancelable m1 m2 i mx `{!Cancelable mx} :
   m1 !! i ≡ mx → m2 !! i ≡ mx →
   (m1, m2) ~l~> (delete i m1, delete i m2).
 Proof.
-  intros Hm1i Hm2i. apply local_update_unital=> n mf Hmv Hm; simpl in *.
-  split; [eauto using delete_validN|].
-  intros j. destruct (decide (i = j)) as [->|].
-  - move: (Hm j). rewrite !lookup_op Hm1i Hm2i !lookup_delete. intros Hmx.
-    rewrite (cancelableN mx n (mf !! j) None) ?right_id // -Hmx -Hm1i. apply Hmv.
-  - by rewrite lookup_op !lookup_delete_ne // Hm lookup_op.
+  intros Hi1 Hi2. apply gmap_local_update=> j.
+  destruct (decide (i = j)) as [->|]; last by rewrite !lookup_delete_ne.
+  rewrite !lookup_delete Hi1 Hi2. by apply delete_option_local_update_cancelable.
 Qed.
 
 Lemma delete_singleton_local_update_cancelable m i x `{!Cancelable (Some x)} :
@@ -621,17 +694,32 @@ Proof.
      right order, namely the order in which they appear in map_to_list.  Here,
      we achieve this by unfolding [big_opM] and doing induction over that list
      instead. *)
-  rewrite big_opM_eq /big_opM_def -{2}(list_to_map_to_list m).
+  rewrite big_op.big_opM_unseal /big_op.big_opM_def -{2}(list_to_map_to_list m).
   assert (NoDup (map_to_list m).*1) as Hnodup by apply NoDup_fst_map_to_list.
   revert Hnodup. induction (map_to_list m) as [|[k x] l IH]; csimpl; first done.
   intros [??]%NoDup_cons. rewrite IH //.
   rewrite insert_singleton_op ?not_elem_of_list_to_map_1 //.
 Qed.
 
+Lemma big_opS_gset_to_gmap (X : gset K) (a : A) :
+  ([^op set] x ∈ X, {[ x := a ]}) ≡ gset_to_gmap a X.
+Proof.
+  induction X as [|x X ? IH] using set_ind_L.
+  { rewrite big_opS_empty gset_to_gmap_empty //. }
+  rewrite big_opS_insert //.
+  rewrite gset_to_gmap_union_singleton.
+  rewrite insert_singleton_op; [|by rewrite lookup_gset_to_gmap_None].
+  by rewrite IH.
+Qed.
+
+Lemma big_opS_gset_to_gmap_L `{!LeibnizEquiv A} (X : gset K) (a : A) :
+  ([^op set] x ∈ X, {[ x := a ]}) = gset_to_gmap a X.
+Proof. apply leibniz_equiv, big_opS_gset_to_gmap. Qed.
+
 End properties.
 
 Section unital_properties.
-Context `{Countable K} {A : ucmra}.
+Context {SI : sidx} `{Countable K} {A : ucmra}.
 Implicit Types m : gmap K A.
 Implicit Types i : K.
 Implicit Types x y : A.
@@ -654,75 +742,93 @@ Qed.
 End unital_properties.
 
 (** Functor *)
-Global Instance gmap_fmap_ne `{Countable K} {A B : ofe} (f : A → B) n :
-  Proper (dist n ==> dist n) f → Proper (dist n ==>dist n) (fmap (M:=gmap K) f).
+Global Instance gmap_fmap_ne {SI : sidx} `{Countable K} {A B : ofe} (f : A → B) n :
+  Proper (dist n ==> dist n) f → Proper (dist n ==> dist (A:=gmap K _) n) (fmap f).
 Proof. by intros ? m m' Hm k; rewrite !lookup_fmap; apply option_fmap_ne. Qed.
-Global Instance gmap_fmap_cmra_morphism `{Countable K} {A B : cmra} (f : A → B)
-  `{!CmraMorphism f} : CmraMorphism (fmap f : gmap K A → gmap K B).
+Lemma gmap_fmap_ne_ext {SI : sidx} `{Countable K}
+  {A : Type} {B : ofe} (f1 f2 : A → B) (m : gmap K A) n :
+  (∀ i x, m !! i = Some x → f1 x ≡{n}≡ f2 x) →
+  f1 <$> m ≡{n}≡ f2 <$> m.
+Proof.
+  move => Hf i. rewrite !lookup_fmap.
+  destruct (m !! i) eqn:?; constructor; by eauto.
+Qed.
+
+Global Instance gmap_fmap_cmra_morphism {SI : sidx} `{Countable K} {A B : cmra}
+  (f : A → B) `{!CmraMorphism f} : CmraMorphism (fmap f : gmap K A → gmap K B).
 Proof.
   split; try apply _.
   - by intros n m ? i; rewrite lookup_fmap; apply (cmra_morphism_validN _).
   - intros m. apply Some_proper=>i. rewrite lookup_fmap !lookup_omap lookup_fmap.
-    case: (m!!i)=>//= ?. apply cmra_morphism_pcore, _.
+    case: (m!!i)=> //= ?. apply cmra_morphism_pcore, _.
   - intros m1 m2 i. by rewrite lookup_op !lookup_fmap lookup_op cmra_morphism_op.
 Qed.
-Definition gmapO_map `{Countable K} {A B} (f: A -n> B) :
+Definition gmapO_map {SI : sidx} `{Countable K} {A B: ofe} (f: A -n> B) :
   gmapO K A -n> gmapO K B := OfeMor (fmap f : gmapO K A → gmapO K B).
-Global Instance gmapO_map_ne `{Countable K} {A B} :
-  NonExpansive (@gmapO_map K _ _ A B).
+Global Instance gmapO_map_ne {SI : sidx} `{Countable K} {A B: ofe} :
+  NonExpansive (@gmapO_map _ K _ _ A B).
 Proof.
   intros n f g Hf m k; rewrite /= !lookup_fmap.
   destruct (_ !! k) eqn:?; simpl; constructor; apply Hf.
 Qed.
 
-Program Definition gmapOF K `{Countable K} (F : oFunctor) : oFunctor := {|
+Program Definition gmapOF {SI : sidx} K `{Countable K}
+    (F : oFunctor) : oFunctor := {|
   oFunctor_car A _ B _ := gmapO K (oFunctor_car F A B);
   oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := gmapO_map (oFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros K ?? F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, oFunctor_map_ne.
+  intros ? K ?? F A1 ? A2 ? B1 ? B2 ? n f g Hfg.
+  by apply gmapO_map_ne, oFunctor_map_ne.
 Qed.
 Next Obligation.
-  intros K ?? F A ? B ? x. rewrite /= -{2}(map_fmap_id x).
-  apply map_fmap_equiv_ext=>y ??; apply oFunctor_map_id.
+  intros ? K ?? F A ? B ? m; simpl in *. rewrite /= -{2}(map_fmap_id m).
+  apply: map_fmap_equiv_ext=>y ??; apply oFunctor_map_id.
 Qed.
 Next Obligation.
-  intros K ?? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -map_fmap_compose.
-  apply map_fmap_equiv_ext=>y ??; apply oFunctor_map_compose.
+  intros ? K ?? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' m.
+  rewrite /= -map_fmap_compose.
+  apply: map_fmap_equiv_ext=>y ??; apply oFunctor_map_compose.
 Qed.
-Global Instance gmapOF_contractive K `{Countable K} F :
+Global Instance gmapOF_contractive {SI : sidx} `{Countable K} F :
   oFunctorContractive F → oFunctorContractive (gmapOF K F).
 Proof.
-  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, oFunctor_map_contractive.
+  by intros ? ? A1 ? A2 ? B1 ? B2 ? n f g Hfg;
+    apply gmapO_map_ne, oFunctor_map_contractive.
 Qed.
 
-Program Definition gmapURF K `{Countable K} (F : rFunctor) : urFunctor := {|
+Program Definition gmapURF {SI : sidx} K `{Countable K}
+    (F : rFunctor) : urFunctor := {|
   urFunctor_car A _ B _ := gmapUR K (rFunctor_car F A B);
   urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := gmapO_map (rFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros K ?? F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, rFunctor_map_ne.
+  by intros ? K ?? F A1 ? A2 ? B1 ? B2 ? n f g Hfg;
+    apply gmapO_map_ne, rFunctor_map_ne.
 Qed.
 Next Obligation.
-  intros K ?? F A ? B ? x. rewrite /= -{2}(map_fmap_id x).
-  apply map_fmap_equiv_ext=>y ??; apply rFunctor_map_id.
+  intros ? K ?? F A ? B ? m. rewrite /= -{2}(map_fmap_id m).
+  apply: map_fmap_equiv_ext=> y ??. apply rFunctor_map_id.
 Qed.
 Next Obligation.
-  intros K ?? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -map_fmap_compose.
-  apply map_fmap_equiv_ext=>y ??; apply rFunctor_map_compose.
+  intros ? K ?? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' m.
+  rewrite /= -map_fmap_compose.
+  apply: map_fmap_equiv_ext=> y ??. apply rFunctor_map_compose.
 Qed.
-Global Instance gmapURF_contractive K `{Countable K} F :
+Global Instance gmapURF_contractive {SI : sidx} `{Countable K} F :
   rFunctorContractive F → urFunctorContractive (gmapURF K F).
 Proof.
-  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, rFunctor_map_contractive.
+  intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg;
+    by apply gmapO_map_ne, rFunctor_map_contractive.
 Qed.
 
-Program Definition gmapRF K `{Countable K} (F : rFunctor) : rFunctor := {|
+Program Definition gmapRF {SI : sidx} K `{Countable K}
+    (F : rFunctor) : rFunctor := {|
   rFunctor_car A _ B _ := gmapR K (rFunctor_car F A B);
   rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := gmapO_map (rFunctor_map F fg)
 |}.
-Solve Obligations with apply gmapURF.
+Solve Obligations with apply @gmapURF.
 
-Global Instance gmapRF_contractive K `{Countable K} F :
+Global Instance gmapRF_contractive {SI : sidx} `{Countable K} F :
   rFunctorContractive F → rFunctorContractive (gmapRF K F).
 Proof. apply gmapURF_contractive. Qed.

iris/algebra/gmultiset.v

@@ -5,7 +5,7 @@ From iris.prelude Require Import options.
 
 (* The multiset union CMRA *)
 Section gmultiset.
-  Context `{Countable K}.
+  Context `{Countable K} {SI : sidx}.
   Implicit Types X Y : gmultiset K.
 
   Canonical Structure gmultisetO := discreteO (gmultiset K).
@@ -95,6 +95,6 @@ Section gmultiset.
 
 End gmultiset.
 
-Global Arguments gmultisetO _ {_ _}.
-Global Arguments gmultisetR _ {_ _}.
-Global Arguments gmultisetUR _ {_ _}.
+Global Arguments gmultisetO _ {_ _ _}.
+Global Arguments gmultisetR _ {_ _ _}.
+Global Arguments gmultisetUR _ {_ _ _}.

iris/algebra/gset.v

@@ -5,7 +5,7 @@ From iris.prelude Require Import options.
 
 (* The union CMRA *)
 Section gset.
-  Context `{Countable K}.
+  Context {SI : sidx} `{Countable K}.
   Implicit Types X Y : gset K.
 
   Canonical Structure gsetO := discreteO (gset K).
@@ -41,7 +41,7 @@ Section gset.
   Canonical Structure gsetUR := Ucmra (gset K) gset_ucmra_mixin.
 
   Lemma gset_opM X mY : X ⋅? mY = X ∪ default ∅ mY.
-  Proof. destruct mY; by rewrite /= ?right_id_L. Qed.
+  Proof using SI. destruct mY; by rewrite /= ?right_id_L. Qed.
 
   Lemma gset_update X Y : X ~~> Y.
   Proof. done. Qed.
@@ -64,34 +64,42 @@ Section gset.
     - unfold_leibniz. rewrite big_opS_insert // IH //.
   Qed.
 
+  (** Add support [X ≼ Y] to [set_solver]. (We get support for [⋅] for free
+  because it is definitionally equal to [∪]). *)
+  Global Instance set_unfold_gset_included X Y Q :
+    SetUnfold (X ⊆ Y) Q → SetUnfold (X ≼ Y) Q.
+  Proof. intros [?]; constructor. by rewrite gset_included. Qed.
 End gset.
 
-Global Arguments gsetO _ {_ _}.
-Global Arguments gsetR _ {_ _}.
-Global Arguments gsetUR _ {_ _}.
+Global Arguments gsetO {_} _ {_ _}.
+Global Arguments gsetR {_} _ {_ _}.
+Global Arguments gsetUR {_} _ {_ _}.
 
 (* The disjoint union CMRA *)
 Inductive gset_disj K `{Countable K} :=
   | GSet : gset K → gset_disj K
-  | GSetBot : gset_disj K.
+  | GSetInvalid : gset_disj K.
 Global Arguments GSet {_ _ _} _.
-Global Arguments GSetBot {_ _ _}.
+Global Arguments GSetInvalid {_ _ _}.
 
 Section gset_disj.
-  Context `{Countable K}.
+  Context {SI : sidx} `{Countable K}.
   Local Arguments op _ _ !_ !_ /.
   Local Arguments cmra_op _ !_ !_ /.
   Local Arguments ucmra_op _ !_ !_ /.
 
+  Global Instance GSet_inj : Inj (=@{gset K}) (=) GSet.
+  Proof. intros ???. naive_solver. Qed.
+
   Canonical Structure gset_disjO := leibnizO (gset_disj K).
 
   Local Instance gset_disj_valid_instance : Valid (gset_disj K) := λ X,
-    match X with GSet _ => True | GSetBot => False end.
+    match X with GSet _ => True | GSetInvalid => False end.
   Local Instance gset_disj_unit_instance : Unit (gset_disj K) := GSet ∅.
   Local Instance gset_disj_op_instance : Op (gset_disj K) := λ X Y,
     match X, Y with
-    | GSet X, GSet Y => if decide (X ## Y) then GSet (X ∪ Y) else GSetBot
-    | _, _ => GSetBot
+    | GSet X, GSet Y => if decide (X ## Y) then GSet (X ∪ Y) else GSetInvalid
+    | _, _ => GSetInvalid
     end.
   Local Instance gset_disj_pcore_instance : PCore (gset_disj K) := λ _, Some ε.
 
@@ -142,7 +150,7 @@ Section gset_disj.
     GSet X ~~>: Q.
   Proof.
     intros Hfresh HQ.
-    apply cmra_discrete_updateP=> ? /gset_disj_valid_inv_l [Y [->?]].
+    apply cmra_discrete_total_updateP=> ? /gset_disj_valid_inv_l [Y [->?]].
     destruct (Hfresh (X ∪ Y)) as (i&?&?); first set_solver.
     exists (GSet ({[ i ]} ∪ X)); split.
     - apply HQ; set_solver by eauto.
@@ -229,8 +237,22 @@ Section gset_disj.
     intros. rewrite -{2}(right_id_L _ union Z).
     apply gset_disj_alloc_local_update; set_solver.
   Qed.
+
+  (** Add some basic support for [GSet X = GSet Y], [GSet X ≼ GSet Y], and
+  [✓ (GSet X ⋅ GSet Y)] to [set_solver]. There are probably more cases we could
+  cover (e.g., involving [GSetInvalid], or nesting of [⋅]), but it is not clear
+  these are useful in practice, nor how to handle them effectively. *)
+  Global Instance set_unfold_gset_eq (X Y : gset K) Q :
+    SetUnfold (X = Y) Q → SetUnfold (GSet X = GSet Y) Q.
+  Proof. intros [?]; constructor. by rewrite (inj_iff _). Qed.
+  Global Instance set_unfold_gset_disj_included (X Y : gset K) Q :
+    SetUnfold (X ⊆ Y) Q → SetUnfold (GSet X ≼ GSet Y) Q.
+  Proof. intros [?]; constructor. by rewrite gset_disj_included. Qed.
+  Global Instance set_unfold_gset_disj_valid_op (X Y : gset K) Q :
+    SetUnfold (X ## Y) Q → SetUnfold (✓ (GSet X ⋅ GSet Y)) Q.
+  Proof. intros [?]; constructor. by rewrite gset_disj_valid_op. Qed.
 End gset_disj.
 
-Global Arguments gset_disjO _ {_ _}.
-Global Arguments gset_disjR _ {_ _}.
-Global Arguments gset_disjUR _ {_ _}.
+Global Arguments gset_disjO {_} _ {_ _}.
+Global Arguments gset_disjR {_} _ {_ _}.
+Global Arguments gset_disjUR {_} _ {_ _}.

iris/algebra/lib/dfrac_agree.v

+From iris.algebra Require Export dfrac agree updates local_updates.
+From iris.algebra Require Import proofmode_classes.
+From iris.prelude Require Import options.
+
+Definition dfrac_agreeR {SI : sidx} (A : ofe) : cmra := prodR dfracR (agreeR A).
+
+Definition to_dfrac_agree {SI : sidx} {A : ofe} (d : dfrac) (a : A) : dfrac_agreeR A :=
+  (d, to_agree a).
+Global Instance: Params (@to_dfrac_agree) 3 := {}.
+(** To make it easier to work with the [Qp] version of this, we also provide
+    [to_frac_agree] and appropriate lemmas. *)
+Definition to_frac_agree {SI : sidx} {A : ofe} (q : Qp) (a : A) : dfrac_agreeR A :=
+  to_dfrac_agree (DfracOwn q) a.
+Global Instance: Params (@to_frac_agree) 3 := {}.
+
+Section lemmas.
+  Context {SI : sidx} {A : ofe}.
+  Implicit Types (q : Qp) (d : dfrac) (a : A).
+
+  Global Instance to_dfrac_agree_ne d : NonExpansive (@to_dfrac_agree SI A d).
+  Proof. solve_proper. Qed.
+  Global Instance to_dfrac_agree_proper d :
+    Proper ((≡) ==> (≡)) (@to_dfrac_agree SI A d).
+  Proof. solve_proper. Qed.
+
+  Global Instance to_dfrac_agree_exclusive a :
+    Exclusive (to_dfrac_agree (DfracOwn 1) a).
+  Proof. apply _. Qed.
+  Global Instance to_dfrac_agree_discrete d a : Discrete a → Discrete (to_dfrac_agree d a).
+  Proof. apply _. Qed.
+  Global Instance to_dfrac_agree_injN n :
+    Inj2 (dist n) (dist n) (dist n) (@to_dfrac_agree SI A).
+  Proof. by intros d1 a1 d2 a2 [??%(inj to_agree)]. Qed.
+  Global Instance to_dfrac_agree_inj : Inj2 (≡) (≡) (≡) (@to_dfrac_agree SI A).
+  Proof. by intros d1 a1 d2 a2 [??%(inj to_agree)]. Qed.
+
+  Lemma dfrac_agree_op d1 d2 a :
+    to_dfrac_agree (d1 ⋅ d2) a ≡ to_dfrac_agree d1 a ⋅ to_dfrac_agree d2 a.
+  Proof. rewrite /to_dfrac_agree -pair_op agree_idemp //. Qed.
+  Lemma frac_agree_op q1 q2 a :
+    to_frac_agree (q1 + q2) a ≡ to_frac_agree q1 a ⋅ to_frac_agree q2 a.
+  Proof. rewrite -dfrac_agree_op. done. Qed.
+
+  Lemma dfrac_agree_op_valid d1 a1 d2 a2 :
+    ✓ (to_dfrac_agree d1 a1 ⋅ to_dfrac_agree d2 a2) ↔
+    ✓ (d1 ⋅ d2) ∧ a1 ≡ a2.
+  Proof.
+    rewrite /to_dfrac_agree -pair_op pair_valid to_agree_op_valid. done.
+  Qed.
+  Lemma dfrac_agree_op_valid_L `{!LeibnizEquiv A} d1 a1 d2 a2 :
+    ✓ (to_dfrac_agree d1 a1 ⋅ to_dfrac_agree d2 a2) ↔
+    ✓ (d1 ⋅ d2) ∧ a1 = a2.
+  Proof. unfold_leibniz. apply dfrac_agree_op_valid. Qed.
+  Lemma dfrac_agree_op_validN d1 a1 d2 a2 n :
+    ✓{n} (to_dfrac_agree d1 a1 ⋅ to_dfrac_agree d2 a2) ↔
+    ✓ (d1 ⋅ d2) ∧ a1 ≡{n}≡ a2.
+  Proof.
+    rewrite /to_dfrac_agree -pair_op pair_validN to_agree_op_validN. done.
+  Qed.
+
+  Lemma frac_agree_op_valid q1 a1 q2 a2 :
+    ✓ (to_frac_agree q1 a1 ⋅ to_frac_agree q2 a2) ↔
+    (q1 + q2 ≤ 1)%Qp ∧ a1 ≡ a2.
+  Proof. apply dfrac_agree_op_valid. Qed.
+  Lemma frac_agree_op_valid_L `{!LeibnizEquiv A} q1 a1 q2 a2 :
+    ✓ (to_frac_agree q1 a1 ⋅ to_frac_agree q2 a2) ↔
+    (q1 + q2 ≤ 1)%Qp ∧ a1 = a2.
+  Proof. apply dfrac_agree_op_valid_L. Qed.
+  Lemma frac_agree_op_validN q1 a1 q2 a2 n :
+    ✓{n} (to_frac_agree q1 a1 ⋅ to_frac_agree q2 a2) ↔
+    (q1 + q2 ≤ 1)%Qp ∧ a1 ≡{n}≡ a2.
+  Proof. apply dfrac_agree_op_validN. Qed.
+
+  Lemma dfrac_agree_included d1 a1 d2 a2 :
+    to_dfrac_agree d1 a1 ≼ to_dfrac_agree d2 a2 ↔
+    (d1 ≼ d2) ∧ a1 ≡ a2.
+  Proof. by rewrite pair_included to_agree_included. Qed.
+  Lemma dfrac_agree_included_L `{!LeibnizEquiv A} d1 a1 d2 a2 :
+    to_dfrac_agree d1 a1 ≼ to_dfrac_agree d2 a2 ↔
+    (d1 ≼ d2) ∧ a1 = a2.
+  Proof. unfold_leibniz. apply dfrac_agree_included. Qed.
+  Lemma dfrac_agree_includedN d1 a1 d2 a2 n :
+    to_dfrac_agree d1 a1 ≼{n} to_dfrac_agree d2 a2 ↔
+    (d1 ≼ d2) ∧ a1 ≡{n}≡ a2.
+  Proof.
+    by rewrite pair_includedN -cmra_discrete_included_iff
+               to_agree_includedN.
+  Qed.
+
+  Lemma frac_agree_included q1 a1 q2 a2 :
+    to_frac_agree q1 a1 ≼ to_frac_agree q2 a2 ↔
+    (q1 < q2)%Qp ∧ a1 ≡ a2.
+  Proof. by rewrite dfrac_agree_included dfrac_own_included. Qed.
+  Lemma frac_agree_included_L `{!LeibnizEquiv A} q1 a1 q2 a2 :
+    to_frac_agree q1 a1 ≼ to_frac_agree q2 a2 ↔
+    (q1 < q2)%Qp ∧ a1 = a2.
+  Proof. by rewrite dfrac_agree_included_L dfrac_own_included. Qed.
+  Lemma frac_agree_includedN q1 a1 q2 a2 n :
+    to_frac_agree q1 a1 ≼{n} to_frac_agree q2 a2 ↔
+    (q1 < q2)%Qp ∧ a1 ≡{n}≡ a2.
+  Proof. by rewrite dfrac_agree_includedN dfrac_own_included. Qed.
+
+  (** While [cmra_update_exclusive] takes care of most updates, it is not sufficient
+      for this one since there is no abstraction-preserving way to rewrite
+      [to_dfrac_agree d1 v1 ⋅ to_dfrac_agree d2 v2] into something simpler. *)
+  Lemma dfrac_agree_update_2 d1 d2 a1 a2 a' :
+    d1 ⋅ d2 = DfracOwn 1 →
+    to_dfrac_agree d1 a1 ⋅ to_dfrac_agree d2 a2 ~~>
+    to_dfrac_agree d1 a' ⋅ to_dfrac_agree d2 a'.
+  Proof.
+    intros Hq. rewrite -pair_op Hq.
+    apply cmra_update_exclusive.
+    rewrite dfrac_agree_op_valid Hq //.
+  Qed.
+  Lemma frac_agree_update_2 q1 q2 a1 a2 a' :
+    (q1 + q2 = 1)%Qp →
+    to_frac_agree q1 a1 ⋅ to_frac_agree q2 a2 ~~>
+    to_frac_agree q1 a' ⋅ to_frac_agree q2 a'.
+  Proof. intros Hq. apply dfrac_agree_update_2. rewrite dfrac_op_own Hq //. Qed.
+
+  Lemma dfrac_agree_persist d a :
+    to_dfrac_agree d a ~~> to_dfrac_agree DfracDiscarded a.
+  Proof.
+    rewrite /to_dfrac_agree. apply prod_update; last done.
+    simpl. apply dfrac_discard_update.
+  Qed.
+
+  Lemma dfrac_agree_unpersist a :
+    to_dfrac_agree DfracDiscarded a ~~>: λ k, ∃ q, k = to_dfrac_agree (DfracOwn q) a.
+  Proof.
+    rewrite /to_dfrac_agree. eapply prod_updateP; first apply dfrac_undiscard_update.
+    { by eapply cmra_update_updateP. }
+    naive_solver.
+  Qed.
+
+End lemmas.
+
+Definition dfrac_agreeRF {SI : sidx} (F : oFunctor) : rFunctor :=
+  prodRF (constRF dfracR) (agreeRF F).
+
+Global Instance dfrac_agreeRF_contractive {SI : sidx} F :
+  oFunctorContractive F → rFunctorContractive (dfrac_agreeRF F).
+Proof. apply _. Qed.
+
+Global Typeclasses Opaque to_dfrac_agree.
+(* [to_frac_agree] is deliberately transparent to reuse the [to_dfrac_agree] instances *)

iris/algebra/lib/excl_auth.v

@@ -6,35 +6,37 @@ From iris.prelude Require Import options.
 This is effectively a single "ghost variable" with two views, the frament [◯E a]
 and the authority [●E a]. *)
 
-Definition excl_authR (A : ofe) : cmra :=
+Definition excl_authR {SI : sidx} (A : ofe) : cmra :=
   authR (optionUR (exclR A)).
-Definition excl_authUR (A : ofe) : ucmra :=
+Definition excl_authUR {SI : sidx} (A : ofe) : ucmra :=
   authUR (optionUR (exclR A)).
 
-Definition excl_auth_auth {A : ofe} (a : A) : excl_authR A :=
+Definition excl_auth_auth {SI : sidx} {A : ofe} (a : A) : excl_authR A :=
   ● (Some (Excl a)).
-Definition excl_auth_frag {A : ofe} (a : A) : excl_authR A :=
+Definition excl_auth_frag {SI : sidx} {A : ofe} (a : A) : excl_authR A :=
   ◯ (Some (Excl a)).
 
-Typeclasses Opaque excl_auth_auth excl_auth_frag.
+Global Typeclasses Opaque excl_auth_auth excl_auth_frag.
 
-Global Instance: Params (@excl_auth_auth) 1 := {}.
-Global Instance: Params (@excl_auth_frag) 2 := {}.
+Global Instance: Params (@excl_auth_auth) 2 := {}.
+Global Instance: Params (@excl_auth_frag) 3 := {}.
 
 Notation "●E a" := (excl_auth_auth a) (at level 10).
 Notation "◯E a" := (excl_auth_frag a) (at level 10).
 
 Section excl_auth.
-  Context {A : ofe}.
+  Context {SI : sidx} {A : ofe}.
   Implicit Types a b : A.
 
-  Global Instance excl_auth_auth_ne : NonExpansive (@excl_auth_auth A).
+  Global Instance excl_auth_auth_ne : NonExpansive (@excl_auth_auth SI A).
   Proof. solve_proper. Qed.
-  Global Instance excl_auth_auth_proper : Proper ((≡) ==> (≡)) (@excl_auth_auth A).
+  Global Instance excl_auth_auth_proper :
+    Proper ((≡) ==> (≡)) (@excl_auth_auth SI A).
   Proof. solve_proper. Qed.
-  Global Instance excl_auth_frag_ne : NonExpansive (@excl_auth_frag A).
+  Global Instance excl_auth_frag_ne : NonExpansive (@excl_auth_frag SI A).
   Proof. solve_proper. Qed.
-  Global Instance excl_auth_frag_proper : Proper ((≡) ==> (≡)) (@excl_auth_frag A).
+  Global Instance excl_auth_frag_proper :
+    Proper ((≡) ==> (≡)) (@excl_auth_frag SI A).
   Proof. solve_proper. Qed.
 
   Global Instance excl_auth_auth_discrete a : Discrete a → Discrete (●E a).
@@ -59,9 +61,14 @@ Section excl_auth.
   Lemma excl_auth_agree_L `{!LeibnizEquiv A} a b : ✓ (●E a ⋅ ◯E b) → a = b.
   Proof. intros. by apply leibniz_equiv, excl_auth_agree. Qed.
 
-  Lemma excl_auth_frag_validN_op_1_l n a b : ✓{n} (◯E a ⋅ ◯E b) → False.
+  Lemma excl_auth_auth_op_validN n a b : ✓{n} (●E a ⋅ ●E b) ↔ False.
+  Proof. apply auth_auth_op_validN. Qed.
+  Lemma excl_auth_auth_op_valid a b : ✓ (●E a ⋅ ●E b) ↔ False.
+  Proof. apply auth_auth_op_valid. Qed.
+
+  Lemma excl_auth_frag_op_validN n a b : ✓{n} (◯E a ⋅ ◯E b) ↔ False.
   Proof. by rewrite -auth_frag_op auth_frag_validN. Qed.
-  Lemma excl_auth_frag_valid_op_1_l a b : ✓ (◯E a ⋅ ◯E b) → False.
+  Lemma excl_auth_frag_op_valid a b : ✓ (◯E a ⋅ ◯E b) ↔ False.
   Proof. by rewrite -auth_frag_op auth_frag_valid. Qed.
 
   Lemma excl_auth_update a b a' : ●E a ⋅ ◯E b ~~> ●E a' ⋅ ◯E a'.
@@ -69,3 +76,17 @@ Section excl_auth.
     intros. by apply auth_update, option_local_update, exclusive_local_update.
   Qed.
 End excl_auth.
+
+Definition excl_authURF {SI : sidx} (F : oFunctor) : urFunctor :=
+  authURF (optionURF (exclRF F)).
+
+Global Instance excl_authURF_contractive {SI : sidx} F :
+  oFunctorContractive F → urFunctorContractive (excl_authURF F).
+Proof. apply _. Qed.
+
+Definition excl_authRF {SI : sidx} (F : oFunctor) : rFunctor :=
+  authRF (optionURF (exclRF F)).
+
+Global Instance excl_authRF_contractive {SI : sidx} F :
+  oFunctorContractive F → rFunctorContractive (excl_authRF F).
+Proof. apply _. Qed.

iris/algebra/lib/frac_agree.v

-From iris.algebra Require Export frac agree updates local_updates.
-From iris.algebra Require Import proofmode_classes.
-From iris.prelude Require Import options.
-
-Definition frac_agreeR (A : ofe) : cmra := prodR fracR (agreeR A).
-
-Definition to_frac_agree {A : ofe} (q : frac) (a : A) : frac_agreeR A :=
-  (q, to_agree a).
-
-Section lemmas.
-  Context {A : ofe}.
-  Implicit Types (q : frac) (a : A).
-
-  Global Instance to_frac_agree_ne q : NonExpansive (@to_frac_agree A q).
-  Proof. solve_proper. Qed.
-  Global Instance to_frac_agree_proper q : Proper ((≡) ==> (≡)) (@to_frac_agree A q).
-  Proof. solve_proper. Qed.
-
-  Global Instance to_frac_agree_exclusive a : Exclusive (to_frac_agree 1 a).
-  Proof. apply _. Qed.
-  Global Instance to_frac_discrete a : Discrete a → Discrete (to_frac_agree 1 a).
-  Proof. apply _. Qed.
-  Global Instance to_frac_injN n : Inj2 (dist n) (dist n) (dist n) (@to_frac_agree A).
-  Proof. by intros q1 a1 q2 a2 [??%(inj to_agree)]. Qed.
-  Global Instance to_frac_inj : Inj2 (≡) (≡) (≡) (@to_frac_agree A).
-  Proof. by intros q1 a1 q2 a2 [??%(inj to_agree)]. Qed.
-
-  Lemma frac_agree_op q1 q2 a :
-    to_frac_agree (q1 + q2) a ≡ to_frac_agree q1 a ⋅ to_frac_agree q2 a.
-  Proof. rewrite /to_frac_agree -pair_op agree_idemp //. Qed.
-
-  Lemma frac_agree_op_valid q1 a1 q2 a2 :
-    ✓ (to_frac_agree q1 a1 ⋅ to_frac_agree q2 a2) →
-    (q1 + q2 ≤ 1)%Qp ∧ a1 ≡ a2.
-  Proof.
-    intros [Hq Ha]%pair_valid. simpl in *. split; first done.
-    apply to_agree_op_inv. done.
-  Qed.
-  Lemma frac_agree_op_valid_L `{!LeibnizEquiv A} q1 a1 q2 a2 :
-    ✓ (to_frac_agree q1 a1 ⋅ to_frac_agree q2 a2) →
-    (q1 + q2 ≤ 1)%Qp ∧ a1 = a2.
-  Proof. unfold_leibniz. apply frac_agree_op_valid. Qed.
-  Lemma frac_agree_op_validN q1 a1 q2 a2 n :
-    ✓{n} (to_frac_agree q1 a1 ⋅ to_frac_agree q2 a2) →
-    (q1 + q2 ≤ 1)%Qp ∧ a1 ≡{n}≡ a2.
-  Proof.
-    intros [Hq Ha]%pair_validN. simpl in *. split; first done.
-    apply to_agree_op_invN. done.
-  Qed.
-
-  Lemma frac_agree_included q1 a1 q2 a2 :
-    to_frac_agree q1 a1 ≼ to_frac_agree q2 a2 ↔
-    (q1 < q2)%Qp ∧ a1 ≡ a2.
-  Proof. by rewrite pair_included frac_included to_agree_included. Qed.
-  Lemma frac_agree_included_L `{!LeibnizEquiv A} q1 a1 q2 a2 :
-    to_frac_agree q1 a1 ≼ to_frac_agree q2 a2 ↔
-    (q1 < q2)%Qp ∧ a1 = a2.
-  Proof. unfold_leibniz. apply frac_agree_included. Qed.
-  Lemma frac_agree_includedN q1 a1 q2 a2 n :
-    to_frac_agree q1 a1 ≼{n} to_frac_agree q2 a2 ↔
-    (q1 < q2)%Qp ∧ a1 ≡{n}≡ a2.
-  Proof.
-    by rewrite pair_includedN -cmra_discrete_included_iff
-               frac_included to_agree_includedN.
-  Qed.
-
-  (** No frame-preserving update lemma needed -- use [cmra_update_exclusive] with
-  the above [Exclusive] instance. *)
-
-End lemmas.
-
-Typeclasses Opaque to_frac_agree.

iris/algebra/lib/frac_auth.v

@@ -9,36 +9,39 @@ From iris.prelude Require Import options.
   split the authoritative part into fractions.
 *)
 
-Definition frac_authR (A : cmra) : cmra :=
+Definition frac_authR {SI : sidx} (A : cmra) : cmra :=
   authR (optionUR (prodR fracR A)).
-Definition frac_authUR (A : cmra) : ucmra :=
+Definition frac_authUR {SI : sidx} (A : cmra) : ucmra :=
   authUR (optionUR (prodR fracR A)).
 
-Definition frac_auth_auth {A : cmra} (x : A) : frac_authR A :=
+Definition frac_auth_auth {SI : sidx} {A : cmra} (x : A) : frac_authR A :=
   ● (Some (1%Qp,x)).
-Definition frac_auth_frag {A : cmra} (q : frac) (x : A) : frac_authR A :=
+Definition frac_auth_frag {SI : sidx}
+    {A : cmra} (q : frac) (x : A) : frac_authR A :=
   ◯ (Some (q,x)).
 
-Typeclasses Opaque frac_auth_auth frac_auth_frag.
+Global Typeclasses Opaque frac_auth_auth frac_auth_frag.
 
-Global Instance: Params (@frac_auth_auth) 1 := {}.
-Global Instance: Params (@frac_auth_frag) 2 := {}.
+Global Instance: Params (@frac_auth_auth) 2 := {}.
+Global Instance: Params (@frac_auth_frag) 3 := {}.
 
 Notation "●F a" := (frac_auth_auth a) (at level 10).
 Notation "◯F{ q } a" := (frac_auth_frag q a) (at level 10, format "◯F{ q }  a").
 Notation "◯F a" := (frac_auth_frag 1 a) (at level 10).
 
 Section frac_auth.
-  Context {A : cmra}.
+  Context {SI : sidx} {A : cmra}.
   Implicit Types a b : A.
 
-  Global Instance frac_auth_auth_ne : NonExpansive (@frac_auth_auth A).
+  Global Instance frac_auth_auth_ne : NonExpansive (@frac_auth_auth SI A).
   Proof. solve_proper. Qed.
-  Global Instance frac_auth_auth_proper : Proper ((≡) ==> (≡)) (@frac_auth_auth A).
+  Global Instance frac_auth_auth_proper :
+    Proper ((≡) ==> (≡)) (@frac_auth_auth SI A).
   Proof. solve_proper. Qed.
-  Global Instance frac_auth_frag_ne q : NonExpansive (@frac_auth_frag A q).
+  Global Instance frac_auth_frag_ne q : NonExpansive (@frac_auth_frag SI A q).
   Proof. solve_proper. Qed.
-  Global Instance frac_auth_frag_proper q : Proper ((≡) ==> (≡)) (@frac_auth_frag A q).
+  Global Instance frac_auth_frag_proper q :
+    Proper ((≡) ==> (≡)) (@frac_auth_frag SI A q).
   Proof. solve_proper. Qed.
 
   Global Instance frac_auth_auth_discrete a : Discrete a → Discrete (●F a).
@@ -65,13 +68,13 @@ Section frac_auth.
 
   Lemma frac_auth_includedN n q a b : ✓{n} (●F a ⋅ ◯F{q} b) → Some b ≼{n} Some a.
   Proof. by rewrite auth_both_validN /= => -[/Some_pair_includedN [_ ?] _]. Qed.
-  Lemma frac_auth_included `{CmraDiscrete A} q a b :
+  Lemma frac_auth_included `{!CmraDiscrete A} q a b :
     ✓ (●F a ⋅ ◯F{q} b) → Some b ≼ Some a.
   Proof. by rewrite auth_both_valid_discrete /= => -[/Some_pair_included [_ ?] _]. Qed.
-  Lemma frac_auth_includedN_total `{CmraTotal A} n q a b :
+  Lemma frac_auth_includedN_total `{!CmraTotal A} n q a b :
     ✓{n} (●F a ⋅ ◯F{q} b) → b ≼{n} a.
   Proof. intros. by eapply Some_includedN_total, frac_auth_includedN. Qed.
-  Lemma frac_auth_included_total `{CmraDiscrete A, CmraTotal A} q a b :
+  Lemma frac_auth_included_total `{!CmraDiscrete A, !CmraTotal A} q a b :
     ✓ (●F a ⋅ ◯F{q} b) → b ≼ a.
   Proof. intros. by eapply Some_included_total, frac_auth_included. Qed.
 
@@ -92,10 +95,12 @@ Section frac_auth.
   Lemma frac_auth_frag_op q1 q2 a1 a2 : ◯F{q1+q2} (a1 ⋅ a2) ≡ ◯F{q1} a1 ⋅ ◯F{q2} a2.
   Proof. done. Qed.
 
-  Lemma frac_auth_frag_validN_op_1_l n q a b : ✓{n} (◯F{1} a ⋅ ◯F{q} b) → False.
-  Proof. rewrite -frac_auth_frag_op frac_auth_frag_validN=> -[/Qp_not_add_le_l []]. Qed.
-  Lemma frac_auth_frag_valid_op_1_l q a b : ✓ (◯F{1} a ⋅ ◯F{q} b) → False.
-  Proof. rewrite -frac_auth_frag_op frac_auth_frag_valid=> -[/Qp_not_add_le_l []]. Qed.
+  Lemma frac_auth_frag_op_validN n q1 q2 a b :
+    ✓{n} (◯F{q1} a ⋅ ◯F{q2} b) ↔ (q1 + q2 ≤ 1)%Qp ∧ ✓{n} (a ⋅ b).
+  Proof. by rewrite -frac_auth_frag_op frac_auth_frag_validN. Qed.
+  Lemma frac_auth_frag_op_valid q1 q2 a b :
+    ✓ (◯F{q1} a ⋅ ◯F{q2} b) ↔ (q1 + q2 ≤ 1)%Qp ∧ ✓ (a ⋅ b).
+  Proof. by rewrite -frac_auth_frag_op frac_auth_frag_valid. Qed.
 
   Global Instance frac_auth_is_op (q q1 q2 : frac) (a a1 a2 : A) :
     IsOp q q1 q2 → IsOp a a1 a2 → IsOp' (◯F{q} a) (◯F{q1} a1) (◯F{q2} a2).
@@ -119,3 +124,17 @@ Section frac_auth.
     intros. by apply auth_update, option_local_update, exclusive_local_update.
   Qed.
 End frac_auth.
+
+Definition frac_authURF {SI : sidx} (F : rFunctor) : urFunctor :=
+  authURF (optionURF (prodRF (constRF fracR) F)).
+
+Global Instance frac_authURF_contractive {SI : sidx} F :
+  rFunctorContractive F → urFunctorContractive (frac_authURF F).
+Proof. apply _. Qed.
+
+Definition frac_authRF {SI : sidx} (F : rFunctor) : rFunctor :=
+  authRF (optionURF (prodRF (constRF fracR) F)).
+
+Global Instance frac_authRF_contractive {SI : sidx} F :
+  rFunctorContractive F → rFunctorContractive (frac_authRF F).
+Proof. apply _. Qed.

iris/algebra/lib/gmap_view.v

@@ -20,70 +20,77 @@ NOTE: The API surface for [gmap_view] is experimental and subject to change.  We
 plan to add notations for authoritative elements and fragments, and hope to
 support arbitrary maps as fragments. *)
 
-Local Definition gmap_view_fragUR (K : Type) `{Countable K} (V : ofe) : ucmra :=
-  gmapUR K (prodR dfracR (agreeR V)).
+Local Definition gmap_view_fragUR {SI : sidx}
+     (K : Type) `{Countable K} (V : cmra) : ucmra :=
+  gmapUR K (prodR dfracR V).
 
 (** View relation. *)
 Section rel.
-  Context (K : Type) `{Countable K} (V : ofe).
-  Implicit Types (m : gmap K V) (k : K) (v : V) (n : nat).
-  Implicit Types (f : gmap K (dfrac * agree V)).
-
-  Local Definition gmap_view_rel_raw n m f : Prop :=
-    map_Forall (λ k dv, ∃ v, dv.2 ≡{n}≡ to_agree v ∧ ✓ dv.1 ∧ m !! k = Some v) f.
+  Context {SI : sidx} (K : Type) `{Countable K} (V : cmra).
+  Implicit Types (m : gmap K V) (k : K) (v : V) (n : SI).
+  Implicit Types (f : gmap K (dfrac * V)).
+
+  (* If we exactly followed [auth], we'd write something like [f ≼{n} m ∧ ✓{n} m],
+  which is equivalent to:
+  [map_Forall (λ k fv, ∃ v, m !! k = Some v ∧ Some fv ≼{n} Some v ∧ ✓{n} v) f].
+  (Note the use of [Some] in the inclusion; the elementwise RA might not have a
+  unit and we want a reflexive relation!) However, [f] and [m] do not have the
+  same type, so this definition does not type-check: the fractions have been
+  erased from the authoritative [m]. So we additionally quantify over the erased
+  fraction [dq] and [(dq, v)] becomes the authoritative value.
+
+  An alternative definition one might consider is to replace the erased fraction
+  by a hard-coded [DfracOwn 1], the biggest possible fraction. That would not
+  work: we would end up with [Some dv ≼{n} Some (DfracOwn 1, v)] but that cannot
+  be satisfied if [dv.1 = DfracDiscarded], a case that we definitely want to
+  allow!
+
+  It is possible that [∀ k, ∃ dq, let auth := (pair dq) <$> m !! k in ✓{n} auth
+  ∧ f !! k ≼{n} auth] would also work, but now the proofs are all done already.  ;)
+  The two are probably equivalent, with a proof similar to [lookup_includedN]? *)
+  Local Definition gmap_view_rel_raw n m f :=
+    map_Forall (λ k fv,
+      ∃ v dq, m !! k = Some v ∧ ✓{n} (dq, v) ∧ (Some fv ≼{n} Some (dq, v))) f.
 
   Local Lemma gmap_view_rel_raw_mono n1 n2 m1 m2 f1 f2 :
     gmap_view_rel_raw n1 m1 f1 →
     m1 ≡{n2}≡ m2 →
     f2 ≼{n2} f1 →
-    n2 ≤ n1 →
+    (n2 ≤ n1)%sidx →
     gmap_view_rel_raw n2 m2 f2.
   Proof.
-    intros Hrel Hm Hf Hn k [q va] Hk.
+    intros Hrel Hm Hf Hn k [dqa va] Hk.
     (* For some reason applying the lemma in [Hf] does not work... *)
-    destruct (lookup_includedN n2 f2 f1) as [Hf' _]. specialize (Hf' Hf). clear Hf.
-    specialize (Hf' k). rewrite Hk in Hf'.
-    apply option_includedN in Hf'.
-    destruct Hf' as [[=]|(? & [q' va'] & [= <-] & Hf1 & Hincl)].
-    specialize (Hrel _ _ Hf1) as (v & Hagree & Hdval & Hm1). simpl in *.
+    destruct (lookup_includedN n2 f2 f1) as [Hf' _].
+    specialize (Hf' Hf k). clear Hf. rewrite Hk in Hf'.
+    destruct (Some_includedN_is_Some _ _ _ Hf') as [[q' va'] Heq]. rewrite Heq in Hf'.
+    specialize (Hrel _ _ Heq) as (v & dq & Hm1 & [Hvval Hdqval] & Hvincl). simpl in *.
     specialize (Hm k).
     edestruct (dist_Some_inv_l _ _ _ _ Hm Hm1) as (v' & Hm2 & Hv).
-    exists v'. rewrite assoc. split; last done.
-    rewrite -Hv.
-    destruct Hincl as [[Heqq Heqva]|[Hinclq Hinclva]%pair_includedN].
-    - simpl in *. split.
-      + rewrite Heqva. eapply dist_le; last eassumption. done.
-      + rewrite <-discrete_iff in Heqq; last by apply _.
-        fold_leibniz. subst q'. done.
-    - split.
-      + etrans; last first.
-        { eapply dist_le; last eassumption. done. }
-        eapply agree_valid_includedN; last done.
-        eapply cmra_validN_le; last eassumption.
-        rewrite Hagree. done.
-      + rewrite <-cmra_discrete_included_iff in Hinclq.
-        eapply cmra_valid_included; done.
+    eexists. exists dq. split; first done. split.
+    { split; first done. simpl. rewrite -Hv. eapply cmra_validN_le; done. }
+    rewrite -Hv. etrans; first exact Hf'.
+    apply: cmra_includedN_le; done.
   Qed.
 
   Local Lemma gmap_view_rel_raw_valid n m f :
     gmap_view_rel_raw n m f → ✓{n} f.
   Proof.
-    intros Hrel k. destruct (f !! k) as [[q va]|] eqn:Hf; rewrite Hf; last done.
-    specialize (Hrel _ _ Hf) as (v & Hagree & Hdval & Hm1). simpl in *.
-    split; simpl.
-    - apply cmra_discrete_valid_iff. done.
-    - rewrite Hagree. done.
+    intros Hrel k. destruct (f !! k) as [[dqa va]|] eqn:Hf; rewrite Hf; last done.
+    specialize (Hrel _ _ Hf) as (v & dq & Hmval & Hvval & Hvincl). simpl in *.
+    eapply cmra_validN_includedN. 2:done. done.
   Qed.
 
   Local Lemma gmap_view_rel_raw_unit n :
     ∃ m, gmap_view_rel_raw n m ε.
   Proof. exists ∅. apply: map_Forall_empty. Qed.
 
-  Local Canonical Structure gmap_view_rel : view_rel (gmapO K V) (gmap_view_fragUR K V) :=
+  Local Canonical Structure gmap_view_rel :
+      view_rel (gmapO K V) (gmap_view_fragUR K V) :=
     ViewRel gmap_view_rel_raw gmap_view_rel_raw_mono
             gmap_view_rel_raw_valid gmap_view_rel_raw_unit.
 
-  Local Lemma gmap_view_rel_exists n (f : gmap K (dfrac * agreeR V)) :
+  Local Lemma gmap_view_rel_exists n f :
     (∃ m, gmap_view_rel n m f) ↔ ✓{n} f.
   Proof.
     split.
@@ -91,16 +98,16 @@ Section rel.
     intros Hf.
     cut (∃ m, gmap_view_rel n m f ∧ ∀ k, f !! k = None → m !! k = None).
     { naive_solver. }
-    induction f as [|k [dq ag] f Hk' IH] using map_ind.
+    induction f as [|k [dq v] f Hk' IH] using map_ind.
     { exists ∅. split; [|done]. apply: map_Forall_empty. }
     move: (Hf k). rewrite lookup_insert=> -[/= ??].
-    destruct (to_agree_uninjN n ag) as [v ?]; [done|].
     destruct IH as (m & Hm & Hdom).
     { intros k'. destruct (decide (k = k')) as [->|?]; [by rewrite Hk'|].
       move: (Hf k'). by rewrite lookup_insert_ne. }
     exists (<[k:=v]> m).
     rewrite /gmap_view_rel /= /gmap_view_rel_raw map_Forall_insert //=. split_and!.
-    - exists v. by rewrite lookup_insert.
+    - exists v, dq. split; first by rewrite lookup_insert.
+      split; first by split. done.
     - eapply map_Forall_impl; [apply Hm|]; simpl.
       intros k' [dq' ag'] (v'&?&?&?). exists v'.
       rewrite lookup_insert_ne; naive_solver.
@@ -111,14 +118,13 @@ Section rel.
   Proof. apply: map_Forall_empty. Qed.
 
   Local Lemma gmap_view_rel_discrete :
-    OfeDiscrete V → ViewRelDiscrete gmap_view_rel.
+    CmraDiscrete V → ViewRelDiscrete gmap_view_rel.
   Proof.
     intros ? n m f Hrel k [df va] Hk.
-    destruct (Hrel _ _ Hk) as (v & Hagree & Hdval & Hm).
-    exists v. split; last by auto.
-    eapply discrete_iff; first by apply _.
-    eapply discrete_iff; first by apply _.
-    done.
+    destruct (Hrel _ _ Hk) as (v & dq & Hm & Hvval & Hvincl).
+    exists v, dq. split; first done.
+    split; first by apply cmra_discrete_valid_iff_0.
+    rewrite -cmra_discrete_included_iff_0. done.
   Qed.
 End rel.
 
@@ -126,236 +132,307 @@ Local Existing Instance gmap_view_rel_discrete.
 
 (** [gmap_view] is a notation to give canonical structure search the chance
 to infer the right instances (see [auth]). *)
-Notation gmap_view K V := (view (@gmap_view_rel_raw K _ _ V)).
-Definition gmap_viewO (K : Type) `{Countable K} (V : ofe) : ofe :=
+Notation gmap_view K V := (view (gmap_view_rel_raw K V)).
+Definition gmap_viewO {SI : sidx} (K : Type) `{Countable K} (V : cmra) : ofe :=
   viewO (gmap_view_rel K V).
-Definition gmap_viewR (K : Type) `{Countable K} (V : ofe) : cmra :=
+Definition gmap_viewR {SI : sidx} (K : Type) `{Countable K} (V : cmra) : cmra :=
   viewR (gmap_view_rel K V).
-Definition gmap_viewUR (K : Type) `{Countable K} (V : ofe) : ucmra :=
+Definition gmap_viewUR {SI : sidx} (K : Type) `{Countable K} (V : cmra) : ucmra :=
   viewUR (gmap_view_rel K V).
 
 Section definitions.
-  Context {K : Type} `{Countable K} {V : ofe}.
+  Context {SI : sidx} `{Countable K} {V : cmra}.
 
-  Definition gmap_view_auth (q : frac) (m : gmap K V) : gmap_viewR K V :=
-    ●V{#q} m.
+  Definition gmap_view_auth (dq : dfrac) (m : gmap K V) : gmap_viewR K V :=
+    ●V{dq} m.
   Definition gmap_view_frag (k : K) (dq : dfrac) (v : V) : gmap_viewR K V :=
-    ◯V {[k := (dq, to_agree v)]}.
+    ◯V {[k := (dq, v)]}.
 End definitions.
 
 Section lemmas.
-  Context {K : Type} `{Countable K} {V : ofe}.
+  Context {SI : sidx} `{Countable K} {V : cmra}.
   Implicit Types (m : gmap K V) (k : K) (q : Qp) (dq : dfrac) (v : V).
 
-  Global Instance : Params (@gmap_view_auth) 5 := {}.
-  Global Instance gmap_view_auth_ne q : NonExpansive (gmap_view_auth (K:=K) (V:=V) q).
+  Global Instance : Params (@gmap_view_auth) 6 := {}.
+  Global Instance gmap_view_auth_ne dq :
+    NonExpansive (gmap_view_auth (K:=K) (V:=V) dq).
   Proof. solve_proper. Qed.
-  Global Instance gmap_view_auth_proper q : Proper ((≡) ==> (≡)) (gmap_view_auth (K:=K) (V:=V) q).
+  Global Instance gmap_view_auth_proper dq :
+    Proper ((≡) ==> (≡)) (gmap_view_auth (K:=K) (V:=V) dq).
   Proof. apply ne_proper, _. Qed.
 
-  Global Instance : Params (@gmap_view_frag) 6 := {}.
+  Global Instance : Params (@gmap_view_frag) 7 := {}.
   Global Instance gmap_view_frag_ne k oq : NonExpansive (gmap_view_frag (V:=V) k oq).
   Proof. solve_proper. Qed.
-  Global Instance gmap_view_frag_proper k oq : Proper ((≡) ==> (≡)) (gmap_view_frag (V:=V) k oq).
+  Global Instance gmap_view_frag_proper k oq :
+    Proper ((≡) ==> (≡)) (gmap_view_frag (V:=V) k oq).
   Proof. apply ne_proper, _. Qed.
 
   (* Helper lemmas *)
   Local Lemma gmap_view_rel_lookup n m k dq v :
-    gmap_view_rel K V n m {[k := (dq, to_agree v)]} ↔ ✓ dq ∧ m !! k ≡{n}≡ Some v.
+    gmap_view_rel K V n m {[k := (dq, v)]} ↔
+    ∃ v' dq', m !! k = Some v' ∧ ✓{n} (dq', v') ∧ Some (dq, v) ≼{n} Some (dq', v').
   Proof.
     split.
     - intros Hrel.
-      edestruct (Hrel k) as (v' & Hagree & Hval & ->).
+      edestruct (Hrel k) as (v' & dq' & Hlookup & Hval & Hinc).
       { rewrite lookup_singleton. done. }
-      simpl in *. apply (inj _) in Hagree. rewrite Hagree.
-      done.
-    - intros [Hval (v' & Hm & Hv')%dist_Some_inv_r'] j [df va].
+      simpl in *. eexists _, _. split_and!; done.
+    - intros (v' & dq' & Hlookup & Hval & ?) j [df va].
       destruct (decide (k = j)) as [<-|Hne]; last by rewrite lookup_singleton_ne.
       rewrite lookup_singleton. intros [= <- <-]. simpl.
-      exists v'. split_and!; by rewrite ?Hv'.
+      exists v', dq'. split_and!; by rewrite ?Hv'.
   Qed.
 
   (** Composition and validity *)
-  Lemma gmap_view_auth_frac_op p q m :
-    gmap_view_auth (p + q) m ≡ gmap_view_auth p m ⋅ gmap_view_auth q m.
-  Proof. by rewrite /gmap_view_auth -dfrac_op_own view_auth_dfrac_op. Qed.
-  Global Instance gmap_view_auth_frac_is_op q q1 q2 m :
-    IsOp q q1 q2 → IsOp' (gmap_view_auth q m) (gmap_view_auth q1 m) (gmap_view_auth q2 m).
+  Lemma gmap_view_auth_dfrac_op dp dq m :
+    gmap_view_auth (dp ⋅ dq) m ≡
+    gmap_view_auth dp m ⋅ gmap_view_auth dq m.
+  Proof. by rewrite /gmap_view_auth view_auth_dfrac_op. Qed.
+  Global Instance gmap_view_auth_dfrac_is_op dq dq1 dq2 m :
+    IsOp dq dq1 dq2 →
+    IsOp' (gmap_view_auth dq m) (gmap_view_auth dq1 m) (gmap_view_auth dq2 m).
   Proof. rewrite /gmap_view_auth. apply _. Qed.
 
-  Lemma gmap_view_auth_frac_op_invN n p m1 q m2 :
-    ✓{n} (gmap_view_auth p m1 ⋅ gmap_view_auth q m2) → m1 ≡{n}≡ m2.
+  Lemma gmap_view_auth_dfrac_op_invN n dp m1 dq m2 :
+    ✓{n} (gmap_view_auth dp m1 ⋅ gmap_view_auth dq m2) → m1 ≡{n}≡ m2.
   Proof. apply view_auth_dfrac_op_invN. Qed.
-  Lemma gmap_view_auth_frac_op_inv p m1 q m2 :
-    ✓ (gmap_view_auth p m1 ⋅ gmap_view_auth q m2) → m1 ≡ m2.
+  Lemma gmap_view_auth_dfrac_op_inv dp m1 dq m2 :
+    ✓ (gmap_view_auth dp m1 ⋅ gmap_view_auth dq m2) → m1 ≡ m2.
   Proof. apply view_auth_dfrac_op_inv. Qed.
-  Lemma gmap_view_auth_frac_op_inv_L `{!LeibnizEquiv V} q m1 p m2 :
-    ✓ (gmap_view_auth p m1 ⋅ gmap_view_auth q m2) → m1 = m2.
-  Proof. apply view_auth_dfrac_op_inv_L, _. Qed.
 
-  Lemma gmap_view_auth_frac_valid m q : ✓ gmap_view_auth q m ↔ (q ≤ 1)%Qp.
+  Lemma gmap_view_auth_dfrac_validN m n dq : ✓{n} gmap_view_auth dq m ↔ ✓ dq.
+  Proof.
+    rewrite view_auth_dfrac_validN. intuition eauto using gmap_view_rel_unit.
+  Qed.
+  Lemma gmap_view_auth_dfrac_valid m dq : ✓ gmap_view_auth dq m ↔ ✓ dq.
   Proof.
     rewrite view_auth_dfrac_valid. intuition eauto using gmap_view_rel_unit.
   Qed.
-  Lemma gmap_view_auth_valid m : ✓ gmap_view_auth 1 m.
-  Proof. rewrite gmap_view_auth_frac_valid. done. Qed.
+  Lemma gmap_view_auth_valid m : ✓ gmap_view_auth (DfracOwn 1) m.
+  Proof. rewrite gmap_view_auth_dfrac_valid. done. Qed.
 
-  Lemma gmap_view_auth_frac_op_validN n q1 q2 m1 m2 :
-    ✓{n} (gmap_view_auth q1 m1 ⋅ gmap_view_auth q2 m2) ↔ ✓ (q1 + q2)%Qp ∧ m1 ≡{n}≡ m2.
+  Lemma gmap_view_auth_dfrac_op_validN n dq1 dq2 m1 m2 :
+    ✓{n} (gmap_view_auth dq1 m1 ⋅ gmap_view_auth dq2 m2) ↔ ✓ (dq1 ⋅ dq2) ∧ m1 ≡{n}≡ m2.
   Proof.
     rewrite view_auth_dfrac_op_validN. intuition eauto using gmap_view_rel_unit.
   Qed.
-  Lemma gmap_view_auth_frac_op_valid q1 q2 m1 m2 :
-    ✓ (gmap_view_auth q1 m1 ⋅ gmap_view_auth q2 m2) ↔ (q1 + q2 ≤ 1)%Qp ∧ m1 ≡ m2.
+  Lemma gmap_view_auth_dfrac_op_valid dq1 dq2 m1 m2 :
+    ✓ (gmap_view_auth dq1 m1 ⋅ gmap_view_auth dq2 m2) ↔ ✓ (dq1 ⋅ dq2) ∧ m1 ≡ m2.
   Proof.
     rewrite view_auth_dfrac_op_valid. intuition eauto using gmap_view_rel_unit.
   Qed.
-  Lemma gmap_view_auth_frac_op_valid_L `{!LeibnizEquiv V} q1 q2 m1 m2 :
-    ✓ (gmap_view_auth q1 m1 ⋅ gmap_view_auth q2 m2) ↔ ✓ (q1 + q2)%Qp ∧ m1 = m2.
-  Proof. unfold_leibniz. apply gmap_view_auth_frac_op_valid. Qed.
 
   Lemma gmap_view_auth_op_validN n m1 m2 :
-    ✓{n} (gmap_view_auth 1 m1 ⋅ gmap_view_auth 1 m2) ↔ False.
+    ✓{n} (gmap_view_auth (DfracOwn 1) m1 ⋅ gmap_view_auth (DfracOwn 1) m2) ↔ False.
   Proof. apply view_auth_op_validN. Qed.
   Lemma gmap_view_auth_op_valid m1 m2 :
-    ✓ (gmap_view_auth 1 m1 ⋅ gmap_view_auth 1 m2) ↔ False.
+    ✓ (gmap_view_auth (DfracOwn 1) m1 ⋅ gmap_view_auth (DfracOwn 1) m2) ↔ False.
   Proof. apply view_auth_op_valid. Qed.
 
-  Lemma gmap_view_frag_validN n k dq v : ✓{n} gmap_view_frag k dq v ↔ ✓ dq.
+  Lemma gmap_view_frag_validN n k dq v : ✓{n} gmap_view_frag k dq v ↔ ✓ dq ∧ ✓{n} v.
   Proof.
     rewrite view_frag_validN gmap_view_rel_exists singleton_validN pair_validN.
     naive_solver.
   Qed.
-  Lemma gmap_view_frag_valid k dq v : ✓ gmap_view_frag k dq v ↔ ✓ dq.
+  Lemma gmap_view_frag_valid k dq v : ✓ gmap_view_frag k dq v ↔ ✓ dq ∧ ✓ v.
   Proof.
     rewrite cmra_valid_validN. setoid_rewrite gmap_view_frag_validN.
-    naive_solver eauto using O.
+    rewrite cmra_valid_validN. pose 0ᵢ. naive_solver.
   Qed.
 
-  Lemma gmap_view_frag_op k dq1 dq2 v :
-    gmap_view_frag k (dq1 ⋅ dq2) v ≡ gmap_view_frag k dq1 v ⋅ gmap_view_frag k dq2 v.
-  Proof. rewrite -view_frag_op singleton_op -pair_op agree_idemp //. Qed.
-  Lemma gmap_view_frag_add k q1 q2 v :
-    gmap_view_frag k (DfracOwn (q1 + q2)) v ≡
-      gmap_view_frag k (DfracOwn q1) v ⋅ gmap_view_frag k (DfracOwn q2) v.
+  Lemma gmap_view_frag_op k dq1 dq2 v1 v2 :
+    gmap_view_frag k (dq1 ⋅ dq2) (v1 ⋅ v2) ≡
+      gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2.
+  Proof. rewrite -view_frag_op singleton_op -pair_op //. Qed.
+  Lemma gmap_view_frag_add k q1 q2 v1 v2 :
+    gmap_view_frag k (DfracOwn (q1 + q2)) (v1 ⋅ v2) ≡
+      gmap_view_frag k (DfracOwn q1) v1 ⋅ gmap_view_frag k (DfracOwn q2) v2.
   Proof. rewrite -gmap_view_frag_op. done. Qed.
 
   Lemma gmap_view_frag_op_validN n k dq1 dq2 v1 v2 :
     ✓{n} (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ↔
-      ✓ (dq1 ⋅ dq2) ∧ v1 ≡{n}≡ v2.
+      ✓ (dq1 ⋅ dq2) ∧ ✓{n} (v1 ⋅ v2).
   Proof.
     rewrite view_frag_validN gmap_view_rel_exists singleton_op singleton_validN.
-    by rewrite -pair_op pair_validN to_agree_op_validN.
+    by rewrite -pair_op pair_validN.
   Qed.
   Lemma gmap_view_frag_op_valid k dq1 dq2 v1 v2 :
-    ✓ (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ↔ ✓ (dq1 ⋅ dq2) ∧ v1 ≡ v2.
+    ✓ (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ↔
+      ✓ (dq1 ⋅ dq2) ∧ ✓ (v1 ⋅ v2).
   Proof.
     rewrite view_frag_valid. setoid_rewrite gmap_view_rel_exists.
     rewrite -cmra_valid_validN singleton_op singleton_valid.
-    by rewrite -pair_op pair_valid to_agree_op_valid.
+    by rewrite -pair_op pair_valid.
   Qed.
-  (* FIXME: Having a [valid_L] lemma is not consistent with [auth] and [view]; they
-     have [inv_L] lemmas instead that just have an equality on the RHS. *)
-  Lemma gmap_view_frag_op_valid_L `{!LeibnizEquiv V} k dq1 dq2 v1 v2 :
-    ✓ (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ↔ ✓ (dq1 ⋅ dq2) ∧ v1 = v2.
-  Proof. unfold_leibniz. apply gmap_view_frag_op_valid. Qed.
-
-  Lemma gmap_view_both_frac_validN n q m k dq v :
-    ✓{n} (gmap_view_auth q m ⋅ gmap_view_frag k dq v) ↔
-      (q ≤ 1)%Qp ∧ ✓ dq ∧ m !! k ≡{n}≡ Some v.
+
+  Lemma gmap_view_both_dfrac_validN n dp m k dq v :
+    ✓{n} (gmap_view_auth dp m ⋅ gmap_view_frag k dq v) ↔
+      ∃ v' dq', ✓ dp ∧ m !! k = Some v' ∧ ✓{n} (dq', v') ∧
+                Some (dq, v) ≼{n} Some (dq', v').
   Proof.
     rewrite /gmap_view_auth /gmap_view_frag.
-    rewrite view_both_dfrac_validN gmap_view_rel_lookup.
-    naive_solver.
+    rewrite view_both_dfrac_validN gmap_view_rel_lookup. naive_solver.
   Qed.
-  Lemma gmap_view_both_validN n m k dq v :
-    ✓{n} (gmap_view_auth 1 m ⋅ gmap_view_frag k dq v) ↔
-      ✓ dq ∧ m !! k ≡{n}≡ Some v.
-  Proof. rewrite gmap_view_both_frac_validN. naive_solver done. Qed.
-  Lemma gmap_view_both_frac_valid q m k dq v :
-    ✓ (gmap_view_auth q m ⋅ gmap_view_frag k dq v) ↔
-    (q ≤ 1)%Qp ∧ ✓ dq ∧ m !! k ≡ Some v.
+  Lemma gmap_view_both_validN n dp m k v :
+    ✓{n} (gmap_view_auth dp m ⋅ gmap_view_frag k (DfracOwn 1) v) ↔
+      ✓ dp ∧ ✓{n} v ∧ m !! k ≡{n}≡ Some v.
   Proof.
-    rewrite /gmap_view_auth /gmap_view_frag.
-    rewrite view_both_dfrac_valid. setoid_rewrite gmap_view_rel_lookup.
-    split=>[[Hq Hm]|[Hq Hm]].
-    - split; first done. split.
-      + apply (Hm 0%nat).
-      + apply equiv_dist=>n. apply Hm.
-    - split; first done. intros n. split.
-      + apply Hm.
-      + revert n. apply equiv_dist. apply Hm.
+    rewrite gmap_view_both_dfrac_validN. split.
+    - intros [Hdp (v' & dq' & Hlookup & Hvalid & Hincl)].
+      split; first done. rewrite Hlookup.
+      destruct (Some_includedN_exclusive _ _ _ Hincl Hvalid) as [_ Heq].
+      simpl in Heq. split.
+      + rewrite pair_validN in Hvalid. rewrite Heq. naive_solver.
+      + by rewrite Heq.
+    - intros (Hdp & Hval & Hlookup).
+      apply dist_Some_inv_r' in Hlookup as [v' [Hlookup Heq]].
+      exists v', (DfracOwn 1). do 2 (split; [done|]). split.
+      + rewrite pair_validN. by rewrite -Heq.
+      + by apply: Some_includedN_refl.
+  Qed.
+  (** The backwards direction here does not hold: if [dq = DfracOwn 1] but
+  [v ≠ v'], we have to find a suitable erased fraction [dq'] to satisfy the view
+  relation, but there is no way to satisfy [Some (DfracOwn 1, v) ≼{n} Some (dq', v')]
+  for any [dq']. The "if and only if" version of this lemma would have to
+  involve some extra condition like [dq = DfracOwn 1 → v = v'], or phrased
+  more like the view relation itself: [∃ dq', ✓ dq' ∧ Some (v, dq) ≼{n} Some (v', dq')]. *)
+  Lemma gmap_view_both_dfrac_validN_total `{!CmraTotal V} n dp m k dq v :
+    ✓{n} (gmap_view_auth dp m ⋅ gmap_view_frag k dq v) →
+    ∃ v', ✓ dp ∧ ✓ dq ∧ m !! k = Some v' ∧ ✓{n} v' ∧ v ≼{n} v'.
+  Proof.
+    rewrite gmap_view_both_dfrac_validN.
+    intros (v' & dq' & Hdp & Hlookup & Hvalid & Hincl).
+    exists v'. split; first done. split.
+    - eapply (cmra_valid_Some_included dq'); first by apply Hvalid.
+      eapply cmra_discrete_included_iff.
+      eapply Some_pair_includedN_l. done.
+    - split; first done. split; first apply Hvalid.
+      move:Hincl=> /Some_pair_includedN_r /Some_includedN_total. done.
+  Qed.
+
+  (** Without [CmraDiscrete], we cannot do much better than [∀ n, <same as above>].
+  This is because both the [dq'] and the witness for the [≼{n}] can be different for
+  each step-index. It is totally possible that at low step-indices, [v] has a frame
+  (and [dq' > dq]) while at higher step-indices, [v] has no frame (and [dq' = dq]). *)
+  Lemma gmap_view_both_dfrac_valid_discrete `{!CmraDiscrete V} dp m k dq v :
+    ✓ (gmap_view_auth dp m ⋅ gmap_view_frag k dq v) ↔
+      ∃ v' dq', ✓ dp ∧ m !! k = Some v' ∧
+                ✓ (dq', v') ∧
+                Some (dq, v) ≼ Some (dq', v').
+  Proof.
+    rewrite cmra_valid_validN. setoid_rewrite gmap_view_both_dfrac_validN. split.
+    - intros Hvalid. specialize (Hvalid 0ᵢ).
+      destruct Hvalid as (v' & dq' & Hdp & Hlookup & Hvalid & Hincl).
+      exists v', dq'. do 2 (split; first done).
+      split; first by apply cmra_discrete_valid.
+      by apply: cmra_discrete_included_r.
+    - intros (v' & dq' & Hdp & Hlookup & Hvalid & Hincl) n.
+      exists v', dq'. do 2 (split; first done).
+      split; first by apply cmra_valid_validN.
+      by apply: cmra_included_includedN.
+  Qed.
+  (** The backwards direction here does not hold: if [dq = DfracOwn 1] but
+  [v ≠ v'], we have to find a suitable erased fraction [dq'] to satisfy the view
+  relation, but there is no way to satisfy [Some (DfracOwn 1, v) ≼ Some (dq', v')]
+  for any [dq']. The "if and only if" version of this lemma would have to
+  involve some extra condition like [dq = DfracOwn 1 → v = v'], or phrased
+  more like the view relation itself: [∃ dq', ✓ dq' ∧ Some (v, dq) ≼ Some (v', dq')]. *)
+  Lemma gmap_view_both_dfrac_valid_discrete_total
+      `{!CmraDiscrete V, !CmraTotal V} dp m k dq v :
+    ✓ (gmap_view_auth dp m ⋅ gmap_view_frag k dq v) →
+    ∃ v', ✓ dp ∧ ✓ dq ∧ m !! k = Some v' ∧ ✓ v' ∧ v ≼ v'.
+  Proof.
+    rewrite gmap_view_both_dfrac_valid_discrete.
+    intros (v' & dq' & Hdp & Hlookup & Hvalid & Hincl).
+    exists v'. split; first done. split.
+    - eapply (cmra_valid_Some_included dq'); first by apply Hvalid.
+      eapply Some_pair_included_l. done.
+    - split; first done. split; first apply Hvalid.
+      move:Hincl=> /Some_pair_included_r /Some_included_total. done.
+  Qed.
+  (** On the other hand, this one holds for all CMRAs, not just discrete ones. *)
+  Lemma gmap_view_both_valid m dp k v :
+    ✓ (gmap_view_auth dp m ⋅ gmap_view_frag k (DfracOwn 1) v) ↔
+    ✓ dp ∧ ✓ v ∧ m !! k ≡ Some v.
+  Proof.
+    rewrite cmra_valid_validN. setoid_rewrite gmap_view_both_validN. split.
+    - intros Hvalid. split; last split.
+      + eapply (Hvalid 0ᵢ).
+      + apply cmra_valid_validN. intros n. eapply Hvalid.
+      + apply equiv_dist. intros n. eapply Hvalid.
+    - intros (Hdp & Hval & Hlookup). intros n.
+      split; first done. split.
+      + apply cmra_valid_validN. done.
+      + rewrite Hlookup. done.
   Qed.
-  Lemma gmap_view_both_frac_valid_L `{!LeibnizEquiv V} q m k dq v :
-    ✓ (gmap_view_auth q m ⋅ gmap_view_frag k dq v) ↔
-    ✓ q ∧ ✓ dq ∧ m !! k = Some v.
-  Proof. unfold_leibniz. apply gmap_view_both_frac_valid. Qed.
-  Lemma gmap_view_both_valid m k dq v :
-    ✓ (gmap_view_auth 1 m ⋅ gmap_view_frag k dq v) ↔
-    ✓ dq ∧ m !! k ≡ Some v.
-  Proof. rewrite gmap_view_both_frac_valid. naive_solver done. Qed.
-  (* FIXME: Having a [valid_L] lemma is not consistent with [auth] and [view]; they
-     have [inv_L] lemmas instead that just have an equality on the RHS. *)
-  Lemma gmap_view_both_valid_L `{!LeibnizEquiv V} m k dq v :
-    ✓ (gmap_view_auth 1 m ⋅ gmap_view_frag k dq v) ↔
-    ✓ dq ∧ m !! k = Some v.
-  Proof. unfold_leibniz. apply gmap_view_both_valid. Qed.
 
   (** Frame-preserving updates *)
   Lemma gmap_view_alloc m k dq v :
     m !! k = None →
     ✓ dq →
-    gmap_view_auth 1 m ~~> gmap_view_auth 1 (<[k := v]> m) ⋅ gmap_view_frag k dq v.
+    ✓ v →
+    gmap_view_auth (DfracOwn 1) m ~~>
+      gmap_view_auth (DfracOwn 1) (<[k := v]> m) ⋅ gmap_view_frag k dq v.
   Proof.
-    intros Hfresh Hdq. apply view_update_alloc=>n bf Hrel j [df va] /=.
+    intros Hfresh Hdq Hval. apply view_update_alloc=>n bf Hrel j [df va] /=.
     rewrite lookup_op. destruct (decide (j = k)) as [->|Hne].
     - assert (bf !! k = None) as Hbf.
       { destruct (bf !! k) as [[df' va']|] eqn:Hbf; last done.
-        specialize (Hrel _ _ Hbf). destruct Hrel as (v' & _ & _ & Hm).
+        specialize (Hrel _ _ Hbf). destruct Hrel as (v' & dq' & Hm & _).
         exfalso. rewrite Hm in Hfresh. done. }
       rewrite lookup_singleton Hbf right_id.
-      intros [= <- <-]. eexists. do 2 (split; first done).
-      rewrite lookup_insert. done.
+      intros [= <- <-]. eexists _, _.
+      rewrite lookup_insert. split; first done.
+      split; last by apply: Some_includedN_refl.
+      split; first done. by eapply cmra_valid_validN.
     - rewrite lookup_singleton_ne; last done.
       rewrite left_id=>Hbf.
-      specialize (Hrel _ _ Hbf). destruct Hrel as (v' & ? & ? & Hm).
-      eexists. do 2 (split; first done).
+      specialize (Hrel _ _ Hbf). destruct Hrel as (v' & ? & Hm & ?).
+      eexists _, _. split; last done.
       rewrite lookup_insert_ne //.
   Qed.
 
   Lemma gmap_view_alloc_big m m' dq :
     m' ##ₘ m →
     ✓ dq →
-    gmap_view_auth 1 m ~~>
-      gmap_view_auth 1 (m' ∪ m) ⋅ ([^op map] k↦v ∈ m', gmap_view_frag k dq v).
+    map_Forall (λ k v, ✓ v) m' →
+    gmap_view_auth (DfracOwn 1) m ~~>
+      gmap_view_auth (DfracOwn 1) (m' ∪ m) ⋅
+      ([^op map] k↦v ∈ m', gmap_view_frag k dq v).
   Proof.
-    intros. induction m' as [|k v m' ? IH] using map_ind; decompose_map_disjoint.
+    intros ?? Hm'.
+    induction m' as [|k v m' ? IH] using map_ind; decompose_map_disjoint.
     { rewrite big_opM_empty left_id_L right_id. done. }
-    rewrite IH //.
-    rewrite big_opM_insert // assoc.
+    apply map_Forall_insert in Hm' as [??]; last done.
+    rewrite IH //. rewrite big_opM_insert // assoc.
     apply cmra_update_op; last done.
-    rewrite -insert_union_l. apply (gmap_view_alloc _ k dq); last done.
+    rewrite -insert_union_l. apply (gmap_view_alloc _ k dq); [|done..].
     by apply lookup_union_None.
   Qed.
 
   Lemma gmap_view_delete m k v :
-    gmap_view_auth 1 m ⋅ gmap_view_frag k (DfracOwn 1) v ~~>
-    gmap_view_auth 1 (delete k m).
+    gmap_view_auth (DfracOwn 1) m ⋅ gmap_view_frag k (DfracOwn 1) v ~~>
+    gmap_view_auth (DfracOwn 1) (delete k m).
   Proof.
     apply view_update_dealloc=>n bf Hrel j [df va] Hbf /=.
     destruct (decide (j = k)) as [->|Hne].
-    - edestruct (Hrel k) as (v' & _ & Hdf & _).
+    - edestruct (Hrel k) as (v' & dq' & ? & Hval & Hincl).
       { rewrite lookup_op Hbf lookup_singleton -Some_op. done. }
-      exfalso. apply: dfrac_full_exclusive. apply Hdf.
-    - edestruct (Hrel j) as (v' & ? & ? & Hm).
+      eapply (cmra_validN_Some_includedN _ _ _ Hval) in Hincl as Hval'.
+      exfalso. clear Hval Hincl.
+      rewrite pair_validN /= in Hval'.
+      apply: dfrac_full_exclusive. apply Hval'.
+    - edestruct (Hrel j) as (v' & ? & ? & ?).
       { rewrite lookup_op lookup_singleton_ne // Hbf. done. }
-      exists v'. do 2 (split; first done).
+      eexists v', _. split; last done.
       rewrite lookup_delete_ne //.
   Qed.
 
   Lemma gmap_view_delete_big m m' :
-    gmap_view_auth 1 m ⋅ ([^op map] k↦v ∈ m', gmap_view_frag k (DfracOwn 1) v) ~~>
-    gmap_view_auth 1 (m ∖ m').
+    gmap_view_auth (DfracOwn 1) m ⋅
+    ([^op map] k↦v ∈ m', gmap_view_frag k (DfracOwn 1) v) ~~>
+      gmap_view_auth (DfracOwn 1) (m ∖ m').
   Proof.
     induction m' as [|k v m' ? IH] using map_ind.
     { rewrite right_id_L big_opM_empty right_id //. }
@@ -364,157 +441,277 @@ Section lemmas.
     rewrite -delete_difference. done.
   Qed.
 
-  Lemma gmap_view_update m k v v' :
-    gmap_view_auth 1 m ⋅ gmap_view_frag k (DfracOwn 1) v ~~>
-      gmap_view_auth 1 (<[k := v']> m) ⋅ gmap_view_frag k (DfracOwn 1) v'.
+  (** We do not use [local_update] ([~l~>]) in the premise because we also want
+  to expose the role of the fractions. *)
+  Lemma gmap_view_update m k dq v mv' v' dq' :
+    (∀ n mv f,
+      m !! k = Some mv →
+      ✓{n} ((dq, v) ⋅? f) →
+      mv ≡{n}≡ v ⋅? (snd <$> f) →
+      ✓{n} ((dq', v') ⋅? f) ∧ mv' ≡{n}≡ v' ⋅? (snd <$> f)) →
+    gmap_view_auth (DfracOwn 1) m ⋅ gmap_view_frag k dq v ~~>
+      gmap_view_auth (DfracOwn 1) (<[k := mv']> m) ⋅ gmap_view_frag k dq' v'.
   Proof.
-    rewrite gmap_view_delete.
-    rewrite (gmap_view_alloc _ k (DfracOwn 1) v') //; last by rewrite lookup_delete.
-    rewrite insert_delete_insert //.
+    intros Hup. apply view_update=> n bf Hrel j [df va].
+    rewrite lookup_op.
+    destruct (decide (j = k)) as [->|Hne]; last first.
+    { (* prove that other keys are unaffected *)
+      simplify_map_eq. rewrite lookup_singleton_ne //.
+      (* FIXME simplify_map_eq should have done this *)
+      rewrite left_id. intros Hbf.
+      edestruct (Hrel j) as (mva & mdf & Hlookup & Hval & Hincl).
+      { rewrite lookup_op lookup_singleton_ne // left_id //. }
+      naive_solver. }
+    simplify_map_eq. rewrite lookup_singleton.
+    (* FIXME simplify_map_eq should have done this *)
+    intros Hbf.
+    edestruct (Hrel k) as (mv & mdf & Hlookup & Hval & Hincl).
+    { rewrite lookup_op lookup_singleton // Some_op_opM //. }
+    rewrite Some_includedN_opM in Hincl.
+    destruct Hincl as [f' Hincl]. rewrite cmra_opM_opM_assoc in Hincl.
+    set f := bf !! k ⋅ f'. (* the complete frame *)
+    change (bf !! k ⋅ f') with f in Hincl.
+    specialize (Hup n mv f). destruct Hup as (Hval' & Hincl').
+    { done. }
+    { rewrite -Hincl. done. }
+    { destruct Hincl as [_ Hincl]. simpl in Hincl. rewrite Hincl.
+      by destruct f. }
+    eexists mv', (dq' ⋅? (fst <$> f)). split; first done.
+    rewrite -Hbf. clear Hbf. split.
+    - rewrite Hincl'. destruct Hval'. by destruct f.
+    - rewrite Some_op_opM. rewrite Some_includedN_opM.
+      exists f'. rewrite Hincl'. 
+      rewrite cmra_opM_opM_assoc. change (bf !! k ⋅ f') with f.
+      by destruct f.
   Qed.
 
-  Lemma gmap_view_update_big m m0 m1 :
-    dom (gset K) m0 = dom (gset K) m1 →
-    gmap_view_auth 1 m ⋅ ([^op map] k↦v ∈ m0, gmap_view_frag k (DfracOwn 1) v) ~~>
-      gmap_view_auth 1 (m1 ∪ m) ⋅ ([^op map] k↦v ∈ m1, gmap_view_frag k (DfracOwn 1) v).
+  (** This derived version cannot exploit [dq = DfracOwn 1]. *)
+  Lemma gmap_view_update_local m k dq mv v mv' v' :
+    m !! k = Some mv →
+    (mv, v) ~l~> (mv', v') →
+    gmap_view_auth (DfracOwn 1) m ⋅ gmap_view_frag k dq v ~~>
+    gmap_view_auth (DfracOwn 1) (<[k := mv']> m) ⋅ gmap_view_frag k dq v'.
+  Proof.
+    intros Hlookup Hup. apply gmap_view_update.
+    intros n mv0 f Hmv0 Hval Hincl.
+    rewrite Hlookup in Hmv0. injection Hmv0 as [= <-].
+    specialize (Hup n (snd <$> f)). destruct Hup as (Hval' & Hincl').
+    { rewrite Hincl. destruct Hval. by destruct f. }
+    { simpl. done. }
+    split; last done. split.
+    - destruct Hval. by destruct f.
+    - simpl in *. replace (((dq, v') ⋅? f).2) with (v' ⋅? (snd <$> f)).
+      2:{ by destruct f. }
+      rewrite -Hincl'. done.
+  Qed.
+
+  Lemma gmap_view_replace m k v v' :
+    ✓ v' →
+    gmap_view_auth (DfracOwn 1) m ⋅ gmap_view_frag k (DfracOwn 1) v ~~>
+      gmap_view_auth (DfracOwn 1) (<[k := v']> m) ⋅ gmap_view_frag k (DfracOwn 1) v'.
+  Proof.
+    (* There would be a simple proof via delete-then-insert... but we use this as a
+       sanity check to make sure the update lemma is strong enough. *)
+    intros Hval'. apply gmap_view_update.
+    intros n mv f Hlookup Hval Hincl.
+    destruct f; simpl.
+    { apply exclusiveN_l in Hval; first done. apply _. }
+    split; last done.
+    split; first done. simpl. apply cmra_valid_validN. done.
+  Qed.
+
+  Lemma gmap_view_replace_big m m0 m1 :
+    dom m0 = dom m1 →
+    map_Forall (λ k v, ✓ v) m1 →
+    gmap_view_auth (DfracOwn 1) m ⋅
+    ([^op map] k↦v ∈ m0, gmap_view_frag k (DfracOwn 1) v) ~~>
+      gmap_view_auth (DfracOwn 1) (m1 ∪ m) ⋅
+      ([^op map] k↦v ∈ m1, gmap_view_frag k (DfracOwn 1) v).
   Proof.
     intros Hdom%eq_sym. revert m1 Hdom.
-    induction m0 as [|k v m0 Hnotdom IH] using map_ind; intros m1 Hdom.
+    induction m0 as [|k v m0 Hnotdom IH] using map_ind; intros m1 Hdom Hval.
     { rewrite dom_empty_L in Hdom.
       apply dom_empty_iff_L in Hdom as ->.
       rewrite left_id_L big_opM_empty. done. }
     rewrite dom_insert_L in Hdom.
-    assert (k ∈ dom (gset K) m1) as Hindom by set_solver.
+    assert (k ∈ dom m1) as Hindom by set_solver.
     apply elem_of_dom in Hindom as [v' Hlookup].
     rewrite big_opM_insert //.
     rewrite [gmap_view_frag _ _ _ ⋅ _]comm assoc.
     rewrite (IH (delete k m1)); last first.
+    { by apply map_Forall_delete. }
     { rewrite dom_delete_L Hdom.
       apply not_elem_of_dom in Hnotdom. set_solver -Hdom. }
     rewrite -assoc [_ ⋅ gmap_view_frag _ _ _]comm assoc.
-    rewrite (gmap_view_update _ _ _ v').
+    rewrite (gmap_view_replace _ _ _ v').
+    2:{ eapply Hval. done. }
     rewrite (big_opM_delete _ m1 k v') // -assoc.
     rewrite insert_union_r; last by rewrite lookup_delete.
     rewrite union_delete_insert //.
   Qed.
 
-  Lemma gmap_view_persist k dq v :
+  Lemma gmap_view_auth_persist dq m :
+    gmap_view_auth dq m ~~> gmap_view_auth DfracDiscarded m.
+  Proof. apply view_update_auth_persist. Qed.
+
+  Lemma gmap_view_auth_unpersist m :
+    gmap_view_auth DfracDiscarded m ~~>: λ a, ∃ q, a = gmap_view_auth (DfracOwn q) m.
+  Proof. apply view_updateP_auth_unpersist. Qed.
+
+  Local Lemma gmap_view_frag_dfrac k dq P v :
+    dq ~~>: P →
+    gmap_view_frag k dq v ~~>: λ a, ∃ dq', a = gmap_view_frag k dq' v ∧ P dq'.
+  Proof.
+    intros Hdq.
+    eapply cmra_updateP_weaken;
+      [apply view_updateP_frag
+         with (P := λ b', ∃ dq', ◯V b' = gmap_view_frag k dq' v ∧ P dq')
+      |naive_solver].
+    intros m n bf Hrel.
+    destruct (Hrel k ((dq, v) ⋅? bf !! k)) as (v' & dq' & Hlookup & Hval & Hincl).
+    { by rewrite lookup_op lookup_singleton Some_op_opM. }
+    rewrite Some_includedN_opM in Hincl.
+    destruct Hincl as [f' Hincl]. rewrite cmra_opM_opM_assoc in Hincl.
+    set f := bf !! k ⋅ f'. (* the complete frame *)
+    change (bf !! k ⋅ f') with f in Hincl.
+    destruct (Hdq n (option_map fst f)) as (dq'' & HPdq'' & Hvdq'').
+    { destruct Hincl as [Heq _]. simpl in Heq. rewrite Heq in Hval.
+      destruct Hval as [Hval _]. by destruct f. }
+    eexists. split; first by exists dq''.
+    intros j [df va] Heq.
+    destruct (decide (k = j)) as [->|Hne].
+    - rewrite lookup_op lookup_singleton in Heq.
+      eexists v', (dq'' ⋅? (fst <$> f)).
+      split; first done. split.
+      + split; last by apply Hval. simpl. done.
+      + rewrite -Heq. exists f'.
+        rewrite -assoc. change (bf !! j ⋅ f') with f.
+        destruct Hincl as [_ Hincl]. simpl in Hincl. rewrite Hincl.
+        by destruct f.
+    - rewrite lookup_op lookup_singleton_ne // left_id in Heq.
+      eapply Hrel. rewrite lookup_op lookup_singleton_ne // left_id Heq //.
+  Qed.
+
+  Lemma gmap_view_frag_persist k dq v :
     gmap_view_frag k dq v ~~> gmap_view_frag k DfracDiscarded v.
   Proof.
-    apply view_update_frag=>m n bf Hrel j [df va] /=.
-    rewrite lookup_op. destruct (decide (j = k)) as [->|Hne].
-    - rewrite lookup_singleton.
-      edestruct (Hrel k ((dq, to_agree v) ⋅? bf !! k)) as (v' & Hdf & Hva & Hm).
-      { rewrite lookup_op lookup_singleton.
-        destruct (bf !! k) eqn:Hbf; by rewrite Hbf. }
-      rewrite Some_op_opM. intros [= Hbf].
-      exists v'. rewrite assoc; split; last done.
-      destruct (bf !! k) as [[df' va']|] eqn:Hbfk; rewrite Hbfk in Hbf; clear Hbfk.
-      + simpl in *. rewrite -pair_op in Hbf.
-        move:Hbf=>[= <- <-]. split; first done.
-        eapply cmra_discrete_valid.
-        eapply (dfrac_discard_update _ _ (Some df')).
-        apply cmra_discrete_valid_iff. done.
-      + simpl in *. move:Hbf=>[= <- <-]. split; done.
-    - rewrite lookup_singleton_ne //.
-      rewrite left_id=>Hbf.
-      edestruct (Hrel j) as (v'' & ? & ? & Hm).
-      { rewrite lookup_op lookup_singleton_ne // left_id. done. }
-      simpl in *. eexists. do 2 (split; first done). done.
+    eapply (cmra_update_lift_updateP (λ dq, gmap_view_frag k dq v)).
+    - intros. by apply gmap_view_frag_dfrac.
+    - apply dfrac_discard_update.
+  Qed.
+
+  Lemma gmap_view_frag_unpersist k v :
+    gmap_view_frag k DfracDiscarded v ~~>:
+      λ a, ∃ q, a = gmap_view_frag k (DfracOwn q) v.
+  Proof.
+    eapply cmra_updateP_weaken.
+    { apply gmap_view_frag_dfrac, dfrac_undiscard_update. }
+    naive_solver.
   Qed.
 
   (** Typeclass instances *)
-  Global Instance gmap_view_frag_core_id k dq v : CoreId dq → CoreId (gmap_view_frag k dq v).
+  Global Instance gmap_view_frag_core_id k dq v :
+    CoreId dq → CoreId v → CoreId (gmap_view_frag k dq v).
   Proof. apply _. Qed.
 
-  Global Instance gmap_view_cmra_discrete : OfeDiscrete V → CmraDiscrete (gmap_viewR K V).
+  Global Instance gmap_view_cmra_discrete :
+    CmraDiscrete V → CmraDiscrete (gmap_viewR K V).
   Proof. apply _. Qed.
 
-  Global Instance gmap_view_frag_mut_is_op dq dq1 dq2 k v :
+  Global Instance gmap_view_frag_mut_is_op dq dq1 dq2 k v v1 v2 :
     IsOp dq dq1 dq2 →
-    IsOp' (gmap_view_frag k dq v) (gmap_view_frag k dq1 v) (gmap_view_frag k dq2 v).
-  Proof. rewrite /IsOp' /IsOp => ->. apply gmap_view_frag_op. Qed.
+    IsOp v v1 v2 →
+    IsOp' (gmap_view_frag k dq v) (gmap_view_frag k dq1 v1) (gmap_view_frag k dq2 v2).
+  Proof. rewrite /IsOp' /IsOp => -> ->. apply gmap_view_frag_op. Qed.
 End lemmas.
 
 (** Functor *)
-Program Definition gmap_viewURF (K : Type) `{Countable K} (F : oFunctor) : urFunctor := {|
-  urFunctor_car A _ B _ := gmap_viewUR K (oFunctor_car F A B);
+Program Definition gmap_viewURF {SI : sidx} (K : Type) `{Countable K}
+    (F : rFunctor) : urFunctor := {|
+  urFunctor_car A _ B _ := gmap_viewUR K (rFunctor_car F A B);
   urFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
-    viewO_map (rel:=gmap_view_rel K (oFunctor_car F A1 B1))
-              (rel':=gmap_view_rel K (oFunctor_car F A2 B2))
-              (gmapO_map (K:=K) (oFunctor_map F fg))
-              (gmapO_map (K:=K) (prodO_map cid (agreeO_map (oFunctor_map F fg))))
+    viewO_map (rel:=gmap_view_rel K (rFunctor_car F A1 B1))
+              (rel':=gmap_view_rel K (rFunctor_car F A2 B2))
+              (gmapO_map (K:=K) (rFunctor_map F fg))
+              (gmapO_map (K:=K) (prodO_map cid (rFunctor_map F fg)))
 |}.
 Next Obligation.
-  intros K ?? F A1 ? A2 ? B1 ? B2 ? n f g Hfg.
+  intros ? K ?? F A1 ? A2 ? B1 ? B2 ? n f g Hfg.
   apply viewO_map_ne.
-  - apply gmapO_map_ne, oFunctor_map_ne. done.
+  - apply gmapO_map_ne, rFunctor_map_ne. done.
   - apply gmapO_map_ne. apply prodO_map_ne; first done.
-    apply agreeO_map_ne, oFunctor_map_ne. done.
+    apply rFunctor_map_ne. done.
 Qed.
 Next Obligation.
-  intros K ?? F A ? B ? x; simpl in *. rewrite -{2}(view_map_id x).
+  intros ? K ? ? F A ? B ? m; simpl in *. rewrite -{2}(view_map_id m).
   apply (view_map_ext _ _ _ _)=> y.
   - rewrite /= -{2}(map_fmap_id y).
-    apply map_fmap_equiv_ext=>k ??.
-    apply oFunctor_map_id.
+    apply: map_fmap_equiv_ext=>k ??.
+    apply rFunctor_map_id.
   - rewrite /= -{2}(map_fmap_id y).
-    apply map_fmap_equiv_ext=>k [df va] ?.
+    apply: map_fmap_equiv_ext=>k [df va] ?.
     split; first done. simpl.
-    rewrite -{2}(agree_map_id va).
-    eapply agree_map_ext; first by apply _.
-    apply oFunctor_map_id.
+    apply rFunctor_map_id.
 Qed.
 Next Obligation.
-  intros K ?? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl in *.
+  intros ? K ?? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' m; simpl in *.
   rewrite -view_map_compose.
   apply (view_map_ext _ _ _ _)=> y.
   - rewrite /= -map_fmap_compose.
-    apply map_fmap_equiv_ext=>k ??.
-    apply oFunctor_map_compose.
+    apply: map_fmap_equiv_ext=>k ??.
+    apply rFunctor_map_compose.
   - rewrite /= -map_fmap_compose.
-    apply map_fmap_equiv_ext=>k [df va] ?.
+    apply: map_fmap_equiv_ext=>k [df va] ?.
     split; first done. simpl.
-    rewrite -agree_map_compose.
-    eapply agree_map_ext; first by apply _.
-    apply oFunctor_map_compose.
+    apply rFunctor_map_compose.
 Qed.
 Next Obligation.
-  intros K ?? F A1 ? A2 ? B1 ? B2 ? fg; simpl.
+  intros ? K ?? F A1 ? A2 ? B1 ? B2 ? fg; simpl.
   (* [apply] does not work, probably the usual unification probem (Coq #6294) *)
-  apply: view_map_cmra_morphism; [apply _..|]=> n m f.
+  eapply @view_map_cmra_morphism; [apply _..|]=> n m f.
   intros Hrel k [df va] Hf. move: Hf.
   rewrite !lookup_fmap.
   destruct (f !! k) as [[df' va']|] eqn:Hfk; rewrite Hfk; last done.
   simpl=>[= <- <-].
-  specialize (Hrel _ _ Hfk). simpl in Hrel. destruct Hrel as (v & Hagree & Hdval & Hm).
-  exists (oFunctor_map F fg v).
-  rewrite Hm. split; last by auto.
-  rewrite Hagree. rewrite agree_map_to_agree. done.
+  specialize (Hrel _ _ Hfk). simpl in Hrel.
+  destruct Hrel as (v & dq & Hlookup & Hval & Hincl).
+  eexists (rFunctor_map F fg v), dq.
+  rewrite Hlookup. split; first done. split.
+  - split; first by apply Hval. simpl. apply: cmra_morphism_validN. apply Hval.
+  - destruct Hincl as [[[fdq fv]|] Hincl].
+    + apply: Some_includedN_mono. rewrite -Some_op in Hincl.
+      apply (inj _) in Hincl. rewrite -pair_op in Hincl.
+      exists (fdq, rFunctor_map F fg fv). rewrite -pair_op.
+      split; first apply Hincl. rewrite -cmra_morphism_op.
+      simpl. f_equiv. apply Hincl.
+    + exists None. rewrite right_id in Hincl. apply (inj _) in Hincl.
+      rewrite right_id. f_equiv. split; first apply Hincl.
+      simpl. f_equiv. apply Hincl.
 Qed.
 
-Global Instance gmap_viewURF_contractive (K : Type) `{Countable K} F :
-  oFunctorContractive F → urFunctorContractive (gmap_viewURF K F).
+Global Instance gmap_viewURF_contractive {SI : sidx} `{Countable K} F :
+  rFunctorContractive F → urFunctorContractive (gmap_viewURF K F).
 Proof.
   intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg.
   apply viewO_map_ne.
-  - apply gmapO_map_ne. apply oFunctor_map_contractive. done.
+  - apply gmapO_map_ne. apply rFunctor_map_contractive. done.
   - apply gmapO_map_ne. apply prodO_map_ne; first done.
-    apply agreeO_map_ne, oFunctor_map_contractive. done.
+    apply rFunctor_map_contractive. done.
 Qed.
 
-Program Definition gmap_viewRF (K : Type) `{Countable K} (F : oFunctor) : rFunctor := {|
-  rFunctor_car A _ B _ := gmap_viewR K (oFunctor_car F A B);
+Program Definition gmap_viewRF {SI : sidx} (K : Type) `{Countable K}
+     (F : rFunctor) : rFunctor := {|
+  rFunctor_car A _ B _ := gmap_viewR K (rFunctor_car F A B);
   rFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
-    viewO_map (rel:=gmap_view_rel K (oFunctor_car F A1 B1))
-              (rel':=gmap_view_rel K (oFunctor_car F A2 B2))
-              (gmapO_map (K:=K) (oFunctor_map F fg))
-              (gmapO_map (K:=K) (prodO_map cid (agreeO_map (oFunctor_map F fg))))
+    viewO_map (rel:=gmap_view_rel K (rFunctor_car F A1 B1))
+              (rel':=gmap_view_rel K (rFunctor_car F A2 B2))
+              (gmapO_map (K:=K) (rFunctor_map F fg))
+              (gmapO_map (K:=K) (prodO_map cid (rFunctor_map F fg)))
 |}.
-Solve Obligations with apply gmap_viewURF.
+Solve Obligations with apply @gmap_viewURF.
 
-Global Instance gmap_viewRF_contractive (K : Type) `{Countable K} F :
-  oFunctorContractive F → rFunctorContractive (gmap_viewRF K F).
+Global Instance gmap_viewRF_contractive {SI : sidx} `{Countable K} F :
+  rFunctorContractive F → rFunctorContractive (gmap_viewRF K F).
 Proof. apply gmap_viewURF_contractive. Qed.
 
-Typeclasses Opaque gmap_view_auth gmap_view_frag.
+Global Typeclasses Opaque gmap_view_auth gmap_view_frag.

iris/algebra/lib/gset_bij.v

@@ -16,7 +16,7 @@ From iris.algebra Require Import updates.
 From iris.prelude Require Import options.
 
 Section gset_bijective.
-  Context `{Countable A, Countable B}.
+  Context {SI : sidx} `{Countable A, Countable B}.
   Implicit Types (a : A) (b : B).
 
   (** [gset_bijective] states that for a graph [L] of [(a, b)] pairs, [L] maps
@@ -59,17 +59,17 @@ Section gset_bijective.
 End gset_bijective.
 
 Section gset_bij_view_rel.
-  Context `{Countable A, Countable B}.
+  Context {SI : sidx} `{Countable A, Countable B}.
   Implicit Types (bijL : gset (A * B)) (L : gsetUR (A * B)).
 
-  Local Definition gset_bij_view_rel_raw (n : nat) bijL L: Prop :=
+  Local Definition gset_bij_view_rel_raw (n : SI) bijL L: Prop :=
     L ⊆ bijL ∧ gset_bijective bijL.
 
   Local Lemma gset_bij_view_rel_raw_mono n1 n2 bijL1 bijL2 L1 L2 :
     gset_bij_view_rel_raw n1 bijL1 L1 →
     bijL1 ≡{n2}≡ bijL2 →
     L2 ≼{n2} L1 →
-    n2 ≤ n1 →
+    (n2 ≤ n1)%sidx →
     gset_bij_view_rel_raw n2 bijL2 L2.
   Proof.
     intros [??] <-%(discrete_iff _ _)%leibniz_equiv ?%gset_included _.
@@ -96,23 +96,24 @@ Section gset_bij_view_rel.
   Proof. done. Qed.
 End gset_bij_view_rel.
 
-Definition gset_bij A B `{Countable A, Countable B} :=
+Definition gset_bij {SI : sidx} A B `{Countable A, Countable B} :=
   view (gset_bij_view_rel_raw (A:=A) (B:=B)).
-Definition gset_bijO A B `{Countable A, Countable B} : ofe :=
+Definition gset_bijO {SI : sidx} A B `{Countable A, Countable B} : ofe :=
   viewO (gset_bij_view_rel (A:=A) (B:=B)).
-Definition gset_bijR A B `{Countable A, Countable B} : cmra :=
+Definition gset_bijR {SI : sidx} A B `{Countable A, Countable B} : cmra :=
   viewR (gset_bij_view_rel (A:=A) (B:=B)).
-Definition gset_bijUR A B `{Countable A, Countable B} : ucmra :=
+Definition gset_bijUR {SI : sidx} A B `{Countable A, Countable B} : ucmra :=
   viewUR (gset_bij_view_rel (A:=A) (B:=B)).
 
-Definition gset_bij_auth `{Countable A, Countable B}
+Definition gset_bij_auth {SI : sidx} `{Countable A, Countable B}
   (dq : dfrac) (L : gset (A * B)) : gset_bij A B := ●V{dq} L ⋅ ◯V L.
-Definition gset_bij_elem `{Countable A, Countable B}
+Definition gset_bij_elem {SI : sidx} `{Countable A, Countable B}
   (a : A) (b : B) : gset_bij A B := ◯V {[ (a, b) ]}.
 
+
 Section gset_bij.
-  Context `{Countable A, Countable B}.
-  Implicit Types (a:A) (b:B).
+  Context {SI : sidx} `{Countable A, Countable B}.
+  Implicit Types (a : A) (b : B).
   Implicit Types (L : gset (A*B)).
   Implicit Types dq : dfrac.
 
@@ -130,8 +131,7 @@ Section gset_bij.
   Lemma gset_bij_auth_dfrac_valid dq L : ✓ gset_bij_auth dq L ↔ ✓ dq ∧ gset_bijective L.
   Proof.
     rewrite /gset_bij_auth view_both_dfrac_valid.
-    setoid_rewrite gset_bij_view_rel_iff.
-    naive_solver eauto using O.
+    setoid_rewrite gset_bij_view_rel_iff. pose 0ᵢ. naive_solver.
   Qed.
   Lemma gset_bij_auth_valid L : ✓ gset_bij_auth (DfracOwn 1) L ↔ gset_bijective L.
   Proof. rewrite gset_bij_auth_dfrac_valid. naive_solver by done. Qed.
@@ -150,7 +150,7 @@ Section gset_bij.
     rewrite /gset_bij_auth (comm _ (●V{dq2} _)) -!assoc (assoc _ (◯V _)).
     rewrite -view_frag_op (comm _ (◯V _)) assoc. split.
     - move=> /cmra_valid_op_l /view_auth_dfrac_op_valid.
-      setoid_rewrite gset_bij_view_rel_iff. naive_solver eauto using 0.
+      setoid_rewrite gset_bij_view_rel_iff. pose 0ᵢ. naive_solver.
     - intros (?&->&?). rewrite -core_id_dup -view_auth_dfrac_op.
       apply view_both_dfrac_valid. setoid_rewrite gset_bij_view_rel_iff. naive_solver.
   Qed.
@@ -162,8 +162,7 @@ Section gset_bij.
     ✓ (gset_bij_auth dq L ⋅ gset_bij_elem a b) ↔ ✓ dq ∧ gset_bijective L ∧ (a, b) ∈ L.
   Proof.
     rewrite /gset_bij_auth /gset_bij_elem -assoc -view_frag_op view_both_dfrac_valid.
-    setoid_rewrite gset_bij_view_rel_iff.
-    set_solver by eauto using O.
+    setoid_rewrite gset_bij_view_rel_iff. pose 0ᵢ. set_solver.
   Qed.
   Lemma bij_both_valid L a b :
     ✓ (gset_bij_auth (DfracOwn 1) L ⋅ gset_bij_elem a b) ↔ gset_bijective L ∧ (a, b) ∈ L.
@@ -174,7 +173,7 @@ Section gset_bij.
   Proof.
     rewrite /gset_bij_elem -view_frag_op gset_op view_frag_valid.
     setoid_rewrite gset_bij_view_rel_iff. intros. apply gset_bijective_pair.
-    naive_solver eauto using subseteq_gset_bijective, O.
+    pose 0ᵢ. naive_solver eauto using subseteq_gset_bijective.
   Qed.
 
   Lemma bij_view_included dq L a b :

iris/algebra/lib/mono_Z.v

+From iris.algebra Require Export auth.
+From iris.algebra Require Import numbers updates.
+From iris.prelude Require Import options.
+
+(** Authoritative CMRA over [max_Z]. The authoritative element is a
+monotonically increasing [Z], while a fragment is a lower bound. *)
+
+Definition mono_Z   {SI: sidx} := auth (option max_ZR).
+Definition mono_ZR  {SI: sidx} := authR (optionUR max_ZR).
+Definition mono_ZUR {SI: sidx} := authUR (optionUR max_ZR).
+
+(** [mono_Z_auth] is the authoritative element. The definition includes the
+fragment at the same value so that lemma [mono_Z_included], which states that
+[mono_Z_lb n ≼ mono_Z_auth dq n], holds. Without this trick, a frame-preserving
+update lemma would be required instead. *)
+Definition mono_Z_auth {SI : sidx} (dq : dfrac) (n : Z) : mono_Z :=
+  ●{dq} (Some (MaxZ n)) ⋅ ◯ (Some (MaxZ n)).
+Definition mono_Z_lb {SI : sidx} (n : Z) : mono_Z := ◯ (Some (MaxZ n)).
+
+Notation "●MZ dq a" := (mono_Z_auth dq a)
+  (at level 20, dq custom dfrac at level 1, format "●MZ dq  a").
+Notation "◯MZ a" := (mono_Z_lb a) (at level 20).
+
+Section mono_Z.
+  Context {SI : sidx}.
+  Implicit Types (n : Z).
+
+  Local Open Scope Z_scope.
+
+  Global Instance mono_Z_lb_core_id n : CoreId (◯MZ n).
+  Proof. apply _. Qed.
+  Global Instance mono_Z_auth_core_id l : CoreId (●MZ□ l).
+  Proof. apply _. Qed.
+
+  Lemma mono_Z_auth_dfrac_op dq1 dq2 n :
+    ●MZ{dq1 ⋅ dq2} n ≡ ●MZ{dq1} n ⋅ ●MZ{dq2} n.
+  Proof.
+    rewrite /mono_Z_auth auth_auth_dfrac_op.
+    rewrite (comm _ (●{dq2} _)) -!assoc (assoc _ (◯ _)).
+    by rewrite -core_id_dup (comm _ (◯ _)).
+  Qed.
+
+  Lemma mono_Z_lb_op n1 n2 :
+    ◯MZ (n1 `max` n2) = ◯MZ n1 ⋅ ◯MZ n2.
+  Proof. rewrite -auth_frag_op -Some_op max_Z_op //. Qed.
+
+  Lemma mono_Z_auth_lb_op dq n :
+    ●MZ{dq} n ≡ ●MZ{dq} n ⋅ ◯MZ n.
+  Proof.
+    rewrite /mono_Z_auth /mono_Z_lb.
+    rewrite -!assoc -auth_frag_op -Some_op max_Z_op.
+    rewrite Z.max_id //.
+  Qed.
+
+  Global Instance mono_Z_auth_dfrac_is_op dq dq1 dq2 n :
+    IsOp dq dq1 dq2 → IsOp' (●MZ{dq} n) (●MZ{dq1} n) (●MZ{dq2} n).
+  Proof. rewrite /IsOp' /IsOp=> ->. rewrite mono_Z_auth_dfrac_op //. Qed.
+  Global Instance mono_Z_lb_max_is_op n n1 n2 :
+    IsOp (MaxZ n) (MaxZ n1) (MaxZ n2) → IsOp' (◯MZ n) (◯MZ n1) (◯MZ n2).
+  Proof. rewrite /IsOp' /IsOp /mono_Z_lb=> ->. done. Qed.
+
+  (** rephrasing of [mono_Z_lb_op] useful for weakening a fragment to a
+  smaller lower-bound *)
+  Lemma mono_Z_lb_op_le_l n n' :
+    n' ≤ n →
+    ◯MZ n = ◯MZ n' ⋅ ◯MZ n.
+  Proof. intros. rewrite -mono_Z_lb_op Z.max_r //. Qed.
+
+  Lemma mono_Z_auth_dfrac_valid dq n : (✓ ●MZ{dq} n) ↔ ✓ dq.
+  Proof.
+    rewrite /mono_Z_auth auth_both_dfrac_valid_discrete /=. naive_solver.
+  Qed.
+  Lemma mono_Z_auth_valid n : ✓ ●MZ n.
+  Proof. by apply auth_both_valid. Qed.
+
+  Lemma mono_Z_auth_dfrac_op_valid dq1 dq2 n1 n2 :
+    ✓ (●MZ{dq1} n1 ⋅ ●MZ{dq2} n2) ↔ ✓ (dq1 ⋅ dq2) ∧ n1 = n2.
+  Proof.
+    rewrite /mono_Z_auth (comm _ (●{dq2} _)) -!assoc (assoc _ (◯ _)).
+    rewrite -auth_frag_op (comm _ (◯ _)) assoc. split.
+    - move=> /cmra_valid_op_l /auth_auth_dfrac_op_valid. naive_solver.
+    - intros [? ->]. rewrite -core_id_dup -auth_auth_dfrac_op.
+      by apply auth_both_dfrac_valid_discrete.
+  Qed.
+  Lemma mono_Z_auth_op_valid n1 n2 :
+    ✓ (●MZ n1 ⋅ ●MZ n2) ↔ False.
+  Proof. rewrite mono_Z_auth_dfrac_op_valid. naive_solver. Qed.
+
+  Lemma mono_Z_both_dfrac_valid dq n m :
+    ✓ (●MZ{dq} n ⋅ ◯MZ m) ↔ ✓ dq ∧ m ≤ n.
+  Proof.
+    rewrite /mono_Z_auth /mono_Z_lb -assoc -auth_frag_op.
+    rewrite auth_both_dfrac_valid_discrete Some_included_total max_Z_included /=.
+    naive_solver lia.
+  Qed.
+  Lemma mono_Z_both_valid n m :
+    ✓ (●MZ n ⋅ ◯MZ m) ↔ m ≤ n.
+  Proof. rewrite mono_Z_both_dfrac_valid dfrac_valid_own. naive_solver. Qed.
+
+  Lemma mono_Z_lb_mono n1 n2 : n1 ≤ n2 → ◯MZ n1 ≼ ◯MZ n2.
+  Proof.
+    intros. by apply auth_frag_mono, Some_included_total, max_Z_included.
+  Qed.
+
+  Lemma mono_Z_included dq n : ◯MZ n ≼ ●MZ{dq} n.
+  Proof. apply: cmra_included_r. Qed.
+
+  Lemma mono_Z_update {n} n' :
+    n ≤ n' → ●MZ n ~~> ●MZ n'.
+  Proof.
+    intros. rewrite /mono_Z_auth /mono_Z_lb.
+    by apply auth_update, option_local_update, max_Z_local_update.
+  Qed.
+
+  Lemma mono_Z_auth_persist n dq :
+    ●MZ{dq} n ~~> ●MZ□ n.
+  Proof.
+    intros. rewrite /mono_Z_auth /mono_Z_lb.
+    eapply cmra_update_op_proper; last done.
+    eapply auth_update_auth_persist.
+  Qed.
+  Lemma mono_Z_auth_unpersist n :
+    ●MZ□ n ~~>: λ k, ∃ q, k = ●MZ{# q} n.
+  Proof. eapply auth_updateP_both_unpersist. Qed.
+End mono_Z.
+
+Global Typeclasses Opaque mono_Z_auth mono_Z_lb.

iris_staging/algebra/mono_list.v → iris/algebra/lib/mono_list.v

-(* This file is still experimental. See its tracking issue
-https://gitlab.mpi-sws.org/iris/iris/-/issues/415 for details on remaining
-issues before stabilization. *)
-From iris.algebra Require Export auth dfrac max_prefix_list.
-From iris.algebra Require Import updates local_updates proofmode_classes.
-From iris.prelude Require Import options.
-
 (** Authoritative CMRA of append-only lists, where the fragment represents a
   snap-shot of the list, and the authoritative element can only grow by
   appending. *)
+From iris.algebra Require Export auth dfrac max_prefix_list.
+From iris.algebra Require Import updates local_updates proofmode_classes.
+From iris.prelude Require Import options.
 
-Definition mono_listR (A : ofe) : cmra  := authR (max_prefix_listUR A).
-Definition mono_listUR (A : ofe) : ucmra  := authUR (max_prefix_listUR A).
+Definition mono_listR {SI : sidx} (A : ofe) : cmra := authR (max_prefix_listUR A).
+Definition mono_listUR {SI : sidx} (A : ofe) : ucmra := authUR (max_prefix_listUR A).
 
-Definition mono_list_auth {A : ofe} (q : dfrac) (l : list A) : mono_listR A :=
+Definition mono_list_auth {SI : sidx}
+    {A : ofe} (q : dfrac) (l : list A) : mono_listR A :=
   ●{q} (to_max_prefix_list l) ⋅ ◯ (to_max_prefix_list l).
-Definition mono_list_lb {A : ofe} (l : list A) : mono_listR A :=
+Definition mono_list_lb {SI : sidx} {A : ofe} (l : list A) : mono_listR A :=
   ◯ (to_max_prefix_list l).
-Global Instance: Params (@mono_list_auth) 2 := {}.
-Global Instance: Params (@mono_list_lb) 1 := {}.
-Typeclasses Opaque mono_list_auth mono_list_lb.
-
-(** FIXME: Refactor these notations using custom entries once Coq bug #13654
-has been fixed. *)
-Notation "●ML{ dq } l" :=
-  (mono_list_auth dq l) (at level 20, format "●ML{ dq }  l").
-Notation "●ML{# q } l" :=
-  (mono_list_auth (DfracOwn q) l) (at level 20, format "●ML{# q }  l").
-Notation "●□ML l" := (mono_list_auth DfracDiscarded l) (at level 20).
-Notation "●ML l" := (mono_list_auth (DfracOwn 1) l) (at level 20).
+Global Instance: Params (@mono_list_auth) 3 := {}.
+Global Instance: Params (@mono_list_lb) 2 := {}.
+Global Typeclasses Opaque mono_list_auth mono_list_lb.
+
+Notation "●ML dq l" := (mono_list_auth dq l)
+  (at level 20, dq custom dfrac at level 1, format "●ML dq  l").
 Notation "◯ML l" := (mono_list_lb l) (at level 20).
 
 Section mono_list_props.
-  Context {A : ofe}.
+  Context {SI : sidx} {A : ofe}.
   Implicit Types l : list A.
   Implicit Types q : frac.
   Implicit Types dq : dfrac.
 
   (** Setoid properties *)
-  Global Instance mono_list_auth_ne dq : NonExpansive (@mono_list_auth A dq).
+  Global Instance mono_list_auth_ne dq : NonExpansive (@mono_list_auth SI A dq).
   Proof. solve_proper. Qed.
-  Global Instance mono_list_auth_proper dq : Proper ((≡) ==> (≡)) (@mono_list_auth A dq).
+  Global Instance mono_list_auth_proper dq :
+    Proper ((≡) ==> (≡)) (@mono_list_auth SI A dq).
   Proof. solve_proper. Qed.
-  Global Instance mono_list_lb_ne : NonExpansive (@mono_list_lb A).
+  Global Instance mono_list_lb_ne : NonExpansive (@mono_list_lb SI A).
   Proof. solve_proper. Qed.
-  Global Instance mono_list_lb_proper : Proper ((≡) ==> (≡)) (@mono_list_lb A).
+  Global Instance mono_list_lb_proper : Proper ((≡) ==> (≡)) (@mono_list_lb SI A).
   Proof. solve_proper. Qed.
 
-  Global Instance mono_list_lb_dist_inj n : Inj (dist n) (dist n) (@mono_list_lb A).
+  Global Instance mono_list_lb_dist_inj n :
+    Inj (dist n) (dist n) (@mono_list_lb SI A).
   Proof. rewrite /mono_list_lb. by intros ?? ?%(inj _)%(inj _). Qed.
-  Global Instance mono_list_lb_inj : Inj (≡) (≡) (@mono_list_lb A).
+  Global Instance mono_list_lb_inj : Inj (≡) (≡) (@mono_list_lb SI A).
   Proof. rewrite /mono_list_lb. by intros ?? ?%(inj _)%(inj _). Qed.
 
   (** * Operation *)
   Global Instance mono_list_lb_core_id l : CoreId (◯ML l).
   Proof. rewrite /mono_list_lb. apply _. Qed.
+  Global Instance mono_list_auth_core_id l : CoreId (●ML□ l).
+  Proof. rewrite /mono_list_auth. apply _. Qed.
 
   Lemma mono_list_auth_dfrac_op dq1 dq2 l :
     ●ML{dq1 ⋅ dq2} l ≡ ●ML{dq1} l ⋅ ●ML{dq2} l.
@@ -62,9 +57,6 @@ Section mono_list_props.
     rewrite (comm _ (●{dq2} _)) -!assoc (assoc _ (◯ _)).
     by rewrite -core_id_dup (comm _ (◯ _)).
   Qed.
-  Lemma mono_list_auth_frac_op q1 q2 l :
-    ●ML{#(q1 + q2)} l ≡ ●ML{#q1} l ⋅ ●ML{#q2} l.
-  Proof. by rewrite -mono_list_auth_dfrac_op dfrac_op_own. Qed.
 
   Lemma mono_list_lb_op_l l1 l2 : l1 `prefix_of` l2 → ◯ML l1 ⋅ ◯ML l2 ≡ ◯ML l2.
   Proof. intros ?. by rewrite /mono_list_lb -auth_frag_op to_max_prefix_list_op_l. Qed.
@@ -75,8 +67,9 @@ Section mono_list_props.
     by rewrite /mono_list_auth /mono_list_lb -!assoc -auth_frag_op -core_id_dup.
   Qed.
 
-  Global Instance mono_list_lb_is_op l : IsOp' (◯ML l) (◯ML l) (◯ML l).
-  Proof. by rewrite /IsOp' /IsOp -core_id_dup. Qed.
+  Global Instance mono_list_auth_dfrac_is_op dq dq1 dq2 l :
+    IsOp dq dq1 dq2 → IsOp' (●ML{dq} l) (●ML{dq1} l) (●ML{dq2} l).
+  Proof. rewrite /IsOp' /IsOp=> ->. rewrite mono_list_auth_dfrac_op //. Qed.
 
   (** * Validity *)
   Lemma mono_list_auth_dfrac_validN n dq l : ✓{n} (●ML{dq} l) ↔ ✓ dq.
@@ -105,9 +98,6 @@ Section mono_list_props.
     - intros [? ->]. rewrite -core_id_dup -auth_auth_dfrac_op auth_both_dfrac_validN.
       naive_solver apply to_max_prefix_list_validN.
   Qed.
-  Lemma mono_list_auth_frac_op_validN n q1 q2 l1 l2 :
-    ✓{n} (●ML{#q1} l1 ⋅ ●ML{#q2} l2) ↔ (q1 + q2 ≤ 1)%Qp ∧ l1 ≡{n}≡ l2.
-  Proof. by apply mono_list_auth_dfrac_op_validN. Qed.
   Lemma mono_list_auth_op_validN n l1 l2 : ✓{n} (●ML l1 ⋅ ●ML l2) ↔ False.
   Proof. rewrite mono_list_auth_dfrac_op_validN. naive_solver. Qed.
 
@@ -115,20 +105,14 @@ Section mono_list_props.
     ✓ (●ML{dq1} l1 ⋅ ●ML{dq2} l2) ↔ ✓ (dq1 ⋅ dq2) ∧ l1 ≡ l2.
   Proof.
     rewrite cmra_valid_validN equiv_dist.
-    setoid_rewrite mono_list_auth_dfrac_op_validN. naive_solver eauto using O.
+    setoid_rewrite mono_list_auth_dfrac_op_validN. pose 0ᵢ. naive_solver.
   Qed.
-  Lemma mono_list_auth_frac_op_valid q1 q2 l1 l2 :
-    ✓ (●ML{#q1} l1 ⋅ ●ML{#q2} l2) ↔ (q1 + q2 ≤ 1)%Qp ∧ l1 ≡ l2.
-  Proof. by apply mono_list_auth_dfrac_op_valid. Qed.
   Lemma mono_list_auth_op_valid l1 l2 : ✓ (●ML l1 ⋅ ●ML l2) ↔ False.
   Proof. rewrite mono_list_auth_dfrac_op_valid. naive_solver. Qed.
 
   Lemma mono_list_auth_dfrac_op_valid_L `{!LeibnizEquiv A} dq1 dq2 l1 l2 :
     ✓ (●ML{dq1} l1 ⋅ ●ML{dq2} l2) ↔ ✓ (dq1 ⋅ dq2) ∧ l1 = l2.
   Proof. unfold_leibniz. apply mono_list_auth_dfrac_op_valid. Qed.
-  Lemma mono_list_auth_frac_op_valid_L `{!LeibnizEquiv A} q1 q2 l1 l2 :
-    ✓ (●ML{#q1} l1 ⋅ ●ML{#q2} l2) ↔ (q1 + q2 ≤ 1)%Qp ∧ l1 = l2.
-  Proof. unfold_leibniz. apply mono_list_auth_frac_op_valid. Qed.
 
   Lemma mono_list_both_dfrac_validN n dq l1 l2 :
     ✓{n} (●ML{dq} l1 ⋅ ◯ML l2) ↔ ✓ dq ∧ ∃ l, l1 ≡{n}≡ l2 ++ l.
@@ -192,9 +176,26 @@ Section mono_list_props.
   (** * Update *)
   Lemma mono_list_update {l1} l2 : l1 `prefix_of` l2 → ●ML l1 ~~> ●ML l2.
   Proof. intros ?. by apply auth_update, max_prefix_list_local_update. Qed.
-  Lemma mono_list_update_auth_persist dq l : ●ML{dq} l ~~> ●□ML l.
+  Lemma mono_list_auth_persist dq l : ●ML{dq} l ~~> ●ML□ l.
   Proof.
     rewrite /mono_list_auth. apply cmra_update_op; [|done].
     by apply auth_update_auth_persist.
   Qed.
+  Lemma mono_list_auth_unpersist l :
+    ●ML□ l ~~>: λ k, ∃ q, k = ●ML{#q} l.
+  Proof. eapply auth_updateP_both_unpersist. Qed.
 End mono_list_props.
+
+Definition mono_listURF {SI : sidx} (F : oFunctor) : urFunctor :=
+  authURF (max_prefix_listURF F).
+
+Global Instance mono_listURF_contractive {SI : sidx} F :
+  oFunctorContractive F → urFunctorContractive (mono_listURF F).
+Proof. apply _. Qed.
+
+Definition mono_listRF {SI : sidx} (F : oFunctor) : rFunctor :=
+  authRF (max_prefix_listURF F).
+
+Global Instance mono_listRF_contractive {SI : sidx} F :
+  oFunctorContractive F → rFunctorContractive (mono_listRF F).
+Proof. apply _. Qed.

iris/algebra/lib/mono_nat.v

@@ -5,95 +5,119 @@ From iris.prelude Require Import options.
 (** Authoritative CMRA over [max_nat]. The authoritative element is a
 monotonically increasing [nat], while a fragment is a lower bound. *)
 
-Definition mono_nat   := auth max_natUR.
-Definition mono_natR  := authR max_natUR.
-Definition mono_natUR := authUR max_natUR.
+Definition mono_nat {SI : sidx}  := auth max_natUR.
+Definition mono_natR {SI : sidx} := authR max_natUR.
+Definition mono_natUR {SI : sidx} := authUR max_natUR.
 
 (** [mono_nat_auth] is the authoritative element. The definition includes the
 fragment at the same value so that lemma [mono_nat_included], which states that
-[mono_nat_lb n ≼ mono_nat_auth q n], does not require a frame-preserving
-update. *)
-Definition mono_nat_auth (q : Qp) (n : nat) : mono_nat :=
-  ●{#q} MaxNat n ⋅ ◯ MaxNat n.
-Definition mono_nat_lb (n : nat) : mono_nat := ◯ MaxNat n.
+[mono_nat_lb n ≼ mono_nat_auth dq n], holds. Without this trick, a
+frame-preserving update lemma would be required instead. *)
+Definition mono_nat_auth {SI : sidx} (dq : dfrac) (n : nat) : mono_nat :=
+  ●{dq} MaxNat n ⋅ ◯ MaxNat n.
+Definition mono_nat_lb {SI : sidx} (n : nat) : mono_nat := ◯ MaxNat n.
+
+Notation "●MN dq a" := (mono_nat_auth dq a)
+  (at level 20, dq custom dfrac at level 1, format "●MN dq  a").
+Notation "◯MN a" := (mono_nat_lb a) (at level 20).
 
 Section mono_nat.
+  Context {SI : sidx}.
   Implicit Types (n : nat).
 
-  Global Instance mono_nat_lb_core_id n : CoreId (mono_nat_lb n).
+  Global Instance mono_nat_lb_core_id n : CoreId (◯MN n).
+  Proof. apply _. Qed.
+  Global Instance mono_nat_auth_core_id l : CoreId (●MN□ l).
   Proof. apply _. Qed.
 
-  Lemma mono_nat_auth_frac_op q1 q2 n :
-    mono_nat_auth q1 n ⋅ mono_nat_auth q2 n ≡ mono_nat_auth (q1 + q2) n.
+  Lemma mono_nat_auth_dfrac_op dq1 dq2 n :
+    ●MN{dq1 ⋅ dq2} n ≡ ●MN{dq1} n ⋅ ●MN{dq2} n.
   Proof.
-    rewrite /mono_nat_auth -dfrac_op_own auth_auth_dfrac_op.
-    rewrite (comm _ (●{#q2} _)) -!assoc (assoc _ (◯ _)).
+    rewrite /mono_nat_auth auth_auth_dfrac_op.
+    rewrite (comm _ (●{dq2} _)) -!assoc (assoc _ (◯ _)).
     by rewrite -core_id_dup (comm _ (◯ _)).
   Qed.
 
   Lemma mono_nat_lb_op n1 n2 :
-    mono_nat_lb n1 ⋅ mono_nat_lb n2 = mono_nat_lb (n1 `max` n2).
+    ◯MN (n1 `max` n2) = ◯MN n1 ⋅ ◯MN n2.
   Proof. rewrite -auth_frag_op max_nat_op //. Qed.
 
-  Lemma mono_nat_auth_lb_op q n :
-    mono_nat_auth q n ≡ mono_nat_auth q n ⋅ mono_nat_lb n.
+  Lemma mono_nat_auth_lb_op dq n :
+    ●MN{dq} n ≡ ●MN{dq} n ⋅ ◯MN n.
   Proof.
     rewrite /mono_nat_auth /mono_nat_lb.
     rewrite -!assoc -auth_frag_op max_nat_op.
     rewrite Nat.max_id //.
   Qed.
 
+  Global Instance mono_nat_auth_dfrac_is_op dq dq1 dq2 n :
+    IsOp dq dq1 dq2 → IsOp' (●MN{dq} n) (●MN{dq1} n) (●MN{dq2} n).
+  Proof. rewrite /IsOp' /IsOp=> ->. rewrite mono_nat_auth_dfrac_op //. Qed.
+  Global Instance mono_nat_lb_max_is_op n n1 n2 :
+    IsOp (MaxNat n) (MaxNat n1) (MaxNat n2) → IsOp' (◯MN n) (◯MN n1) (◯MN n2).
+  Proof. rewrite /IsOp' /IsOp /mono_nat_lb=> ->. done. Qed.
+
   (** rephrasing of [mono_nat_lb_op] useful for weakening a fragment to a
   smaller lower-bound *)
   Lemma mono_nat_lb_op_le_l n n' :
     n' ≤ n →
-    mono_nat_lb n = mono_nat_lb n' ⋅ mono_nat_lb n.
-  Proof. intros. rewrite mono_nat_lb_op Nat.max_r //. Qed.
+    ◯MN n = ◯MN n' ⋅ ◯MN n.
+  Proof. intros. rewrite -mono_nat_lb_op Nat.max_r //. Qed.
 
-  Lemma mono_nat_auth_frac_valid q n : ✓ mono_nat_auth q n ↔ (q ≤ 1)%Qp.
+  Lemma mono_nat_auth_dfrac_valid dq n : (✓ ●MN{dq} n) ↔ ✓ dq.
   Proof.
     rewrite /mono_nat_auth auth_both_dfrac_valid_discrete /=. naive_solver.
   Qed.
-  Lemma mono_nat_auth_valid n : ✓ mono_nat_auth 1 n.
+  Lemma mono_nat_auth_valid n : ✓ ●MN n.
   Proof. by apply auth_both_valid. Qed.
 
-  Lemma mono_nat_auth_frac_op_valid q1 q2 n1 n2 :
-    ✓ (mono_nat_auth q1 n1 ⋅ mono_nat_auth q2 n2) ↔ (q1 + q2 ≤ 1)%Qp ∧ n1 = n2.
+  Lemma mono_nat_auth_dfrac_op_valid dq1 dq2 n1 n2 :
+    ✓ (●MN{dq1} n1 ⋅ ●MN{dq2} n2) ↔ ✓ (dq1 ⋅ dq2) ∧ n1 = n2.
   Proof.
-    rewrite /mono_nat_auth (comm _ (●{#q2} _)) -!assoc (assoc _ (◯ _)).
+    rewrite /mono_nat_auth (comm _ (●{dq2} _)) -!assoc (assoc _ (◯ _)).
     rewrite -auth_frag_op (comm _ (◯ _)) assoc. split.
     - move=> /cmra_valid_op_l /auth_auth_dfrac_op_valid. naive_solver.
     - intros [? ->]. rewrite -core_id_dup -auth_auth_dfrac_op.
       by apply auth_both_dfrac_valid_discrete.
   Qed.
   Lemma mono_nat_auth_op_valid n1 n2 :
-    ✓ (mono_nat_auth 1 n1 ⋅ mono_nat_auth 1 n2) ↔ False.
-  Proof. rewrite mono_nat_auth_frac_op_valid. naive_solver. Qed.
+    ✓ (●MN n1 ⋅ ●MN n2) ↔ False.
+  Proof. rewrite mono_nat_auth_dfrac_op_valid. naive_solver. Qed.
 
-  Lemma mono_nat_both_frac_valid q n m :
-    ✓ (mono_nat_auth q n ⋅ mono_nat_lb m) ↔ (q ≤ 1)%Qp ∧ m ≤ n.
+  Lemma mono_nat_both_dfrac_valid dq n m :
+    ✓ (●MN{dq} n ⋅ ◯MN m) ↔ ✓ dq ∧ m ≤ n.
   Proof.
     rewrite /mono_nat_auth /mono_nat_lb -assoc -auth_frag_op.
     rewrite auth_both_dfrac_valid_discrete max_nat_included /=.
     naive_solver lia.
   Qed.
   Lemma mono_nat_both_valid n m :
-    ✓ (mono_nat_auth 1 n ⋅ mono_nat_lb m) ↔ m ≤ n.
-  Proof. rewrite mono_nat_both_frac_valid. naive_solver. Qed.
+    ✓ (●MN n ⋅ ◯MN m) ↔ m ≤ n.
+  Proof. rewrite mono_nat_both_dfrac_valid dfrac_valid_own. naive_solver. Qed.
 
-  Lemma mono_nat_lb_mono n1 n2 : n1 ≤ n2 → mono_nat_lb n1 ≼ mono_nat_lb n2.
+  Lemma mono_nat_lb_mono n1 n2 : n1 ≤ n2 → ◯MN n1 ≼ ◯MN n2.
   Proof. intros. by apply auth_frag_mono, max_nat_included. Qed.
 
-  Lemma mono_nat_included q n : mono_nat_lb n ≼ mono_nat_auth q n.
+  Lemma mono_nat_included dq n : ◯MN n ≼ ●MN{dq} n.
   Proof. apply cmra_included_r. Qed.
 
   Lemma mono_nat_update {n} n' :
-    n ≤ n' →
-    mono_nat_auth 1 n ~~> mono_nat_auth 1 n'.
+    n ≤ n' → ●MN n ~~> ●MN n'.
   Proof.
     intros. rewrite /mono_nat_auth /mono_nat_lb.
     by apply auth_update, max_nat_local_update.
   Qed.
+
+  Lemma mono_nat_auth_persist n dq :
+    ●MN{dq} n ~~> ●MN□ n.
+  Proof.
+    intros. rewrite /mono_nat_auth /mono_nat_lb.
+    eapply cmra_update_op_proper; last done.
+    eapply auth_update_auth_persist.
+  Qed.
+  Lemma mono_nat_auth_unpersist n :
+    ●MN□ n ~~>: λ k, ∃ q, k = ●MN{# q} n.
+  Proof. eapply auth_updateP_both_unpersist. Qed.
 End mono_nat.
 
-Typeclasses Opaque mono_nat_auth mono_nat_lb.
+Global Typeclasses Opaque mono_nat_auth mono_nat_lb.

iris/algebra/lib/ufrac_auth.v

@@ -9,20 +9,20 @@ difference:
   if we have the authoritative element we can always increase its fraction
   and allocate a new fragment.
 
-  <<<
-  ✓ (a ⋅ b) → ●U{p} a ~~> ●U{p + q} (a ⋅ b) ⋅ ◯U{q} b
-  >>>
+<<
+✓ (a ⋅ b) → ●U_p a ~~> ●U_(p + q) (a ⋅ b) ⋅ ◯U_q b
+>>
 
-- We no longer have the [◯U{1} a] is the exclusive fragmental element (cf.
-  [frac_auth_frag_validN_op_1_l]).
+- We no longer have the [◯U_1 a] is an exclusive fragmental element. That is,
+  while [◯F{1} a ⋅ ◯F{q} b] is vacuously false, [◯U_1 a ⋅ ◯U_q2 b] is not.
 *)
 From iris.algebra Require Export auth frac updates local_updates.
 From iris.algebra Require Import ufrac proofmode_classes.
 From iris.prelude Require Import options.
 
-Definition ufrac_authR (A : cmra) : cmra :=
+Definition ufrac_authR {SI : sidx} (A : cmra) : cmra :=
   authR (optionUR (prodR ufracR A)).
-Definition ufrac_authUR (A : cmra) : ucmra :=
+Definition ufrac_authUR {SI : sidx} (A : cmra) : ucmra :=
   authUR (optionUR (prodR ufracR A)).
 
 (** Note in the signature of [ufrac_auth_auth] and [ufrac_auth_frag] we use
@@ -32,118 +32,163 @@ instances with carrier [Qp], namely [fracR] and [ufracR]. When writing things
 like [ufrac_auth_auth q a ∧ ✓ q] we want Coq to infer the type of [q] as [Qp]
 such that the [✓] of the default [fracR] camera is used, and not the [✓] of
 the [ufracR] camera. *)
-Definition ufrac_auth_auth {A : cmra} (q : Qp) (x : A) : ufrac_authR A :=
+Definition ufrac_auth_auth {SI : sidx} {A : cmra}
+    (q : Qp) (x : A) : ufrac_authR A :=
   ● (Some (q : ufracR,x)).
-Definition ufrac_auth_frag {A : cmra} (q : Qp) (x : A) : ufrac_authR A :=
+Definition ufrac_auth_frag {SI : sidx} {A : cmra}
+    (q : Qp) (x : A) : ufrac_authR A :=
   ◯ (Some (q : ufracR,x)).
 
-Typeclasses Opaque ufrac_auth_auth ufrac_auth_frag.
+Global Typeclasses Opaque ufrac_auth_auth ufrac_auth_frag.
 
-Global Instance: Params (@ufrac_auth_auth) 2 := {}.
-Global Instance: Params (@ufrac_auth_frag) 2 := {}.
+Global Instance: Params (@ufrac_auth_auth) 3 := {}.
+Global Instance: Params (@ufrac_auth_frag) 3 := {}.
 
-Notation "●U{ q } a" := (ufrac_auth_auth q a) (at level 10, format "●U{ q }  a").
-Notation "◯U{ q } a" := (ufrac_auth_frag q a) (at level 10, format "◯U{ q }  a").
+Notation "●U_ q a" := (ufrac_auth_auth q a) (at level 10, q at level 9, format "●U_ q  a").
+Notation "◯U_ q a" := (ufrac_auth_frag q a) (at level 10, q at level 9, format "◯U_ q  a").
 
 Section ufrac_auth.
-  Context {A : cmra}.
+  Context {SI : sidx} {A : cmra}.
   Implicit Types a b : A.
 
-  Global Instance ufrac_auth_auth_ne q : NonExpansive (@ufrac_auth_auth A q).
+  Global Instance ufrac_auth_auth_ne q : NonExpansive (@ufrac_auth_auth SI A q).
   Proof. solve_proper. Qed.
-  Global Instance ufrac_auth_auth_proper q : Proper ((≡) ==> (≡)) (@ufrac_auth_auth A q).
+  Global Instance ufrac_auth_auth_proper q :
+    Proper ((≡) ==> (≡)) (@ufrac_auth_auth SI A q).
   Proof. solve_proper. Qed.
-  Global Instance ufrac_auth_frag_ne q : NonExpansive (@ufrac_auth_frag A q).
+  Global Instance ufrac_auth_frag_ne q : NonExpansive (@ufrac_auth_frag SI A q).
   Proof. solve_proper. Qed.
-  Global Instance ufrac_auth_frag_proper q : Proper ((≡) ==> (≡)) (@ufrac_auth_frag A q).
+  Global Instance ufrac_auth_frag_proper q :
+    Proper ((≡) ==> (≡)) (@ufrac_auth_frag SI A q).
   Proof. solve_proper. Qed.
 
-  Global Instance ufrac_auth_auth_discrete q a : Discrete a → Discrete (●U{q} a).
+  Global Instance ufrac_auth_auth_discrete q a : Discrete a → Discrete (●U_q a).
   Proof. intros. apply auth_auth_discrete; [apply Some_discrete|]; apply _. Qed.
-  Global Instance ufrac_auth_frag_discrete q a : Discrete a → Discrete (◯U{q} a).
+  Global Instance ufrac_auth_frag_discrete q a : Discrete a → Discrete (◯U_q a).
   Proof. intros. apply auth_frag_discrete; apply Some_discrete; apply _. Qed.
 
-  Lemma ufrac_auth_validN n a p : ✓{n} a → ✓{n} (●U{p} a ⋅ ◯U{p} a).
+  Lemma ufrac_auth_validN n a p : ✓{n} a → ✓{n} (●U_p a ⋅ ◯U_p a).
   Proof. by rewrite auth_both_validN. Qed.
-  Lemma ufrac_auth_valid p a : ✓ a → ✓ (●U{p} a ⋅ ◯U{p} a).
+  Lemma ufrac_auth_valid p a : ✓ a → ✓ (●U_p a ⋅ ◯U_p a).
   Proof. intros. by apply auth_both_valid_2. Qed.
 
-  Lemma ufrac_auth_agreeN n p a b : ✓{n} (●U{p} a ⋅ ◯U{p} b) → a ≡{n}≡ b.
+  Lemma ufrac_auth_agreeN n p a b : ✓{n} (●U_p a ⋅ ◯U_p b) → a ≡{n}≡ b.
   Proof.
     rewrite auth_both_validN=> -[/Some_includedN [[_ ? //]|Hincl] _].
     move: Hincl=> /pair_includedN=> -[/ufrac_included Hincl _].
     by destruct (irreflexivity (<)%Qp p).
   Qed.
-  Lemma ufrac_auth_agree p a b : ✓ (●U{p} a ⋅ ◯U{p} b) → a ≡ b.
+  Lemma ufrac_auth_agree p a b : ✓ (●U_p a ⋅ ◯U_p b) → a ≡ b.
   Proof.
     intros. apply equiv_dist=> n. by eapply ufrac_auth_agreeN, cmra_valid_validN.
   Qed.
-  Lemma ufrac_auth_agree_L `{!LeibnizEquiv A} p a b : ✓ (●U{p} a ⋅ ◯U{p} b) → a = b.
+  Lemma ufrac_auth_agree_L `{!LeibnizEquiv A} p a b : ✓ (●U_p a ⋅ ◯U_p b) → a = b.
   Proof. intros. by eapply leibniz_equiv, ufrac_auth_agree. Qed.
 
-  Lemma ufrac_auth_includedN n p q a b : ✓{n} (●U{p} a ⋅ ◯U{q} b) → Some b ≼{n} Some a.
+  Lemma ufrac_auth_includedN n p q a b : ✓{n} (●U_p a ⋅ ◯U_q b) → Some b ≼{n} Some a.
   Proof. by rewrite auth_both_validN=> -[/Some_pair_includedN [_ ?] _]. Qed.
-  Lemma ufrac_auth_included `{CmraDiscrete A} q p a b :
-    ✓ (●U{p} a ⋅ ◯U{q} b) → Some b ≼ Some a.
+  Lemma ufrac_auth_included `{!CmraDiscrete A} q p a b :
+    ✓ (●U_p a ⋅ ◯U_q b) → Some b ≼ Some a.
   Proof. rewrite auth_both_valid_discrete=> -[/Some_pair_included [_ ?] _] //. Qed.
-  Lemma ufrac_auth_includedN_total `{CmraTotal A} n q p a b :
-    ✓{n} (●U{p} a ⋅ ◯U{q} b) → b ≼{n} a.
+  Lemma ufrac_auth_includedN_total `{!CmraTotal A} n q p a b :
+    ✓{n} (●U_p a ⋅ ◯U_q b) → b ≼{n} a.
   Proof. intros. by eapply Some_includedN_total, ufrac_auth_includedN. Qed.
-  Lemma ufrac_auth_included_total `{CmraDiscrete A, CmraTotal A} q p a b :
-    ✓ (●U{p} a ⋅ ◯U{q} b) → b ≼ a.
+  Lemma ufrac_auth_included_total `{!CmraDiscrete A, !CmraTotal A} q p a b :
+    ✓ (●U_p a ⋅ ◯U_q b) → b ≼ a.
   Proof. intros. by eapply Some_included_total, ufrac_auth_included. Qed.
 
-  Lemma ufrac_auth_auth_validN n q a : ✓{n} (●U{q} a) ↔ ✓{n} a.
+  Lemma ufrac_auth_auth_validN n q a : ✓{n} (●U_q a) ↔ ✓{n} a.
   Proof.
     rewrite auth_auth_dfrac_validN Some_validN. split.
     - by intros [?[]].
     - intros. by split.
   Qed.
-  Lemma ufrac_auth_auth_valid q a : ✓ (●U{q} a) ↔ ✓ a.
+  Lemma ufrac_auth_auth_valid q a : ✓ (●U_q a) ↔ ✓ a.
   Proof. rewrite !cmra_valid_validN. by setoid_rewrite ufrac_auth_auth_validN. Qed.
 
-  Lemma ufrac_auth_frag_validN n q a : ✓{n} (◯U{q} a) ↔ ✓{n} a.
+  Lemma ufrac_auth_frag_validN n q a : ✓{n} (◯U_q a) ↔ ✓{n} a.
   Proof.
     rewrite auth_frag_validN. split.
     - by intros [??].
     - by split.
   Qed.
-  Lemma ufrac_auth_frag_valid q a : ✓ (◯U{q} a) ↔ ✓ a.
+  Lemma ufrac_auth_frag_valid q a : ✓ (◯U_q a) ↔ ✓ a.
   Proof.
     rewrite auth_frag_valid. split.
     - by intros [??].
     - by split.
   Qed.
 
-  Lemma ufrac_auth_frag_op q1 q2 a1 a2 : ◯U{q1+q2} (a1 ⋅ a2) ≡ ◯U{q1} a1 ⋅ ◯U{q2} a2.
+  Lemma ufrac_auth_frag_op q1 q2 a1 a2 : ◯U_(q1+q2) (a1 ⋅ a2) ≡ ◯U_q1 a1 ⋅ ◯U_q2 a2.
   Proof. done. Qed.
 
+  Lemma ufrac_auth_frag_op_validN n q1 q2 a b :
+    ✓{n} (◯U_q1 a ⋅ ◯U_q2 b) ↔ ✓{n} (a ⋅ b).
+  Proof. by rewrite -ufrac_auth_frag_op ufrac_auth_frag_validN. Qed.
+  Lemma ufrac_auth_frag_op_valid q1 q2 a b :
+    ✓ (◯U_q1 a ⋅ ◯U_q2 b) ↔ ✓ (a ⋅ b).
+  Proof. by rewrite -ufrac_auth_frag_op ufrac_auth_frag_valid. Qed.
+
   Global Instance ufrac_auth_is_op q q1 q2 a a1 a2 :
-    IsOp q q1 q2 → IsOp a a1 a2 → IsOp' (◯U{q} a) (◯U{q1} a1) (◯U{q2} a2).
+    IsOp q q1 q2 → IsOp a a1 a2 → IsOp' (◯U_q a) (◯U_q1 a1) (◯U_q2 a2).
   Proof. by rewrite /IsOp' /IsOp=> /leibniz_equiv_iff -> ->. Qed.
 
   Global Instance ufrac_auth_is_op_core_id q q1 q2 a :
-    CoreId a → IsOp q q1 q2 → IsOp' (◯U{q} a) (◯U{q1} a) (◯U{q2} a).
+    CoreId a → IsOp q q1 q2 → IsOp' (◯U_q a) (◯U_q1 a) (◯U_q2 a).
   Proof.
     rewrite /IsOp' /IsOp=> ? /leibniz_equiv_iff ->.
     by rewrite -ufrac_auth_frag_op -core_id_dup.
   Qed.
 
   Lemma ufrac_auth_update p q a b a' b' :
-    (a,b) ~l~> (a',b') → ●U{p} a ⋅ ◯U{q} b ~~> ●U{p} a' ⋅ ◯U{q} b'.
+    (a,b) ~l~> (a',b') → ●U_p a ⋅ ◯U_q b ~~> ●U_p a' ⋅ ◯U_q b'.
   Proof.
     intros. apply: auth_update.
     apply: option_local_update. by apply: prod_local_update_2.
   Qed.
 
   Lemma ufrac_auth_update_surplus p q a b :
-   ✓ (a ⋅ b) → ●U{p} a ~~> ●U{p + q} (a ⋅ b) ⋅ ◯U{q} b.
+    ✓ (a ⋅ b) → ●U_p a ~~> ●U_(p+q) (a ⋅ b) ⋅ ◯U_q b.
   Proof.
-    intros Hconsistent. apply: auth_update_alloc.
-    intros n m; simpl; intros [Hvalid1 Hvalid2] Heq.
+    intros Hconsistent. apply: auth_update_alloc. apply local_update_unital.
+    intros n mpa; simpl; intros [Hvalid1 Hvalid2] Heq; simplify_eq/=.
     split.
     - split; by apply cmra_valid_validN.
     - rewrite pair_op Some_op Heq comm.
-      destruct m; simpl; [rewrite left_id | rewrite right_id]; done.
+      destruct mpa; simpl; [rewrite left_id | rewrite right_id]; done.
+  Qed.
+
+  Lemma ufrac_auth_update_surplus_cancel p q a b :
+    Cancelable b →
+    ●U_(p+q) (a ⋅ b) ⋅ ◯U_q b ~~> ●U_p a.
+  Proof.
+    intros. apply: auth_update_dealloc. apply local_update_unital.
+    intros n mpa; simpl; intros [Hvalid1 Hvalid2] Heq; simplify_eq/=.
+    split.
+    { split; by eapply cmra_validN_op_l. }
+    rewrite (comm _ p) (comm _ a) in Heq.
+    destruct mpa as [[p' a']|]; simplify_eq/=.
+    - rewrite -Some_op in Heq.
+      apply (inj _) in Heq as [Hp%leibniz_equiv Ha]; simplify_eq/=.
+      apply (inj _) in Hp as ->.
+      apply (cancelableN _) in Ha; last by rewrite comm.
+      by repeat constructor.
+    - rewrite right_id in Heq.
+      apply (inj _) in Heq as [Hp%leibniz_equiv _]; simplify_eq/=.
+      by apply Qp.add_id_free in Hp.
   Qed.
 End ufrac_auth.
+
+Definition ufrac_authURF {SI : sidx} (F : rFunctor) : urFunctor :=
+  authURF (optionURF (prodRF (constRF ufracR) F)).
+
+Global Instance ufrac_authURF_contractive {SI : sidx} F :
+  rFunctorContractive F → urFunctorContractive (ufrac_authURF F).
+Proof. apply _. Qed.
+
+Definition ufrac_authRF {SI : sidx} (F : rFunctor) : rFunctor :=
+  authRF (optionURF (prodRF (constRF ufracR) F)).
+
+Global Instance ufrac_authRF_contractive {SI : sidx} F :
+  rFunctorContractive F → rFunctorContractive (ufrac_authRF F).
+Proof. apply _. Qed.

iris/algebra/list.v

@@ -4,13 +4,15 @@ From iris.algebra Require Import big_op.
 From iris.prelude Require Import options.
 
 Section ofe.
-Context {A : ofe}.
+Context {SI : sidx} {A : ofe}.
 Implicit Types l : list A.
 
 Local Instance list_dist : Dist (list A) := λ n, Forall2 (dist n).
 
+Lemma list_dist_Forall2 n l k : l ≡{n}≡ k ↔ Forall2 (dist n) l k.
+Proof. done. Qed.
 Lemma list_dist_lookup n l1 l2 : l1 ≡{n}≡ l2 ↔ ∀ i, l1 !! i ≡{n}≡ l2 !! i.
-Proof. setoid_rewrite dist_option_Forall2. apply Forall2_lookup. Qed.
+Proof. setoid_rewrite option_dist_Forall2. apply Forall2_lookup. Qed.
 
 Global Instance cons_ne : NonExpansive2 (@cons A) := _.
 Global Instance app_ne : NonExpansive2 (@app A) := _.
@@ -21,109 +23,177 @@ Global Instance drop_ne n : NonExpansive (@drop A n) := _.
 Global Instance head_ne : NonExpansive (head (A:=A)).
 Proof. destruct 1; by constructor. Qed.
 Global Instance list_lookup_ne i : NonExpansive (lookup (M:=list A) i).
-Proof. intros ????. by apply dist_option_Forall2, Forall2_lookup. Qed.
+Proof. intros ????. by apply option_dist_Forall2, Forall2_lookup. Qed.
 Global Instance list_lookup_total_ne `{!Inhabited A} i :
   NonExpansive (lookup_total (M:=list A) i).
 Proof. intros ???. rewrite !list_lookup_total_alt. by intros ->. Qed.
-Global Instance list_alter_ne n f i :
-  Proper (dist n ==> dist n) f →
-  Proper (dist n ==> dist n) (alter (M:=list A) f i) := _.
+Global Instance list_alter_ne n :
+  Proper ((dist n ==> dist n) ==> (=) ==> dist n ==> dist n) (alter (M:=list A)) := _.
 Global Instance list_insert_ne i : NonExpansive2 (insert (M:=list A) i) := _.
 Global Instance list_inserts_ne i : NonExpansive2 (@list_inserts A i) := _.
 Global Instance list_delete_ne i : NonExpansive (delete (M:=list A) i) := _.
 Global Instance option_list_ne : NonExpansive (@option_list A).
-Proof. intros ????; by apply Forall2_option_list, dist_option_Forall2. Qed.
+Proof. intros ????; by apply Forall2_option_list, option_dist_Forall2. Qed.
 Global Instance list_filter_ne n P `{∀ x, Decision (P x)} :
   Proper (dist n ==> iff) P →
   Proper (dist n ==> dist n) (filter (B:=list A) P) := _.
 Global Instance replicate_ne n : NonExpansive (@replicate A n) := _.
 Global Instance reverse_ne : NonExpansive (@reverse A) := _.
 Global Instance last_ne : NonExpansive (@last A).
-Proof. intros ????; by apply dist_option_Forall2, Forall2_last. Qed.
+Proof. intros ????; by apply option_dist_Forall2, Forall2_last. Qed.
 Global Instance resize_ne n : NonExpansive2 (@resize A n) := _.
 
-Lemma list_dist_cons_inv_l n x l k :
-  x :: l ≡{n}≡ k → ∃ y k', x ≡{n}≡ y ∧ l ≡{n}≡ k' ∧ k = y :: k'.
-Proof. apply Forall2_cons_inv_l. Qed.
-Lemma list_dist_cons_inv_r n l k y :
+Global Instance cons_dist_inj n :
+  Inj2 (dist n) (dist n) (dist n) (@cons A).
+Proof. by inversion_clear 1. Qed.
+
+Lemma nil_dist_eq n l : l ≡{n}≡ [] ↔ l = [].
+Proof. split; by inversion 1. Qed.
+Lemma cons_dist_eq n l k y :
   l ≡{n}≡ y :: k → ∃ x l', x ≡{n}≡ y ∧ l' ≡{n}≡ k ∧ l = x :: l'.
 Proof. apply Forall2_cons_inv_r. Qed.
+Lemma app_dist_eq n l k1 k2 :
+  l ≡{n}≡ k1 ++ k2 ↔ ∃ k1' k2', l = k1' ++ k2' ∧ k1' ≡{n}≡ k1 ∧ k2' ≡{n}≡ k2.
+Proof. rewrite list_dist_Forall2 Forall2_app_inv_r. naive_solver. Qed.
+Lemma list_singleton_dist_eq n l x :
+  l ≡{n}≡ [x] ↔ ∃ x', l = [x'] ∧ x' ≡{n}≡ x.
+Proof.
+  split; [|by intros (?&->&->)].
+  intros (?&?&?&->%Forall2_nil_inv_r&->)%list_dist_Forall2%Forall2_cons_inv_r.
+  eauto.
+Qed.
 
 Definition list_ofe_mixin : OfeMixin (list A).
 Proof.
   split.
-  - intros l k. rewrite equiv_Forall2 -Forall2_forall.
+  - intros l k. rewrite list_equiv_Forall2 -Forall2_forall.
     split; induction 1; constructor; intros; try apply equiv_dist; auto.
   - apply _.
-  - rewrite /dist /list_dist. eauto using Forall2_impl, dist_S.
+  - rewrite /dist /list_dist. eauto using Forall2_impl, dist_le.
 Qed.
 Canonical Structure listO := Ofe (list A) list_ofe_mixin.
 
 (** To define [compl : chain (list A) → list A] we make use of the fact that
 given a given chain [c0, c1, c2, ...] of lists, the list [c0] completely
-determines the shape (i.e. the length) of all lists in the chain. So, the
+determines the shape (i.e., the length) of all lists in the chain. So, the
 [compl] operation is defined by structural recursion on [c0], and takes the
 completion of the elements of all lists in the chain point-wise. We use [head]
 and [tail] as the inverse of [cons]. *)
 Fixpoint list_compl_go `{!Cofe A} (c0 : list A) (c : chain listO) : listO :=
   match c0 with
   | [] => []
-  | x :: c0 => compl (chain_map (default x ∘ head) c) :: list_compl_go c0 (chain_map tail c)
+  | x :: c0 => compl (chain_map (default x ∘ head) c) ::
+               list_compl_go c0 (chain_map tail c)
+  end.
+
+Fixpoint list_lbcompl_go `{!Cofe A} (c0 : list A) {n} Hn (c : bchain listO n) : listO :=
+  match c0 with
+  | [] => []
+  | x :: c0 => lbcompl Hn (bchain_map (default x ∘ head) c) ::
+               list_lbcompl_go c0 Hn (bchain_map tail c)
   end.
 
-Global Program Instance list_cofe `{!Cofe A} : Cofe listO :=
-  {| compl c := list_compl_go (c 0) c |}.
+Global Program Instance list_cofe `{!Cofe A} : Cofe listO := {
+  compl c := list_compl_go (c 0ᵢ) c;
+  lbcompl n Hn c := list_lbcompl_go (c _ (SIdx.limit_lt_0 _ Hn)) Hn c
+}.
 Next Obligation.
-  intros ? n c; rewrite /compl.
-  assert (c 0 ≡{0}≡ c n) as Hc0 by (symmetry; apply chain_cauchy; lia).
-  revert Hc0. generalize (c 0)=> c0. revert c.
+  intros ? n c; simpl.
+  assert (c 0ᵢ ≡{0ᵢ}≡ c n) as Hc0 by (symmetry; apply chain_cauchy, SIdx.le_0_l).
+  revert Hc0. generalize (c 0ᵢ)=> c0. revert c.
   induction c0 as [|x c0 IH]=> c Hc0 /=.
   { by inversion Hc0. }
-  apply list_dist_cons_inv_l in Hc0 as (x' & xs' & Hx & Hc0 & Hcn).
+  apply symmetry, cons_dist_eq in Hc0 as (x' & xs' & Hx & Hc0 & Hcn).
   rewrite Hcn. f_equiv.
-  - by rewrite conv_compl /= Hcn /=.
-  - rewrite IH /= ?Hcn //.
+  - rewrite conv_compl.
+    by rewrite /chain_map //= Hcn.
+  - rewrite IH /chain_map /= ?Hcn //.
+Qed.
+Next Obligation.
+  intros ? n Hn c m Hm; simpl.
+  assert (c _ (SIdx.limit_lt_0 _ Hn) ≡{0ᵢ}≡ c m Hm) as Hc0 
+    by (symmetry; apply bchain_cauchy, SIdx.le_0_l).
+  revert Hc0. generalize (c _ (SIdx.limit_lt_0 _ Hn))=> c0. revert c.
+  induction c0 as [|x c0 IH]=> c Hc0 /=.
+  { by inversion Hc0. }
+  apply symmetry in Hc0.
+  apply cons_dist_eq in Hc0 as (x' & xs' & Hx & Hc0 & Hcn).
+  rewrite Hcn. f_equiv.
+  - rewrite (conv_lbcompl _ _ Hm). by rewrite /bchain_map //= Hcn.
+  - rewrite IH /bchain_map /= ?Hcn //.
+Qed.
+Next Obligation.
+  intros ? n Hn c1 c2 m Hc; simpl.
+  specialize (Hc _ (SIdx.limit_lt_0 _ Hn)) as Heq.
+  move: Heq. generalize (c1 _ (SIdx.limit_lt_0 _ Hn)) as c0 => c0.
+  generalize (c2 _ (SIdx.limit_lt_0 _ Hn)) as d0 => d0 Heq.
+  induction Heq as [ | ???? Heq1 Heq2 IH ] in c1, c2, Hc |-*; simpl; f_equiv.
+  - apply lbcompl_ne=> γ Hγ. by rewrite /bchain_map //= Hc Heq1.
+  - apply IH=> γ Hγ. by rewrite /bchain_map /= Hc.
 Qed.
 
 Global Instance list_ofe_discrete : OfeDiscrete A → OfeDiscrete listO.
-Proof. induction 2; constructor; try apply (discrete _); auto. Qed.
+Proof. induction 2; constructor; try apply (discrete_0 _); auto. Qed.
 
 Global Instance nil_discrete : Discrete (@nil A).
 Proof. inversion_clear 1; constructor. Qed.
 Global Instance cons_discrete x l : Discrete x → Discrete l → Discrete (x :: l).
-Proof. intros ??; inversion_clear 1; constructor; by apply discrete. Qed.
+Proof. intros ??; inversion_clear 1; constructor; by apply discrete_0. Qed.
 
+Lemma dist_Permutation n l1 l2 l3 :
+  l1 ≡{n}≡ l2 → l2 ≡ₚ l3 → ∃ l2', l1 ≡ₚ l2' ∧ l2' ≡{n}≡ l3.
+Proof.
+  intros Hequiv Hperm. revert l1 Hequiv.
+  induction Hperm as [|x l2 l3 _ IH|x y l2|l2 l3 l4 _ IH1 _ IH2]; intros l1.
+  - intros ?. by exists l1.
+  - intros (x'&l2'&?&(l2''&?&?)%IH&->)%cons_dist_eq.
+    exists (x' :: l2''). by repeat constructor.
+  - intros (y'&?&?&(x'&l2'&?&?&->)%cons_dist_eq&->)%cons_dist_eq.
+    exists (x' :: y' :: l2'). by repeat constructor.
+  - intros (l2'&?&(l3'&?&?)%IH2)%IH1. exists l3'. split; [by etrans|done].
+Qed.
 End ofe.
 
-Global Arguments listO : clear implicits.
+Global Arguments listO {SI} _.
 
 (** Non-expansiveness of higher-order list functions and big-ops *)
-Global Instance list_fmap_ne {A B : ofe} (f : A → B) n :
-  Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (fmap (M:=list) f).
-Proof. intros Hf l k ?; by eapply Forall2_fmap, Forall2_impl; eauto. Qed.
-Global Instance list_omap_ne {A B : ofe} (f : A → option B) n :
-  Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (omap (M:=list) f).
+Global Instance list_fmap_ne {SI : sidx} {A B : ofe} n :
+  Proper ((dist n ==> dist n) ==> (≡{n}@{list A}≡) ==> (≡{n}@{list B}≡)) fmap.
+Proof. intros f1 f2 Hf l1 l2 Hl; by eapply Forall2_fmap, Forall2_impl; eauto. Qed.
+Global Instance list_omap_ne {SI : sidx} {A B : ofe} n :
+  Proper ((dist n ==> dist n) ==> (≡{n}@{list A}≡) ==> (≡{n}@{list B}≡)) omap.
 Proof.
-  intros Hf. induction 1 as [|x1 x2 l1 l2 Hx Hl]; csimpl; [constructor|].
+  intros f1 f2 Hf. induction 1 as [|x1 x2 l1 l2 Hx Hl]; csimpl; [constructor|].
   destruct (Hf _ _ Hx); [f_equiv|]; auto.
 Qed.
-Global Instance imap_ne {A B : ofe} (f : nat → A → B) n :
-  (∀ i, Proper (dist n ==> dist n) (f i)) → Proper (dist n ==> dist n) (imap f).
+Global Instance imap_ne {SI : sidx} {A B : ofe} n :
+  Proper (pointwise_relation _ ((dist n ==> dist n)) ==> dist n ==> dist n)
+         (imap (A:=A) (B:=B)).
 Proof.
-  intros Hf l1 l2 Hl. revert f Hf.
-  induction Hl; intros f Hf; simpl; [constructor|f_equiv; naive_solver].
+  intros f1 f2 Hf l1 l2 Hl. revert f1 f2 Hf.
+  induction Hl as [|x1 x2 l1 l2 ?? IH]; intros f1 f2 Hf; simpl; [constructor|].
+  f_equiv; [by apply Hf|]. apply IH. intros i y1 y2 Hy. by apply Hf.
 Qed.
-Global Instance list_bind_ne {A B : ofe} (f : A → list A) n :
-  Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (mbind f).
-Proof. induction 2; simpl; [constructor|solve_proper]. Qed.
-Global Instance list_join_ne {A : ofe} : NonExpansive (mjoin (M:=list) (A:=A)).
+Global Instance list_bind_ne {SI : sidx} {A B : ofe} n :
+  Proper ((dist n ==> dist n) ==> (≡{n}@{list B}≡) ==> (≡{n}@{list A}≡)) mbind.
+Proof. intros f1 f2 Hf. induction 1; csimpl; [constructor|f_equiv; auto]. Qed.
+Global Instance list_join_ne {SI : sidx} {A : ofe} n :
+  Proper (dist n ==> (≡{n}@{list A}≡)) mjoin.
 Proof. induction 1; simpl; [constructor|solve_proper]. Qed.
-Global Instance zip_with_ne {A B C : ofe} (f : A → B → C) n :
-  Proper (dist n ==> dist n ==> dist n) f →
-  Proper (dist n ==> dist n ==> dist n) (zip_with f).
-Proof. induction 2; destruct 1; simpl; [constructor..|f_equiv; [f_equiv|]; auto]. Qed.
+Global Instance zip_with_ne {SI : sidx} {A B C : ofe} n :
+  Proper ((dist n ==> dist n ==> dist n) ==> dist n ==> dist n ==> dist n)
+         (zip_with (A:=A) (B:=B) (C:=C)).
+Proof.
+  intros f1 f2 Hf.
+  induction 1; destruct 1; simpl; [constructor..|f_equiv; try apply Hf; auto].
+Qed.
+
+Global Instance list_fmap_dist_inj {SI : sidx} {A B : ofe} (f : A → B) n :
+  Inj (≡{n}≡) (≡{n}≡) f → Inj (≡{n}@{list A}≡) (≡{n}@{list B}≡) (fmap f).
+Proof. apply list_fmap_inj. Qed.
 
-Lemma big_opL_ne_2 `{Monoid M o} {A : ofe} (f g : nat → A → M) l1 l2 n :
+Lemma big_opL_ne_2 {SI : sidx} {M : ofe}
+    {o : M → M → M} `{!Monoid o} {A : ofe} (f g : nat → A → M) l1 l2 n :
   l1 ≡{n}≡ l2 →
   (∀ k y1 y2,
     l1 !! k = Some y1 → l2 !! k = Some y2 → y1 ≡{n}≡ y2 → f k y1 ≡{n}≡ g k y2) →
@@ -136,32 +206,33 @@ Proof.
 Qed.
 
 (** Functor *)
-Lemma list_fmap_ext_ne {A} {B : ofe} (f g : A → B) (l : list A) n :
+Lemma list_fmap_ext_ne {SI : sidx} {A} {B : ofe} (f g : A → B) (l : list A) n :
   (∀ x, f x ≡{n}≡ g x) → f <$> l ≡{n}≡ g <$> l.
 Proof. intros Hf. by apply Forall2_fmap, Forall_Forall2_diag, Forall_true. Qed.
-Definition listO_map {A B} (f : A -n> B) : listO A -n> listO B :=
+Definition listO_map {SI : sidx} {A B} (f : A -n> B) : listO A -n> listO B :=
   OfeMor (fmap f : listO A → listO B).
-Global Instance listO_map_ne A B : NonExpansive (@listO_map A B).
+Global Instance listO_map_ne {SI : sidx} A B : NonExpansive (@listO_map SI A B).
 Proof. intros n f g ? l. by apply list_fmap_ext_ne. Qed.
 
-Program Definition listOF (F : oFunctor) : oFunctor := {|
+Program Definition listOF {SI : sidx} (F : oFunctor) : oFunctor := {|
   oFunctor_car A _ B _ := listO (oFunctor_car F A B);
   oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := listO_map (oFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, oFunctor_map_ne.
+  by intros ? F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, oFunctor_map_ne.
 Qed.
 Next Obligation.
-  intros F A ? B ? x. rewrite /= -{2}(list_fmap_id x).
-  apply list_fmap_equiv_ext=>y. apply oFunctor_map_id.
+  intros ? F A ? B ? x. rewrite /= -{2}(list_fmap_id x).
+  apply list_fmap_equiv_ext=>???. apply oFunctor_map_id.
 Qed.
 Next Obligation.
-  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -list_fmap_compose.
-  apply list_fmap_equiv_ext=>y; apply oFunctor_map_compose.
+  intros ? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -list_fmap_compose.
+  apply list_fmap_equiv_ext=>???; apply oFunctor_map_compose.
 Qed.
 
-Global Instance listOF_contractive F :
+Global Instance listOF_contractive {SI : sidx} F :
   oFunctorContractive F → oFunctorContractive (listOF F).
 Proof.
-  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, oFunctor_map_contractive.
+  intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg;
+    by apply listO_map_ne, oFunctor_map_contractive.
 Qed.

iris/algebra/local_updates.v

@@ -2,20 +2,20 @@ From iris.algebra Require Export cmra.
 From iris.prelude Require Import options.
 
 (** * Local updates *)
-Definition local_update {A : cmra} (x y : A * A) := ∀ n mz,
+Definition local_update {SI : sidx} {A : cmra} (x y : A * A) := ∀ n mz,
   ✓{n} x.1 → x.1 ≡{n}≡ x.2 ⋅? mz → ✓{n} y.1 ∧ y.1 ≡{n}≡ y.2 ⋅? mz.
-Global Instance: Params (@local_update) 1 := {}.
+Global Instance: Params (@local_update) 2 := {}.
 Infix "~l~>" := local_update (at level 70).
 
 Section updates.
-  Context {A : cmra}.
+  Context {SI : sidx} {A : cmra}.
   Implicit Types x y : A.
 
   Global Instance local_update_proper :
-    Proper ((≡) ==> (≡) ==> iff) (@local_update A).
+    Proper ((≡) ==> (≡) ==> iff) (@local_update SI A).
   Proof. unfold local_update. by repeat intro; setoid_subst. Qed.
 
-  Global Instance local_update_preorder : PreOrder (@local_update A).
+  Global Instance local_update_preorder : PreOrder (@local_update SI A).
   Proof. split; unfold local_update; red; naive_solver. Qed.
 
   Lemma exclusive_local_update `{!Exclusive y} x x' : ✓ x' → (x,y) ~l~> (x',x').
@@ -72,45 +72,43 @@ Section updates.
   Proof.
     rewrite /local_update /=. setoid_rewrite <-cmra_discrete_valid_iff.
     setoid_rewrite <-(λ n, discrete_iff n x).
-    setoid_rewrite <-(λ n, discrete_iff n x'). naive_solver eauto using O.
+    setoid_rewrite <-(λ n, discrete_iff n x'). pose 0ᵢ. naive_solver.
   Qed.
 
   Lemma local_update_valid0 x y x' y' :
-    (✓{0} x → ✓{0} y → x ≡{0}≡ y ∨ y ≼{0} x → (x,y) ~l~> (x',y')) →
+    (✓{0ᵢ} x → ✓{0ᵢ} y → Some y ≼{0ᵢ} Some 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.
+    - by apply (cmra_validN_le n), SIdx.le_0_l.
+    - apply (cmra_validN_le n), SIdx.le_0_l.
       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.
+    - eapply (cmra_includedN_le n), SIdx.le_0_l.
+      apply Some_includedN_opM. eauto.
   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').
+    (✓ x → ✓ y → Some y ≼ Some x → (x,y) ~l~> (x',y')) → (x,y) ~l~> (x',y').
   Proof.
-    rewrite !(cmra_discrete_valid_iff 0)
-      (cmra_discrete_included_iff 0) (discrete_iff 0).
+    rewrite !(cmra_discrete_valid_iff 0ᵢ) (cmra_discrete_included_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').
+    (✓{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.
+    intros Hup. apply local_update_valid0=> ?? Hincl. apply Hup; auto.
+    by apply Some_includedN_total.
   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).
+    rewrite !(cmra_discrete_valid_iff 0ᵢ) (cmra_discrete_included_iff 0ᵢ).
     apply local_update_total_valid0.
   Qed.
 End updates.
 
 Section updates_unital.
-  Context {A : ucmra}.
+  Context {SI : sidx} {A : ucmra}.
   Implicit Types x y : A.
 
   Lemma local_update_unital x y x' y' :
@@ -137,66 +135,102 @@ Section updates_unital.
   Proof. rewrite -{2}(right_id ε op x). by apply cancel_local_update. Qed.
 End updates_unital.
 
-(** * Product *)
-Lemma prod_local_update {A B : cmra} (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 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 : cmra} (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 : cmra} (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 : cmra} (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 *)
-(* TODO: Investigate whether we can use these in proving the very similar local
-   updates on finmaps. *)
-Lemma option_local_update {A : cmra} (x y x' y' : A) :
-  (x, y) ~l~> (x',y') →
-  (Some x, Some y) ~l~> (Some x', Some y').
-Proof.
-  intros Hup. apply local_update_unital=>n mz Hxv Hx; simpl in *.
-  destruct (Hup n mz); first done.
-  { destruct mz as [?|]; inversion_clear Hx; auto. }
-  split; first done. destruct mz as [?|]; constructor; auto.
-Qed.
-
-Lemma option_local_update_None {A: ucmra} (x x' y': A):
-  (x, ε) ~l~> (x', y') ->
-  (Some x, None) ~l~> (Some x', Some y').
-Proof.
-  intros Hup. apply local_update_unital=> n mz.
-  rewrite left_id=> ? <-.
-  destruct (Hup n (Some x)); simpl in *; first done.
-  - by rewrite left_id.
-  - split; first done. rewrite -Some_op. by constructor.
-Qed.
-
-Lemma alloc_option_local_update {A : cmra} (x : A) y :
-  ✓ x →
-  (None, y) ~l~> (Some x, Some x).
-Proof.
-  move=>Hx. apply local_update_unital=> n z _ /= Heq. split.
-  { rewrite Some_validN. apply cmra_valid_validN. done. }
-  destruct z as [z|]; last done. destruct y; inversion Heq.
-Qed.
-
-Lemma delete_option_local_update {A : cmra} (x : option A) (y : A) :
-  Exclusive y → (x, Some y) ~l~> (None, None).
-Proof.
-  move=>Hex. apply local_update_unital=>n z /= Hy Heq. split; first done.
-  destruct z as [z|]; last done. exfalso.
-  move: Hy. rewrite Heq /= -Some_op=>Hy. eapply Hex.
-  eapply cmra_validN_le; [|lia]. eapply Hy.
-Qed.
+Section updates_unit.
+  Context {SI : sidx}.
+
+  (** * Unit *)
+  Lemma unit_local_update (x y x' y' : unit) : (x, y) ~l~> (x', y').
+  Proof. destruct x,y,x',y'; reflexivity. Qed.
+End updates_unit.
+
+Section updates_discrete_fun.
+  Context {SI : sidx}.
+
+  (** * Dependently-typed functions over a discrete domain *)
+  Lemma discrete_fun_local_update {A} {B : A → ucmra} (f g f' g' : discrete_fun B) :
+    (∀ x : A, (f x, g x) ~l~> (f' x, g' x)) →
+    (f, g) ~l~> (f', g').
+  Proof.
+    setoid_rewrite local_update_unital. intros Hupd n h Hf Hg.
+    split=> x; eapply Hupd, Hg; eauto.
+  Qed.
+End updates_discrete_fun.
+
+Section updates_product.
+  Context {SI : sidx}.
+
+  (** * Product *)
+  Lemma prod_local_update {A B : cmra} (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 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 : cmra} (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 : cmra} (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 : cmra} (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.
+End updates_product.
+
+Section updates_option.
+  Context {SI : sidx}.
+
+  (** * Option *)
+  (* TODO: Investigate whether we can use these in proving the very similar local
+    updates on finmaps. *)
+  Lemma option_local_update {A : cmra} (x y x' y' : A) :
+    (x, y) ~l~> (x',y') →
+    (Some x, Some y) ~l~> (Some x', Some y').
+  Proof.
+    intros Hup. apply local_update_unital=>n mz Hxv Hx; simpl in *.
+    destruct (Hup n mz); first done.
+    { destruct mz as [?|]; inversion_clear Hx; auto. }
+    split; first done. destruct mz as [?|]; constructor; auto.
+  Qed.
+
+  Lemma option_local_update_None {A: ucmra} (x x' y': A):
+    (x, ε) ~l~> (x', y') ->
+    (Some x, None) ~l~> (Some x', Some y').
+  Proof.
+    intros Hup. apply local_update_unital=> n mz.
+    rewrite left_id=> ? <-.
+    destruct (Hup n (Some x)); simpl in *; first done.
+    - by rewrite left_id.
+    - split; first done. rewrite -Some_op. by constructor.
+  Qed.
+
+  Lemma alloc_option_local_update {A : cmra} (x : A) y :
+    ✓ x →
+    (None, y) ~l~> (Some x, Some x).
+  Proof.
+    move=>Hx. apply local_update_unital=> n z _ /= Heq. split.
+    { rewrite Some_validN. apply cmra_valid_validN. done. }
+    destruct z as [z|]; last done. destruct y; inversion Heq.
+  Qed.
+
+  Lemma delete_option_local_update {A : cmra} (x : option A) (y : A) :
+    Exclusive y → (x, Some y) ~l~> (None, None).
+  Proof.
+    move=>Hex. apply local_update_unital=>n z /= Hy Heq. split; first done.
+    destruct z as [z|]; last done. exfalso.
+    move: Hy. rewrite Heq /= -Some_op=>Hy. eapply Hex.
+    eapply cmra_validN_le, SIdx.le_0_l. eapply Hy.
+  Qed.
+
+  Lemma delete_option_local_update_cancelable {A : cmra} (mx : option A) :
+    Cancelable mx → (mx, mx) ~l~> (None, None).
+  Proof.
+    intros ?. apply local_update_unital=>n mf /= Hmx Heq. split; first done.
+    rewrite left_id. eapply (cancelableN mx); by rewrite right_id_L.
+  Qed.
+End updates_option.