Commit 5e384379 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Generalize insert_delete lemma.

parent 388fef2b
...@@ -53,7 +53,8 @@ Proof. intros ?; by rewrite /big_opM map_to_list_insert. Qed. ...@@ -53,7 +53,8 @@ Proof. intros ?; by rewrite /big_opM map_to_list_insert. Qed.
Lemma big_opM_delete m i x : Lemma big_opM_delete m i x :
m !! i = Some x x big_opM (delete i m) big_opM m. m !! i = Some x x big_opM (delete i m) big_opM m.
Proof. Proof.
intros. by rewrite -{2}(insert_delete m i x) // big_opM_insert ?lookup_delete. intros. rewrite -{2}(insert_id m i x) // -insert_delete.
by rewrite big_opM_insert ?lookup_delete.
Qed. Qed.
Lemma big_opM_singleton i x : big_opM ({[i := x]} : gmap K A) x. Lemma big_opM_singleton i x : big_opM ({[i := x]} : gmap K A) x.
Proof. Proof.
...@@ -69,7 +70,7 @@ Proof. ...@@ -69,7 +70,7 @@ Proof.
destruct (map_equiv_lookup_l (<[i:=x]> m1) m2 i x) destruct (map_equiv_lookup_l (<[i:=x]> m1) m2 i x)
as (y&?&Hxy); auto using lookup_insert. as (y&?&Hxy); auto using lookup_insert.
rewrite Hxy -big_opM_insert; last auto using lookup_delete. rewrite Hxy -big_opM_insert; last auto using lookup_delete.
by rewrite insert_delete. by rewrite insert_delete insert_id.
Qed. Qed.
Lemma big_opM_lookup_valid n m i x : {n} big_opM m m !! i = Some x {n} x. Lemma big_opM_lookup_valid n m i x : {n} big_opM m m !! i = Some x {n} x.
Proof. Proof.
......
...@@ -171,7 +171,10 @@ Section gmap. ...@@ -171,7 +171,10 @@ Section gmap.
Lemma big_sepM_delete Φ (m : gmap K A) i x : Lemma big_sepM_delete Φ (m : gmap K A) i x :
m !! i = Some x m !! i = Some x
([ map] ky m, Φ k y) ⊣⊢ (Φ i x [ map] ky delete i m, Φ k y). ([ map] ky m, Φ k y) ⊣⊢ (Φ i x [ map] ky delete i m, Φ k y).
Proof. intros. by rewrite -big_sepM_insert ?lookup_delete // insert_delete. Qed. Proof.
intros. rewrite -big_sepM_insert ?lookup_delete //.
by rewrite insert_delete insert_id.
Qed.
Lemma big_sepM_singleton Φ i x : ([ map] ky {[i:=x]}, Φ k y) ⊣⊢ Φ i x. Lemma big_sepM_singleton Φ i x : ([ map] ky {[i:=x]}, Φ k y) ⊣⊢ Φ i x.
Proof. Proof.
......
...@@ -366,13 +366,8 @@ Qed. ...@@ -366,13 +366,8 @@ Qed.
Lemma delete_insert {A} (m : M A) i x : Lemma delete_insert {A} (m : M A) i x :
m !! i = None delete i (<[i:=x]>m) = m. m !! i = None delete i (<[i:=x]>m) = m.
Proof. apply delete_partial_alter. Qed. Proof. apply delete_partial_alter. Qed.
Lemma insert_delete {A} (m : M A) i x : Lemma insert_delete {A} (m : M A) i x : <[i:=x]>(delete i m) = <[i:=x]> m.
m !! i = Some x <[i:=x]>(delete i m) = m. Proof. symmetry; apply (partial_alter_compose (λ _, Some x)). Qed.
Proof.
intros Hmi. unfold delete, map_delete, insert, map_insert.
rewrite <-partial_alter_compose. unfold compose. rewrite <-Hmi.
by apply partial_alter_self_alt.
Qed.
Lemma delete_subseteq {A} (m : M A) i : delete i m m. Lemma delete_subseteq {A} (m : M A) i : delete i m m.
Proof. Proof.
rewrite !map_subseteq_spec. intros j x. rewrite lookup_delete_Some. tauto. rewrite !map_subseteq_spec. intros j x. rewrite lookup_delete_Some. tauto.
...@@ -473,8 +468,8 @@ Lemma insert_subset_inv {A} (m1 m2 : M A) i x : ...@@ -473,8 +468,8 @@ Lemma insert_subset_inv {A} (m1 m2 : M A) i x :
m2', m2 = <[i:=x]>m2' m1 m2' m2' !! i = None. m2', m2 = <[i:=x]>m2' m1 m2' m2' !! i = None.
Proof. Proof.
intros Hi Hm1m2. exists (delete i m2). split_and?. intros Hi Hm1m2. exists (delete i m2). split_and?.
- rewrite insert_delete. done. eapply lookup_weaken, strict_include; eauto. - rewrite insert_delete, insert_id. done.
by rewrite lookup_insert. eapply lookup_weaken, strict_include; eauto. by rewrite lookup_insert.
- eauto using insert_delete_subset. - eauto using insert_delete_subset.
- by rewrite lookup_delete. - by rewrite lookup_delete.
Qed. Qed.
......
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