own.v 7.24 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
Set Default Proof Using "Type".
6
7
Import uPred.

8
9
(** 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
10
individual CMRAs instead of (lists of) CMRA *functors*. This additional class is
11
12
13
14
15
16
17
18
19
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.

20
21
22
23
(** This tactic solves the usual obligations "subG ? Σ → {in,?}G ? Σ" *)
Ltac solve_inG :=
  (* Get all assumptions *)
  intros;
24
  (* Unfold the top-level xΣ. We need to support this to be a function. *)
25
  lazymatch goal with
26
27
28
  | H : subG (?xΣ _ _ _ _) _ |- _ => try unfold xΣ in H
  | H : subG (?xΣ _ _ _) _ |- _ => try unfold xΣ in H
  | H : subG (?xΣ _ _) _ |- _ => try unfold xΣ in H
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
  | 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 _).

50
(** * Definition of the connective [own] *)
51
Definition own_def `{inG Σ A} (γ : gname) (a : A) : iProp Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
52
  uPred_ownM (iRes_singleton (inG_id _) γ (cmra_transport inG_prf a)).
53
54
55
Definition own_aux : seal (@own_def). by eexists. Qed.
Definition own {Σ A i} := unseal own_aux Σ A i.
Definition own_eq : @own = @own_def := seal_eq own_aux.
56
Instance: Params (@own) 4.
57
Typeclasses Opaque own.
58

59
(** * Properties about ghost ownership *)
60
Section global.
61
Context `{inG Σ A}.
62
63
Implicit Types a : A.

64
(** ** Properties of [own] *)
65
Global Instance own_ne γ : NonExpansive (@own Σ A _ γ).
66
Proof. rewrite !own_eq. solve_proper. Qed.
67
Global Instance own_proper γ :
68
  Proper (() ==> ()) (@own Σ A _ γ) := ne_proper _.
Robbert Krebbers's avatar
Robbert Krebbers committed
69

70
Lemma own_op γ a1 a2 : own γ (a1  a2)  own γ a1  own γ a2.
Robbert Krebbers's avatar
Robbert Krebbers committed
71
Proof. by rewrite !own_eq /own_def -ownM_op cmra_transport_op iRes_op. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
72
73
74
Lemma own_mono γ a1 a2 : a2  a1  own γ a1  own γ a2.
Proof. move=> [c ->]. rewrite own_op. eauto with I. Qed.

75
76
Global Instance own_cmra_homomorphism : CMRAHomomorphism (own γ).
Proof. split. apply _. apply own_op. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
77
78
Global Instance own_mono' γ : Proper (flip () ==> ()) (@own Σ A _ γ).
Proof. intros a1 a2. apply own_mono. Qed.
79

80
Lemma own_valid γ a : own γ a   a.
Robbert Krebbers's avatar
Robbert Krebbers committed
81
Proof. rewrite !own_eq /own_def ownM_valid iRes_valid. by destruct inG_prf. Qed.
82
Lemma own_valid_2 γ a1 a2 : own γ a1 - own γ a2 -  (a1  a2).
83
Proof. apply wand_intro_r. by rewrite -own_op own_valid. Qed.
84
Lemma own_valid_3 γ a1 a2 a3 : own γ a1 - own γ a2 - own γ a3 -  (a1  a2  a3).
85
Proof. do 2 apply wand_intro_r. by rewrite -!own_op own_valid. Qed.
86
Lemma own_valid_r γ a : own γ a  own γ a   a.
87
Proof. apply: uPred.always_entails_r. apply own_valid. Qed.
88
Lemma own_valid_l γ a : own γ a   a  own γ a.
89
Proof. by rewrite comm -own_valid_r. Qed.
90

91
Global Instance own_timeless γ a : Timeless a  TimelessP (own γ a).
92
Proof. rewrite !own_eq /own_def; apply _. Qed.
93
Global Instance own_core_persistent γ a : Persistent a  PersistentP (own γ a).
94
Proof. rewrite !own_eq /own_def; apply _. Qed.
95

96
(** ** Allocation *)
Robbert Krebbers's avatar
Robbert Krebbers committed
97
98
(* 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. *)
99
Lemma own_alloc_strong a (G : gset gname) :
100
   a  (|==>  γ, ⌜γ  G  own γ a)%I.
