From b10fd76af7c00ccc3bde3a32b67bdd4ae877c482 Mon Sep 17 00:00:00 2001 From: Simon Friis Vindum Date: Mon, 6 Apr 2020 11:34:05 +0200 Subject: [PATCH 1/4] Add insert delete lemma for big ops over gmap --- theories/algebra/big_op.v | 6 ++++++ theories/bi/big_op.v | 4 ++++ 2 files changed, 10 insertions(+) diff --git a/theories/algebra/big_op.v b/theories/algebra/big_op.v index ef7720273..d7abc596f 100644 --- a/theories/algebra/big_op.v +++ b/theories/algebra/big_op.v @@ -323,6 +323,12 @@ Section gmap. by apply big_opL_proper=> ? [??]. Qed. + Lemma big_opM_insert_delete `{Countable K} {B} (f : K → B → M) (m : gmap K B) i x : + ([^o map] k↦y ∈ <[i:=x]> m, f k y) ≡ f i x `o` [^o map] k↦y ∈ (delete i m), f k y. + Proof. + rewrite -insert_delete big_opM_insert; first done. by rewrite lookup_delete. + Qed. + Lemma big_opM_insert_override (f : K → A → M) m i x x' : m !! i = Some x → f i x ≡ f i x' → ([^o map] k↦y ∈ <[i:=x']> m, f k y) ≡ ([^o map] k↦y ∈ m, f k y). diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v index c274e6a75..93c8c01f6 100644 --- a/theories/bi/big_op.v +++ b/theories/bi/big_op.v @@ -789,6 +789,10 @@ Section map. ([∗ map] k↦y ∈ m, Φ k y) ⊣⊢ Φ i x ∗ [∗ map] k↦y ∈ delete i m, Φ k y. Proof. apply big_opM_delete. Qed. + Lemma big_sepM_insert_delete Φ m i x : + ([∗ map] k↦y ∈ <[i:=x]> m, Φ k y) ⊣⊢ Φ i x ∗ [∗ map] k↦y ∈ (delete i m), Φ k y. + Proof. apply big_opM_insert_delete. Qed. + Lemma big_sepM_insert_2 Φ m i x : TCOr (∀ x, Affine (Φ i x)) (Absorbing (Φ i x)) → Φ i x -∗ ([∗ map] k↦y ∈ m, Φ k y) -∗ [∗ map] k↦y ∈ <[i:=x]> m, Φ k y. -- GitLab From c2f41dc4d14bb51cc437c27f71b3bf4b85aa5b8e Mon Sep 17 00:00:00 2001 From: Simon Friis Vindum Date: Mon, 6 Apr 2020 13:32:01 +0200 Subject: [PATCH 2/4] Remove superfluous parentheses --- theories/bi/big_op.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v index 93c8c01f6..61d0c6c18 100644 --- a/theories/bi/big_op.v +++ b/theories/bi/big_op.v @@ -790,7 +790,7 @@ Section map. Proof. apply big_opM_delete. Qed. Lemma big_sepM_insert_delete Φ m i x : - ([∗ map] k↦y ∈ <[i:=x]> m, Φ k y) ⊣⊢ Φ i x ∗ [∗ map] k↦y ∈ (delete i m), Φ k y. + ([∗ map] k↦y ∈ <[i:=x]> m, Φ k y) ⊣⊢ Φ i x ∗ [∗ map] k↦y ∈ delete i m, Φ k y. Proof. apply big_opM_insert_delete. Qed. Lemma big_sepM_insert_2 Φ m i x : -- GitLab From d89709f30741f9f91d3512fbf21168b67e7d7b6d Mon Sep 17 00:00:00 2001 From: Simon Friis Vindum Date: Mon, 6 Apr 2020 13:33:46 +0200 Subject: [PATCH 3/4] Add insert delete lemma for big_sepM2 --- theories/bi/big_op.v | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v index 61d0c6c18..4c702da91 100644 --- a/theories/bi/big_op.v +++ b/theories/bi/big_op.v @@ -1084,6 +1084,14 @@ Section map2. by rewrite map_lookup_zip_with Hx1 Hx2. Qed. + Lemma big_sepM2_insert_delete Φ m1 m2 i x1 x2 : + ([∗ map] k↦y1;y2 ∈ <[i:=x1]>m1; <[i:=x2]>m2, Φ k y1 y2) + ⊣⊢ Φ i x1 x2 ∗ [∗ map] k↦y1;y2 ∈ delete i m1;delete i m2, Φ k y1 y2. + Proof. + rewrite -(insert_delete m1) -(insert_delete m2). + apply big_sepM2_insert; by rewrite lookup_delete. + Qed. + Lemma big_sepM2_insert_acc Φ m1 m2 i x1 x2 : m1 !! i = Some x1 → m2 !! i = Some x2 → ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2) ⊢ -- GitLab From 8c8b9aa647f8c425948bc4bc9876422a00cf1f13 Mon Sep 17 00:00:00 2001 From: Simon Friis Vindum Date: Mon, 6 Apr 2020 14:59:28 +0200 Subject: [PATCH 4/4] Remove unnecessary --- theories/algebra/big_op.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/algebra/big_op.v b/theories/algebra/big_op.v index d7abc596f..420105441 100644 --- a/theories/algebra/big_op.v +++ b/theories/algebra/big_op.v @@ -324,7 +324,7 @@ Section gmap. Qed. Lemma big_opM_insert_delete `{Countable K} {B} (f : K → B → M) (m : gmap K B) i x : - ([^o map] k↦y ∈ <[i:=x]> m, f k y) ≡ f i x `o` [^o map] k↦y ∈ (delete i m), f k y. + ([^o map] k↦y ∈ <[i:=x]> m, f k y) ≡ f i x `o` [^o map] k↦y ∈ delete i m, f k y. Proof. rewrite -insert_delete big_opM_insert; first done. by rewrite lookup_delete. Qed. -- GitLab