Add fraction.

iris/algebra/lib/bij_view.v

@@ -106,10 +106,10 @@ Definition bij_viewR A B `{Countable A, Countable B} : cmraT :=
 Definition bij_viewUR A B `{Countable A, Countable B} : ucmraT :=
   viewUR (bij_view_rel (A:=A) (B:=B)).
 
-Definition bij_auth `{Countable A, Countable B} (L : gset (A * B)) : bij_view A B :=
-  ●V L ⋅ ◯V L.
-Definition bij_elem `{Countable A, Countable B} (a : A) (b : B) : bij_view A B :=
-  ◯V {[a, b]}.
+Definition bij_auth `{Countable A, Countable B}
+  (q : Qp) (L : gset (A * B)) : bij_view A B := ●V{q} L ⋅ ◯V L.
+Definition bij_elem `{Countable A, Countable B}
+  (a : A) (b : B) : bij_view A B := ◯V {[a, b]}.
 
 Section bij.
   Context `{Countable A, Countable B}.
@@ -119,23 +119,55 @@ Section bij.
   Global Instance bij_elem_core_id a b : CoreId (bij_elem a b).
   Proof. apply _. Qed.
 
-  Lemma bij_auth_valid L : ✓ bij_auth L ↔ gset_bijective L.
+  Lemma bij_auth_frac_op q1 q2 L :
+    bij_auth q1 L ⋅ bij_auth q2 L ≡ bij_auth (q1 + q2) L.
   Proof.
-    rewrite /bij_auth view_both_valid.
+    rewrite /bij_auth view_auth_frac_op.
+    rewrite (comm _ (●V{q2} _)) -!assoc (assoc _ (◯V _)).
+    by rewrite -core_id_dup (comm _ (◯V _)).
+  Qed.
+
+  Lemma bij_auth_frac_valid q L : ✓ bij_auth q L ↔ ✓ q ∧ gset_bijective L.
+  Proof.
+    rewrite /bij_auth view_both_frac_valid.
     setoid_rewrite bij_view_rel_iff.
     naive_solver eauto using O.
   Qed.
+  Lemma bij_auth_valid L : ✓ bij_auth 1 L ↔ gset_bijective L.
+  Proof. rewrite bij_auth_frac_valid. naive_solver by done. Qed.
+
+  Lemma bij_auth_empty_frac_valid q : ✓ bij_auth (A:=A) (B:=B) q ∅ ↔ ✓ q.
+  Proof.
+    rewrite bij_auth_frac_valid. naive_solver eauto using gset_bijective_empty.
+  Qed.
+  Lemma bij_auth_empty_valid : ✓ bij_auth (A:=A) (B:=B) 1 ∅.
+  Proof. by apply bij_auth_empty_frac_valid. Qed.
 
-  Lemma bij_auth_valid_empty : ✓ bij_auth (A:=A) (B:=B) ∅.
-  Proof. apply bij_auth_valid, gset_bijective_empty. Qed.
+  Lemma bij_auth_frac_op_valid q1 q2 L1 L2 :
+    ✓ (bij_auth q1 L1 ⋅ bij_auth q2 L2)
+    ↔ ✓ (q1 + q2)%Qp ∧ L1 = L2 ∧ gset_bijective L1.
+  Proof.
+    rewrite /bij_auth (comm _ (●V{q2} _)) -!assoc (assoc _ (◯V _)).
+    rewrite -view_frag_op (comm _ (◯V _)) assoc. split.
+    - move=> /cmra_valid_op_l /view_auth_frac_op_valid.
+      setoid_rewrite bij_view_rel_iff. naive_solver eauto using 0.
+    - intros (?&->&?). rewrite -core_id_dup -view_auth_frac_op.
+      apply view_both_frac_valid. setoid_rewrite bij_view_rel_iff. naive_solver.
+  Qed.
+  Lemma bij_auth_op_valid L1 L2 :
+    ✓ (bij_auth 1 L1 ⋅ bij_auth 1 L2) ↔ False.
+  Proof. rewrite bij_auth_frac_op_valid. naive_solver. Qed.
 
-  Lemma bij_both_el_valid L a b :
-    ✓ (bij_auth L ⋅ bij_elem a b) ↔ gset_bijective L ∧ (a, b) ∈ L.
+  Lemma bij_both_frac_valid q L a b :
+    ✓ (bij_auth q L ⋅ bij_elem a b) ↔ ✓ q ∧ gset_bijective L ∧ (a, b) ∈ L.
   Proof.
-    rewrite /bij_auth /bij_elem -assoc -view_frag_op view_both_valid.
+    rewrite /bij_auth /bij_elem -assoc -view_frag_op view_both_frac_valid.
     setoid_rewrite bij_view_rel_iff.
     set_solver by eauto using O.
   Qed.
+  Lemma bij_both_valid L a b :
+    ✓ (bij_auth 1 L ⋅ bij_elem a b) ↔ gset_bijective L ∧ (a, b) ∈ L.
+  Proof. rewrite bij_both_frac_valid. naive_solver by done. Qed.
 
   Lemma bij_elem_agree a1 b1 a2 b2 :
     ✓ (bij_elem a1 b1 ⋅ bij_elem a2 b2) → (a1 = a2 ↔ b1 = b2).
@@ -145,7 +177,7 @@ Section bij.
     naive_solver eauto using subseteq_gset_bijective, O.
   Qed.
 
-  Lemma bij_view_included L a b : (a,b) ∈ L → bij_elem a b ≼ bij_auth L.
+  Lemma bij_view_included q L a b : (a,b) ∈ L → bij_elem a b ≼ bij_auth q L.
   Proof.
     intros. etrans; [|apply cmra_included_r].
     apply view_frag_mono, gset_included. set_solver.
@@ -153,7 +185,7 @@ Section bij.
 
   Lemma bij_auth_extend L a b :
     (∀ b', (a, b') ∉ L) → (∀ a', (a', b) ∉ L) →
-    bij_auth L ~~> bij_auth ({[(a, b)]} ∪ L).
+    bij_auth 1 L ~~> bij_auth 1 ({[(a, b)]} ∪ L).
   Proof.
     intros. apply view_update=> n bijL.
     rewrite !bij_view_rel_iff gset_op_union.

iris/base_logic/lib/bij.v

@@ -19,6 +19,7 @@ that the set of associations only grows; this is captured by the persistence of
 This library is a logical, ownership-based wrapper around bij_view.v. *)
 
 From iris.algebra.lib Require Import bij_view.
+From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Import own.
 From iris.proofmode Require Import tactics.
 From iris.prelude Require Import options.
@@ -33,37 +34,58 @@ Global Instance subG_bijΣ `{Countable A, Countable B} Σ :
   subG (bijΣ A B) Σ → bijG A B Σ.
 Proof. solve_inG. Qed.
 
