own.v 6.81 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
Lemma own_valid_2 γ a1 a2 : own γ a1  own γ a2   (a1  a2).
72
Proof. by rewrite -own_op own_valid. Qed.
73
Lemma own_valid_3 γ a1 a2 a3 : own γ a1  own γ a2  own γ a3   (a1  a2  a3).
74
75
Proof. by rewrite -!own_op assoc own_valid. Qed.

76
Lemma own_valid_r γ a : own γ a  own γ a   a.
77
Proof. apply (uPred.always_entails_r _ _). apply own_valid. Qed.
78
Lemma own_valid_l γ a : own γ a   a  own γ a.
79
Proof. by rewrite comm -own_valid_r. Qed.
80

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

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

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

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

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

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

(** 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.