Notations and theory for `authR (optionUR (prodR fracR A))`.

_CoqProject

@@ -6,6 +6,7 @@ theories/algebra/big_op.v
 theories/algebra/cmra_big_op.v
 theories/algebra/sts.v
 theories/algebra/auth.v
+theories/algebra/frac_auth.v
 theories/algebra/gmap.v
 theories/algebra/ofe.v
 theories/algebra/base.v

theories/algebra/frac_auth.v

+From iris.algebra Require Export frac auth.
+From iris.algebra Require Export updates local_updates.
+From iris.proofmode Require Import classes.
+
+Definition frac_authR (A : cmraT) : cmraT :=
+  authR (optionUR (prodR fracR A)).
+Definition frac_authUR (A : cmraT) : ucmraT :=
+  authUR (optionUR (prodR fracR A)).
+
+Definition frac_auth_auth {A : cmraT} (x : A) : frac_authR A :=
+  ● (Some (1%Qp,x)).
+Definition frac_auth_frag {A : cmraT} (q : frac) (x : A) : frac_authR A :=
+  ◯ (Some (q,x)).
+
+Typeclasses Opaque frac_auth_auth frac_auth_frag.
+
+Instance: Params (@frac_auth_auth) 1.
+Instance: Params (@frac_auth_frag) 2.
+
+Notation "●! a" := (frac_auth_auth a) (at level 10).
+Notation "◯!{ q } a" := (frac_auth_frag q a) (at level 10, format "◯!{ q }  a").
+Notation "◯! a" := (frac_auth_frag 1 a) (at level 10).
+
+Section frac_auth.
+  Context {A : cmraT}.
+  Implicit Types a b : A.
+
+  Global Instance frac_auth_auth_ne : NonExpansive (@frac_auth_auth A).
+  Proof. solve_proper. Qed.
+  Global Instance frac_auth_auth_proper : Proper ((≡) ==> (≡)) (@frac_auth_auth A).
+  Proof. solve_proper. Qed.
+  Global Instance frac_auth_frag_ne q : NonExpansive (@frac_auth_frag A q).
+  Proof. solve_proper. Qed.
+  Global Instance frac_auth_frag_proper q : Proper ((≡) ==> (≡)) (@frac_auth_frag A q).
+  Proof. solve_proper. Qed.
+
+  Global Instance frac_auth_auth_timeless a : Timeless a → Timeless (●! a).
+  Proof. intros; apply Auth_timeless; apply _. Qed.
+  Global Instance frac_auth_frag_timeless a : Timeless a → Timeless (◯! a).
+  Proof. intros; apply Auth_timeless, Some_timeless; apply _. Qed.
+
+  Lemma frac_auth_validN n a : ✓{n} a → ✓{n} (●! a ⋅ ◯! a).
+  Proof. done. Qed.
+  Lemma frac_auth_valid a : ✓ a → ✓ (●! a ⋅ ◯! a).
+  Proof. done. Qed.
+
+  Lemma frac_auth_agreeN n a b : ✓{n} (●! a ⋅ ◯! b) → a ≡{n}≡ b.
+  Proof.
+    rewrite auth_validN_eq /= => -[Hincl Hvalid].
+    by move: Hincl=> /Some_includedN_exclusive /(_ Hvalid ) [??].
+  Qed.
+  Lemma frac_auth_agree a b : ✓ (●! a ⋅ ◯! b) → a ≡ b.
+  Proof.
+    intros. apply equiv_dist=> n. by apply frac_auth_agreeN, cmra_valid_validN.
+  Qed.
+  Lemma frac_auth_agreeL `{!LeibnizEquiv A} a b : ✓ (●! a ⋅ ◯! b) → a = b.
+  Proof. intros. by apply leibniz_equiv, frac_auth_agree. Qed.
+
+  Lemma frac_auth_includedN n q a b : ✓{n} (●! a ⋅ ◯!{q} b) → Some b ≼{n} Some a.
+  Proof. by rewrite auth_validN_eq /= => -[/Some_pair_includedN [_ ?] _]. Qed.
+  Lemma frac_auth_included `{CMRADiscrete A} q a b :
+    ✓ (●! a ⋅ ◯!{q} b) → Some b ≼ Some a.
+  Proof. by rewrite auth_valid_discrete /= => -[/Some_pair_included [_ ?] _]. Qed.
+  Lemma frac_auth_includedN_total `{CMRATotal A} n q a b :
+    ✓{n} (●! a ⋅ ◯!{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 :
+    ✓ (●! a ⋅ ◯!{q} b) → b ≼ a.
+  Proof. intros. by eapply Some_included_total, frac_auth_included. Qed.
+
+  Lemma frac_auth_auth_validN n a : ✓{n} (●! a) ↔ ✓{n} a.
+  Proof.
+    split; [by intros [_ [??]]|].
+    by repeat split; simpl; auto using ucmra_unit_leastN.
+  Qed.
+  Lemma frac_auth_auth_valid a : ✓ (●! a) ↔ ✓ a.
+  Proof. rewrite !cmra_valid_validN. by setoid_rewrite frac_auth_auth_validN. Qed.
+
+  Lemma frac_auth_frag_validN n q a : ✓{n} (◯!{q} a) ↔ ✓{n} q ∧ ✓{n} a.
+  Proof. done. Qed.
+  Lemma frac_auth_frag_valid q a : ✓ (◯!{q} a) ↔ ✓ q ∧ ✓ a.
+  Proof. done. Qed.
+
+  Lemma frag_auth_op q1 q2 a1 a2 : ◯!{q1+q2} (a1 ⋅ a2) ≡ ◯!{q1} a1 ⋅ ◯!{q2} a2.
+  Proof. done. Qed.
+
+  Global Instance into_op_frac_auth (q q1 q2 : frac) (a a1 a2 : A) :
+    IntoOp q q1 q2 → IntoOp a a1 a2 → IntoOp (◯!{q} a) (◯!{q1} a1) (◯!{q2} a2).
+  Proof. by rewrite /IntoOp=> /leibniz_equiv_iff -> ->. Qed.
+  Global Instance from_op_frac_auth (q q1 q2 : frac) (a a1 a2 : A) :
+    FromOp q q1 q2 → FromOp a a1 a2 → FromOp (◯!{q} a) (◯!{q1} a1) (◯!{q2} a2).
+  Proof. by rewrite /FromOp=> /leibniz_equiv_iff <- <-. Qed.
+
+  Global Instance into_op_frac_auth_persistent (q q1 q2 : frac) (a  : A) :
+    IntoOp q q1 q2 → Persistent a → IntoOp (◯!{q} a) (◯!{q1} a) (◯!{q2} a).
+  Proof.
+    rewrite /IntoOp=> /leibniz_equiv_iff -> ?.
+    by rewrite -frag_auth_op -persistent_dup.
+  Qed.
+  Global Instance from_op_frac_auth_persistent (q q1 q2 : frac) (a : A) :
+    FromOp q q1 q2 → Persistent a → FromOp (◯!{q} a) (◯!{q1} a) (◯!{q2} a).
+  Proof.
+    rewrite /FromOp=> /leibniz_equiv_iff <- ?.
+    by rewrite -frag_auth_op -persistent_dup.
+  Qed.
+
+  Lemma frac_auth_update q a b a' b' :
+    (a,b) ~l~> (a',b') → ●! a ⋅ ◯!{q} b ~~> ●! a' ⋅ ◯!{q} b'.
+  Proof.
+    intros. by apply auth_update, option_local_update, prod_local_update_2.
+  Qed.
+End frac_auth.

theories/heap_lang/lib/counter.v

@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre.
 From iris.base_logic.lib Require Export invariants.
 From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import frac auth.
+From iris.algebra Require Import frac_auth auth.
 From iris.heap_lang Require Import proofmode notation.
 Set Default Proof Using "Type".
 
@@ -83,9 +83,9 @@ End mono_proof.
 
 (** Counter with contributions *)
 Class ccounterG Σ :=
-  CCounterG { ccounter_inG :> inG Σ (authR (optionUR (prodR fracR natR))) }.
+  CCounterG { ccounter_inG :> inG Σ (frac_authR natR) }.
 Definition ccounterΣ : gFunctors :=
-  #[GFunctor (authR (optionUR (prodR fracR natR)))].
+  #[GFunctor (frac_authR natR)].
 
 Instance subG_ccounterΣ {Σ} : subG ccounterΣ Σ → ccounterG Σ.
 Proof. solve_inG. Qed.
@@ -94,26 +94,25 @@ Section contrib_spec.
   Context `{!heapG Σ, !ccounterG Σ} (N : namespace).
 
   Definition ccounter_inv (γ : gname) (l : loc) : iProp Σ :=