101
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
102
  intros Ha.
Robbert Krebbers's avatar
Robbert Krebbers committed
103
104
  rewrite -(bupd_mono ( m,  γ, γ  G 
    m = iRes_singleton (inG_id _) γ (cmra_transport inG_prf a)  uPred_ownM m))%I.
105
  - rewrite /uPred_valid ownM_empty.
Robbert Krebbers's avatar
Robbert Krebbers committed
106
107
    eapply bupd_ownM_updateP, iRes_alloc_strong;
      [eapply cmra_transport_valid, Ha|naive_solver].
108
  - apply exist_elim=>m; apply pure_elim_l=>-[γ [Hfresh ->]].
109
    by rewrite !own_eq /own_def -(exist_intro γ) pure_True // left_id.
110
Qed.
111
Lemma own_alloc a :  a  (|==>  γ, own γ a)%I.
112
Proof.
113
  intros Ha. rewrite /uPred_valid (own_alloc_strong a ) //; [].
114
  apply bupd_mono, exist_mono=>?. eauto with I.
115
Qed.
116

117
(** ** Frame preserving updates *)
Ralf Jung's avatar
Ralf Jung committed
118
Lemma own_updateP P γ a : a ~~>: P  own γ a ==  a', P a'  own γ a'.
119
Proof.
120
  intros Ha. rewrite !own_eq.
Robbert Krebbers's avatar
Robbert Krebbers committed
121
122
123
124
  rewrite -(bupd_mono ( m,  a',
    m = iRes_singleton (inG_id _) γ (cmra_transport inG_prf a') 
    P a'  uPred_ownM m)%I).
  - eapply bupd_ownM_updateP, iRes_updateP; [by apply cmra_transport_updateP'|].
Robbert Krebbers's avatar
Robbert Krebbers committed
125
    naive_solver.
126
127
  - apply exist_elim=>m; apply pure_elim_l=>-[a' [-> HP]].
    rewrite -(exist_intro a'). by apply and_intro; [apply pure_intro|].
128
129
Qed.

130
Lemma own_update γ a a' : a ~~> a'  own γ a == own γ a'.
131
Proof.
132
  intros; rewrite (own_updateP (a' =)); last by apply cmra_update_updateP.
133
  by apply bupd_mono, exist_elim=> a''; apply pure_elim_l=> ->.
134
Qed.
135
Lemma own_update_2 γ a1 a2 a' :
136
  a1  a2 ~~> a'  own γ a1 - own γ a2 == own γ a'.
137
Proof. intros. apply wand_intro_r. rewrite -own_op. by apply own_update. Qed.
138
Lemma own_update_3 γ a1 a2 a3 a' :
139
  a1  a2  a3 ~~> a'  own γ a1 - own γ a2 - own γ a3 == own γ a'.
140
Proof. intros. do 2 apply wand_intro_r. rewrite -!own_op. by apply own_update. Qed.
141
End global.
142

143
Arguments own_valid {_ _} [_] _ _.
144
145
Arguments own_valid_2 {_ _} [_] _ _ _.
Arguments own_valid_3 {_ _} [_] _ _ _ _.
146
147
148
149
Arguments own_valid_l {_ _} [_] _ _.
Arguments own_valid_r {_ _} [_] _ _.
Arguments own_updateP {_ _} [_] _ _ _ _.
Arguments own_update {_ _} [_] _ _ _ _.
150
151
Arguments own_update_2 {_ _} [_] _ _ _ _ _.
Arguments own_update_3 {_ _} [_] _ _ _ _ _ _.
152

153
Lemma own_empty A `{inG Σ (A:ucmraT)} γ : (|==> own γ )%I.
154
Proof.
155
  rewrite /uPred_valid ownM_empty !own_eq /own_def.
Robbert Krebbers's avatar
Robbert Krebbers committed
156
  apply bupd_ownM_update, iRes_alloc_unit_singleton.
157
158
  - apply cmra_transport_valid, ucmra_unit_valid.
  - intros x; destruct inG_prf. by rewrite left_id.
159
Qed.
160
161
162
163
164
165
166
167
168
169
170
171
172

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