own.v 6.96 KB
Newer Older
1
From iris.algebra Require Import iprod gmap.
2
From iris.base_logic Require Import big_op.
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 20 21 22 23 24
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.

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

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

38 39 40 41 42 43 44 45 46 47 48
(** ** 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] *)
49
Global Instance own_ne γ n : Proper (dist n ==> dist n) (@own Σ A _ γ).
50
Proof. rewrite !own_eq. solve_proper. Qed.
51
Global Instance own_proper γ :
52
  Proper (() ==> ()) (@own Σ A _ γ) := ne_proper _.
Robbert Krebbers's avatar
Robbert Krebbers committed
53

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

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

64
Lemma own_valid γ a : own γ a   a.
65
Proof.
66
  rewrite !own_eq /own_def ownM_valid /iRes_singleton.
67
  rewrite iprod_validI (forall_elim (inG_id _)) iprod_lookup_singleton.
68
  rewrite gmap_validI (forall_elim γ) lookup_singleton option_validI.
69
  (* implicit arguments differ a bit *)
70
  by trans ( cmra_transport inG_prf a : iProp Σ)%I; last destruct inG_prf.
71
Qed.
72
Lemma own_valid_2 γ a1 a2 : own γ a1 - own γ a2 -  (a1  a2).
73
Proof. apply wand_intro_r. by rewrite -own_op own_valid. Qed.
74
Lemma own_valid_3 γ a1 a2 a3 : own γ a1 - own γ a2 - own γ a3 -  (a1  a2  a3).
75
Proof. do 2 apply wand_intro_r. by rewrite -!own_op 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  (|==>  γ, ⌜γ  G  own γ a)%I.
91
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
92
  intros Ha.
Ralf Jung's avatar
Ralf Jung committed
93
  rewrite -(bupd_mono ( m,  γ, γ  G  m = iRes_singleton γ a  uPred_ownM m)%I).
94
  - rewrite /uPred_valid 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
  - apply exist_elim=>m; apply pure_elim_l=>-[γ [Hfresh ->]].
99
    by rewrite !own_eq /own_def -(exist_intro γ) pure_True // left_id.
100
Qed.
101
Lemma own_alloc a :  a  (|==>  γ, own γ a)%I.
102
Proof.
103
  intros Ha. rewrite /uPred_valid (own_alloc_strong a ) //; [].
104
  apply bupd_mono, exist_mono=>?. eauto with I.
105
Qed.
106

107
(** ** Frame preserving updates *)
Ralf Jung's avatar
Ralf Jung committed
108
Lemma own_updateP P γ a : a ~~>: P  own γ a ==  a', P a'  own γ a'.
109
Proof.
110
  intros Ha. rewrite !own_eq.
Ralf Jung's avatar
Ralf Jung committed
111
  rewrite -(bupd_mono ( m,  a', m = iRes_singleton γ a'  P a'  uPred_ownM m)%I).
112
  - 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
Proof. intros. apply wand_intro_r. rewrite -own_op. by apply own_update. Qed.
127
Lemma own_update_3 γ a1 a2 a3 a' :
128
  a1  a2  a3 ~~> a'  own γ a1 - own γ a2 - own γ a3 == own γ a'.
129
Proof. intros. do 2 apply wand_intro_r. rewrite -!own_op. 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)} γ : (|==> own γ )%I.
143
Proof.
144
  rewrite /uPred_valid 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.