-    (∃ n, own γ (● Some (1%Qp, n)) ∗ l ↦ #n)%I.
+    (∃ n, own γ (●! n) ∗ l ↦ #n)%I.
 
   Definition ccounter_ctx (γ : gname) (l : loc) : iProp Σ :=
     inv N (ccounter_inv γ l).
 
   Definition ccounter (γ : gname) (q : frac) (n : nat) : iProp Σ :=
-    own γ (◯ Some (q, n)).
+    own γ (◯!{q} n).
 
   (** The main proofs. *)
   Lemma ccounter_op γ q1 q2 n1 n2 :
-    ccounter γ (q1 + q2) (n1 + n2) ⊣⊢ ccounter γ q1 n1∗ ccounter γ q2 n2.
-  Proof. by rewrite /ccounter -own_op -auth_frag_op. Qed.
+    ccounter γ (q1 + q2) (n1 + n2) ⊣⊢ ccounter γ q1 n1 ∗ ccounter γ q2 n2.
+  Proof. by rewrite /ccounter frag_auth_op -own_op. Qed.
 
   Lemma newcounter_contrib_spec (R : iProp Σ) :
     {{{ True }}} newcounter #()
     {{{ γ l, RET #l; ccounter_ctx γ l ∗ ccounter γ 1 0 }}}.
   Proof.
     iIntros (Φ) "HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
-    iMod (own_alloc (● (Some (1%Qp, O%nat)) ⋅ ◯ (Some (1%Qp, 0%nat))))
-      as (γ) "[Hγ Hγ']"; first done.
+    iMod (own_alloc (●! O%nat ⋅ ◯! 0%nat)) as (γ) "[Hγ Hγ']"; first done.
     iMod (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]").
     { iNext. iExists 0%nat. by iFrame. }
     iModIntro. iApply "HΦ". rewrite /ccounter_ctx /ccounter; eauto 10.
@@ -130,8 +129,7 @@ Section contrib_spec.
     wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]" "Hclose".
     destruct (decide (c' = c)) as [->|].
     - iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
-      { apply auth_update, option_local_update, prod_local_update_2.
-        apply (nat_local_update _ _ (S c) (S n)); omega. }
+      { apply frac_auth_update, (nat_local_update _ _ (S c) (S n)); omega. }
       wp_cas_suc. iMod ("Hclose" with "[Hl Hγ]") as "_".
       { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
       iModIntro. wp_if. by iApply "HΦ".
@@ -146,8 +144,7 @@ Section contrib_spec.
   Proof.
     iIntros (Φ) "[#? Hγf] HΦ".
     rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
-    iDestruct (own_valid_2 with "Hγ Hγf")
-      as %[[? ?%nat_included]%Some_pair_included_total_2 _]%auth_valid_discrete_2.
+    iDestruct (own_valid_2 with "Hγ Hγf") as % ?%frac_auth_included_total%nat_included.
     iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
     iApply ("HΦ" with "[-]"); rewrite /ccounter; eauto 10.
   Qed.
@@ -158,8 +155,7 @@ Section contrib_spec.
   Proof.
     iIntros (Φ) "[#? Hγf] HΦ".
     rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
-    iDestruct (own_valid_2 with "Hγ Hγf") as %[Hn _]%auth_valid_discrete_2.
-    apply (Some_included_exclusive _) in Hn as [= ->]%leibniz_equiv; last done.
+    iDestruct (own_valid_2 with "Hγ Hγf") as % <-%frac_auth_agreeL.
     iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
     by iApply "HΦ".
   Qed.