own.v 10.2 KB
Newer Older
1
From iris.algebra Require Import functions gmap.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
From iris.base_logic.lib Require Export iprop.
3
From iris.algebra Require Import proofmode_classes.
4
Set Default Proof Using "Type".
5 6
Import uPred.

7 8
(** The class [inG Σ A] expresses that the CMRA [A] is in the list of functors
[Σ]. This class is similar to the [subG] class, but written down in terms of
9
individual CMRAs instead of (lists of) CMRA *functors*. This additional class is
10 11 12 13 14 15 16 17 18
needed because Coq is otherwise unable to solve type class constraints due to
higher-order unification problems. *)
Class inG (Σ : gFunctors) (A : cmraT) :=
  InG { inG_id : gid Σ; inG_prf : A = Σ inG_id (iPreProp Σ) }.
Arguments inG_id {_ _} _.

Lemma subG_inG Σ (F : gFunctor) : subG F Σ  inG Σ (F (iPreProp Σ)).
Proof. move=> /(_ 0%fin) /= [j ->]. by exists j. Qed.

19 20 21 22
(** This tactic solves the usual obligations "subG ? Σ → {in,?}G ? Σ" *)
Ltac solve_inG :=
  (* Get all assumptions *)
  intros;
23
  (* Unfold the top-level xΣ. We need to support this to be a function. *)
24
  lazymatch goal with
25 26 27
  | H : subG (?xΣ _ _ _ _) _ |- _ => try unfold xΣ in H
  | H : subG (?xΣ _ _ _) _ |- _ => try unfold xΣ in H
  | H : subG (?xΣ _ _) _ |- _ => try unfold xΣ in H
28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48
  | H : subG (?xΣ _) _ |- _ => try unfold xΣ in H
  | H : subG ?xΣ _ |- _ => try unfold xΣ in H
  end;
  (* Take apart subG for non-"atomic" lists *)
  repeat match goal with
         | H : subG (gFunctors.app _ _) _ |- _ => apply subG_inv in H; destruct H
         end;
  (* Try to turn singleton subG into inG; but also keep the subG for typeclass
     resolution -- to keep them, we put them onto the goal. *)
  repeat match goal with
         | H : subG _ _ |- _ => move:(H); (apply subG_inG in H || clear H)
         end;
  (* Again get all assumptions *)
  intros;
  (* We support two kinds of goals: Things convertible to inG;
     and records with inG and typeclass fields. Try to solve the
     first case. *)
  try done;
  (* That didn't work, now we're in for the second case. *)
  split; (assumption || by apply _).

49
(** * Definition of the connective [own] *)
50
Definition iRes_singleton {Σ A} {i : inG Σ A} (γ : gname) (a : A) : iResUR Σ :=
51
  ofe_fun_singleton (inG_id i) {[ γ := cmra_transport inG_prf a ]}.
52
Instance: Params (@iRes_singleton) 4 := {}.
53

54
Definition own_def `{!inG Σ A} (γ : gname) (a : A) : iProp Σ :=
55
  uPred_ownM (iRes_singleton γ a).
56
Definition own_aux : seal (@own_def). by eexists. Qed.
57 58
Definition own {Σ A i} := own_aux.(unseal) Σ A i.
Definition own_eq : @own = @own_def := own_aux.(seal_eq).
59
Instance: Params (@own) 4 := {}.
60
Typeclasses Opaque own.
61

62
(** * Properties about ghost ownership *)
63
Section global.
64
Context `{Hin: !inG Σ A}.
65 66
Implicit Types a : A.

67 68 69
(** ** Properties of [iRes_singleton] *)
Global Instance iRes_singleton_ne γ :
  NonExpansive (@iRes_singleton Σ A _ γ).
70
Proof. by intros n a a' Ha; apply ofe_fun_singleton_ne; rewrite Ha. Qed.
71 72 73
Lemma iRes_singleton_op γ a1 a2 :
  iRes_singleton γ (a1  a2)  iRes_singleton γ a1  iRes_singleton γ a2.
