big_op.v 27.6 KB
Newer Older
1
2
From iris.algebra Require Export list cmra_big_op.
From iris.base_logic Require Export base_logic.
Robbert Krebbers's avatar
Robbert Krebbers committed
3
From iris.prelude Require Import gmap fin_collections gmultiset functions.
4
Import uPred.
5

6
7
8
9
10
(* We make use of the bigops on CMRAs, so we first define a (somewhat ad-hoc)
CMRA structure on uPred. *)
Section cmra.
  Context {M : ucmraT}.

11
12
  Instance uPred_valid_inst : Valid (uPred M) := λ P,  n x, {n} x  P n x.
  Instance uPred_validN_inst : ValidN (uPred M) := λ n P,
13
14
15
16
     n' x, n'  n  {n'} x  P n' x.
  Instance uPred_op : Op (uPred M) := uPred_sep.
  Instance uPred_pcore : PCore (uPred M) := λ _, Some True%I.

17
  Instance uPred_validN_ne n : Proper (dist n ==> iff) (uPred_validN_inst n).
18
19
20
21
22
23
24
25
  Proof. intros P Q HPQ; split=> H n' x ??; by apply HPQ, H. Qed.

  Lemma uPred_validN_alt n (P : uPred M) : {n} P  P {n} True%I.
  Proof.
    unseal=> HP; split=> n' x ??; split; [done|].
    intros _. by apply HP.
  Qed.

26
  Lemma uPred_cmra_validN_op_l n P Q : {n} (P  Q)%I  {n} P.
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
  Proof.
    unseal. intros HPQ n' x ??.
    destruct (HPQ n' x) as (x1&x2&->&?&?); auto.
    eapply uPred_mono with x1; eauto using cmra_includedN_l.
  Qed.

  Lemma uPred_included P Q : P  Q  Q  P.
  Proof. intros [P' ->]. apply sep_elim_l. Qed.

  Definition uPred_cmra_mixin : CMRAMixin (uPred M).
  Proof.
    apply cmra_total_mixin; try apply _ || by eauto.
    - intros n P Q ??. by cofe_subst.
    - intros P; split.
      + intros HP n n' x ?. apply HP.
      + intros HP n x. by apply (HP n).
    - intros n P HP n' x ?. apply HP; auto.
    - intros P. by rewrite left_id.
    - intros P Q _. exists True%I. by rewrite left_id.
    - intros n P Q. apply uPred_cmra_validN_op_l.
    - intros n P Q1 Q2 HP HPQ. exists True%I, P; split_and!.
      + by rewrite left_id.
      + move: HP; by rewrite HPQ=> /uPred_cmra_validN_op_l /uPred_validN_alt.
      + move: HP; rewrite HPQ=> /uPred_cmra_validN_op_l /uPred_validN_alt=> ->.
        by rewrite left_id.
  Qed.

  Canonical Structure uPredR :=
55
    CMRAT (uPred M) uPred_ofe_mixin uPred_cmra_mixin.
56
57
58
59
60
61
62
63
64
65
66

  Instance uPred_empty : Empty (uPred M) := True%I.

  Definition uPred_ucmra_mixin : UCMRAMixin (uPred M).
  Proof.
    split; last done.
    - by rewrite /empty /uPred_empty uPred_pure_eq.
    - intros P. by rewrite left_id.
  Qed.

  Canonical Structure uPredUR :=
67
    UCMRAT (uPred M) uPred_ofe_mixin uPred_cmra_mixin uPred_ucmra_mixin.
68
69
70
71
72
73
74
75

  Global Instance uPred_always_homomorphism : UCMRAHomomorphism uPred_always.
  Proof. split; [split|]. apply _. apply always_sep. apply always_pure. Qed.
  Global Instance uPred_always_if_homomorphism b :
    UCMRAHomomorphism (uPred_always_if b).
  Proof. split; [split|]. apply _. apply always_if_sep. apply always_if_pure. Qed.
  Global Instance uPred_later_homomorphism : UCMRAHomomorphism uPred_later.
  Proof. split; [split|]. apply _. apply later_sep. apply later_True. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
76
77
  Global Instance uPred_laterN_homomorphism n : UCMRAHomomorphism (uPred_laterN n).
  Proof. split; [split|]. apply _. apply laterN_sep. apply laterN_True. Qed.
78
79
80
81
82
83
84
85
86
87
88
  Global Instance uPred_except_0_homomorphism :
    CMRAHomomorphism uPred_except_0.
  Proof. split. apply _. apply except_0_sep. Qed.
  Global Instance uPred_ownM_homomorphism : UCMRAHomomorphism uPred_ownM.
  Proof. split; [split|]. apply _. apply ownM_op. apply ownM_empty'. Qed.
End cmra.

Arguments uPredR : clear implicits.
Arguments uPredUR : clear implicits.

(* Notations *)
89
Notation "'[∗]' Ps" := (big_op (M:=uPredUR _) Ps) (at level 20) : uPred_scope.
90

91
Notation "'[∗' 'list' ] k ↦ x ∈ l , P" := (big_opL (M:=uPredUR _) l (λ k x, P))
92
  (at level 200, l at level 10, k, x at level 1, right associativity,
93
94
   format "[∗  list ]  k ↦ x  ∈  l ,  P") : uPred_scope.
Notation "'[∗' 'list' ] x ∈ l , P" := (big_opL (M:=uPredUR _) l (λ _ x, P))
95
  (at level 200, l at level 10, x at level 1, right associativity,
96
   format "[∗  list ]  x  ∈  l ,  P") : uPred_scope.
97

98
Notation "'[∗' 'map' ] k ↦ x ∈ m , P" := (big_opM (M:=uPredUR _) m (λ k x, P))
99
  (at level 200, m at level 10, k, x at level 1, right associativity,
100
101
   format "[∗  map ]  k ↦ x  ∈  m ,  P") : uPred_scope.
Notation "'[∗' 'map' ] x ∈ m , P" := (big_opM (M:=uPredUR _) m (λ _ x, P))
102
  (at level 200, m at level 10, x at level 1, right associativity,
103
   format "[∗  map ]  x  ∈  m ,  P") : uPred_scope.
104

105
Notation "'[∗' 'set' ] x ∈ X , P" := (big_opS (M:=uPredUR _) X (λ x, P))
106
  (at level 200, X at level 10, x at level 1, right associativity,
107
   format "[∗  set ]  x  ∈  X ,  P") : uPred_scope.
108

Robbert Krebbers's avatar
Robbert Krebbers committed
109
110
111
112
Notation "'[∗' 'mset' ] x ∈ X , P" := (big_opMS (M:=uPredUR _) X (λ x, P))
  (at level 200, X at level 10, x at level 1, right associativity,
   format "[∗  mset ]  x  ∈  X ,  P") : uPred_scope.

113
(** * Persistence and timelessness of lists of uPreds *)
114
Class PersistentL {M} (Ps : list (uPred M)) :=
115
  persistentL : Forall PersistentP Ps.
116
Arguments persistentL {_} _ {_}.
117

118
119
120
121
Class TimelessL {M} (Ps : list (uPred M)) :=
  timelessL : Forall TimelessP Ps.
Arguments timelessL {_} _ {_}.

122
(** * Properties *)
123
Section big_op.
124
Context {M : ucmraT}.
125
126
127
Implicit Types Ps Qs : list (uPred M).
Implicit Types A : Type.

128
129
Global Instance big_sep_mono' :
  Proper (Forall2 () ==> ()) (big_op (M:=uPredUR M)).
130
131
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.

132
Lemma big_sep_app Ps Qs : [] (Ps ++ Qs)  [] Ps  [] Qs.
133
Proof. by rewrite big_op_app. Qed.
134

135
Lemma big_sep_contains Ps Qs : Qs `contains` Ps  [] Ps  [] Qs.
136
Proof. intros. apply uPred_included. by apply: big_op_contains. Qed.
137
Lemma big_sep_elem_of Ps P : P  Ps  [] Ps  P.
138
Proof. intros. apply uPred_included. by apply: big_sep_elem_of. Qed.
139
140
141
142
143
144
Lemma big_sep_elem_of_acc Ps P : P  Ps  [] Ps  P  (P - [] Ps).
Proof.
  intros (Ps1&Ps2&->)%elem_of_list_split.
  rewrite !big_sep_app /=. rewrite assoc (comm _ _ P) -assoc.
  by apply sep_mono_r, wand_intro_l.
Qed.
145

146
(** ** Persistence *)
147
Global Instance big_sep_persistent Ps : PersistentL Ps  PersistentP ([] Ps).
148
149
150
151
152
153
154
155
156
157
158
159
160
Proof. induction 1; apply _. Qed.

Global Instance nil_persistent : PersistentL (@nil (uPred M)).
Proof. constructor. Qed.
Global Instance cons_persistent P Ps :
  PersistentP P  PersistentL Ps  PersistentL (P :: Ps).
Proof. by constructor. Qed.
Global Instance app_persistent Ps Ps' :
  PersistentL Ps  PersistentL Ps'  PersistentL (Ps ++ Ps').
Proof. apply Forall_app_2. Qed.

Global Instance fmap_persistent {A} (f : A  uPred M) xs :
  ( x, PersistentP (f x))  PersistentL (f <$> xs).
161
Proof. intros. apply Forall_fmap, Forall_forall; auto. Qed.
162
163
164
165
166
Global Instance zip_with_persistent {A B} (f : A  B  uPred M) xs ys :
  ( x y, PersistentP (f x y))  PersistentL (zip_with f xs ys).
Proof.
  unfold PersistentL=> ?; revert ys; induction xs=> -[|??]; constructor; auto.
Qed.
167
168
169
170
171
Global Instance imap_persistent {A} (f : nat  A  uPred M) xs :
  ( i x, PersistentP (f i x))  PersistentL (imap f xs).
Proof.
  rewrite /PersistentL /imap=> ?. generalize 0. induction xs; constructor; auto.
Qed.
172
173

(** ** Timelessness *)
174
Global Instance big_sep_timeless Ps : TimelessL Ps  TimelessP ([] Ps).
175
176
177
178
179
180
181
182
183
184
185
186
187
Proof. induction 1; apply _. Qed.

Global Instance nil_timeless : TimelessL (@nil (uPred M)).
Proof. constructor. Qed.
Global Instance cons_timeless P Ps :
  TimelessP P  TimelessL Ps  TimelessL (P :: Ps).
Proof. by constructor. Qed.
Global Instance app_timeless Ps Ps' :
  TimelessL Ps  TimelessL Ps'  TimelessL (Ps ++ Ps').
Proof. apply Forall_app_2. Qed.

Global Instance fmap_timeless {A} (f : A  uPred M) xs :
  ( x, TimelessP (f x))  TimelessL (f <$> xs).
188
Proof. intros. apply Forall_fmap, Forall_forall; auto. Qed.
189
190
191
192
193
Global Instance zip_with_timeless {A B} (f : A  B  uPred M) xs ys :
  ( x y, TimelessP (f x y))  TimelessL (zip_with f xs ys).
Proof.
  unfold TimelessL=> ?; revert ys; induction xs=> -[|??]; constructor; auto.
Qed.
194
195
196
197
198
199
200
201
202
203
204
205
Global Instance imap_timeless {A} (f : nat  A  uPred M) xs :
  ( i x, TimelessP (f i x))  TimelessL (imap f xs).
Proof.
  rewrite /TimelessL /imap=> ?. generalize 0. induction xs; constructor; auto.
Qed.

(** ** Big ops over lists *)
Section list.
  Context {A : Type}.
  Implicit Types l : list A.
  Implicit Types Φ Ψ : nat  A  uPred M.

206
  Lemma big_sepL_nil Φ : ([ list] ky  nil, Φ k y)  True.
207
208
  Proof. done. Qed.
  Lemma big_sepL_cons Φ x l :
209
    ([ list] ky  x :: l, Φ k y)  Φ 0 x  [ list] ky  l, Φ (S k) y.
210
  Proof. by rewrite big_opL_cons. Qed.
211
  Lemma big_sepL_singleton Φ x : ([ list] ky  [x], Φ k y)  Φ 0 x.
212
213
  Proof. by rewrite big_opL_singleton. Qed.
  Lemma big_sepL_app Φ l1 l2 :
214
215
    ([ list] ky  l1 ++ l2, Φ k y)
     ([ list] ky  l1, Φ k y)  ([ list] ky  l2, Φ (length l1 + k) y).
216
217
  Proof. by rewrite big_opL_app. Qed.

218
219
  Lemma big_sepL_mono Φ Ψ l :
    ( k y, l !! k = Some y  Φ k y  Ψ k y) 
220
    ([ list] k  y  l, Φ k y)  [ list] k  y  l, Ψ k y.
221
  Proof. apply big_opL_forall; apply _. Qed.
222
223
  Lemma big_sepL_proper Φ Ψ l :
    ( k y, l !! k = Some y  Φ k y  Ψ k y) 
224
    ([ list] k  y  l, Φ k y)  ([ list] k  y  l, Ψ k y).
225
  Proof. apply big_opL_proper. Qed.
226
227
228

  Global Instance big_sepL_mono' l :
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
229
230
           (big_opL (M:=uPredUR M) l).
  Proof. intros f g Hf. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
231
232

  Lemma big_sepL_lookup Φ l i x :
233
    l !! i = Some x  ([ list] ky  l, Φ k y)  Φ i x.
234
  Proof. intros. apply uPred_included. by apply: big_opL_lookup. Qed.
235

Robbert Krebbers's avatar
Robbert Krebbers committed
236
  Lemma big_sepL_elem_of (Φ : A  uPred M) l x :
237
    x  l  ([ list] y  l, Φ y)  Φ x.
238
  Proof. intros. apply uPred_included. by apply: big_opL_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
239

240
  Lemma big_sepL_fmap {B} (f : A  B) (Φ : nat  B  uPred M) l :
241
    ([ list] ky  f <$> l, Φ k y)  ([ list] ky  l, Φ k (f y)).
242
  Proof. by rewrite big_opL_fmap. Qed.
243
244

  Lemma big_sepL_sepL Φ Ψ l :
245
246
    ([ list] kx  l, Φ k x  Ψ k x)
     ([ list] kx  l, Φ k x)  ([ list] kx  l, Ψ k x).
247
  Proof. by rewrite big_opL_opL. Qed.
248

249
250
251
252
253
  Lemma big_sepL_and Φ Ψ l :
    ([ list] kx  l, Φ k x  Ψ k x)
     ([ list] kx  l, Φ k x)  ([ list] kx  l, Ψ k x).
  Proof. auto using big_sepL_mono with I. Qed.

254
  Lemma big_sepL_later Φ l :
255
     ([ list] kx  l, Φ k x)  ([ list] kx  l,  Φ k x).
256
  Proof. apply (big_opL_commute _). Qed.
257

Robbert Krebbers's avatar
Robbert Krebbers committed
258
259
260
261
  Lemma big_sepL_laterN Φ n l :
    ^n ([ list] kx  l, Φ k x)  ([ list] kx  l, ^n Φ k x).
  Proof. apply (big_opL_commute _). Qed.

262
  Lemma big_sepL_always Φ l :
263
    ( [ list] kx  l, Φ k x)  ([ list] kx  l,  Φ k x).
264
  Proof. apply (big_opL_commute _). Qed.
265
266

  Lemma big_sepL_always_if p Φ l :
267
    ?p ([ list] kx  l, Φ k x)  ([ list] kx  l, ?p Φ k x).
268
  Proof. apply (big_opL_commute _). Qed.
269
270
271

  Lemma big_sepL_forall Φ l :
    ( k x, PersistentP (Φ k x)) 
Ralf Jung's avatar
Ralf Jung committed
272
    ([ list] kx  l, Φ k x)  ( k x, l !! k = Some x  Φ k x).
273
274
275
276
277
278
279
  Proof.
    intros HΦ. apply (anti_symm _).
    { apply forall_intro=> k; apply forall_intro=> x.
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepL_lookup. }
    revert Φ HΦ. induction l as [|x l IH]=> Φ HΦ.
    { rewrite big_sepL_nil; auto with I. }
    rewrite big_sepL_cons. rewrite -always_and_sep_l; apply and_intro.
280
    - by rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl.
281
282
283
284
    - rewrite -IH. apply forall_intro=> k; by rewrite (forall_elim (S k)).
  Qed.

  Lemma big_sepL_impl Φ Ψ l :
Ralf Jung's avatar
Ralf Jung committed
285
     ( k x, l !! k = Some x  Φ k x  Ψ k x)  ([ list] kx  l, Φ k x)
286
     [ list] kx  l, Ψ k x.
287
288
289
290
291
292
293
  Proof.
    rewrite always_and_sep_l. do 2 setoid_rewrite always_forall.
    setoid_rewrite always_impl; setoid_rewrite always_pure.
    rewrite -big_sepL_forall -big_sepL_sepL. apply big_sepL_mono; auto=> k x ?.
    by rewrite -always_wand_impl always_elim wand_elim_l.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
294
  Global Instance big_sepL_nil_persistent Φ :
295
    PersistentP ([ list] kx  [], Φ k x).
296
  Proof. rewrite /big_opL. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
297
  Global Instance big_sepL_persistent Φ l :
298
    ( k x, PersistentP (Φ k x))  PersistentP ([ list] kx  l, Φ k x).
299
  Proof. rewrite /big_opL. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
300
  Global Instance big_sepL_nil_timeless Φ :
301
    TimelessP ([ list] kx  [], Φ k x).
302
  Proof. rewrite /big_opL. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
303
  Global Instance big_sepL_timeless Φ l :
304
    ( k x, TimelessP (Φ k x))  TimelessP ([ list] kx  l, Φ k x).
305
  Proof. rewrite /big_opL. apply _. Qed.
306
307
End list.

308

309
(** ** Big ops over finite maps *)
310
311
312
Section gmap.
  Context `{Countable K} {A : Type}.
  Implicit Types m : gmap K A.
313
  Implicit Types Φ Ψ : K  A  uPred M.
314

315
  Lemma big_sepM_mono Φ Ψ m1 m2 :
316
    m2  m1  ( k x, m2 !! k = Some x  Φ k x  Ψ k x) 
317
    ([ map] k  x  m1, Φ k x)  [ map] k  x  m2, Ψ k x.
318
  Proof.
319
    intros Hm HΦ. trans ([ map] kx  m2, Φ k x)%I.
320
321
322
    - apply uPred_included. apply: big_op_contains.
      by apply fmap_contains, map_to_list_contains.
    - apply big_opM_forall; apply _ || auto.
323
  Qed.
324
325
  Lemma big_sepM_proper Φ Ψ m :
    ( k x, m !! k = Some x  Φ k x  Ψ k x) 
326
    ([ map] k  x  m, Φ k x)  ([ map] k  x  m, Ψ k x).
327
  Proof. apply big_opM_proper. Qed.
328
329

  Global Instance big_sepM_mono' m :
330
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
331
332
           (big_opM (M:=uPredUR M) m).
  Proof. intros f g Hf. apply big_opM_forall; apply _ || intros; apply Hf. Qed.
333

334
  Lemma big_sepM_empty Φ : ([ map] kx  , Φ k x)  True.
335
  Proof. by rewrite big_opM_empty. Qed.
336

337
  Lemma big_sepM_insert Φ m i x :
338
    m !! i = None 
339
    ([ map] ky  <[i:=x]> m, Φ k y)  Φ i x  [ map] ky  m, Φ k y.
340
  Proof. apply: big_opM_insert. Qed.
341

342
  Lemma big_sepM_delete Φ m i x :
343
    m !! i = Some x 
344
    ([ map] ky  m, Φ k y)  Φ i x  [ map] ky  delete i m, Φ k y.
345
  Proof. apply: big_opM_delete. Qed.
346

347
348
349
350
351
352
353
  Lemma big_sepM_lookup_acc Φ m i x :
    m !! i = Some x 
    ([ map] ky  m, Φ k y)  Φ i x  (Φ i x - ([ map] ky  m, Φ k y)).
  Proof.
    intros. rewrite big_sepM_delete //. by apply sep_mono_r, wand_intro_l.
  Qed.

354
  Lemma big_sepM_lookup Φ m i x :
355
    m !! i = Some x  ([ map] ky  m, Φ k y)  Φ i x.
356
357
  Proof. intros. apply uPred_included. by apply: big_opM_lookup. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
358
359
360
  Lemma big_sepM_lookup_dom (Φ : K  uPred M) m i :
    is_Some (m !! i)  ([ map] k_  m, Φ k)  Φ i.
  Proof. intros [x ?]. by eapply (big_sepM_lookup (λ i x, Φ i)). Qed.
361

362
  Lemma big_sepM_singleton Φ i x : ([ map] ky  {[i:=x]}, Φ k y)  Φ i x.
363
  Proof. by rewrite big_opM_singleton. Qed.
364

365
  Lemma big_sepM_fmap {B} (f : A  B) (Φ : K  B  uPred M) m :
366
    ([ map] ky  f <$> m, Φ k y)  ([ map] ky  m, Φ k (f y)).
367
  Proof. by rewrite big_opM_fmap. Qed.
368

369
  Lemma big_sepM_insert_override (Φ : K  uPred M) m i x y :
370
    m !! i = Some x 
371
    ([ map] k_  <[i:=y]> m, Φ k)  ([ map] k_  m, Φ k).
372
  Proof. apply: big_opM_insert_override. Qed.
373

374
  Lemma big_sepM_fn_insert {B} (Ψ : K  A  B  uPred M) (f : K  B) m i x b :
375
    m !! i = None 
376
377
       ([ map] ky  <[i:=x]> m, Ψ k y (<[i:=b]> f k))
     (Ψ i x b  [ map] ky  m, Ψ k y (f k)).
378
379
  Proof. apply: big_opM_fn_insert. Qed.

380
381
  Lemma big_sepM_fn_insert' (Φ : K  uPred M) m i x P :
    m !! i = None 
382
    ([ map] ky  <[i:=x]> m, <[i:=P]> Φ k)  (P  [ map] ky  m, Φ k).
383
  Proof. apply: big_opM_fn_insert'. Qed.
384

385
  Lemma big_sepM_sepM Φ Ψ m :
386
    ([ map] kx  m, Φ k x  Ψ k x)
387
     ([ map] kx  m, Φ k x)  ([ map] kx  m, Ψ k x).
388
  Proof. apply: big_opM_opM. Qed.
389

390
391
392
393
394
  Lemma big_sepM_and Φ Ψ m :
    ([ map] kx  m, Φ k x  Ψ k x)
     ([ map] kx  m, Φ k x)  ([ map] kx  m, Ψ k x).
  Proof. auto using big_sepM_mono with I. Qed.

395
  Lemma big_sepM_later Φ m :
396
     ([ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
397
  Proof. apply (big_opM_commute _). Qed.
398

Robbert Krebbers's avatar
Robbert Krebbers committed
399
400
401
402
  Lemma big_sepM_laterN Φ n m :
    ^n ([ map] kx  m, Φ k x)  ([ map] kx  m, ^n Φ k x).
  Proof. apply (big_opM_commute _). Qed.

403
  Lemma big_sepM_always Φ m :
404
    ( [ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
405
  Proof. apply (big_opM_commute _). Qed.
406
407

  Lemma big_sepM_always_if p Φ m :
408
    ?p ([ map] kx  m, Φ k x)  ([ map] kx  m, ?p Φ k x).
409
  Proof. apply (big_opM_commute _). Qed.
410
411
412

  Lemma big_sepM_forall Φ m :
    ( k x, PersistentP (Φ k x)) 
Ralf Jung's avatar
Ralf Jung committed
413
    ([ map] kx  m, Φ k x)  ( k x, m !! k = Some x  Φ k x).
414
415
416
  Proof.
    intros. apply (anti_symm _).
    { apply forall_intro=> k; apply forall_intro=> x.
417
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepM_lookup. }
418
419
420
    induction m as [|i x m ? IH] using map_ind; [rewrite ?big_sepM_empty; auto|].
    rewrite big_sepM_insert // -always_and_sep_l. apply and_intro.
    - rewrite (forall_elim i) (forall_elim x) lookup_insert.
421
      by rewrite pure_True // True_impl.
422
    - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
423
424
      apply impl_intro_l, pure_elim_l=> ?.
      rewrite lookup_insert_ne; last by intros ?; simplify_map_eq.
425
      by rewrite pure_True // True_impl.
426
427
428
  Qed.

  Lemma big_sepM_impl Φ Ψ m :
Ralf Jung's avatar
Ralf Jung committed
429
     ( k x, m !! k = Some x  Φ k x  Ψ k x)  ([ map] kx  m, Φ k x)
430
     [ map] kx  m, Ψ k x.
431
432
  Proof.
    rewrite always_and_sep_l. do 2 setoid_rewrite always_forall.
433
    setoid_rewrite always_impl; setoid_rewrite always_pure.
434
435
436
    rewrite -big_sepM_forall -big_sepM_sepM. apply big_sepM_mono; auto=> k x ?.
    by rewrite -always_wand_impl always_elim wand_elim_l.
  Qed.
437

Robbert Krebbers's avatar
Robbert Krebbers committed
438
  Global Instance big_sepM_empty_persistent Φ :
439
    PersistentP ([ map] kx  , Φ k x).
440
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
441
  Global Instance big_sepM_persistent Φ m :
442
    ( k x, PersistentP (Φ k x))  PersistentP ([ map] kx  m, Φ k x).
443
  Proof. intros. apply big_sep_persistent, fmap_persistent=>-[??] /=; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
444
  Global Instance big_sepM_nil_timeless Φ :
445
    TimelessP ([ map] kx  , Φ k x).
446
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
447
  Global Instance big_sepM_timeless Φ m :
448
    ( k x, TimelessP (Φ k x))  TimelessP ([ map] kx  m, Φ k x).
449
  Proof. intro. apply big_sep_timeless, fmap_timeless=> -[??] /=; auto. Qed.
450
451
End gmap.

452

453
(** ** Big ops over finite sets *)
454
455
456
Section gset.
  Context `{Countable A}.
  Implicit Types X : gset A.
457
  Implicit Types Φ : A  uPred M.
458

459
  Lemma big_sepS_mono Φ Ψ X Y :
460
    Y  X  ( x, x  Y  Φ x  Ψ x) 
461
    ([ set] x  X, Φ x)  [ set] x  Y, Ψ x.
462
  Proof.
463
    intros HX HΦ. trans ([ set] x  Y, Φ x)%I.
464
465
466
    - apply uPred_included. apply: big_op_contains.
      by apply fmap_contains, elements_contains.
    - apply big_opS_forall; apply _ || auto.
467
  Qed.
468
469
  Lemma big_sepS_proper Φ Ψ X :
    ( x, x  X  Φ x  Ψ x) 
470
    ([ set] x  X, Φ x)  ([ set] x  X, Ψ x).
471
  Proof. apply: big_opS_proper. Qed.
472

473
  Global Instance big_sepS_mono' X :
474
475
476
     Proper (pointwise_relation _ () ==> ()) (big_opS (M:=uPredUR M) X).
  Proof. intros f g Hf. apply big_opS_forall; apply _ || intros; apply Hf. Qed.

477
  Lemma big_sepS_empty Φ : ([ set] x  , Φ x)  True.
478
  Proof. by rewrite big_opS_empty. Qed.
479

480
  Lemma big_sepS_insert Φ X x :
481
    x  X  ([ set] y  {[ x ]}  X, Φ y)  (Φ x  [ set] y  X, Φ y).
482
483
  Proof. apply: big_opS_insert. Qed.

484
  Lemma big_sepS_fn_insert {B} (Ψ : A  B  uPred M) f X x b :
485
    x  X 
486
487
       ([ set] y  {[ x ]}  X, Ψ y (<[x:=b]> f y))
     (Ψ x b  [ set] y  X, Ψ y (f y)).
488
489
  Proof. apply: big_opS_fn_insert. Qed.

490
  Lemma big_sepS_fn_insert' Φ X x P :
491
    x  X  ([ set] y  {[ x ]}  X, <[x:=P]> Φ y)  (P  [ set] y  X, Φ y).
492
  Proof. apply: big_opS_fn_insert'. Qed.
493

Robbert Krebbers's avatar
Robbert Krebbers committed
494
495
496
497
498
  Lemma big_sepS_union Φ X Y :
    X  Y 
    ([ set] y  X  Y, Φ y)  ([ set] y  X, Φ y)  ([ set] y  Y, Φ y).
  Proof. apply: big_opS_union. Qed.

499
  Lemma big_sepS_delete Φ X x :
500
    x  X  ([ set] y  X, Φ y)  Φ x  [ set] y  X  {[ x ]}, Φ y.
501
  Proof. apply: big_opS_delete. Qed.
502

503
  Lemma big_sepS_elem_of Φ X x : x  X  ([ set] y  X, Φ y)  Φ x.
504
  Proof. intros. apply uPred_included. by apply: big_opS_elem_of. Qed.
505

506
507
508
509
510
511
512
  Lemma big_sepS_elem_of_acc Φ X x :
    x  X 
    ([ set] y  X, Φ y)  Φ x  (Φ x - ([ set] y  X, Φ y)).
  Proof.
    intros. rewrite big_sepS_delete //. by apply sep_mono_r, wand_intro_l.
  Qed.

513
  Lemma big_sepS_singleton Φ x : ([ set] y  {[ x ]}, Φ y)  Φ x.
514
  Proof. apply: big_opS_singleton. Qed.
515

516
  Lemma big_sepS_filter (P : A  Prop) `{ x, Decision (P x)} Φ X :
Ralf Jung's avatar
Ralf Jung committed
517
    ([ set] y  filter P X, Φ y)  ([ set] y  X, P y  Φ y).
518
519
520
521
522
523
524
525
526
527
528
  Proof.
    induction X as [|x X ? IH] using collection_ind_L.
    { by rewrite filter_empty_L !big_sepS_empty. }
    destruct (decide (P x)).
    - rewrite filter_union_L filter_singleton_L //.
      rewrite !big_sepS_insert //; last set_solver.
      by rewrite IH pure_True // left_id.
    - rewrite filter_union_L filter_singleton_not_L // left_id_L.
      by rewrite !big_sepS_insert // IH pure_False // False_impl left_id.
  Qed.

529
  Lemma big_sepS_sepS Φ Ψ X :
530
    ([ set] y  X, Φ y  Ψ y)  ([ set] y  X, Φ y)  ([ set] y  X, Ψ y).
531
  Proof. apply: big_opS_opS. Qed.
532

533
534
535
536
  Lemma big_sepS_and Φ Ψ X :
    ([ set] y  X, Φ y  Ψ y)  ([ set] y  X, Φ y)  ([ set] y  X, Ψ y).
  Proof. auto using big_sepS_mono with I. Qed.

537
  Lemma big_sepS_later Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
538
  Proof. apply (big_opS_commute _). Qed.
539

Robbert Krebbers's avatar
Robbert Krebbers committed
540
541
542
543
  Lemma big_sepS_laterN Φ n X :
    ^n ([ set] y  X, Φ y)  ([ set] y  X, ^n Φ y).
  Proof. apply (big_opS_commute _). Qed.

544
  Lemma big_sepS_always Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
545
  Proof. apply (big_opS_commute _). Qed.
546

547
  Lemma big_sepS_always_if q Φ X :
548
    ?q ([ set] y  X, Φ y)  ([ set] y  X, ?q Φ y).
549
  Proof. apply (big_opS_commute _). Qed.
550
551

  Lemma big_sepS_forall Φ X :
Ralf Jung's avatar
Ralf Jung committed
552
    ( x, PersistentP (Φ x))  ([ set] x  X, Φ x)  ( x, x  X  Φ x).
553
554
555
  Proof.
    intros. apply (anti_symm _).
    { apply forall_intro=> x.
556
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. }
557
    induction X as [|x X ? IH] using collection_ind_L.
558
559
    { rewrite big_sepS_empty; auto. }
    rewrite big_sepS_insert // -always_and_sep_l. apply and_intro.
560
    - by rewrite (forall_elim x) pure_True ?True_impl; last set_solver.
561
    - rewrite -IH. apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
562
      by rewrite pure_True ?True_impl; last set_solver.
563
564
565
  Qed.

  Lemma big_sepS_impl Φ Ψ X :
Ralf Jung's avatar
Ralf Jung committed
566
     ( x, x  X  Φ x  Ψ x)  ([ set] x  X, Φ x)  [ set] x  X, Ψ x.
567
568
  Proof.
    rewrite always_and_sep_l always_forall.
569
    setoid_rewrite always_impl; setoid_rewrite always_pure.
570
571
572
    rewrite -big_sepS_forall -big_sepS_sepS. apply big_sepS_mono; auto=> x ?.
    by rewrite -always_wand_impl always_elim wand_elim_l.
  Qed.
573

574
  Global Instance big_sepS_empty_persistent Φ : PersistentP ([ set] x  , Φ x).
575
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
576
  Global Instance big_sepS_persistent Φ X :
577
    ( x, PersistentP (Φ x))  PersistentP ([ set] x  X, Φ x).
578
  Proof. rewrite /big_opS. apply _. Qed.
579
  Global Instance big_sepS_nil_timeless Φ : TimelessP ([ set] x  , Φ x).
580
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
581
  Global Instance big_sepS_timeless Φ X :
582
    ( x, TimelessP (Φ x))  TimelessP ([ set] x  X, Φ x).
583
  Proof. rewrite /big_opS. apply _. Qed.
584
End gset.
Robbert Krebbers's avatar
Robbert Krebbers committed
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624


(** ** Big ops over finite multisets *)
Section gmultiset.
  Context `{Countable A}.
  Implicit Types X : gmultiset A.
  Implicit Types Φ : A  uPred M.

  Lemma big_sepMS_mono Φ Ψ X Y :
    Y  X  ( x, x  Y  Φ x  Ψ x) 
    ([ mset] x  X, Φ x)  [ mset] x  Y, Ψ x.
  Proof.
    intros HX HΦ. trans ([ mset] x  Y, Φ x)%I.
    - apply uPred_included. apply: big_op_contains.
      by apply fmap_contains, gmultiset_elements_contains.
    - apply big_opMS_forall; apply _ || auto.
  Qed.
  Lemma big_sepMS_proper Φ Ψ X :
    ( x, x  X  Φ x  Ψ x) 
    ([ mset] x  X, Φ x)  ([ mset] x  X, Ψ x).
  Proof. apply: big_opMS_proper. Qed.

  Global Instance big_sepMS_mono' X :
     Proper (pointwise_relation _ () ==> ()) (big_opMS (M:=uPredUR M) X).
  Proof. intros f g Hf. apply big_opMS_forall; apply _ || intros; apply Hf. Qed.

  Lemma big_sepMS_empty Φ : ([ mset] x  , Φ x)  True.
  Proof. by rewrite big_opMS_empty. Qed.

  Lemma big_sepMS_union Φ X Y :
    ([ mset] y  X  Y, Φ y)  ([ mset] y  X, Φ y)  [ mset] y  Y, Φ y.
  Proof. apply: big_opMS_union. Qed.

  Lemma big_sepMS_delete Φ X x :
    x  X  ([ mset] y  X, Φ y)  Φ x  [ mset] y  X  {[ x ]}, Φ y.
  Proof. apply: big_opMS_delete. Qed.

  Lemma big_sepMS_elem_of Φ X x : x  X  ([ mset] y  X, Φ y)  Φ x.
  Proof. intros. apply uPred_included. by apply: big_opMS_elem_of. Qed. 

625
626
627
628
629
630
631
  Lemma big_sepMS_elem_of_acc Φ X x :
    x  X 
    ([ mset] y  X, Φ y)  Φ x  (Φ x - ([ mset] y  X, Φ y)).
  Proof.
    intros. rewrite big_sepMS_delete //. by apply sep_mono_r, wand_intro_l.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
632
633
634
635
636
637
638
  Lemma big_sepMS_singleton Φ x : ([ mset] y  {[ x ]}, Φ y)  Φ x.
  Proof. apply: big_opMS_singleton. Qed.

  Lemma big_sepMS_sepMS Φ Ψ X :
    ([ mset] y  X, Φ y  Ψ y)  ([ mset] y  X, Φ y)  ([ mset] y  X, Ψ y).
  Proof. apply: big_opMS_opMS. Qed.

639
640
641
642
  Lemma big_sepMS_and Φ Ψ X :
    ([ mset] y  X, Φ y  Ψ y)  ([ mset] y  X, Φ y)  ([ mset] y  X, Ψ y).
  Proof. auto using big_sepMS_mono with I. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
643
644
645
  Lemma big_sepMS_later Φ X :  ([ mset] y  X, Φ y)  ([ mset] y  X,  Φ y).
  Proof. apply (big_opMS_commute _). Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
646
647
648
649
  Lemma big_sepMS_laterN Φ n X :
    ^n ([ mset] y  X, Φ y)  ([ mset] y  X, ^n Φ y).
  Proof. apply (big_opMS_commute _). Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
  Lemma big_sepMS_always Φ X :  ([ mset] y  X, Φ y)  ([ mset] y  X,  Φ y).
  Proof. apply (big_opMS_commute _). Qed.

  Lemma big_sepMS_always_if q Φ X :
    ?q ([ mset] y  X, Φ y)  ([ mset] y  X, ?q Φ y).
  Proof. apply (big_opMS_commute _). Qed.

  Global Instance big_sepMS_empty_persistent Φ : PersistentP ([ mset] x  , Φ x).
  Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
  Global Instance big_sepMS_persistent Φ X :
    ( x, PersistentP (Φ x))  PersistentP ([ mset] x  X, Φ x).
  Proof. rewrite /big_opMS. apply _. Qed.
  Global Instance big_sepMS_nil_timeless Φ : TimelessP ([ mset] x  , Φ x).
  Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
  Global Instance big_sepMS_timeless Φ X :
    ( x, TimelessP (Φ x))  TimelessP ([ mset] x  X, Φ x).
  Proof. rewrite /big_opMS. apply _. Qed.
End gmultiset.
668
End big_op.