From 32abe0c0c6cf7c91dbf14f12732ab83eb64b03da Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Mon, 21 Nov 2016 15:22:41 +0100 Subject: [PATCH] Big op over set union. --- algebra/cmra_big_op.v | 10 ++++++++++ base_logic/big_op.v | 5 +++++ 2 files changed, 15 insertions(+) diff --git a/algebra/cmra_big_op.v b/algebra/cmra_big_op.v index f20066f74..4c7517be3 100644 --- a/algebra/cmra_big_op.v +++ b/algebra/cmra_big_op.v @@ -378,6 +378,16 @@ Section gset. 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_union f X Y : + X ⊥ Y → + ([⋅ set] y ∈ X ∪ Y, f y) ≡ ([⋅ set] y ∈ X, f y) ⋅ ([⋅ set] y ∈ Y, f y). + Proof. + intros. induction X as [|x X ? IH] using collection_ind_L. + { by rewrite left_id_L big_opS_empty left_id. } + rewrite -assoc_L !big_opS_insert; [|set_solver..]. + by rewrite -assoc IH; last set_solver. + Qed. + Lemma big_opS_delete f X x : x ∈ X → ([⋅ set] y ∈ X, f y) ≡ f x ⋅ [⋅ set] y ∈ X ∖ {[ x ]}, f y. Proof. diff --git a/base_logic/big_op.v b/base_logic/big_op.v index 40a0a71f2..d5de9ac2c 100644 --- a/base_logic/big_op.v +++ b/base_logic/big_op.v @@ -457,6 +457,11 @@ Section gset. x ∉ X → ([∗ set] y ∈ {[ x ]} ∪ X, <[x:=P]> Φ y) ⊣⊢ (P ∗ [∗ set] y ∈ X, Φ y). Proof. apply: big_opS_fn_insert'. Qed. + 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. + Lemma big_sepS_delete Φ X x : x ∈ X → ([∗ set] y ∈ X, Φ y) ⊣⊢ Φ x ∗ [∗ set] y ∈ X ∖ {[ x ]}, Φ y. Proof. apply: big_opS_delete. Qed. -- GitLab