Proof.
74
  by rewrite /iRes_singleton ofe_fun_op_singleton op_singleton cmra_transport_op.
75 76
Qed.

77
(** ** Properties of [own] *)
78
Global Instance own_ne γ : NonExpansive (@own Σ A _ γ).
79
Proof. rewrite !own_eq. solve_proper. Qed.
80
Global Instance own_proper γ :
81
  Proper (() ==> ()) (@own Σ A _ γ) := ne_proper _.
Robbert Krebbers's avatar
Robbert Krebbers committed
82

83
Lemma own_op γ a1 a2 : own γ (a1  a2)  own γ a1  own γ a2.
84
Proof. by rewrite !own_eq /own_def -ownM_op iRes_singleton_op. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
85
Lemma own_mono γ a1 a2 : a2  a1  own γ a1  own γ a2.
Robbert Krebbers's avatar
Robbert Krebbers committed
86
Proof. move=> [c ->]. by rewrite own_op sep_elim_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
87 88 89

Global Instance own_mono' γ : Proper (flip () ==> ()) (@own Σ A _ γ).
Proof. intros a1 a2. apply own_mono. Qed.
90

91
Lemma own_valid γ a : own γ a   a.
92 93
Proof.
  rewrite !own_eq /own_def ownM_valid /iRes_singleton.
94
  rewrite ofe_fun_validI (forall_elim (inG_id _)) ofe_fun_lookup_singleton.
95 96 97 98
  rewrite gmap_validI (forall_elim γ) lookup_singleton option_validI.
  (* implicit arguments differ a bit *)
  by trans ( cmra_transport inG_prf a : iProp Σ)%I; last destruct inG_prf.
Qed.
99
Lemma own_valid_2 γ a1 a2 : own γ a1 - own γ a2 -  (a1  a2).
100
Proof. apply wand_intro_r. by rewrite -own_op own_valid. Qed.
101
Lemma own_valid_3 γ a1 a2 a3 : own γ a1 - own γ a2 - own γ a3 -  (a1  a2  a3).
102
Proof. do 2 apply wand_intro_r. by rewrite -!own_op own_valid. Qed.
103
Lemma own_valid_r γ a : own γ a  own γ a   a.
Robbert Krebbers's avatar
Robbert Krebbers committed
104
Proof. apply: bi.persistent_entails_r. apply own_valid. Qed.
105
Lemma own_valid_l γ a : own γ a   a  own γ a.
106
Proof. by rewrite comm -own_valid_r. Qed.
107

108
Global Instance own_timeless γ a : Discrete a  Timeless (own γ a).
109
Proof. rewrite !own_eq /own_def; apply _. Qed.
110
Global Instance own_core_persistent γ a : CoreId a  Persistent (own γ a).
111
Proof. rewrite !own_eq /own_def; apply _. Qed.
112

113 114 115
Lemma later_own γ a :  own γ a -  ( b, own γ b   (a  b)).
Proof.
  rewrite own_eq /own_def later_ownM. apply exist_elim=> r.
116
  assert (NonExpansive (λ r : iResUR Σ, r (inG_id Hin) !! γ)).
117
  { intros n r1 r2 Hr. f_equiv. by specialize (Hr (inG_id _)). }
118
  rewrite (f_equiv (λ r : iResUR Σ, r (inG_id Hin) !! γ) _ r).
119 120 121 122 123 124 125 126 127
  rewrite {1}/iRes_singleton ofe_fun_lookup_singleton lookup_singleton.
  rewrite option_equivI. case Hb: (r (inG_id _) !! γ)=> [b|]; last first.
  { by rewrite and_elim_r /sbi_except_0 -or_intro_l. }
  rewrite -except_0_intro -(exist_intro (cmra_transport (eq_sym inG_prf) b)).
  apply and_mono.
  - rewrite /iRes_singleton. assert ( {A A' : cmraT} (Heq : A' = A) (a : A),
      cmra_transport Heq (cmra_transport (eq_sym Heq) a) = a) as ->
      by (by intros ?? ->).
    apply ownM_mono=> /=.
