Commit 299cc1a2 authored by Robbert's avatar Robbert

Merge branch 'big-op-insert-delete' into 'master'

Add insert delete lemma for big ops over gmap

See merge request iris/iris!420
parents 99d4fcc4 18037263
......@@ -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] ky <[i:=x]> m, f k y) f i x `o` [^o map] ky 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] ky <[i:=x']> m, f k y) ([^o map] ky m, f k y).
......
......@@ -789,6 +789,10 @@ Section map.
([ map] ky m, Φ k y) Φ i x [ map] ky delete i m, Φ k y.
Proof. apply big_opM_delete. Qed.
Lemma big_sepM_insert_delete Φ m i x :
([ map] ky <[i:=x]> m, Φ k y) Φ i x [ map] ky 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] ky m, Φ k y) - [ map] ky <[i:=x]> m, Φ k y.
......@@ -1080,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] ky1;y2 <[i:=x1]>m1; <[i:=x2]>m2, Φ k y1 y2)
Φ i x1 x2 [ map] ky1;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] ky1;y2 m1;m2, Φ k y1 y2)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment