updates.v 9.13 KB
Newer Older
1
From stdpp Require Import coPset.
2
From iris.bi Require Import interface derived_laws big_op.
3

4
Class BUpd (PROP : Type) : Type := bupd : PROP  PROP.
5
6
7
8
9
10
11
12
13
Instance : Params (@bupd) 2.

Notation "|==> Q" := (bupd Q)
  (at level 99, Q at level 200, format "|==>  Q") : bi_scope.
Notation "P ==∗ Q" := (P  |==> Q)
  (at level 99, Q at level 200, only parsing) : stdpp_scope.
Notation "P ==∗ Q" := (P - |==> Q)%I
  (at level 99, Q at level 200, format "P  ==∗  Q") : bi_scope.

14
Class FUpd (PROP : Type) : Type := fupd : coPset  coPset  PROP  PROP.
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
Instance: Params (@fupd) 4.

Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q)
  (at level 99, E1, E2 at level 50, Q at level 200,
   format "|={ E1 , E2 }=>  Q") : bi_scope.
Notation "P ={ E1 , E2 }=∗ Q" := (P - |={E1,E2}=> Q)%I
  (at level 99, E1,E2 at level 50, Q at level 200,
   format "P  ={ E1 , E2 }=∗  Q") : bi_scope.
Notation "P ={ E1 , E2 }=∗ Q" := (P - |={E1,E2}=> Q)
  (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : stdpp_scope.

Notation "|={ E }=> Q" := (fupd E E Q)
  (at level 99, E at level 50, Q at level 200,
   format "|={ E }=>  Q") : bi_scope.
Notation "P ={ E }=∗ Q" := (P - |={E}=> Q)%I
  (at level 99, E at level 50, Q at level 200,
   format "P  ={ E }=∗  Q") : bi_scope.
Notation "P ={ E }=∗ Q" := (P - |={E}=> Q)
  (at level 99, E at level 50, Q at level 200, only parsing) : stdpp_scope.
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48

(** Fancy updates that take a step. *)

Notation "|={ E1 , E2 }▷=> Q" := (|={E1,E2}=> ( |={E2,E1}=> Q))%I
  (at level 99, E1, E2 at level 50, Q at level 200,
   format "|={ E1 , E2 }▷=>  Q") : bi_scope.
Notation "P ={ E1 , E2 }▷=∗ Q" := (P - |={ E1 , E2 }=> Q)%I
  (at level 99, E1, E2 at level 50, Q at level 200,
   format "P  ={ E1 , E2 }▷=∗  Q") : bi_scope.
Notation "|={ E }▷=> Q" := (|={E,E}=> Q)%I
  (at level 99, E at level 50, Q at level 200,
   format "|={ E }▷=>  Q") : bi_scope.
Notation "P ={ E }▷=∗ Q" := (P ={E,E}= Q)%I
  (at level 99, E at level 50, Q at level 200,
   format "P  ={ E }▷=∗  Q") : bi_scope.
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
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
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219

(** BUpd facts  *)

Class BUpdFacts (PROP : bi) `{BUpd PROP} : Prop :=
  { bupd_ne :> NonExpansive bupd;
    bupd_intro P : P == P;
    bupd_mono P Q : (P  Q)  (|==> P) == Q;
    bupd_trans P : (|==> |==> P) == P;
    bupd_frame_r P R : (|==> P)  R == P  R;
    bupd_plainly P : (|==> bi_plainly P) - P }.

Section bupd_derived.
  Context `{BUpdFacts PROP}.

  Global Instance bupd_proper : Proper (() ==> ()) bupd := ne_proper _.

  (** BUpd derived rules *)

  Global Instance bupd_mono' : Proper (() ==> ()) bupd.
  Proof. intros P Q; apply bupd_mono. Qed.
  Global Instance bupd_flip_mono' : Proper (flip () ==> flip ()) bupd.
  Proof. intros P Q; apply bupd_mono. Qed.

  Lemma bupd_frame_l R Q : (R  |==> Q) == R  Q.
  Proof. rewrite !(comm _ R); apply bupd_frame_r. Qed.
  Lemma bupd_wand_l P Q : (P - Q)  (|==> P) == Q.
  Proof. by rewrite bupd_frame_l bi.wand_elim_l. Qed.
  Lemma bupd_wand_r P Q : (|==> P)  (P - Q) == Q.
  Proof. by rewrite bupd_frame_r bi.wand_elim_r. Qed.
  Lemma bupd_sep P Q : (|==> P)  (|==> Q) == P  Q.
  Proof. by rewrite bupd_frame_r bupd_frame_l bupd_trans. Qed.
  Lemma bupd_affinely_plainly `{BiAffine PROP} P : (|==>  P)  P.
  Proof. by rewrite bi.affine_affinely bupd_plainly. Qed.
  Lemma bupd_plain P `{!Plain P} : (|==> P)  P.
  Proof. by rewrite {1}(plain P) bupd_plainly. Qed.
End bupd_derived.

Lemma except_0_bupd {PROP : sbi} `{BUpdFacts PROP} (P : PROP) :
   (|==> P)  (|==>  P).
Proof.
  rewrite /sbi_except_0. apply bi.or_elim; eauto using bupd_mono, bi.or_intro_r.
  by rewrite -bupd_intro -bi.or_intro_l.
Qed.

(** FUpd facts  *)

(* Currently, this requires an SBI, because of [except_0_fupd] and
   [later_fupd_plain]. If need be, we can generalize this to BIs by
   extracting these propertes as lemmas to be proved by hand. *)
Class FUpdFacts (PROP : sbi) `{BUpd PROP, FUpd PROP} : Prop :=
  { fupd_bupd_facts :> BUpdFacts PROP;
    fupd_ne E1 E2 :> NonExpansive (fupd E1 E2);
    fupd_intro_mask E1 E2 P : E2  E1  P  |={E1,E2}=> |={E2,E1}=> P;
    bupd_fupd E P : (|==> P) ={E}= P;
    except_0_fupd E1 E2 P :  (|={E1,E2}=> P) ={E1,E2}= P;
    fupd_mono E1 E2 P Q : (P  Q)  (|={E1,E2}=> P)  |={E1,E2}=> Q;
    fupd_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P)  |={E1,E3}=> P;
    fupd_mask_frame_r' E1 E2 Ef P :
      E1 ## Ef  (|={E1,E2}=> E2 ## Ef  P) ={E1  Ef,E2  Ef}= P;
    fupd_frame_r E1 E2 P Q : (|={E1,E2}=> P)  Q ={E1,E2}= P  Q;
    fupd_plain' E1 E2 E2' P Q `{!Plain P} :
      E1  E2 
      (Q ={E1, E2'}= P) - (|={E1, E2}=> Q) ={E1}= (|={E1, E2}=> Q)  P;
    later_fupd_plain E P `{!Plain P} : ( |={E}=> P) ={E}=   P }.

Section fupd_derived.
  Context `{FUpdFacts PROP}.

  Global Instance fupd_proper E1 E2 : Proper (() ==> ()) (fupd E1 E2) := ne_proper _.

  (** FUpd derived rules *)

  Global Instance fupd_mono' E1 E2 : Proper (() ==> ()) (fupd E1 E2).
  Proof. intros P Q; apply fupd_mono. Qed.
  Global Instance fupd_flip_mono' E1 E2 :
    Proper (flip () ==> flip ()) (fupd E1 E2).
  Proof. intros P Q; apply fupd_mono. Qed.

  Lemma fupd_intro E P : P ={E}= P.
  Proof. rewrite -bupd_fupd. apply bupd_intro. Qed.
  Lemma fupd_intro_mask' E1 E2 : E2  E1  (|={E1,E2}=> |={E2,E1}=> emp)%I.
  Proof. exact: fupd_intro_mask. Qed.
  Lemma fupd_except_0 E1 E2 P : (|={E1,E2}=>  P) ={E1,E2}= P.
  Proof. by rewrite {1}(fupd_intro E2 P) except_0_fupd fupd_trans. Qed.

  Lemma fupd_frame_l E1 E2 P Q : (P  |={E1,E2}=> Q) ={E1,E2}= P  Q.
  Proof. rewrite !(comm _ P); apply fupd_frame_r. Qed.
  Lemma fupd_wand_l E1 E2 P Q : (P - Q)  (|={E1,E2}=> P) ={E1,E2}= Q.
  Proof. by rewrite fupd_frame_l bi.wand_elim_l. Qed.
  Lemma fupd_wand_r E1 E2 P Q : (|={E1,E2}=> P)  (P - Q) ={E1,E2}= Q.
  Proof. by rewrite fupd_frame_r bi.wand_elim_r. Qed.

  Lemma fupd_trans_frame E1 E2 E3 P Q :
    ((Q ={E2,E3}= emp)  |={E1,E2}=> (Q  P)) ={E1,E3}= P.
  Proof.
    rewrite fupd_frame_l assoc -(comm _ Q) bi.wand_elim_r.
    by rewrite fupd_frame_r left_id fupd_trans.
  Qed.

  Lemma fupd_mask_frame_r E1 E2 Ef P :
    E1 ## Ef  (|={E1,E2}=> P) ={E1  Ef,E2  Ef}= P.
  Proof.
    intros ?. rewrite -fupd_mask_frame_r' //. f_equiv.
    apply bi.impl_intro_l, bi.and_elim_r.
  Qed.
  Lemma fupd_mask_mono E1 E2 P : E1  E2  (|={E1}=> P) ={E2}= P.
  Proof.
    intros (Ef&->&?)%subseteq_disjoint_union_L. by apply fupd_mask_frame_r.
  Qed.

  Lemma fupd_sep E P Q : (|={E}=> P)  (|={E}=> Q) ={E}= P  Q.
  Proof. by rewrite fupd_frame_r fupd_frame_l fupd_trans. Qed.
  Lemma fupd_big_sepL {A} E (Φ : nat  A  PROP) (l : list A) :
    ([ list] kx  l, |={E}=> Φ k x) ={E}= [ list] kx  l, Φ k x.
  Proof.
    apply (big_opL_forall (λ P Q, P ={E}= Q)); auto using fupd_intro.
    intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
  Qed.
  Lemma fupd_big_sepM `{Countable K} {A} E (Φ : K  A  PROP) (m : gmap K A) :
    ([ map] kx  m, |={E}=> Φ k x) ={E}= [ map] kx  m, Φ k x.
  Proof.
    apply (big_opM_forall (λ P Q, P ={E}= Q)); auto using fupd_intro.
    intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
  Qed.
  Lemma fupd_big_sepS `{Countable A} E (Φ : A  PROP) X :
    ([ set] x  X, |={E}=> Φ x) ={E}= [ set] x  X, Φ x.
  Proof.
    apply (big_opS_forall (λ P Q, P ={E}= Q)); auto using fupd_intro.
    intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
  Qed.

  Lemma fupd_plain E1 E2 P Q `{!Plain P} :
    E1  E2  (Q - P) - (|={E1, E2}=> Q) ={E1}= (|={E1, E2}=> Q)  P.
  Proof.
    intros HE. rewrite -(fupd_plain' _ _ E1) //. apply bi.wand_intro_l.
    by rewrite bi.wand_elim_r -fupd_intro.
  Qed.

  (** Fancy updates that take a step derived rules. *)

  Lemma step_fupd_wand E1 E2 P Q : (|={E1,E2}=> P) - (P - Q) - |={E1,E2}=> Q.
  Proof.
    apply bi.wand_intro_l.
    by rewrite (bi.later_intro (P - Q)%I) fupd_frame_l -bi.later_sep fupd_frame_l
               bi.wand_elim_l.
  Qed.

  Lemma step_fupd_mask_frame_r E1 E2 Ef P :
    E1 ## Ef  E2 ## Ef  (|={E1,E2}=> P)  |={E1  Ef,E2  Ef}=> P.
  Proof.
    intros. rewrite -fupd_mask_frame_r //. do 2 f_equiv. by apply fupd_mask_frame_r.
  Qed.

  Lemma step_fupd_mask_mono E1 E2 F1 F2 P :
    F1  F2  E1  E2  (|={E1,F2}=> P)  |={E2,F1}=> P.
  Proof.
    intros ??. rewrite -(left_id emp%I _ (|={E1,F2}=> P)%I).
    rewrite (fupd_intro_mask E2 E1 emp%I) //.
    rewrite fupd_frame_r -(fupd_trans E2 E1 F1). f_equiv.
    rewrite fupd_frame_l -(fupd_trans E1 F2 F1). f_equiv.
    rewrite (fupd_intro_mask F2 F1 (|={_,_}=> emp)%I) //.
    rewrite fupd_frame_r. f_equiv.
    rewrite [X in (X  _)%I]bi.later_intro -bi.later_sep. f_equiv.
    rewrite fupd_frame_r -(fupd_trans F1 F2 E2). f_equiv.
    rewrite fupd_frame_l -(fupd_trans F2 E1 E2). f_equiv.
    by rewrite fupd_frame_r left_id.
  Qed.

  Lemma step_fupd_intro E1 E2 P : E2  E1   P - |={E1,E2}=> P.
  Proof. intros. by rewrite -(step_fupd_mask_mono E2 _ _ E2) // -!fupd_intro. Qed.
End fupd_derived.