128
    exists (ofe_fun_insert (inG_id _) (delete γ (r (inG_id Hin))) r).
129 130 131 132 133 134 135 136 137 138 139 140 141 142
    intros i'. rewrite ofe_fun_lookup_op.
    destruct (decide (i' = inG_id _)) as [->|?].
    + rewrite ofe_fun_lookup_insert ofe_fun_lookup_singleton.
      intros γ'. rewrite lookup_op. destruct (decide (γ' = γ)) as [->|?].
      * by rewrite lookup_singleton lookup_delete Hb.
      * by rewrite lookup_singleton_ne // lookup_delete_ne // left_id.
    + rewrite ofe_fun_lookup_insert_ne //.
      by rewrite ofe_fun_lookup_singleton_ne // left_id.
  - apply later_mono.
    by assert ( {A A' : cmraT} (Heq : A' = A) (a' : A') (a : A),
      cmra_transport Heq a'  a @{iPropI Σ}
        a'  cmra_transport (eq_sym Heq) a) as -> by (by intros ?? ->).
Qed.

143
(** ** Allocation *)
Robbert Krebbers's avatar
Robbert Krebbers committed
144 145
(* TODO: This also holds if we just have ✓ a at the current step-idx, as Iris
   assertion. However, the map_updateP_alloc does not suffice to show this. *)
146
Lemma own_alloc_strong a (G : gset gname) :
147
   a  (|==>  γ, ⌜γ  G  own γ a)%I.
148
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
149
  intros Ha.
150
  rewrite -(bupd_mono ( m,  γ, γ  G  m = iRes_singleton γ a  uPred_ownM m)%I).
151
  - rewrite /uPred_valid /bi_emp_valid (ownM_unit emp).
152
    eapply bupd_ownM_updateP, (ofe_fun_singleton_updateP_empty (inG_id _));
153 154
      first (eapply alloc_updateP_strong', cmra_transport_valid, Ha);
      naive_solver.
155
  - apply exist_elim=>m; apply pure_elim_l=>-[γ [Hfresh ->]].
156
    by rewrite !own_eq /own_def -(exist_intro γ) pure_True // left_id.
157
Qed.
158
Lemma own_alloc a :  a  (|==>  γ, own γ a)%I.
159
Proof.
Ralf Jung's avatar
Ralf Jung committed
160
  intros Ha. rewrite /uPred_valid /bi_emp_valid (own_alloc_strong a ) //; [].
Ralf Jung's avatar
Ralf Jung committed
161
  apply bupd_mono, exist_mono=>?. eauto using and_elim_r.
162
Qed.
163

164
(** ** Frame preserving updates *)
Ralf Jung's avatar
Ralf Jung committed
165
Lemma own_updateP P γ a : a ~~>: P  own γ a ==  a', P a'  own γ a'.
166
Proof.
167
  intros Ha. rewrite !own_eq.
168
  rewrite -(bupd_mono ( m,  a', m = iRes_singleton γ a'  P a'  uPred_ownM m)%I).
169
  - eapply bupd_ownM_updateP, ofe_fun_singleton_updateP;
170
      first by (eapply singleton_updateP', cmra_transport_updateP', Ha).
Robbert Krebbers's avatar
Robbert Krebbers committed
171
    naive_solver.
172 173
  - apply exist_elim=>m; apply pure_elim_l=>-[a' [-> HP]].
    rewrite -(exist_intro a'). by apply and_intro; [apply pure_intro|].
174 175
Qed.

176
Lemma own_update γ a a' : a ~~> a'  own γ a == own γ a'.
177
Proof.
178
  intros; rewrite (own_updateP (a' =)); last by apply cmra_update_updateP.
179
  by apply bupd_mono, exist_elim=> a''; apply pure_elim_l=> ->.
180
Qed.
181
Lemma own_update_2 γ a1 a2 a' :
182
  a1  a2 ~~> a'  own γ a1 - own γ a2 == own γ a'.
183
Proof. intros. apply wand_intro_r. rewrite -own_op. by apply own_update. Qed.
184
Lemma own_update_3 γ a1 a2 a3 a' :
185
  a1  a2  a3 ~~> a'  own γ a1 - own γ a2 - own γ a3 == own γ a'.
186
Proof. intros. do 2 apply wand_intro_r. rewrite -!own_op. by apply own_update. Qed.
187
End global.
188

189
Arguments own_valid {_ _} [_] _ _.
190 191
Arguments own_valid_2 {_ _} [_] _ _ _.
Arguments own_valid_3 {_ _} [_] _ _ _ _.
192 193 194 195
Arguments own_valid_l {_ _} [_] _ _.
Arguments own_valid_r {_ _} [_] _ _.
Arguments own_updateP {_ _} [_] _ _ _ _.
Arguments own_update {_ _} [_] _ _ _ _.
196 197
Arguments own_update_2 {_ _} [_] _ _ _ _ _.
Arguments own_update_3 {_ _} [_] _ _ _ _ _ _.
198

199
Lemma own_unit A `{!inG Σ (A:ucmraT)} γ : (|==> own γ ε)%I.
200
Proof.
201
  rewrite /uPred_valid /bi_emp_valid (ownM_unit emp) !own_eq /own_def.
202
  apply bupd_ownM_update, ofe_fun_singleton_update_empty.
Robbert Krebbers's avatar
Robbert Krebbers committed
203
  apply (alloc_unit_singleton_update (cmra_transport inG_prf ε)); last done.
204 205
  - apply cmra_transport_valid, ucmra_unit_valid.
  - intros x; destruct inG_prf. by rewrite left_id.
206
Qed.
207

208
(** Big op class instances *)
209
Instance own_cmra_sep_homomorphism `{!inG Σ (A:ucmraT)} :
210 211
  WeakMonoidHomomorphism op uPred_sep () (own γ).
Proof. split; try apply _. apply own_op. Qed.
212

213 214
(** Proofmode class instances *)
Section proofmode_classes.
215
  Context `{!inG Σ A}.
216 217
  Implicit Types a b : A.

218 219
  Global Instance into_sep_own γ a b1 b2 :
    IsOp a b1 b2  IntoSep (own γ a) (own γ b1) (own γ b2).
Robbert Krebbers's avatar
Robbert Krebbers committed
220
  Proof. intros. by rewrite /IntoSep (is_op a) own_op. Qed.
221
  Global Instance into_and_own p γ a b1 b2 :
222
    IsOp a b1 b2  IntoAnd p (own γ a) (own γ b1) (own γ b2).
Robbert Krebbers's avatar
Robbert Krebbers committed
223 224 225 226 227
  Proof. intros. by rewrite /IntoAnd (is_op a) own_op sep_and. Qed.

  Global Instance from_sep_own γ a b1 b2 :
    IsOp a b1 b2  FromSep (own γ a) (own γ b1) (own γ b2).
  Proof. intros. by rewrite /FromSep -own_op -is_op. Qed.
228
  Global Instance from_and_own_persistent γ a b1 b2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
229 230
    IsOp a b1 b2  TCOr (CoreId b1) (CoreId b2) 
    FromAnd (own γ a) (own γ b1) (own γ b2).
231
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
232
    intros ? Hb. rewrite /FromAnd (is_op a) own_op.
233
    destruct Hb; by rewrite persistent_and_sep.
234
  Qed.
235
End proofmode_classes.