add a simple logic-level ghost_var library

CHANGELOG.md

@@ -18,6 +18,8 @@ With this release, we dropped support for Coq 8.9.
   `ufrac_auth_agreeL` to `ufrac_auth_agree_L`.
 * Add constructions to define a camera through restriction of the validity predicate
   (`iso_cmra_mixin_restrict`) and through an isomophism (`iso_cmra_mixin`).
+* Add a `frac_agree` library which encapsulates `frac * agree A` for some OFE
+  `A`, and provides some useful lemmas.
 
 **Changes in `proofmode`:**
 
@@ -34,6 +36,11 @@ With this release, we dropped support for Coq 8.9.
   pure facts rather than the previous default of `a`. This also requires some
   changes if you were implementing `FromForall`, in order to forward names.
 
+**Changes in `base_logic`:**
+
+* Add a `ghost_var` library that provides (fractional) ownership of a ghost
+  variable of arbitrary `Type`.
+
 The following `sed` script helps adjust your code to the renaming (on macOS,
 replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
 Note that the script is not idempotent, do not run it twice.

_CoqProject

@@ -36,6 +36,7 @@ theories/algebra/namespace_map.v
 theories/algebra/lib/excl_auth.v
 theories/algebra/lib/frac_auth.v
 theories/algebra/lib/ufrac_auth.v
+theories/algebra/lib/frac_agree.v
 theories/si_logic/siprop.v
 theories/si_logic/bi.v
 theories/bi/notation.v
@@ -83,6 +84,7 @@ theories/base_logic/lib/gen_heap.v
 theories/base_logic/lib/gen_inv_heap.v
 theories/base_logic/lib/fancy_updates_from_vs.v
 theories/base_logic/lib/proph_map.v
+theories/base_logic/lib/ghost_var.v
 theories/program_logic/adequacy.v
 theories/program_logic/lifting.v
 theories/program_logic/weakestpre.v

theories/algebra/cmra.v

@@ -1165,11 +1165,14 @@ Section prod.
   Proof. done. Qed.
   Lemma pair_valid (a : A) (b : B) : ✓ (a, b) ↔ ✓ a ∧ ✓ b.
   Proof. done. Qed.
-  Lemma pair_validN n (a : A) (b : B) : ✓{n} (a, b) ↔ ✓{n} a ∧ ✓{n} b.
+  Lemma pair_validN (a : A) (b : B) n : ✓{n} (a, b) ↔ ✓{n} a ∧ ✓{n} b.
   Proof. done. Qed.
   Lemma pair_included (a a' : A) (b b' : B) :
     (a, b) ≼ (a', b') ↔ a ≼ a' ∧ b ≼ b'.
   Proof. apply prod_included. Qed.
+  Lemma pair_includedN (a a' : A) (b b' : B) n :
+    (a, b) ≼{n} (a', b') ↔ a ≼{n} a' ∧ b ≼{n} b'.
+  Proof. apply prod_includedN. Qed.
   Lemma pair_pcore (a : A) (b : B) :
     pcore (a, b) = c1 ← pcore a; c2 ← pcore b; Some (c1, c2).
   Proof. done. Qed.

theories/algebra/lib/frac_agree.v

+From iris.algebra Require Export frac agree updates local_updates.
+From iris.algebra Require Import proofmode_classes.
+From iris Require Import options.
+
+Definition frac_agreeR (A : ofeT) : cmraT := prodR fracR (agreeR A).
+
+Definition to_frac_agree {A : ofeT} (q : frac) (a : A) : frac_agreeR A :=
+  (q, to_agree a).
+
+Section lemmas.
+  Context {A : ofeT}.
+  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_valid q1 a1 q2 a2 :
+    ✓ (to_frac_agree q1 a1 ⋅ to_frac_agree q2 a2) →
+    ✓ (q1 + q2)%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)%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)%Qp ∧ a1 ≡{n}≡ a2.
+  Proof.
+    intros [Hq Ha]%pair_validN. simpl in *. split; first done.
+    apply to_agree_op_invN. done.
+  Qed.
+
+  (** No frame-preserving update lemma needed -- use [cmra_update_exclusive] with
+  the above [Exclusive] instance. *)
+
+End lemmas.
+
+Typeclasses Opaque to_frac_agree.

