11(* Modified version supporting persistent ghost vars. *)
22
3- (** A simple "ghost variable" of arbitrary type with fractional ownership.
4- Can be mutated when fully owned. *)
5- From iris.algebra Require Import dfrac dfrac_agree.
6- From iris.bi.lib Require Import fractional.
3+ From iris.algebra Require Import dfrac_agree.
74From iris.proofmode Require Import proofmode.
8- From iris.base_logic.lib Require Export own.
5+ From iris.base_logic.lib Require Export own ghost_var .
96From iris.prelude Require Import options.
107
11- (** The CMRA we need. *)
12- Class ghost_varG Σ (A : Type ) := GhostVarG {
13- ghost_var_inG : inG Σ (dfrac_agreeR $ leibnizO A);
14- }.
158Local Existing Instance ghost_var_inG.
16- Global Hint Mode ghost_varG - ! : typeclass_instances.
17-
18- Definition ghost_varΣ (A : Type ) : gFunctors :=
19- #[ GFunctor (dfrac_agreeR $ leibnizO A) ].
20-
21- Global Instance subG_ghost_varΣ Σ A : subG (ghost_varΣ A) Σ → ghost_varG Σ A.
22- Proof . solve_inG. Qed .
23-
24- Local Definition ghost_var_def `{!ghost_varG Σ A}
25- (γ : gname) (q : Qp) (a : A) : iProp Σ :=
26- own γ (to_frac_agree (A:=leibnizO A) q a).
27- Local Definition ghost_var_aux : seal (@ghost_var_def). Proof . by eexists. Qed .
28- Definition ghost_var := ghost_var_aux.(unseal).
29- Local Definition ghost_var_unseal :
30- @ghost_var = @ghost_var_def := ghost_var_aux.(seal_eq).
31- Global Arguments ghost_var {Σ A _} γ q a.
329
3310Local Definition persistent_ghost_var_def `{!ghost_varG Σ A}
3411 (γ : gname) (a : A) : iProp Σ :=
@@ -39,88 +16,46 @@ Local Definition persistent_ghost_var_unseal :
3916 @persistent_ghost_var = @persistent_ghost_var_def := persistent_ghost_var_aux.(seal_eq).
4017Global Arguments persistent_ghost_var {Σ A _} γ a.
4118
42- Local Ltac unseal := rewrite ?ghost_var_unseal /ghost_var_def ?persistent_ghost_var_unseal /persistent_ghost_var_def.
19+ Local Ltac unseal := rewrite
20+ ?ghost_var.ghost_var_unseal /ghost_var.ghost_var_def
21+ ?persistent_ghost_var_unseal /persistent_ghost_var_def.
4322
4423Section lemmas.
4524 Context `{!ghost_varG Σ A}.
4625 Implicit Types (a b : A) (q : Qp).
4726
48- Global Instance ghost_var_timeless γ q a : Timeless (ghost_var γ q a).
49- Proof . unseal. apply _. Qed .
50-
51- Global Instance ghost_var_fractional γ a : Fractional (λ q, ghost_var γ q a).
52- Proof . intros q1 q2. unseal. rewrite -own_op -frac_agree_op //. Qed .
53- Global Instance ghost_var_as_fractional γ a q :
54- AsFractional (ghost_var γ q a) (λ q, ghost_var γ q a) q.
55- Proof . split; [done|]. apply _. Qed .
56-
5727 Global Instance persistent_ghost_var_timeless γ a : Timeless (persistent_ghost_var γ a).
5828 Proof . unseal. apply _. Qed .
5929 Global Instance persistent_ghost_var_persistent γ a : Persistent (persistent_ghost_var γ a).
6030 Proof . unseal. apply _. Qed .
6131
62- Lemma ghost_var_alloc_strong a (P : gname → Prop ) :
63- pred_infinite P →
64- ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ ghost_var γ 1 a.
65- Proof . unseal. intros. iApply own_alloc_strong; done. Qed .
66- Lemma ghost_var_alloc a :
67- ⊢ |==> ∃ γ, ghost_var γ 1 a.
68- Proof . unseal. iApply own_alloc. done. Qed .
32+ (** Persistent ghost var rules *)
33+ Lemma ghost_var_persist γ q a :
34+ ghost_var γ q a ==∗ persistent_ghost_var γ a.
35+ Proof . unseal. iApply own_update. apply dfrac_agree_persist. Qed .
6936
70- Lemma ghost_var_valid_2 γ a1 q1 a2 q2 :
71- ghost_var γ q1 a1 -∗ ghost_var γ q2 a2 -∗ ⌜(q1 + q2 ≤ 1)%Qp ∧ a1 = a2⌝.
37+ Lemma persistent_ghost_var_valid_2 γ a1 a2 q2 :
38+ persistent_ghost_var γ a1 -∗ ghost_var γ q2 a2 -∗ ⌜(q2 < 1)%Qp ∧ a1 = a2⌝.
7239 Proof .
7340 unseal. iIntros "Hvar1 Hvar2".
74- by iCombine "Hvar1 Hvar2" gives %?%frac_agree_op_valid.
41+ iCombine "Hvar1 Hvar2" gives %[Hq Ha]%dfrac_agree_op_valid_L.
42+ done.
7543 Qed .
7644 (** Almost all the time, this is all you really need. *)
77- Lemma ghost_var_agree γ a1 q1 a2 q2 :
78- ghost_var γ q1 a1 -∗ ghost_var γ q2 a2 -∗ ⌜a1 = a2⌝.
45+ Lemma persistent_ghost_var_agree γ a1 a2 q2 :
46+ persistent_ghost_var γ a1 -∗ ghost_var γ q2 a2 -∗ ⌜a1 = a2⌝.
7947 Proof .
8048 iIntros "Hvar1 Hvar2".
81- iDestruct (ghost_var_valid_2 with "Hvar1 Hvar2") as %[_ ?]. done.
49+ iDestruct (persistent_ghost_var_valid_2 with "Hvar1 Hvar2") as %[_ ?]. done.
8250 Qed .
8351
84- (** This is just an instance of fractionality above, but that can be hard to find. *)
85- Lemma ghost_var_split γ a q1 q2 :
86- ghost_var γ (q1 + q2) a -∗ ghost_var γ q1 a ∗ ghost_var γ q2 a.
87- Proof . iIntros "[$$]". Qed .
88-
89- (** Update the ghost variable to new value [b]. *)
90- Lemma ghost_var_update b γ a :
91- ghost_var γ 1 a ==∗ ghost_var γ 1 b.
52+ Global Instance ghost_var_combine_gives γ a1 a2 q2 :
53+ CombineSepGives (persistent_ghost_var γ a1) (ghost_var γ q2 a2)
54+ ⌜(q2 < 1)%Qp ∧ a1 = a2⌝.
9255 Proof .
93- unseal. iApply own_update. apply cmra_update_exclusive. done.
56+ rewrite /CombineSepGives. iIntros "[H1 H2]".
57+ iDestruct (persistent_ghost_var_valid_2 with "H1 H2") as %[H1 H2].
58+ eauto.
9459 Qed .
95- Lemma ghost_var_update_2 b γ a1 q1 a2 q2 :
96- (q1 + q2 = 1)%Qp →
97- ghost_var γ q1 a1 -∗ ghost_var γ q2 a2 ==∗ ghost_var γ q1 b ∗ ghost_var γ q2 b.
98- Proof .
99- intros Hq. unseal. rewrite -own_op. iApply own_update_2.
100- apply frac_agree_update_2. done.
101- Qed .
102- Lemma ghost_var_update_halves b γ a1 a2 :
103- ghost_var γ (1/2) a1 -∗
104- ghost_var γ (1/2) a2 ==∗
105- ghost_var γ (1/2) b ∗ ghost_var γ (1/2) b.
106- Proof . iApply ghost_var_update_2. apply Qp.half_half. Qed .
107-
108- (** Framing support *)
109- Global Instance frame_ghost_var p γ a q1 q2 q :
110- FrameFractionalQp q1 q2 q →
111- Frame p (ghost_var γ q1 a) (ghost_var γ q2 a) (ghost_var γ q a) | 5.
112- Proof . apply: frame_fractional. Qed .
113-
114- (** Persistent ghost var rules *)
115- Lemma ghost_var_persist γ q a :
116- ghost_var γ q a ==∗ persistent_ghost_var γ a.
117- Proof . unseal. iApply own_update. apply dfrac_agree_persist. Qed .
11860
119- Lemma persistent_ghost_var_agree γ a1 a2 q2 :
120- persistent_ghost_var γ a1 -∗ ghost_var γ q2 a2 -∗ ⌜a1 = a2⌝.
121- Proof .
122- unseal. iIntros "Hvar1 Hvar2".
123- by iCombine "Hvar1 Hvar2" gives %[? ?]%dfrac_agree_op_valid_L.
124- Qed .
12561End lemmas.
126-
0 commit comments