fancy_updates.v 9.55 KB
Newer Older
1
From iris.base_logic.lib Require Export own.
Ralf Jung's avatar
Ralf Jung committed
2
From stdpp Require Export coPset.
3
From iris.base_logic.lib Require Import wsat.
4
5
From iris.algebra Require Import gmap.
From iris.base_logic Require Import big_op.
6
From iris.proofmode Require Import tactics classes.
7
Set Default Proof Using "Type".
8
Export invG.
9
10
Import uPred.

11
Program Definition fupd_def `{invG Σ}
12
    (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
13
  (wsat  ownE E1 ==  (wsat  ownE E2  P))%I.
14
15
16
Definition fupd_aux : seal (@fupd_def). by eexists. Qed.
Definition fupd := unseal fupd_aux.
Definition fupd_eq : @fupd = @fupd_def := seal_eq fupd_aux.
17
18
Arguments fupd {_ _} _ _ _%I.
Instance: Params (@fupd) 4.
19
20
21
22

Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q)
  (at level 99, E1, E2 at level 50, Q at level 200,
   format "|={ E1 , E2 }=>  Q") : uPred_scope.
23
Notation "P ={ E1 , E2 }=∗ Q" := (P - |={E1,E2}=> Q)%I
24
  (at level 99, E1,E2 at level 50, Q at level 200,
25
   format "P  ={ E1 , E2 }=∗  Q") : uPred_scope.
26
Notation "P ={ E1 , E2 }=∗ Q" := (P - |={E1,E2}=> Q)
27
28
29
30
31
  (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : C_scope.

Notation "|={ E }=> Q" := (fupd E E Q)
  (at level 99, E at level 50, Q at level 200,
   format "|={ E }=>  Q") : uPred_scope.
32
Notation "P ={ E }=∗ Q" := (P - |={E}=> Q)%I
33
  (at level 99, E at level 50, Q at level 200,
34
   format "P  ={ E }=∗  Q") : uPred_scope.
35
Notation "P ={ E }=∗ Q" := (P - |={E}=> Q)
36
37
38
  (at level 99, E at level 50, Q at level 200, only parsing) : C_scope.

Section fupd.
39
Context `{invG Σ}.
40
41
Implicit Types P Q : iProp Σ.

42
Global Instance fupd_ne E1 E2 : NonExpansive (@fupd Σ _ E1 E2).
43
Proof. rewrite fupd_eq. solve_proper. Qed.
44
Global Instance fupd_proper E1 E2 : Proper (() ==> ()) (@fupd Σ _ E1 E2).
45
46
47
48
49
Proof. apply ne_proper, _. Qed.

Lemma fupd_intro_mask E1 E2 P : E2  E1  P  |={E1,E2}=> |={E2,E1}=> P.
Proof.
  intros (E1''&->&?)%subseteq_disjoint_union_L.
50
51
  rewrite fupd_eq /fupd_def ownE_op //.
  by iIntros "$ ($ & $ & HE) !> !> [$ $] !> !>" .
52
53
Qed.

54
Lemma except_0_fupd E1 E2 P :  (|={E1,E2}=> P) ={E1,E2}= P.
55
Proof. rewrite fupd_eq. iIntros ">H [Hw HE]". iApply "H"; by iFrame. Qed.
56

57
Lemma bupd_fupd E P : (|==> P) ={E}= P.
58
Proof. rewrite fupd_eq /fupd_def. by iIntros ">? [$ $] !> !>". Qed.
59

60
Lemma fupd_mono E1 E2 P Q : (P  Q)  (|={E1,E2}=> P)  |={E1,E2}=> Q.
61
62
63
64
65
Proof.
  rewrite fupd_eq /fupd_def. iIntros (HPQ) "HP HwE".
  rewrite -HPQ. by iApply "HP".
Qed.

66
Lemma fupd_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P)  |={E1,E3}=> P.
67
68
Proof.
  rewrite fupd_eq /fupd_def. iIntros "HP HwE".
69
  iMod ("HP" with "HwE") as ">(Hw & HE & HP)". iApply "HP"; by iFrame.
70
71
72
Qed.

Lemma fupd_mask_frame_r' E1 E2 Ef P :
Ralf Jung's avatar
Ralf Jung committed
73
  E1  Ef  (|={E1,E2}=> E2  Ef  P) ={E1  Ef,E2  Ef}= P.
74
75
Proof.
  intros. rewrite fupd_eq /fupd_def ownE_op //. iIntros "Hvs (Hw & HE1 &HEf)".
76
  iMod ("Hvs" with "[Hw HE1]") as ">($ & HE2 & HP)"; first by iFrame.
