Merge branch 'ralf/dfrac_agree' into 'master'

equip frac_agree with support for dfrac

See merge request iris/iris!766

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/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 (A : ofe) : cmra := prodR dfracR (agreeR A).
+
+Definition to_dfrac_agree {A : ofe} (d : dfrac) (a : A) : dfrac_agreeR A :=
+  (d, to_agree a).
+Global Instance: Params (@to_dfrac_agree) 2 := {}.
+(** 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.
+Global Instance: Params (@to_frac_agree) 2 := {}.
+
+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.
+(* [to_frac_agree] is deliberately transparent to reuse the [to_dfrac_agree] instances *)

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/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.
@@ -78,11 +78,8 @@ Section lemmas.
     (q1 + q2 = 1)%Qp →
     ghost_var γ q1 a1 -∗ ghost_var γ q2 a2 ==∗ ghost_var γ q1 b ∗ ghost_var γ q2 b.
   Proof.
-    iIntros (Hq) "H1 H2".
-    iDestruct (ghost_var_valid_2 with "H1 H2") as %[_ ->].
-    iDestruct (fractional_merge with "H1 H2") as "H". simpl. rewrite Hq.
-    iMod (ghost_var_update with "H") as "H".
-    rewrite -Hq. iApply ghost_var_split. done.
+    intros Hq. unseal. rewrite -own_op. iApply own_update_2.
+    apply to_frac_agree_update_2. done.
   Qed.
   Lemma ghost_var_update_halves b γ a1 a2 :
     ghost_var γ (1/2) a1 -∗