diff --git a/CHANGELOG.md b/CHANGELOG.md
index 0dc1c0662689c222dbc3d8016f7a58afdae0e1ad..d29a6eea1ed174550b05750579313740c0edf6fd 100644
--- a/CHANGELOG.md
+++ b/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
```
diff --git a/_CoqProject b/_CoqProject
index 3748f986d048b61a10f0b86c3d60d379effe74fe..985d186bf819a83e945df5774c0bf0a73f6a299f 100644
--- a/_CoqProject
+++ b/_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
diff --git a/iris/algebra/lib/dfrac_agree.v b/iris/algebra/lib/dfrac_agree.v
new file mode 100644
index 0000000000000000000000000000000000000000..e6ddd88c1158f1a149936ea5d7048e4d3a7e3769
--- /dev/null
+++ b/iris/algebra/lib/dfrac_agree.v
@@ -0,0 +1,126 @@
+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 (A : ofe) : cmra := prodR dfracR (agreeR 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 : Qp) (d : dfrac) (a : A).
+
+ Global Instance to_dfrac_agree_ne d : NonExpansive (@to_dfrac_agree A d).
+ Proof. solve_proper. Qed.
+ Global Instance to_dfrac_agree_proper d : Proper ((≡) ==> (≡)) (@to_dfrac_agree 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 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 -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 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.
+ rewrite /to_dfrac_agree. apply prod_update; last done.
+ simpl. apply dfrac_discard_update.
+ Qed.
+
+End lemmas.
+
+Typeclasses Opaque to_dfrac_agree.
diff --git a/iris/algebra/lib/frac_agree.v b/iris/algebra/lib/frac_agree.v
deleted file mode 100644
index 30495e642e0fe059fa2720e1496a51abb36f2da6..0000000000000000000000000000000000000000
--- a/iris/algebra/lib/frac_agree.v
+++ /dev/null
@@ -1,80 +0,0 @@
-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.
- rewrite /to_frac_agree -pair_op pair_valid to_agree_op_valid. 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.
- rewrite /to_frac_agree -pair_op pair_validN to_agree_op_validN. 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.
-
- (** 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. *)
- 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. rewrite -pair_op frac_op Hq.
- apply cmra_update_exclusive.
- rewrite frac_agree_op_valid Hq //.
- Qed.
-
-End lemmas.
-
-Typeclasses Opaque to_frac_agree.
diff --git a/iris/base_logic/lib/ghost_var.v b/iris/base_logic/lib/ghost_var.v
index 6a7c16a388c5f6df2952b92b15d83440f968545a..46a0fd5f188c40f54086b44fc60821bed23937ad 100644
--- a/iris/base_logic/lib/ghost_var.v
+++ b/iris/base_logic/lib/ghost_var.v
@@ -1,6 +1,6 @@
(** 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.