+Definition bij_own_auth_def `{bijG A B Σ} (γ : gname)
+  (q : Qp) (L : gset (A * B)) : iProp Σ := own γ (bij_auth q L).
+Definition bij_own_auth_aux : seal (@bij_own_auth_def). Proof. by eexists. Qed.
+Definition bij_own_auth := unseal bij_own_auth_aux.
+Definition bij_own_auth_eq :
+  @bij_own_auth = @bij_own_auth_def := seal_eq bij_own_auth_aux.
+Arguments bij_own_auth {_ _ _ _ _ _ _ _}.
+
+Definition bij_own_elem_def `{bijG A B Σ} (γ : gname)
+  (a : A) (b : B) : iProp Σ := own γ (bij_elem a b).
+Definition bij_own_elem_aux : seal (@bij_own_elem_def). Proof. by eexists. Qed.
+Definition bij_own_elem := unseal bij_own_elem_aux.
+Definition bij_own_elem_eq :
+  @bij_own_elem = @bij_own_elem_def := seal_eq bij_own_elem_aux.
+Arguments bij_own_elem {_ _ _ _ _ _ _ _}.
+
 Section bij.
   Context `{bijG A B Σ}.
-  Implicit Types (L: gsetO (A * B)).
-  Implicit Types (a:A) (b:B).
-
-  Definition bij_own_auth_def γ L : iProp Σ := own γ (bij_auth L).
-  Definition bij_own_auth_aux : seal (@bij_own_auth_def). Proof. by eexists. Qed.
-  Definition bij_own_auth := unseal bij_own_auth_aux.
-  Definition bij_own_auth_eq :
-    @bij_own_auth = @bij_own_auth_def := seal_eq bij_own_auth_aux.
-
-  Definition bij_own_elem_def γ a b: iProp Σ := own γ (bij_elem a b).
-  Definition bij_own_elem_aux : seal (@bij_own_elem_def). Proof. by eexists. Qed.
-  Definition bij_own_elem := unseal bij_own_elem_aux.
-  Definition bij_own_elem_eq :
-    @bij_own_elem = @bij_own_elem_def := seal_eq bij_own_elem_aux.
-
-  Global Instance bij_own_auth_timeless γ L : Timeless (bij_own_auth γ L).
-  Proof. rewrite bij_own_auth_eq. apply _. Qed.
+  Implicit Types (L : gset (A * B)) (a : A) (b : B).
 
+  Global Instance bij_own_auth_timeless γ q L : Timeless (bij_own_auth γ q L).
+  Proof. rewrite bij_own_auth_eq. apply _. Qed.
   Global Instance bij_own_elem_timeless γ a b : Timeless (bij_own_elem γ a b).
   Proof. rewrite bij_own_elem_eq. apply _. Qed.
-
   Global Instance bij_own_elem_persistent γ a b : Persistent (bij_own_elem γ a b).
   Proof. rewrite bij_own_elem_eq. apply _. Qed.
 
-  Lemma bij_own_bijective γ L :
-    bij_own_auth γ L -∗ ⌜gset_bijective L⌝.
+  Global Instance bij_own_auth_fractional γ L : Fractional (λ q, bij_own_auth γ q L).
+  Proof. intros p q. rewrite bij_own_auth_eq -own_op bij_auth_frac_op //. Qed.
+  Global Instance bij_own_auth_as_fractional γ q L :
+    AsFractional (bij_own_auth γ q L) (λ q, bij_own_auth γ q L) q.
+  Proof. split; [auto|apply _]. Qed.
+
+  Lemma bij_own_auth_agree γ q1 q2 L1 L2 :
+    bij_own_auth γ q1 L1 -∗ bij_own_auth γ q2 L2 -∗
+    ⌜✓ (q1 + q2)%Qp ∧ L1 = L2 ∧ gset_bijective L1⌝.
+  Proof.
+    rewrite bij_own_auth_eq. iIntros "H1 H2".
+    by iDestruct (own_valid_2 with "H1 H2") as %?%bij_auth_frac_op_valid.
+  Qed.
+  Lemma bij_own_auth_exclusive γ L1 L2 :
+    bij_own_auth γ 1 L1 -∗ bij_own_auth γ 1 L2 -∗ False.
+  Proof.
+    iIntros "H1 H2".
+    by iDestruct (bij_own_auth_agree with "H1 H2") as %[[] _].
+  Qed.
+
+  Lemma bij_own_valid γ q L :
+    bij_own_auth γ q L -∗ ⌜✓ q ∧ gset_bijective L⌝.
   Proof.
     rewrite bij_own_auth_eq. iIntros "Hauth".
-    iDestruct (own_valid with "Hauth") as %?%bij_auth_valid; done.
+    by iDestruct (own_valid with "Hauth") as %?%bij_auth_frac_valid.
   Qed.
 
   Lemma bij_own_elem_agree γ L a a' b b' :
@@ -74,15 +96,15 @@ Section bij.
     by iDestruct (own_valid_2 with "Hel1 Hel2") as %?%bij_elem_agree.
   Qed.
 
-  Lemma bij_get_elem γ L a b :
+  Lemma bij_get_elem γ q L a b :
     (a, b) ∈ L →
-    bij_own_auth γ L -∗ bij_own_elem γ a b.
+    bij_own_auth γ q L -∗ bij_own_elem γ a b.
   Proof.
     intros. rewrite bij_own_auth_eq bij_own_elem_eq.
     by apply own_mono, bij_view_included.
   Qed.
-  Lemma bij_get_big_sepS_elem γ L :
-    bij_own_auth γ L -∗ [∗ set] ab ∈ L, bij_own_elem γ ab.1 ab.2.
+  Lemma bij_get_big_sepS_elem γ q L :
+    bij_own_auth γ q L -∗ [∗ set] ab ∈ L, bij_own_elem γ ab.1 ab.2.
   Proof.
     iIntros "Hauth". iApply big_sepS_forall. iIntros ([a b] ?) "/=".
     by iApply bij_get_elem.
@@ -90,22 +112,22 @@ Section bij.
 
   Lemma bij_own_alloc L :
     gset_bijective L →
-    ⊢ |==> ∃ γ, bij_own_auth γ L ∗ [∗ set] ab ∈ L, bij_own_elem γ ab.1 ab.2.
+    ⊢ |==> ∃ γ, bij_own_auth γ 1 L ∗ [∗ set] ab ∈ L, bij_own_elem γ ab.1 ab.2.
   Proof.
-    intro. iAssert (∃ γ, bij_own_auth γ L)%I with "[>]" as (γ) "Hauth".
+    intro. iAssert (∃ γ, bij_own_auth γ 1 L)%I with "[>]" as (γ) "Hauth".
     { rewrite bij_own_auth_eq. iApply own_alloc. by apply bij_auth_valid. }
     iExists γ. iModIntro. iSplit; [done|]. by iApply bij_get_big_sepS_elem.
  Qed.
   Lemma bij_own_alloc_empty :
-    ⊢ |==> ∃ γ, bij_own_auth γ ∅.
+    ⊢ |==> ∃ γ, bij_own_auth γ 1 ∅.
   Proof. iMod (bij_own_alloc ∅) as (γ) "[Hauth _]"; by auto. Qed.
 
   Lemma bij_own_extend γ L a b :
     (∀ b', (a, b') ∉ L) → (∀ a', (a', b) ∉ L) →
-    bij_own_auth γ L ==∗ bij_own_auth γ ({[(a, b)]} ∪ L) ∗ bij_own_elem γ a b.
+    bij_own_auth γ 1 L ==∗ bij_own_auth γ 1 ({[(a, b)]} ∪ L) ∗ bij_own_elem γ a b.
   Proof.
     iIntros (??) "Hauth".
-    iAssert (bij_own_auth γ ({[a, b]} ∪ L)) with "[> Hauth]" as "Hauth".
+    iAssert (bij_own_auth γ 1 ({[a, b]} ∪ L)) with "[> Hauth]" as "Hauth".
     { rewrite bij_own_auth_eq. iApply (own_update with "Hauth").
       by apply bij_auth_extend. }
     iModIntro. iSplit; [done|]. iApply (bij_get_elem with "Hauth"). set_solver.
@@ -114,7 +136,7 @@ Section bij.
   Lemma bij_own_extend_internal γ L a b :
     (∀ b', bij_own_elem γ a b' -∗ False) -∗
     (∀ a', bij_own_elem γ a' b -∗ False) -∗
-    bij_own_auth γ L ==∗ bij_own_auth γ ({[(a, b)]} ∪ L) ∗ bij_own_elem γ a b.
+    bij_own_auth γ 1 L ==∗ bij_own_auth γ 1 ({[(a, b)]} ∪ L) ∗ bij_own_elem γ a b.
   Proof.
     iIntros "Ha Hb HL".
     iAssert ⌜∀ b', (a, b') ∉ L⌝%I as %?.