Commit 5fd7dae1 authored by Robbert's avatar Robbert

Merge branch 'bigop_overwrite' into 'master'

A stronger version of `big_sepM_insert_override_{1,2}`.

See merge request iris/iris!166
parents ba2d414a a5b6db8b
......@@ -99,6 +99,7 @@ Changes in Coq:
* A new tactic, `wp_pures`, executes as many pure steps as possible, excluding
steps that would require unlocking subterms. Every impure wp_ tactic executes
this tactic before doing anything else.
* Add `big_sepM_insert_acc`.
## Iris 3.1.0 (released 2017-12-19)
......
......@@ -628,6 +628,17 @@ Section gmap.
rewrite -insert_delete big_sepM_insert ?lookup_delete //.
Qed.
Lemma big_sepM_insert_acc Φ m i x :
m !! i = Some x
([ map] ky m, Φ k y)
Φ i x ( x', Φ i x' - ([ map] ky <[i:=x']> m, Φ k y)).
Proof.
intros ?. rewrite {1}big_sepM_delete //. apply sep_mono; [done|].
apply forall_intro=> x'.
rewrite -insert_delete big_sepM_insert ?lookup_delete //.
by apply wand_intro_l.
Qed.
Lemma big_sepM_fn_insert {B} (Ψ : K A B PROP) (f : K B) m i x b :
m !! i = None
([ map] ky <[i:=x]> m, Ψ k y (<[i:=b]> f k))
......
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