theories/base_logic/lib/ghost_var.v

+(** A simple "ghost variable" of arbitrary type with fractional ownership.
+Can be mutated when fully owned. *)
+From iris.bi.lib Require Import fractional.
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import frac_agree.
+From iris.base_logic.lib Require Export own.
+From iris Require Import options.
+
+(** The CMRA we need. *)
+Class ghost_varG Σ (A : Type) := GhostVarG {
+  ghost_var_inG :> inG Σ (frac_agreeR $ leibnizO A);
+}.
+Definition ghost_varΣ (A : Type) : gFunctors := #[ GFunctor (frac_agreeR $ leibnizO A) ].
+
+Instance subG_ghost_varΣ Σ A : subG (ghost_varΣ A) Σ → ghost_varG Σ A.
+Proof. solve_inG. Qed.
+
+Section definitions.
+  Context `{!ghost_varG Σ A} (γ : gname).
+
+  Definition ghost_var (q : Qp) (a : A) : iProp Σ :=
+    own γ (to_frac_agree (A:=leibnizO A) q a).
+End definitions.
+
+Section lemmas.
+  Context `{!ghost_varG Σ A}.
+  Implicit Types (a : A) (q : Qp).
+
+  Global Instance ghost_var_timeless γ q a : Timeless (ghost_var γ q a).
+  Proof. apply _. Qed.
+
+  Global Instance ghost_var_fractional γ a : Fractional (λ q, ghost_var γ q a).
+  Proof. intros q1 q2. rewrite /ghost_var -own_op -pair_op agree_idemp //. Qed.
+  Global Instance ghost_var_as_fractional γ a q :
+    AsFractional (ghost_var γ q a) (λ q, ghost_var γ q a) q.
+  Proof. split. done. apply _. Qed.
+
+  Lemma ghost_var_alloc_strong a (P : gname → Prop) :
+    pred_infinite P →
+    ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ ghost_var γ 1 a.
+  Proof.
+    iIntros (?). rewrite /ghost_var.
+    iMod (own_alloc_strong _ P) as (γ ?) "Hown"; by eauto.
+  Qed.
+  Lemma ghost_var_alloc a :
+    ⊢ |==> ∃ γ, ghost_var γ 1 a.
+  Proof. rewrite /ghost_var. iApply own_alloc. done. Qed.
+
+  Lemma ghost_var_op_valid γ a1 q1 a2 q2 :
+    ghost_var γ q1 a1 -∗ ghost_var γ q2 a2 -∗ ⌜✓ (q1 + q2)%Qp ∧ a1 = a2⌝.
+  Proof.
+    iIntros "Hvar1 Hvar2".
+    iDestruct (own_valid_2 with "Hvar1 Hvar2") as %[Hq Ha]%frac_agree_op_valid.
+    done.
+  Qed.
+
+  (** This is just an instance of fractionality above, but that can be hard to find. *)
+  Lemma ghost_var_split γ a q1 q2 :
+    ghost_var γ (q1 + q2) a -∗ ghost_var γ q1 a ∗ ghost_var γ q2 a.
+  Proof. iIntros "[$$]". Qed.
+
+  (** Update the ghost variable to new value [b]. *)
+  Lemma ghost_var_update b γ a :
+    ghost_var γ 1 a ==∗ ghost_var γ 1 b.
+  Proof.
+    iApply own_update. apply cmra_update_exclusive. done.
+  Qed. 
+
+End lemmas.
+
+Typeclasses Opaque ghost_var.