From eec9bb1ef465465031bbf69e2a692ec7def2f446 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 15 Sep 2020 22:53:29 +0200
Subject: [PATCH] add a simple logic-level ghost_var library
---
CHANGELOG.md | 7 +++
_CoqProject | 2 +
theories/algebra/cmra.v | 5 +-
theories/algebra/lib/frac_agree.v | 52 +++++++++++++++++++++
theories/base_logic/lib/ghost_var.v | 71 +++++++++++++++++++++++++++++
5 files changed, 136 insertions(+), 1 deletion(-)
create mode 100644 theories/algebra/lib/frac_agree.v
create mode 100644 theories/base_logic/lib/ghost_var.v
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 14f70ed9b..577fa1fa4 100644
--- a/CHANGELOG.md
+++ b/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.
diff --git a/_CoqProject b/_CoqProject
index 5cbaf6389..f6180b181 100644
--- a/_CoqProject
+++ b/_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
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index cb92fba97..6d0a9041e 100644
--- a/theories/algebra/cmra.v
+++ b/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.
diff --git a/theories/algebra/lib/frac_agree.v b/theories/algebra/lib/frac_agree.v
new file mode 100644
index 000000000..b096e871f
--- /dev/null
+++ b/theories/algebra/lib/frac_agree.v
@@ -0,0 +1,52 @@
+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.
diff --git a/theories/base_logic/lib/ghost_var.v b/theories/base_logic/lib/ghost_var.v
new file mode 100644
index 000000000..d8e270e00
--- /dev/null
+++ b/theories/base_logic/lib/ghost_var.v
@@ -0,0 +1,71 @@
+(** 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.
--
GitLab