upred_big_op.v 9.53 KB
Newer Older
1
From algebra Require Export upred.
2
From prelude Require Import gmap fin_collections.
3
Import uPred.
4

5
6
(** * Big ops over lists *)
(* These are the basic building blocks for other big ops *)
7
8
9
10
11
12
13
14
Fixpoint uPred_big_and {M} (Ps : list (uPred M)) : uPred M:=
  match Ps with [] => True | P :: Ps => P  uPred_big_and Ps end%I.
Instance: Params (@uPred_big_and) 1.
Notation "'Π∧' Ps" := (uPred_big_and Ps) (at level 20) : uPred_scope.
Fixpoint uPred_big_sep {M} (Ps : list (uPred M)) : uPred M :=
  match Ps with [] => True | P :: Ps => P  uPred_big_sep Ps end%I.
Instance: Params (@uPred_big_sep) 1.
Notation "'Π★' Ps" := (uPred_big_sep Ps) (at level 20) : uPred_scope.
15

16
17
(** * Other big ops *)
(** We use a type class to obtain overloaded notations *)
18
Definition uPred_big_sepM {M} `{Countable K} {A}
19
20
    (m : gmap K A) (Φ : K  A  uPred M) : uPred M :=
  uPred_big_sep (curry Φ <$> map_to_list m).
21
Instance: Params (@uPred_big_sepM) 6.
22
23
Notation "'Π★{map' m } Φ" := (uPred_big_sepM m Φ)
  (at level 20, m at level 10, format "Π★{map  m }  Φ") : uPred_scope.
24

25
Definition uPred_big_sepS {M} `{Countable A}
26
  (X : gset A) (Φ : A  uPred M) : uPred M := uPred_big_sep (Φ <$> elements X).
27
Instance: Params (@uPred_big_sepS) 5.
28
29
Notation "'Π★{set' X } Φ" := (uPred_big_sepS X Φ)
  (at level 20, X at level 10, format "Π★{set  X }  Φ") : uPred_scope.
30
31

(** * Always stability for lists *)
32
33
34
35
36
37
38
39
40
41
Class AlwaysStableL {M} (Ps : list (uPred M)) :=
  always_stableL : Forall AlwaysStable Ps.
Arguments always_stableL {_} _ {_}.

Section big_op.
Context {M : cmraT}.
Implicit Types Ps Qs : list (uPred M).
Implicit Types A : Type.

(* Big ops *)
42
Global Instance big_and_proper : Proper (() ==> ()) (@uPred_big_and M).
43
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
44
Global Instance big_sep_proper : Proper (() ==> ()) (@uPred_big_sep M).
45
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
46
47
48
49
50
51
52
53
54
55
56
57
58

Global Instance big_and_ne n :
  Proper (Forall2 (dist n) ==> dist n) (@uPred_big_and M).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance big_sep_ne n :
  Proper (Forall2 (dist n) ==> dist n) (@uPred_big_sep M).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.

Global Instance big_and_mono' : Proper (Forall2 () ==> ()) (@uPred_big_and M).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance big_sep_mono' : Proper (Forall2 () ==> ()) (@uPred_big_sep M).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.

59
Global Instance big_and_perm : Proper (() ==> ()) (@uPred_big_and M).
60
61
Proof.
  induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
62
63
  - by rewrite IH.
  - by rewrite !assoc (comm _ P).
64
  - etrans; eauto.
65
Qed.
66
Global Instance big_sep_perm : Proper (() ==> ()) (@uPred_big_sep M).
67
68
Proof.
  induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
69
70
  - by rewrite IH.
  - by rewrite !assoc (comm _ P).
71
  - etrans; eauto.
72
Qed.
73

74
Lemma big_and_app Ps Qs : (Π (Ps ++ Qs))%I  (Π Ps  Π Qs)%I.
75
Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
76
Lemma big_sep_app Ps Qs : (Π★ (Ps ++ Qs))%I  (Π★ Ps  Π★ Qs)%I.
77
Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
78
79
80

