cmra_big_op.v 19.9 KB
 Robbert Krebbers committed Mar 21, 2016 1 ``````From iris.algebra Require Export cmra list. `````` Robbert Krebbers committed Sep 28, 2016 2 ``````From iris.prelude Require Import functions gmap. `````` Robbert Krebbers committed Feb 01, 2016 3 `````` `````` Robbert Krebbers committed Sep 28, 2016 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 ``````(** The operator [ [⋅] Ps ] folds [⋅] over the list [Ps]. This operator is not a quantifier, so it binds strongly. Apart from that, we define the following big operators with binders build in: - The operator [ [⋅ list] k ↦ x ∈ l, P ] folds over a list [l]. The binder [x] refers to each element at index [k]. - The operator [ [⋅ map] k ↦ x ∈ m, P ] folds over a map [m]. The binder [x] refers to each element at index [k]. - The operator [ [⋅ set] x ∈ X, P ] folds over a set [m]. The binder [x] refers to each element. Since these big operators are like quantifiers, they have the same precedence as [∀] and [∃]. *) (** * Big ops over lists *) (* This is the basic building block for other big ops *) Fixpoint big_op {M : ucmraT} (xs : list M) : M := `````` Robbert Krebbers committed Feb 01, 2016 22 `````` match xs with [] => ∅ | x :: xs => x ⋅ big_op xs end. `````` Robbert Krebbers committed May 27, 2016 23 24 ``````Arguments big_op _ !_ /. Instance: Params (@big_op) 1. `````` Robbert Krebbers committed Sep 28, 2016 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 ``````Notation "'[⋅]' xs" := (big_op xs) (at level 20) : C_scope. (** * Other big ops *) Definition big_opL {M : ucmraT} {A} (l : list A) (f : nat → A → M) : M := [⋅] (imap f l). Instance: Params (@big_opL) 2. Typeclasses Opaque big_opL. Notation "'[⋅' 'list' ] k ↦ x ∈ l , P" := (big_opL l (λ k x, P)) (at level 200, l at level 10, k, x at level 1, right associativity, format "[⋅ list ] k ↦ x ∈ l , P") : C_scope. Notation "'[⋅' 'list' ] x ∈ l , P" := (big_opL l (λ _ x, P)) (at level 200, l at level 10, x at level 1, right associativity, format "[⋅ list ] x ∈ l , P") : C_scope. Definition big_opM {M : ucmraT} `{Countable K} {A} (m : gmap K A) (f : K → A → M) : M := [⋅] (curry f <\$> map_to_list m). Instance: Params (@big_opM) 6. Typeclasses Opaque big_opM. Notation "'[⋅' 'map' ] k ↦ x ∈ m , P" := (big_opM m (λ k x, P)) (at level 200, m at level 10, k, x at level 1, right associativity, format "[⋅ map ] k ↦ x ∈ m , P") : C_scope. `````` Robbert Krebbers committed Sep 28, 2016 47 48 49 ``````Notation "'[⋅' 'map' ] x ∈ m , P" := (big_opM m (λ _ x, P)) (at level 200, m at level 10, x at level 1, right associativity, format "[⋅ map ] x ∈ m , P") : C_scope. `````` Robbert Krebbers committed Sep 28, 2016 50 51 52 53 54 55 56 57 `````` Definition big_opS {M : ucmraT} `{Countable A} (X : gset A) (f : A → M) : M := [⋅] (f <\$> elements X). Instance: Params (@big_opS) 5. Typeclasses Opaque big_opS. Notation "'[⋅' 'set' ] x ∈ X , P" := (big_opS X (λ x, P)) (at level 200, X at level 10, x at level 1, right associativity, format "[⋅ set ] x ∈ X , P") : C_scope. `````` Robbert Krebbers committed Feb 01, 2016 58 59 60 `````` (** * Properties about big ops *) Section big_op. `````` Robbert Krebbers committed Sep 28, 2016 61 62 ``````Context {M : ucmraT}. Implicit Types xs : list M. `````` Robbert Krebbers committed Feb 01, 2016 63 64 `````` (** * Big ops *) `````` Robbert Krebbers committed Sep 28, 2016 65 66 67 68 69 ``````Lemma big_op_Forall2 R : Reflexive R → Proper (R ==> R ==> R) (@op M _) → Proper (Forall2 R ==> R) (@big_op M). Proof. rewrite /Proper /respectful. induction 3; eauto. Qed. `````` Robbert Krebbers committed Sep 28, 2016 70 ``````Global Instance big_op_ne n : Proper (dist n ==> dist n) (@big_op M). `````` Robbert Krebbers committed Sep 28, 2016 71 ``````Proof. apply big_op_Forall2; apply _. Qed. `````` Robbert Krebbers committed Sep 28, 2016 72 73 74 ``````Global Instance big_op_proper : Proper ((≡) ==> (≡)) (@big_op M) := ne_proper _. Lemma big_op_nil : [⋅] (@nil M) = ∅. `````` Robbert Krebbers committed Feb 01, 2016 75 ``````Proof. done. Qed. `````` Robbert Krebbers committed Sep 28, 2016 76 ``````Lemma big_op_cons x xs : [⋅] (x :: xs) = x ⋅ [⋅] xs. `````` Robbert Krebbers committed Feb 01, 2016 77 ``````Proof. done. Qed. `````` Robbert Krebbers committed Sep 28, 2016 78 79 80 81 82 83 84 85 86 87 ``````Lemma big_op_app xs ys : [⋅] (xs ++ ys) ≡ [⋅] xs ⋅ [⋅] ys. Proof. induction xs as [|x xs IH]; simpl; first by rewrite ?left_id. by rewrite IH assoc. Qed. Lemma big_op_mono xs ys : Forall2 (≼) xs ys → [⋅] xs ≼ [⋅] ys. Proof. induction 1 as [|x y xs ys Hxy ? IH]; simpl; eauto using cmra_mono. Qed. Global Instance big_op_permutation : Proper ((≡ₚ) ==> (≡)) (@big_op M). `````` Robbert Krebbers committed Feb 01, 2016 88 89 ``````Proof. induction 1 as [|x xs1 xs2 ? IH|x y xs|xs1 xs2 xs3]; simpl; auto. `````` Robbert Krebbers committed Feb 17, 2016 90 91 `````` - by rewrite IH. - by rewrite !assoc (comm _ x). `````` Ralf Jung committed Feb 20, 2016 92 `````` - by trans (big_op xs2). `````` Robbert Krebbers committed Feb 01, 2016 93 ``````Qed. `````` Robbert Krebbers committed Sep 28, 2016 94 95 `````` Lemma big_op_contains xs ys : xs `contains` ys → [⋅] xs ≼ [⋅] ys. `````` Robbert Krebbers committed Feb 01, 2016 96 ``````Proof. `````` Robbert Krebbers committed Feb 17, 2016 97 98 `````` intros [xs' ->]%contains_Permutation. rewrite big_op_app; apply cmra_included_l. `````` Robbert Krebbers committed Feb 01, 2016 99 ``````Qed. `````` Robbert Krebbers committed Sep 28, 2016 100 101 `````` Lemma big_op_delete xs i x : xs !! i = Some x → x ⋅ [⋅] delete i xs ≡ [⋅] xs. `````` Robbert Krebbers committed Feb 01, 2016 102 103 ``````Proof. by intros; rewrite {2}(delete_Permutation xs i x). Qed. `````` Robbert Krebbers committed Sep 28, 2016 104 ``````Lemma big_sep_elem_of xs x : x ∈ xs → x ≼ [⋅] xs. `````` Robbert Krebbers committed Feb 01, 2016 105 ``````Proof. `````` Robbert Krebbers committed Sep 28, 2016 106 107 `````` intros [i ?]%elem_of_list_lookup. rewrite -big_op_delete //. apply cmra_included_l. `````` Robbert Krebbers committed Feb 01, 2016 108 ``````Qed. `````` Robbert Krebbers committed Sep 28, 2016 109 110 111 112 113 114 115 `````` (** ** Big ops over lists *) Section list. Context {A : Type}. Implicit Types l : list A. Implicit Types f g : nat → A → M. `````` Robbert Krebbers committed Sep 28, 2016 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 `````` Lemma big_opL_nil f : ([⋅ list] k↦y ∈ nil, f k y) = ∅. Proof. done. Qed. Lemma big_opL_cons f x l : ([⋅ list] k↦y ∈ x :: l, f k y) = f 0 x ⋅ [⋅ list] k↦y ∈ l, f (S k) y. Proof. by rewrite /big_opL imap_cons. Qed. Lemma big_opL_singleton f x : ([⋅ list] k↦y ∈ [x], f k y) ≡ f 0 x. Proof. by rewrite big_opL_cons big_opL_nil right_id. Qed. Lemma big_opL_app f l1 l2 : ([⋅ list] k↦y ∈ l1 ++ l2, f k y) ≡ ([⋅ list] k↦y ∈ l1, f k y) ⋅ ([⋅ list] k↦y ∈ l2, f (length l1 + k) y). Proof. by rewrite /big_opL imap_app big_op_app. Qed. Lemma big_opL_forall R f g l : Reflexive R → Proper (R ==> R ==> R) (@op M _) → (∀ k y, l !! k = Some y → R (f k y) (g k y)) → R ([⋅ list] k ↦ y ∈ l, f k y) ([⋅ list] k ↦ y ∈ l, g k y). Proof. intros ? Hop. revert f g. induction l as [|x l IH]=> f g Hf; [done|]. rewrite !big_opL_cons. apply Hop; eauto. Qed. `````` Robbert Krebbers committed Sep 28, 2016 137 138 139 `````` Lemma big_opL_mono f g l : (∀ k y, l !! k = Some y → f k y ≼ g k y) → ([⋅ list] k ↦ y ∈ l, f k y) ≼ [⋅ list] k ↦ y ∈ l, g k y. `````` Robbert Krebbers committed Sep 28, 2016 140 `````` Proof. apply big_opL_forall; apply _. Qed. `````` Robbert Krebbers committed Sep 28, 2016 141 142 143 `````` Lemma big_opL_proper f g l : (∀ k y, l !! k = Some y → f k y ≡ g k y) → ([⋅ list] k ↦ y ∈ l, f k y) ≡ ([⋅ list] k ↦ y ∈ l, g k y). `````` Robbert Krebbers committed Sep 28, 2016 144 `````` Proof. apply big_opL_forall; apply _. Qed. `````` Robbert Krebbers committed Sep 28, 2016 145 146 147 148 `````` Global Instance big_opL_ne l n : Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n)) (big_opL (M:=M) l). `````` Robbert Krebbers committed Sep 28, 2016 149 `````` Proof. intros f g Hf. apply big_opL_forall; apply _ || intros; apply Hf. Qed. `````` Robbert Krebbers committed Sep 28, 2016 150 151 152 `````` Global Instance big_opL_proper' l : Proper (pointwise_relation _ (pointwise_relation _ (≡)) ==> (≡)) (big_opL (M:=M) l). `````` Robbert Krebbers committed Sep 28, 2016 153 `````` Proof. intros f g Hf. apply big_opL_forall; apply _ || intros; apply Hf. Qed. `````` Robbert Krebbers committed Sep 28, 2016 154 155 156 `````` Global Instance big_opL_mono' l : Proper (pointwise_relation _ (pointwise_relation _ (≼)) ==> (≼)) (big_opL (M:=M) l). `````` Robbert Krebbers committed Sep 28, 2016 157 `````` Proof. intros f g Hf. apply big_opL_forall; apply _ || intros; apply Hf. Qed. `````` Robbert Krebbers committed Sep 28, 2016 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 `````` Lemma big_opL_lookup f l i x : l !! i = Some x → f i x ≼ [⋅ list] k↦y ∈ l, f k y. Proof. intros. rewrite -(take_drop_middle l i x) // big_opL_app big_opL_cons. rewrite Nat.add_0_r take_length_le; eauto using lookup_lt_Some, Nat.lt_le_incl. eapply transitivity, cmra_included_r; eauto using cmra_included_l. Qed. Lemma big_opL_elem_of (f : A → M) l x : x ∈ l → f x ≼ [⋅ list] y ∈ l, f y. Proof. intros [i ?]%elem_of_list_lookup; eauto using (big_opL_lookup (λ _, f)). Qed. Lemma big_opL_fmap {B} (h : A → B) (f : nat → B → M) l : ([⋅ list] k↦y ∈ h <\$> l, f k y) ≡ ([⋅ list] k↦y ∈ l, f k (h y)). Proof. by rewrite /big_opL imap_fmap. Qed. Lemma big_opL_opL f g l : ([⋅ list] k↦x ∈ l, f k x ⋅ g k x) ≡ ([⋅ list] k↦x ∈ l, f k x) ⋅ ([⋅ list] k↦x ∈ l, g k x). Proof. revert f g; induction l as [|x l IH]=> f g. { by rewrite !big_opL_nil left_id. } rewrite !big_opL_cons IH. by rewrite -!assoc (assoc _ (g _ _)) [(g _ _ ⋅ _)]comm -!assoc. Qed. End list. (** ** Big ops over finite maps *) Section gmap. Context `{Countable K} {A : Type}. Implicit Types m : gmap K A. Implicit Types f g : K → A → M. `````` Robbert Krebbers committed Sep 28, 2016 193 194 195 196 197 198 199 200 201 `````` Lemma big_opM_forall R f g m : Reflexive R → Proper (R ==> R ==> R) (@op M _) → (∀ k x, m !! k = Some x → R (f k x) (g k x)) → R ([⋅ map] k ↦ x ∈ m, f k x) ([⋅ map] k ↦ x ∈ m, g k x). Proof. intros ?? Hf. apply (big_op_Forall2 R _ _), Forall2_fmap, Forall_Forall2. apply Forall_forall=> -[i x] ? /=. by apply Hf, elem_of_map_to_list. Qed. `````` Robbert Krebbers committed Sep 28, 2016 202 203 204 205 `````` Lemma big_opM_mono f g m1 m2 : m1 ⊆ m2 → (∀ k x, m2 !! k = Some x → f k x ≼ g k x) → ([⋅ map] k ↦ x ∈ m1, f k x) ≼ [⋅ map] k ↦ x ∈ m2, g k x. Proof. `````` Robbert Krebbers committed Sep 28, 2016 206 `````` intros Hm Hf. trans ([⋅ map] k↦x ∈ m2, f k x). `````` Robbert Krebbers committed Sep 28, 2016 207 `````` - by apply big_op_contains, fmap_contains, map_to_list_contains. `````` Robbert Krebbers committed Sep 28, 2016 208 `````` - apply big_opM_forall; apply _ || auto. `````` Robbert Krebbers committed Sep 28, 2016 209 210 211 212 `````` Qed. Lemma big_opM_proper f g m : (∀ k x, m !! k = Some x → f k x ≡ g k x) → ([⋅ map] k ↦ x ∈ m, f k x) ≡ ([⋅ map] k ↦ x ∈ m, g k x). `````` Robbert Krebbers committed Sep 28, 2016 213 `````` Proof. apply big_opM_forall; apply _. Qed. `````` Robbert Krebbers committed Sep 28, 2016 214 215 216 217 `````` Global Instance big_opM_ne m n : Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n)) (big_opM (M:=M) m). `````` Robbert Krebbers committed Sep 28, 2016 218 `````` Proof. intros f g Hf. apply big_opM_forall; apply _ || intros; apply Hf. Qed. `````` Robbert Krebbers committed Sep 28, 2016 219 220 221 `````` Global Instance big_opM_proper' m : Proper (pointwise_relation _ (pointwise_relation _ (≡)) ==> (≡)) (big_opM (M:=M) m). `````` Robbert Krebbers committed Sep 28, 2016 222 `````` Proof. intros f g Hf. apply big_opM_forall; apply _ || intros; apply Hf. Qed. `````` Robbert Krebbers committed Sep 28, 2016 223 224 225 `````` Global Instance big_opM_mono' m : Proper (pointwise_relation _ (pointwise_relation _ (≼)) ==> (≼)) (big_opM (M:=M) m). `````` Robbert Krebbers committed Sep 28, 2016 226 `````` Proof. intros f g Hf. apply big_opM_forall; apply _ || intros; apply Hf. Qed. `````` Robbert Krebbers committed Sep 28, 2016 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 `````` Lemma big_opM_empty f : ([⋅ map] k↦x ∈ ∅, f k x) = ∅. Proof. by rewrite /big_opM map_to_list_empty. Qed. Lemma big_opM_insert f m i x : m !! i = None → ([⋅ map] k↦y ∈ <[i:=x]> m, f k y) ≡ f i x ⋅ [⋅ map] k↦y ∈ m, f k y. Proof. intros ?. by rewrite /big_opM map_to_list_insert. Qed. Lemma big_opM_delete f m i x : m !! i = Some x → ([⋅ map] k↦y ∈ m, f k y) ≡ f i x ⋅ [⋅ map] k↦y ∈ delete i m, f k y. Proof. intros. rewrite -big_opM_insert ?lookup_delete //. by rewrite insert_delete insert_id. Qed. Lemma big_opM_lookup f m i x : m !! i = Some x → f i x ≼ [⋅ map] k↦y ∈ m, f k y. Proof. intros. rewrite big_opM_delete //. apply cmra_included_l. Qed. Lemma big_opM_singleton f i x : ([⋅ map] k↦y ∈ {[i:=x]}, f k y) ≡ f i x. Proof. rewrite -insert_empty big_opM_insert/=; last auto using lookup_empty. by rewrite big_opM_empty right_id. Qed. Lemma big_opM_fmap {B} (h : A → B) (f : K → B → M) m : ([⋅ map] k↦y ∈ h <\$> m, f k y) ≡ ([⋅ map] k↦y ∈ m, f k (h y)). Proof. rewrite /big_opM map_to_list_fmap -list_fmap_compose. f_equiv; apply reflexive_eq, list_fmap_ext. by intros []. done. Qed. Lemma big_opM_insert_override (f : K → M) m i x y : m !! i = Some x → ([⋅ map] k↦_ ∈ <[i:=y]> m, f k) ≡ ([⋅ map] k↦_ ∈ m, f k). Proof. intros. rewrite -insert_delete big_opM_insert ?lookup_delete //. by rewrite -big_opM_delete. Qed. Lemma big_opM_fn_insert {B} (g : K → A → B → M) (f : K → B) m i (x : A) b : m !! i = None → ([⋅ map] k↦y ∈ <[i:=x]> m, g k y (<[i:=b]> f k)) ≡ (g i x b ⋅ [⋅ map] k↦y ∈ m, g k y (f k)). Proof. intros. rewrite big_opM_insert // fn_lookup_insert. apply cmra_op_proper', big_opM_proper; auto=> k y ?. by rewrite fn_lookup_insert_ne; last set_solver. Qed. Lemma big_opM_fn_insert' (f : K → M) m i x P : m !! i = None → ([⋅ map] k↦y ∈ <[i:=x]> m, <[i:=P]> f k) ≡ (P ⋅ [⋅ map] k↦y ∈ m, f k). Proof. apply (big_opM_fn_insert (λ _ _, id)). Qed. Lemma big_opM_opM f g m : ([⋅ map] k↦x ∈ m, f k x ⋅ g k x) ≡ ([⋅ map] k↦x ∈ m, f k x) ⋅ ([⋅ map] k↦x ∈ m, g k x). Proof. rewrite /big_opM. induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?right_id //. by rewrite IH -!assoc (assoc _ (g _ _)) [(g _ _ ⋅ _)]comm -!assoc. Qed. End gmap. (** ** Big ops over finite sets *) Section gset. Context `{Countable A}. Implicit Types X : gset A. Implicit Types f : A → M. `````` Robbert Krebbers committed Sep 28, 2016 300 301 302 303 304 305 306 307 308 `````` Lemma big_opS_forall R f g X : Reflexive R → Proper (R ==> R ==> R) (@op M _) → (∀ x, x ∈ X → R (f x) (g x)) → R ([⋅ set] x ∈ X, f x) ([⋅ set] x ∈ X, g x). Proof. intros ?? Hf. apply (big_op_Forall2 R _ _), Forall2_fmap, Forall_Forall2. apply Forall_forall=> x ? /=. by apply Hf, elem_of_elements. Qed. `````` Robbert Krebbers committed Sep 28, 2016 309 310 311 312 313 314 `````` Lemma big_opS_mono f g X Y : X ⊆ Y → (∀ x, x ∈ Y → f x ≼ g x) → ([⋅ set] x ∈ X, f x) ≼ [⋅ set] x ∈ Y, g x. Proof. intros HX Hf. trans ([⋅ set] x ∈ Y, f x). - by apply big_op_contains, fmap_contains, elements_contains. `````` Robbert Krebbers committed Sep 28, 2016 315 `````` - apply big_opS_forall; apply _ || auto. `````` Robbert Krebbers committed Sep 28, 2016 316 317 318 319 320 321 322 `````` Qed. Lemma big_opS_proper f g X Y : X ≡ Y → (∀ x, x ∈ X → x ∈ Y → f x ≡ g x) → ([⋅ set] x ∈ X, f x) ≡ ([⋅ set] x ∈ Y, g x). Proof. intros HX Hf. trans ([⋅ set] x ∈ Y, f x). - apply big_op_permutation. by rewrite HX. `````` Robbert Krebbers committed Sep 28, 2016 323 `````` - apply big_opS_forall; try apply _ || set_solver. `````` Robbert Krebbers committed Sep 28, 2016 324 325 326 327 `````` Qed. Lemma big_opS_ne X n : Proper (pointwise_relation _ (dist n) ==> dist n) (big_opS (M:=M) X). `````` Robbert Krebbers committed Sep 28, 2016 328 `````` Proof. intros f g Hf. apply big_opS_forall; apply _ || intros; apply Hf. Qed. `````` Robbert Krebbers committed Sep 28, 2016 329 330 `````` Lemma big_opS_proper' X : Proper (pointwise_relation _ (≡) ==> (≡)) (big_opS (M:=M) X). `````` Robbert Krebbers committed Sep 28, 2016 331 `````` Proof. intros f g Hf. apply big_opS_forall; apply _ || intros; apply Hf. Qed. `````` Robbert Krebbers committed Sep 28, 2016 332 333 `````` Lemma big_opS_mono' X : Proper (pointwise_relation _ (≼) ==> (≼)) (big_opS (M:=M) X). `````` Robbert Krebbers committed Sep 28, 2016 334 `````` Proof. intros f g Hf. apply big_opS_forall; apply _ || intros; apply Hf. Qed. `````` Robbert Krebbers committed Sep 28, 2016 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 `````` Lemma big_opS_empty f : ([⋅ set] x ∈ ∅, f x) = ∅. Proof. by rewrite /big_opS elements_empty. Qed. Lemma big_opS_insert f X x : x ∉ X → ([⋅ set] y ∈ {[ x ]} ∪ X, f y) ≡ (f x ⋅ [⋅ set] y ∈ X, f y). Proof. intros. by rewrite /big_opS elements_union_singleton. Qed. Lemma big_opS_fn_insert {B} (f : A → B → M) h X x b : x ∉ X → ([⋅ set] y ∈ {[ x ]} ∪ X, f y (<[x:=b]> h y)) ≡ (f x b ⋅ [⋅ set] y ∈ X, f y (h y)). Proof. intros. rewrite big_opS_insert // fn_lookup_insert. apply cmra_op_proper', big_opS_proper; auto=> y ??. by rewrite fn_lookup_insert_ne; last set_solver. Qed. Lemma big_opS_fn_insert' f X x P : x ∉ X → ([⋅ set] y ∈ {[ x ]} ∪ X, <[x:=P]> f y) ≡ (P ⋅ [⋅ set] y ∈ X, f y). Proof. apply (big_opS_fn_insert (λ y, id)). Qed. Lemma big_opS_delete f X x : x ∈ X → ([⋅ set] y ∈ X, f y) ≡ f x ⋅ [⋅ set] y ∈ X ∖ {[ x ]}, f y. Proof. intros. rewrite -big_opS_insert; last set_solver. by rewrite -union_difference_L; last set_solver. Qed. Lemma big_opS_elem_of f X x : x ∈ X → f x ≼ [⋅ set] y ∈ X, f y. Proof. intros. rewrite big_opS_delete //. apply cmra_included_l. Qed. Lemma big_opS_singleton f x : ([⋅ set] y ∈ {[ x ]}, f y) ≡ f x. Proof. intros. by rewrite /big_opS elements_singleton /= right_id. Qed. Lemma big_opS_opS f g X : ([⋅ set] y ∈ X, f y ⋅ g y) ≡ ([⋅ set] y ∈ X, f y) ⋅ ([⋅ set] y ∈ X, g y). Proof. rewrite /big_opS. induction (elements X) as [|x l IH]; csimpl; first by rewrite ?right_id. by rewrite IH -!assoc (assoc _ (g _)) [(g _ ⋅ _)]comm -!assoc. Qed. End gset. `````` Robbert Krebbers committed Feb 01, 2016 376 ``````End big_op. `````` Robbert Krebbers committed Sep 28, 2016 377 `````` `````` Robbert Krebbers committed Oct 02, 2016 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 ``````(** Option *) Lemma big_opL_None {M : cmraT} {A} (f : nat → A → option M) l : ([⋅ list] k↦x ∈ l, f k x) = None ↔ ∀ k x, l !! k = Some x → f k x = None. Proof. revert f. induction l as [|x l IH]=> f //=. rewrite big_opL_cons op_None IH. split. - intros [??] [|k] y ?; naive_solver. - intros Hl. split. by apply (Hl 0). intros k. apply (Hl (S k)). Qed. Lemma big_opM_None {M : cmraT} `{Countable K} {A} (f : K → A → option M) m : ([⋅ map] k↦x ∈ m, f k x) = None ↔ ∀ k x, m !! k = Some x → f k x = None. Proof. induction m as [|i x m ? IH] using map_ind=> //=. rewrite -equiv_None big_opM_insert // equiv_None op_None IH. split. { intros [??] k y. rewrite lookup_insert_Some; naive_solver. } intros Hm; split. - apply (Hm i). by simplify_map_eq. - intros k y ?. apply (Hm k). by simplify_map_eq. Qed. Lemma big_opS_None {M : cmraT} `{Countable A} (f : A → option M) X : ([⋅ set] x ∈ X, f x) = None ↔ ∀ x, x ∈ X → f x = None. Proof. induction X as [|x X ? IH] using collection_ind_L; [done|]. rewrite -equiv_None big_opS_insert // equiv_None op_None IH. set_solver. Qed. (** Commuting with respect to homomorphisms *) `````` Robbert Krebbers committed Sep 28, 2016 405 ``````Lemma big_opL_commute {M1 M2 : ucmraT} {A} (h : M1 → M2) `````` Robbert Krebbers committed Sep 28, 2016 406 `````` `{!UCMRAHomomorphism h} (f : nat → A → M1) l : `````` Robbert Krebbers committed Sep 28, 2016 407 408 `````` h ([⋅ list] k↦x ∈ l, f k x) ≡ ([⋅ list] k↦x ∈ l, h (f k x)). Proof. `````` Robbert Krebbers committed Sep 28, 2016 409 410 411 `````` revert f. induction l as [|x l IH]=> f. - by rewrite !big_opL_nil ucmra_homomorphism_unit. - by rewrite !big_opL_cons cmra_homomorphism -IH. `````` Robbert Krebbers committed Sep 28, 2016 412 413 ``````Qed. Lemma big_opL_commute1 {M1 M2 : ucmraT} {A} (h : M1 → M2) `````` Robbert Krebbers committed Sep 28, 2016 414 415 `````` `{!CMRAHomomorphism h} (f : nat → A → M1) l : l ≠ [] → h ([⋅ list] k↦x ∈ l, f k x) ≡ ([⋅ list] k↦x ∈ l, h (f k x)). `````` Robbert Krebbers committed Sep 28, 2016 416 ``````Proof. `````` Robbert Krebbers committed Sep 28, 2016 417 `````` intros ?. revert f. induction l as [|x [|x' l'] IH]=> f //. `````` Robbert Krebbers committed Sep 28, 2016 418 `````` - by rewrite !big_opL_singleton. `````` Robbert Krebbers committed Sep 28, 2016 419 `````` - by rewrite !(big_opL_cons _ x) cmra_homomorphism -IH. `````` Robbert Krebbers committed Sep 28, 2016 420 421 422 ``````Qed. Lemma big_opM_commute {M1 M2 : ucmraT} `{Countable K} {A} (h : M1 → M2) `````` Robbert Krebbers committed Sep 28, 2016 423 `````` `{!UCMRAHomomorphism h} (f : K → A → M1) m : `````` Robbert Krebbers committed Sep 28, 2016 424 425 `````` h ([⋅ map] k↦x ∈ m, f k x) ≡ ([⋅ map] k↦x ∈ m, h (f k x)). Proof. `````` Robbert Krebbers committed Sep 28, 2016 426 427 428 `````` intros. induction m as [|i x m ? IH] using map_ind. - by rewrite !big_opM_empty ucmra_homomorphism_unit. - by rewrite !big_opM_insert // cmra_homomorphism -IH. `````` Robbert Krebbers committed Sep 28, 2016 429 430 ``````Qed. Lemma big_opM_commute1 {M1 M2 : ucmraT} `{Countable K} {A} (h : M1 → M2) `````` Robbert Krebbers committed Sep 28, 2016 431 432 `````` `{!CMRAHomomorphism h} (f : K → A → M1) m : m ≠ ∅ → h ([⋅ map] k↦x ∈ m, f k x) ≡ ([⋅ map] k↦x ∈ m, h (f k x)). `````` Robbert Krebbers committed Sep 28, 2016 433 ``````Proof. `````` Robbert Krebbers committed Sep 28, 2016 434 435 436 437 `````` intros. induction m as [|i x m ? IH] using map_ind; [done|]. destruct (decide (m = ∅)) as [->|]. - by rewrite !big_opM_insert // !big_opM_empty !right_id. - by rewrite !big_opM_insert // cmra_homomorphism -IH //. `````` Robbert Krebbers committed Sep 28, 2016 438 439 ``````Qed. `````` Robbert Krebbers committed Sep 28, 2016 440 441 ``````Lemma big_opS_commute {M1 M2 : ucmraT} `{Countable A} (h : M1 → M2) `{!UCMRAHomomorphism h} (f : A → M1) X : `````` Robbert Krebbers committed Sep 28, 2016 442 443 `````` h ([⋅ set] x ∈ X, f x) ≡ ([⋅ set] x ∈ X, h (f x)). Proof. `````` Robbert Krebbers committed Sep 28, 2016 444 445 446 `````` intros. induction X as [|x X ? IH] using collection_ind_L. - by rewrite !big_opS_empty ucmra_homomorphism_unit. - by rewrite !big_opS_insert // cmra_homomorphism -IH. `````` Robbert Krebbers committed Sep 28, 2016 447 ``````Qed. `````` Robbert Krebbers committed Sep 28, 2016 448 449 450 ``````Lemma big_opS_commute1 {M1 M2 : ucmraT} `{Countable A} (h : M1 → M2) `{!CMRAHomomorphism h} (f : A → M1) X : X ≠ ∅ → h ([⋅ set] x ∈ X, f x) ≡ ([⋅ set] x ∈ X, h (f x)). `````` Robbert Krebbers committed Sep 28, 2016 451 ``````Proof. `````` Robbert Krebbers committed Sep 28, 2016 452 453 454 455 `````` intros. induction X as [|x X ? IH] using collection_ind_L; [done|]. destruct (decide (X = ∅)) as [->|]. - by rewrite !big_opS_insert // !big_opS_empty !right_id. - by rewrite !big_opS_insert // cmra_homomorphism -IH //. `````` Robbert Krebbers committed Sep 28, 2016 456 ``````Qed. `````` Robbert Krebbers committed Sep 28, 2016 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 `````` Lemma big_opL_commute_L {M1 M2 : ucmraT} `{!LeibnizEquiv M2} {A} (h : M1 → M2) `{!UCMRAHomomorphism h} (f : nat → A → M1) l : h ([⋅ list] k↦x ∈ l, f k x) = ([⋅ list] k↦x ∈ l, h (f k x)). Proof. unfold_leibniz. by apply big_opL_commute. Qed. Lemma big_opL_commute1_L {M1 M2 : ucmraT} `{!LeibnizEquiv M2} {A} (h : M1 → M2) `{!CMRAHomomorphism h} (f : nat → A → M1) l : l ≠ [] → h ([⋅ list] k↦x ∈ l, f k x) = ([⋅ list] k↦x ∈ l, h (f k x)). Proof. unfold_leibniz. by apply big_opL_commute1. Qed. Lemma big_opM_commute_L {M1 M2 : ucmraT} `{!LeibnizEquiv M2, Countable K} {A} (h : M1 → M2) `{!UCMRAHomomorphism h} (f : K → A → M1) m : h ([⋅ map] k↦x ∈ m, f k x) = ([⋅ map] k↦x ∈ m, h (f k x)). Proof. unfold_leibniz. by apply big_opM_commute. Qed. Lemma big_opM_commute1_L {M1 M2 : ucmraT} `{!LeibnizEquiv M2, Countable K} {A} (h : M1 → M2) `{!CMRAHomomorphism h} (f : K → A → M1) m : m ≠ ∅ → h ([⋅ map] k↦x ∈ m, f k x) = ([⋅ map] k↦x ∈ m, h (f k x)). Proof. unfold_leibniz. by apply big_opM_commute1. Qed. Lemma big_opS_commute_L {M1 M2 : ucmraT} `{!LeibnizEquiv M2, Countable A} (h : M1 → M2) `{!UCMRAHomomorphism h} (f : A → M1) X : h ([⋅ set] x ∈ X, f x) = ([⋅ set] x ∈ X, h (f x)). Proof. unfold_leibniz. by apply big_opS_commute. Qed. Lemma big_opS_commute1_L {M1 M2 : ucmraT} `{!LeibnizEquiv M2, Countable A} (h : M1 → M2) `{!CMRAHomomorphism h} (f : A → M1) X : X ≠ ∅ → h ([⋅ set] x ∈ X, f x) = ([⋅ set] x ∈ X, h (f x)). Proof. intros. rewrite <-leibniz_equiv_iff. by apply big_opS_commute1. Qed.``````