own.v 6.89 KB
Newer Older
1
From iris.algebra Require Import iprod gmap.
2
From iris.base_logic Require Import big_op.
Ralf Jung's avatar
Ralf Jung committed
3
From iris.base_logic Require Export iprop.
4
From iris.proofmode Require Import classes.
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
19
20
21
22
23
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.

(** * Definition of the connective [own] *)
Definition iRes_singleton `{i : inG Σ A} (γ : gname) (a : A) : iResUR Σ :=
  iprod_singleton (inG_id i) {[ γ := cmra_transport inG_prf a ]}.
Instance: Params (@iRes_singleton) 4.

24
Definition own_def `{inG Σ A} (γ : gname) (a : A) : iProp Σ :=
25
  uPred_ownM (iRes_singleton γ a).
26
Definition own_aux : { x | x = @own_def }. by eexists. Qed.
27
Definition own {Σ A i} := proj1_sig own_aux Σ A i.
28
Definition own_eq : @own = @own_def := proj2_sig own_aux.
29
Instance: Params (@own) 4.
30
Typeclasses Opaque own.
31

32
(** * Properties about ghost ownership *)
33
Section global.
34
Context `{inG Σ A}.
35
36
Implicit Types a : A.

37
38
39
40
41
42
43
44
45
46
47
(** ** Properties of [iRes_singleton] *)
Global Instance iRes_singleton_ne γ n :
  Proper (dist n ==> dist n) (@iRes_singleton Σ A _ γ).
Proof. by intros a a' Ha; apply iprod_singleton_ne; rewrite Ha. Qed.
Lemma iRes_singleton_op γ a1 a2 :
  iRes_singleton γ (a1  a2)  iRes_singleton γ a1  iRes_singleton γ a2.
Proof.
  by rewrite /iRes_singleton iprod_op_singleton op_singleton cmra_transport_op.
Qed.

(** ** Properties of [own] *)
48
Global Instance own_ne γ n : Proper (dist n ==> dist n) (@own Σ A _ γ).
49
Proof. rewrite !own_eq. solve_proper. Qed.
50
Global Instance own_proper γ :
51
  Proper (() ==> ()) (@own Σ A _ γ) := ne_proper _.
Robbert Krebbers's avatar
Robbert Krebbers committed
52

53
Lemma own_op γ a1 a2 : own γ (a1  a2)  own γ a1  own γ a2.
54
Proof. by rewrite !own_eq /own_def -ownM_op iRes_singleton_op. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
55
56
57
Lemma own_mono γ a1 a2 : a2  a1  own γ a1  own γ a2.
Proof. move=> [c ->]. rewrite own_op. eauto with I. Qed.

58
59
Global Instance own_cmra_homomorphism : CMRAHomomorphism (own γ).
Proof. split. apply _. apply own_op. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
60
61
Global Instance own_mono' γ : Proper (flip () ==> ()) (@own Σ A _ γ).
Proof. intros a1 a2. apply own_mono. Qed.
62

63
Lemma own_valid γ a : own γ a   a.
64
Proof.
65
  rewrite !own_eq /own_def ownM_valid /iRes_singleton.
66
  rewrite iprod_validI (forall_elim (inG_id _)) iprod_lookup_singleton.
67
  rewrite gmap_validI (forall_elim γ) lookup_singleton option_validI.
68
  (* implicit arguments differ a bit *)
69
  by trans ( cmra_transport inG_prf a : iProp Σ)%I; last destruct inG_prf.
70
Qed.
71
72
73
74
Lemma own_valid_2 γ a1 a2 : own γ a1  own γ a2 -  (a1  a2).
Proof. apply wand_intro_r. by rewrite -own_op own_valid. Qed.
Lemma own_valid_3 γ a1 a2 a3 : own γ a1  own γ a2 - own γ a3 -  (a1  a2  a3).
Proof. do 2 apply wand_intro_r. by rewrite -!own_op own_valid. Qed.
75
Lemma own_valid_r γ a : own γ a  own γ a   a.
76
Proof. apply (uPred.always_entails_r _ _). apply own_valid. Qed.
77
Lemma own_valid_l γ a : own γ a   a  own γ a.
78
Proof. by rewrite comm -own_valid_r. Qed.
79

80
Global Instance own_timeless γ a : Timeless a  TimelessP (own γ a).
81
Proof. rewrite !own_eq /own_def; apply _. Qed.
82
Global Instance own_core_persistent γ a : Persistent a  PersistentP (own γ a).
83
Proof. rewrite !own_eq /own_def; apply _. Qed.
84

85
(** ** Allocation *)
Robbert Krebbers's avatar
Robbert Krebbers committed
86
87
(* 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. *)
88
Lemma own_alloc_strong a (G : gset gname) :
89
   a  True ==  γ,  (γ  G)  own γ a.
90
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
91
  intros Ha.
92
  rewrite -(bupd_mono ( m,  ( γ, γ  G  m = iRes_singleton γ a)  uPred_ownM m)%I).
93
  - rewrite ownM_empty.
94
    eapply bupd_ownM_updateP, (iprod_singleton_updateP_empty (inG_id _));
95
      first (eapply alloc_updateP_strong', cmra_transport_valid, Ha);
96
      naive_solver.
97
  - apply exist_elim=>m; apply pure_elim_l=>-[γ [Hfresh ->]].
98
    by rewrite !own_eq /own_def -(exist_intro γ) pure_True // left_id.
99
Qed.
100
Lemma own_alloc a :  a  True ==  γ, own γ a.
101
Proof.
102
  intros Ha. rewrite (own_alloc_strong a ) //; [].
103
  apply bupd_mono, exist_mono=>?. eauto with I.
104
Qed.
105

106
(** ** Frame preserving updates *)
107
Lemma own_updateP P γ a : a ~~>: P  own γ a ==  a',  P a'  own γ a'.
108
Proof.
109
  intros Ha. rewrite !own_eq.
110
111
  rewrite -(bupd_mono ( m,  ( a', m = iRes_singleton γ a'  P a')  uPred_ownM m)%I).
  - eapply bupd_ownM_updateP, iprod_singleton_updateP;
112
      first by (eapply singleton_updateP', cmra_transport_updateP', Ha).
Robbert Krebbers's avatar
Robbert Krebbers committed
113
    naive_solver.
114
115
  - apply exist_elim=>m; apply pure_elim_l=>-[a' [-> HP]].
    rewrite -(exist_intro a'). by apply and_intro; [apply pure_intro|].
116
117
Qed.

118
Lemma own_update γ a a' : a ~~> a'  own γ a == own γ a'.
119
Proof.
120
  intros; rewrite (own_updateP (a' =)); last by apply cmra_update_updateP.
121
  by apply bupd_mono, exist_elim=> a''; apply pure_elim_l=> ->.
122
Qed.
123
Lemma own_update_2 γ a1 a2 a' :
124
125
  a1  a2 ~~> a'  own γ a1  own γ a2 == own γ a'.
Proof. intros. apply wand_intro_r. rewrite -own_op. by apply own_update. Qed.
126
Lemma own_update_3 γ a1 a2 a3 a' :
127
128
  a1  a2  a3 ~~> a'  own γ a1  own γ a2 - own γ a3 == own γ a'.
Proof. intros. do 2 apply wand_intro_r. rewrite -!own_op. by apply own_update. Qed.
129
End global.
130

131
Arguments own_valid {_ _} [_] _ _.
132
133
Arguments own_valid_2 {_ _} [_] _ _ _.
Arguments own_valid_3 {_ _} [_] _ _ _ _.
134
135
136
137
Arguments own_valid_l {_ _} [_] _ _.
Arguments own_valid_r {_ _} [_] _ _.
Arguments own_updateP {_ _} [_] _ _ _ _.
Arguments own_update {_ _} [_] _ _ _ _.
138
139
Arguments own_update_2 {_ _} [_] _ _ _ _ _.
Arguments own_update_3 {_ _} [_] _ _ _ _ _ _.
140

141
Lemma own_empty A `{inG Σ (A:ucmraT)} γ : True == own γ .
142
Proof.
143
  rewrite ownM_empty !own_eq /own_def.
144
  apply bupd_ownM_update, iprod_singleton_update_empty.
145
  apply (alloc_unit_singleton_update (cmra_transport inG_prf )); last done.
146
147
  - apply cmra_transport_valid, ucmra_unit_valid.
  - intros x; destruct inG_prf. by rewrite left_id.
148
Qed.
149
150
151
152
153
154
155
156
157
158
159
160
161

(** Proofmode class instances *)
Section proofmode_classes.
  Context `{inG Σ A}.
  Implicit Types a b : A.

  Global Instance into_and_own p γ a b1 b2 :
    IntoOp a b1 b2  IntoAnd p (own γ a) (own γ b1) (own γ b2).
  Proof. intros. apply mk_into_and_sep. by rewrite (into_op a) own_op. Qed.
  Global Instance from_sep_own γ a b1 b2 :
    FromOp a b1 b2  FromSep (own γ a) (own γ b1) (own γ b2).
  Proof. intros. by rewrite /FromSep -own_op from_op. Qed.
End proofmode_classes.