77
  iDestruct (ownE_op' with "[HE2 HEf]") as "[? $]"; first by iFrame.
78
  iIntros "!> !>". by iApply "HP".
79
80
Qed.

81
Lemma fupd_frame_r E1 E2 P Q : (|={E1,E2}=> P)  Q ={E1,E2}= P  Q.
82
83
84
Proof. rewrite fupd_eq /fupd_def. by iIntros "[HwP $]". Qed.

(** * Derived rules *)
85
Global Instance fupd_mono' E1 E2 : Proper (() ==> ()) (@fupd Σ _ E1 E2).
86
87
Proof. intros P Q; apply fupd_mono. Qed.
Global Instance fupd_flip_mono' E1 E2 :
88
  Proper (flip () ==> flip ()) (@fupd Σ _ E1 E2).
89
90
Proof. intros P Q; apply fupd_mono. Qed.

91
Lemma fupd_intro E P : P ={E}= P.
92
Proof. iIntros "HP". by iApply bupd_fupd. Qed.
93
Lemma fupd_intro_mask' E1 E2 : E2  E1  (|={E1,E2}=> |={E2,E1}=> True)%I.
94
Proof. exact: fupd_intro_mask. Qed.
95
Lemma fupd_except_0 E1 E2 P : (|={E1,E2}=>  P) ={E1,E2}= P.
96
Proof. by rewrite {1}(fupd_intro E2 P) except_0_fupd fupd_trans. Qed.
97

98
Lemma fupd_frame_l E1 E2 P Q : (P  |={E1,E2}=> Q) ={E1,E2}= P  Q.
99
Proof. rewrite !(comm _ P); apply fupd_frame_r. Qed.
100
Lemma fupd_wand_l E1 E2 P Q : (P - Q)  (|={E1,E2}=> P) ={E1,E2}= Q.
101
Proof. by rewrite fupd_frame_l wand_elim_l. Qed.
102
Lemma fupd_wand_r E1 E2 P Q : (|={E1,E2}=> P)  (P - Q) ={E1,E2}= Q.
103
104
105
Proof. by rewrite fupd_frame_r wand_elim_r. Qed.

Lemma fupd_trans_frame E1 E2 E3 P Q :
106
  ((Q ={E2,E3}= True)  |={E1,E2}=> (Q  P)) ={E1,E3}= P.
107
108
109
110
111
112
Proof.
  rewrite fupd_frame_l assoc -(comm _ Q) wand_elim_r.
  by rewrite fupd_frame_r left_id fupd_trans.
Qed.

Lemma fupd_mask_frame_r E1 E2 Ef P :
113
  E1  Ef  (|={E1,E2}=> P) ={E1  Ef,E2  Ef}= P.
114
115
116
117
Proof.
  iIntros (?) "H". iApply fupd_mask_frame_r'; auto.
  iApply fupd_wand_r; iFrame "H"; eauto.
Qed.
118
Lemma fupd_mask_mono E1 E2 P : E1  E2  (|={E1}=> P) ={E2}= P.
119
120
121
122
Proof.
  intros (Ef&->&?)%subseteq_disjoint_union_L. by apply fupd_mask_frame_r.
Qed.

123
Lemma fupd_sep E P Q : (|={E}=> P)  (|={E}=> Q) ={E}= P  Q.
124
Proof. by rewrite fupd_frame_r fupd_frame_l fupd_trans. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
125
126
127
128
129
130
Lemma fupd_big_sepL {A} E (Φ : nat  A  iProp Σ) (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.
131
Lemma fupd_big_sepM `{Countable K} {A} E (Φ : K  A  iProp Σ) (m : gmap K A) :
132
  ([ map] kx  m, |={E}=> Φ k x) ={E}= [ map] kx  m, Φ k x.
133
Proof.
134
  apply (big_opM_forall (λ P Q, P ={E}= Q)); auto using fupd_intro.
135
136
137
  intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
Qed.
Lemma fupd_big_sepS `{Countable A} E (Φ : A  iProp Σ) X :
138
  ([ set] x  X, |={E}=> Φ x) ={E}= [ set] x  X, Φ x.
139
Proof.
140
  apply (big_opS_forall (λ P Q, P ={E}= Q)); auto using fupd_intro.
141
142
143
144
145
146
  intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
Qed.
End fupd.

(** Proofmode class instances *)
Section proofmode_classes.
147
  Context `{invG Σ}.
148
149
150
151
152
153
  Implicit Types P Q : iProp Σ.

  Global Instance from_pure_fupd E P φ : FromPure P φ  FromPure (|={E}=> P) φ.
  Proof. rewrite /FromPure. intros <-. apply fupd_intro. Qed.

  Global Instance from_assumption_fupd E p P Q :
154
    FromAssumption p P (|==> Q)  FromAssumption p P (|={E}=> Q)%I.
155
156
  Proof. rewrite /FromAssumption=>->. apply bupd_fupd. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
157
  Global Instance wand_weaken_fupd E1 E2 P Q P' Q' :
158
159
    WandWeaken false P Q P' Q' 
    WandWeaken' false P Q (|={E1,E2}=> P') (|={E1,E2}=> Q').
160
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
161
    rewrite /WandWeaken' /WandWeaken=>->. apply wand_intro_l. by rewrite fupd_wand_r.
162
  Qed.
163

164
165
166
  Global Instance from_and_fupd E P Q1 Q2 :
    FromAnd false P Q1 Q2  FromAnd false (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
  Proof. rewrite /FromAnd=><-. apply fupd_sep. Qed.
167
168
169
170
171
172
173
174
175
176
177

  Global Instance or_split_fupd E1 E2 P Q1 Q2 :
    FromOr P Q1 Q2  FromOr (|={E1,E2}=> P) (|={E1,E2}=> Q1) (|={E1,E2}=> Q2).
  Proof. rewrite /FromOr=><-. apply or_elim; apply fupd_mono; auto with I. Qed.

  Global Instance exists_split_fupd {A} E1 E2 P (Φ : A  iProp Σ) :
    FromExist P Φ  FromExist (|={E1,E2}=> P) (λ a, |={E1,E2}=> Φ a)%I.
  Proof.
    rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
  Qed.

178
179
  Global Instance frame_fupd p E1 E2 R P Q :
    Frame p R P Q  Frame p R (|={E1,E2}=> P) (|={E1,E2}=> Q).
180
181
  Proof. rewrite /Frame=><-. by rewrite fupd_frame_l. Qed.

182
183
  Global Instance is_except_0_fupd E1 E2 P : IsExcept0 (|={E1,E2}=> P).
  Proof. by rewrite /IsExcept0 except_0_fupd. Qed.
184

185
186
  Global Instance from_modal_fupd E P : FromModal (|={E}=> P) P.
  Proof. rewrite /FromModal. apply fupd_intro. Qed.
187

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
188
189
190
  (* Put a lower priority compared to [elim_modal_fupd_fupd], so that
     it is not taken when the first parameter is not specified (in
     spec. patterns). *)
191
  Global Instance elim_modal_bupd_fupd E1 E2 P Q :
192
    ElimModal (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q) | 10.
193
194
  Proof.
    by rewrite /ElimModal (bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans.
195
  Qed.
196
  Global Instance elim_modal_fupd_fupd E1 E2 E3 P Q :
197
    ElimModal (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
198
  Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_trans. Qed.
199
200
End proofmode_classes.

201
Hint Extern 2 (coq_tactics.of_envs _  |={_}=> _) => iModIntro.
202
203
204
205
206
207

(** 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") : uPred_scope.
208
Notation "P ={ E1 , E2 }▷=∗ Q" := (P - |={ E1 , E2 }=> Q)%I
209
  (at level 99, E1, E2 at level 50, Q at level 200,
210
   format "P  ={ E1 , E2 }▷=∗  Q") : uPred_scope.
211
212
213
Notation "|={ E }▷=> Q" := (|={E,E}=> Q)%I
  (at level 99, E at level 50, Q at level 200,
   format "|={ E }▷=>  Q") : uPred_scope.
214
Notation "P ={ E }▷=∗ Q" := (P ={E,E}= Q)%I
215
  (at level 99, E at level 50, Q at level 200,
216
   format "P  ={ E }▷=∗  Q") : uPred_scope.
217
218
219
220

Section step_fupd.
Context `{invG Σ}.

221
222
223
Lemma step_fupd_wand E1 E2 P Q : (|={E1,E2}=> P) - (P - Q) - |={E1,E2}=> Q.
Proof. iIntros "HP HPQ". by iApply "HPQ". Qed.

224
225
226
227
228
229
230
231
232
233
234
Lemma step_fupd_mask_frame_r E1 E2 Ef P :
  E1  Ef  E2  Ef  (|={E1,E2}=> P)  |={E1  Ef,E2  Ef}=> P.
Proof.
  iIntros (??) "HP". iApply fupd_mask_frame_r. done. iMod "HP". iModIntro.
  iNext. by iApply 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.
  iIntros (??) "HP".
235
236
  iMod (fupd_intro_mask') as "HM1"; first done. iMod "HP".
  iMod (fupd_intro_mask') as "HM2"; first done. iModIntro.
237
  iNext. iMod "HM2". iMod "HP". iMod "HM1". done.
238
Qed.
239
240
241

Lemma step_fupd_intro E1 E2 P : E2  E1   P - |={E1,E2}=> P.
Proof. iIntros (?) "HP". iApply (step_fupd_mask_mono E2 _ _ E2); auto. Qed.
242
End step_fupd.