fancy_updates.v 8.92 KB
Newer Older
1
2
From iris.base_logic.lib Require Export own.
From iris.prelude 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
Export invG.
8
9
Import uPred.

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

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.
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") : uPred_scope.
25
Notation "P ={ E1 , E2 }=★ Q" := (P  |={E1,E2}=> Q)
26
27
28
29
30
31
32
33
  (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.
Notation "P ={ E }=★ Q" := (P - |={E}=> Q)%I
  (at level 99, E at level 50, Q at level 200,
   format "P  ={ E }=★  Q") : uPred_scope.
34
Notation "P ={ E }=★ Q" := (P  |={E}=> Q)
35
36
37
  (at level 99, E at level 50, Q at level 200, only parsing) : C_scope.

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

41
Global Instance fupd_ne E1 E2 n : Proper (dist n ==> dist n) (@fupd Σ _ E1 E2).
42
Proof. rewrite fupd_eq. solve_proper. Qed.
43
Global Instance fupd_proper E1 E2 : Proper (() ==> ()) (@fupd Σ _ E1 E2).
44
45
46
47
48
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.
49
50
  rewrite fupd_eq /fupd_def ownE_op //.
  by iIntros "$ ($ & $ & HE) !> !> [$ $] !> !>" .
51
52
Qed.

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

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

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

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

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

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

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

90
Lemma fupd_intro E P : P ={E}= P.
91
92
93
Proof. iIntros "HP". by iApply bupd_fupd. Qed.
Lemma fupd_intro_mask' E1 E2 : E2  E1  True  |={E1,E2}=> |={E2,E1}=> True.
Proof. exact: fupd_intro_mask. Qed.
94
95
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.
96

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

Lemma fupd_trans_frame E1 E2 E3 P Q :
105
  ((Q ={E2,E3}= True)  |={E1,E2}=> (Q  P)) ={E1,E3}= P.
106
107
108
109
110
111
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 :
112
  E1  Ef  (|={E1,E2}=> P) ={E1  Ef,E2  Ef}= P.
113
114
115
116
Proof.
  iIntros (?) "H". iApply fupd_mask_frame_r'; auto.
  iApply fupd_wand_r; iFrame "H"; eauto.
Qed.
117
Lemma fupd_mask_mono E1 E2 P : E1  E2  (|={E1}=> P) ={E2}= P.
118
119
120
121
Proof.
  intros (Ef&->&?)%subseteq_disjoint_union_L. by apply fupd_mask_frame_r.
Qed.

122
Lemma fupd_sep E P Q : (|={E}=> P)  (|={E}=> Q) ={E}= P  Q.
123
124
Proof. by rewrite fupd_frame_r fupd_frame_l fupd_trans. Qed.
Lemma fupd_big_sepM `{Countable K} {A} E (Φ : K  A  iProp Σ) (m : gmap K A) :
125
  ([ map] kx  m, |={E}=> Φ k x) ={E}= [ map] kx  m, Φ k x.
126
Proof.
127
  apply (big_opM_forall (λ P Q, P ={E}= Q)); auto using fupd_intro.
128
129
130
  intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
Qed.
Lemma fupd_big_sepS `{Countable A} E (Φ : A  iProp Σ) X :
131
  ([ set] x  X, |={E}=> Φ x) ={E}= [ set] x  X, Φ x.
132
Proof.
133
  apply (big_opS_forall (λ P Q, P ={E}= Q)); auto using fupd_intro.
134
135
136
137
138
139
  intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
Qed.
End fupd.

(** Proofmode class instances *)
Section proofmode_classes.
140
  Context `{invG Σ}.
141
142
143
144
145
146
  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 :
147
    FromAssumption p P (|==> Q)  FromAssumption p P (|={E}=> Q)%I.
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
  Proof. rewrite /FromAssumption=>->. apply bupd_fupd. Qed.

  Global Instance into_wand_fupd E1 E2 R P Q :
    IntoWand R P Q  IntoWand R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
  Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite fupd_wand_r. Qed.

  Global Instance from_sep_fupd E P Q1 Q2 :
    FromSep P Q1 Q2  FromSep (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
  Proof. rewrite /FromSep=><-. apply fupd_sep. Qed.

  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.

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

172
173
  Global Instance is_except_0_fupd E1 E2 P : IsExcept0 (|={E1,E2}=> P).
  Proof. by rewrite /IsExcept0 except_0_fupd. Qed.
174

175
176
  Global Instance into_modal_fupd E P : IntoModal P (|={E}=> P).
  Proof. rewrite /IntoModal. apply fupd_intro. Qed.
177

178
179
180
181
182
183
184
185
  Global Instance elim_modal_bupd_fupd E1 E2 P Q :
    ElimModal (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q).
  Proof.
    by rewrite /ElimModal (bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans.
 Qed.
  Global Instance elim_modal_fupd_fupd E1 E2 E3 P Q :
    ElimModal (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
  Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_trans. Qed.
186
187
188
End proofmode_classes.

Hint Extern 2 (coq_tactics.of_envs _  _) =>
189
  match goal with |- _  |={_}=> _ => iModIntro end.
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
220
221
222
223
224
225
226
227

(** 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.
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") : uPred_scope.
Notation "|={ E }▷=> Q" := (|={E,E}=> Q)%I
  (at level 99, E at level 50, Q at level 200,
   format "|={ E }▷=>  Q") : uPred_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") : uPred_scope.

Section step_fupd.
Context `{invG Σ}.

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".
  iAssert (|={E2,E1}=> True)%I as "HE".
  { iApply fupd_mono. apply later_intro. by iApply fupd_intro_mask. }
  iAssert (|={F2,F1}=> True)%I as "HF".
  { iApply fupd_mono. apply later_intro. by iApply fupd_intro_mask. }
  iMod "HE". iMod "HP". iMod "HF". iModIntro. iNext. iMod "HF". iMod "HP". by iMod "HE".
Qed.

End step_fupd.