equip frac_agree with support for dfrac

CHANGELOG.md

@@ -16,6 +16,9 @@ lemma.
 * Change `ufrac_auth` notation to not use curly braces, since these fractions do
   not behave like regular fractions (and cannot be made `dfrac`).
   Old: `●U{q} a`, `◯U{q} b`; new: `●U_q a`, `◯U_q b`.
+* Equip `frac_agree` with support for `dfrac` and rename it to `dfrac_agree`.
+  The old `to_frac_agree` and its lemmas still exist, except that the
+  `frac_agree_op_valid` lemmas are made bi-directional.
 
 **Changes in `bi`:**
 
@@ -47,6 +50,8 @@ s/\bleast_fixpoint_strong_ind\b/least_fixpoint_ind/g
 # gmap_view renames from frac to dfrac
 s/\bgmap_view_(auth|both)_frac_(op_invN|op_inv|op_inv_L|valid|op_validN|op_valid|op_valid_L)\b/gmap_view_\1_dfrac_\2/g
 s/\bgmap_view_persist\b/gmap_view_frag_persist/g
+# frac_agree with dfrac
+s/\bfrac_agreeR\b/dfrac_agreeR/g
 EOF
 ```
 

_CoqProject

@@ -52,7 +52,7 @@ iris/algebra/max_prefix_list.v
 iris/algebra/lib/excl_auth.v
 iris/algebra/lib/frac_auth.v
 iris/algebra/lib/ufrac_auth.v
-iris/algebra/lib/frac_agree.v
+iris/algebra/lib/dfrac_agree.v
 iris/algebra/lib/gmap_view.v
 iris/algebra/lib/mono_nat.v
 iris/algebra/lib/gset_bij.v

iris/algebra/lib/frac_agree.v → iris/algebra/lib/dfrac_agree.v

-From iris.algebra Require Export frac agree updates local_updates.
+From iris.algebra Require Export dfrac 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 dfrac_agreeR (A : ofe) : cmra := prodR dfracR (agreeR A).
 
-Definition to_frac_agree {A : ofe} (q : frac) (a : A) : frac_agreeR A :=
-  (q, to_agree a).
+Definition to_dfrac_agree {A : ofe} (d : dfrac) (a : A) : dfrac_agreeR A :=
+  (d, to_agree a).
+(** 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 {A : ofe} (q : Qp) (a : A) : dfrac_agreeR A :=
+  to_dfrac_agree (DfracOwn q) a.
 
 Section lemmas.
   Context {A : ofe}.
-  Implicit Types (q : frac) (a : A).
+  Implicit Types (q : Qp) (d : dfrac) (a : A).
 
-  Global Instance to_frac_agree_ne q : NonExpansive (@to_frac_agree A q).
+  Global Instance to_dfrac_agree_ne d : NonExpansive (@to_dfrac_agree A d).
   Proof. solve_proper. Qed.
-  Global Instance to_frac_agree_proper q : Proper ((≡) ==> (≡)) (@to_frac_agree A q).
+  Global Instance to_dfrac_agree_proper d : Proper ((≡) ==> (≡)) (@to_dfrac_agree A d).
   Proof. solve_proper. Qed.
 
-  Global Instance to_frac_agree_exclusive a : Exclusive (to_frac_agree 1 a).
+  Global Instance to_dfrac_agree_exclusive a :
+    Exclusive (to_dfrac_agree (DfracOwn 1) a).
   Proof. apply _. Qed.
-  Global Instance to_frac_discrete a : Discrete a → Discrete (to_frac_agree 1 a).
+  Global Instance to_dfrac_agree_discrete d a : Discrete a → Discrete (to_dfrac_agree d 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.
+  Global Instance to_dfrac_agree_injN n : Inj2 (dist n) (dist n) (dist n) (@to_dfrac_agree A).
+  Proof. by intros d1 a1 d2 a2 [??%(inj to_agree)]. Qed.
+  Global Instance to_dfrac_agree_inj : Inj2 (≡) (≡) (≡) (@to_dfrac_agree 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 /to_frac_agree -pair_op agree_idemp //. Qed.
+  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.
-    rewrite /to_frac_agree -pair_op pair_valid to_agree_op_valid. done.
-  Qed.
+  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. unfold_leibniz. apply frac_agree_op_valid. Qed.
+  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.
-    rewrite /to_frac_agree -pair_op pair_validN to_agree_op_validN. done.
+    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 pair_included frac_included to_agree_included. Qed.
+  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. unfold_leibniz. apply frac_agree_included. Qed.
+  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 pair_includedN -cmra_discrete_included_iff
-               frac_included to_agree_includedN.
-  Qed.
+  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_frac_agree q1 v1 ⋅ to_frac_agree q2 v2] into something simpler. *)
+      [to_dfrac_agree d1 v1 ⋅ to_dfrac_agree d2 v2] into something simpler. *)
+  Lemma to_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 to_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 to_dfrac_agree_update_2. rewrite dfrac_op_own Hq //. Qed.
+
+  Lemma to_dfrac_agree_persist d a :
+    to_dfrac_agree d a ~~> to_dfrac_agree DfracDiscarded a.
   Proof.
-    intros Hq. rewrite -pair_op frac_op Hq.
-    apply cmra_update_exclusive.
-    rewrite frac_agree_op_valid Hq //.
+    rewrite /to_dfrac_agree. apply prod_update; last done.
+    simpl. apply dfrac_discard_update.
   Qed.
 
 End lemmas.
 
-Typeclasses Opaque to_frac_agree.
+Typeclasses Opaque to_dfrac_agree.

iris/base_logic/lib/ghost_var.v

 (** A simple "ghost variable" of arbitrary type with fractional ownership.
 Can be mutated when fully owned. *)
-From iris.algebra Require Import frac_agree.
+From iris.algebra Require Import dfrac_agree.
 From iris.bi.lib Require Import fractional.
 From iris.proofmode Require Import proofmode.
 From iris.base_logic.lib Require Export own.
@@ -8,12 +8,12 @@ From iris.prelude Require Import options.
 
 (** The CMRA we need. *)
 Class ghost_varG Σ (A : Type) := GhostVarG {
-  ghost_var_inG :> inG Σ (frac_agreeR $ leibnizO A);
+  ghost_var_inG :> inG Σ (dfrac_agreeR $ leibnizO A);
 }.
 Global Hint Mode ghost_varG - ! : typeclass_instances.
 
 Definition ghost_varΣ (A : Type) : gFunctors :=
-  #[ GFunctor (frac_agreeR $ leibnizO A) ].
+  #[ GFunctor (dfrac_agreeR $ leibnizO A) ].
 
 Global Instance subG_ghost_varΣ Σ A : subG (ghost_varΣ A) Σ → ghost_varG Σ A.
 Proof. solve_inG. Qed.