Lemma big_and_contains Ps Qs : Qs `contains` Ps  (Π Ps)%I  (Π Qs)%I.
Proof.
81
  intros [Ps' ->]%contains_Permutation. by rewrite big_and_app and_elim_l.
82
83
84
Qed.
Lemma big_sep_contains Ps Qs : Qs `contains` Ps  (Π★ Ps)%I  (Π★ Qs)%I.
Proof.
85
  intros [Ps' ->]%contains_Permutation. by rewrite big_sep_app sep_elim_l.
86
87
Qed.

88
Lemma big_sep_and Ps : (Π★ Ps)  (Π Ps).
89
Proof. by induction Ps as [|P Ps IH]; simpl; auto with I. Qed.
90

91
Lemma big_and_elem_of Ps P : P  Ps  (Π Ps)  P.
92
Proof. induction 1; simpl; auto with I. Qed.
93
Lemma big_sep_elem_of Ps P : P  Ps  (Π★ Ps)  P.
94
95
Proof. induction 1; simpl; auto with I. Qed.

96
(* Big ops over finite maps *)
97
98
99
Section gmap.
  Context `{Countable K} {A : Type}.
  Implicit Types m : gmap K A.
100
  Implicit Types Φ Ψ : K  A  uPred M.
101

102
103
104
  Lemma big_sepM_mono Φ Ψ m1 m2 :
    m2  m1  ( x k, m2 !! k = Some x  Φ k x  Ψ k x) 
    (Π★{map m1} Φ)  (Π★{map m2} Ψ).
105
  Proof.
106
    intros HX HΦ. trans (Π★{map m2} Φ)%I.
107
108
    - by apply big_sep_contains, fmap_contains, map_to_list_contains.
    - apply big_sep_mono', Forall2_fmap, Forall2_Forall.
109
      apply Forall_forall=> -[i x] ? /=. by apply HΦ, elem_of_map_to_list.
110
  Qed.
111
112
113
114
115

  Global Instance big_sepM_ne m n :
    Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n))
           (uPred_big_sepM (M:=M) m).
  Proof.
116
117
    intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap.
    apply Forall2_Forall, Forall_true=> -[i x]; apply HΦ.
118
119
120
121
122
  Qed.
  Global Instance big_sepM_proper m :
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
           (uPred_big_sepM (M:=M) m).
  Proof.
123
124
    intros Φ1 Φ2 HΦ; apply equiv_dist=> n.
    apply big_sepM_ne=> k x; apply equiv_dist, HΦ.
125
126
127
128
  Qed.
  Global Instance big_sepM_mono' m :
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
           (uPred_big_sepM (M:=M) m).
129
  Proof. intros Φ1 Φ2 HΦ. apply big_sepM_mono; intros; [done|apply HΦ]. Qed.
130

131
  Lemma big_sepM_empty Φ : (Π★{map } Φ)%I  True%I.
132
  Proof. by rewrite /uPred_big_sepM map_to_list_empty. Qed.
133
134
  Lemma big_sepM_insert Φ (m : gmap K A) i x :
    m !! i = None  (Π★{map <[i:=x]> m} Φ)%I  (Φ i x  Π★{map m} Φ)%I.
135
  Proof. intros ?; by rewrite /uPred_big_sepM map_to_list_insert. Qed.
136
  Lemma big_sepM_singleton Φ i x : (Π★{map {[i := x]}} Φ)%I  (Φ i x)%I.
137
138
139
140
  Proof.
    rewrite -insert_empty big_sepM_insert/=; last auto using lookup_empty.
    by rewrite big_sepM_empty right_id.
  Qed.
141

142
143
  Lemma big_sepM_sepM Φ Ψ m :
    (Π★{map m} (λ i x, Φ i x  Ψ i x))%I  (Π★{map m} Φ  Π★{map m} Ψ)%I.
144
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
145
146
    rewrite /uPred_big_sepM.
    induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?right_id //.
147
    by rewrite IH -!assoc (assoc _ (Ψ _ _)) [(Ψ _ _  _)%I]comm -!assoc.
148
  Qed.
149
  Lemma big_sepM_later Φ m : ( Π★{map m} Φ)%I  (Π★{map m} (λ i x,  Φ i x))%I.
150
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
151
152
153
    rewrite /uPred_big_sepM.
    induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?later_True //.
    by rewrite later_sep IH.
154
  Qed.
155
156
157
158
159
160
End gmap.

(* Big ops over finite sets *)
Section gset.
  Context `{Countable A}.
  Implicit Types X : gset A.
161
  Implicit Types Φ : A  uPred M.
162

163
164
  Lemma big_sepS_mono Φ Ψ X Y :
    Y  X  ( x, x  Y  Φ x  Ψ x)  (Π★{set X} Φ)  (Π★{set Y} Ψ).
165
  Proof.
166
    intros HX HΦ. trans (Π★{set Y} Φ)%I.
167
168
    - by apply big_sep_contains, fmap_contains, elements_contains.
    - apply big_sep_mono', Forall2_fmap, Forall2_Forall.
169
      apply Forall_forall=> x ? /=. by apply HΦ, elem_of_elements.
170
171
172
173
174
  Qed.

  Lemma big_sepS_ne X n :
    Proper (pointwise_relation _ (dist n) ==> dist n) (uPred_big_sepS (M:=M) X).
  Proof.
175
176
    intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap.
    apply Forall2_Forall, Forall_true=> x; apply HΦ.
177
178
179
180
  Qed.
  Lemma big_sepS_proper X :
    Proper (pointwise_relation _ () ==> ()) (uPred_big_sepS (M:=M) X).
  Proof.
181
182
    intros Φ1 Φ2 HΦ; apply equiv_dist=> n.
    apply big_sepS_ne=> x; apply equiv_dist, HΦ.
183
184
185
  Qed.
  Lemma big_sepS_mono' X :
    Proper (pointwise_relation _ () ==> ()) (uPred_big_sepS (M:=M) X).
186
  Proof. intros Φ1 Φ2 HΦ. apply big_sepS_mono; naive_solver. Qed.
187

188
  Lemma big_sepS_empty Φ : (Π★{set } Φ)%I  True%I.
189
  Proof. by rewrite /uPred_big_sepS elements_empty. Qed.
190
191
  Lemma big_sepS_insert Φ X x :
    x  X  (Π★{set {[ x ]}  X} Φ)%I  (Φ x  Π★{set X} Φ)%I.
192
  Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed.
193
194
  Lemma big_sepS_delete Φ X x :
    x  X  (Π★{set X} Φ)%I  (Φ x  Π★{set X  {[ x ]}} Φ)%I.
195
  Proof.
196
197
    intros. rewrite -big_sepS_insert; last set_solver.
    by rewrite -union_difference_L; last set_solver.
198
  Qed.
199
  Lemma big_sepS_singleton Φ x : (Π★{set {[ x ]}} Φ)%I  (Φ x)%I.
200
  Proof. intros. by rewrite /uPred_big_sepS elements_singleton /= right_id. Qed.
201

202
203
  Lemma big_sepS_sepS Φ Ψ X :
    (Π★{set X} (λ x, Φ x  Ψ x))%I  (Π★{set X} Φ  Π★{set X} Ψ)%I.
204
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
205
206
    rewrite /uPred_big_sepS.
    induction (elements X) as [|x l IH]; csimpl; first by rewrite ?right_id.
207
    by rewrite IH -!assoc (assoc _ (Ψ _)) [(Ψ _  _)%I]comm -!assoc.
208
209
  Qed.

210
  Lemma big_sepS_later Φ X : ( Π★{set X} Φ)%I  (Π★{set X} (λ x,  Φ x))%I.
211
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
212
213
214
    rewrite /uPred_big_sepS.
    induction (elements X) as [|x l IH]; csimpl; first by rewrite ?later_True.
    by rewrite later_sep IH.
215
  Qed.
216
End gset.
217

218
219
220
(* Always stable *)
Local Notation AS := AlwaysStable.
Local Notation ASL := AlwaysStableL.
221
Global Instance big_and_always_stable Ps : ASL Ps  AS (Π Ps).
222
Proof. induction 1; apply _. Qed.
223
Global Instance big_sep_always_stable Ps : ASL Ps  AS (Π★ Ps).
224
225
226
227
228
229
230
231
232
233
234
Proof. induction 1; apply _. Qed.

Global Instance nil_always_stable : ASL (@nil (uPred M)).
Proof. constructor. Qed.
Global Instance cons_always_stable P Ps : AS P  ASL Ps  ASL (P :: Ps).
Proof. by constructor. Qed.
Global Instance app_always_stable Ps Ps' : ASL Ps  ASL Ps'  ASL (Ps ++ Ps').
Proof. apply Forall_app_2. Qed.
Global Instance zip_with_always_stable {A B} (f : A  B  uPred M) xs ys :
  ( x y, AS (f x y))  ASL (zip_with f xs ys).
Proof. unfold ASL=> ?; revert ys; induction xs=> -[|??]; constructor; auto. Qed.
235
End big_op.