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 `{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 `{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 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142
Lemma later_own γ a :  own γ a -  ( b, own γ b   (a  b)).
Proof.
  rewrite own_eq /own_def later_ownM. apply exist_elim=> r.
  assert (NonExpansive (λ r : iResUR Σ, r (inG_id H) !! γ)).
  { intros n r1 r2 Hr. f_equiv. by specialize (Hr (inG_id _)). }
  rewrite (f_equiv (λ r : iResUR Σ, r (inG_id H) !! γ) _ r).
  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=> /=.
    exists (ofe_fun_insert (inG_id _) (delete γ (r (inG_id H))) r).
    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

Robbert Krebbers's avatar
Robbert Krebbers committed
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 209
(** Big op class instances *)
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 215 216 217
(** Proofmode class instances *)
Section proofmode_classes.
  Context `{inG Σ A}.
  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.