Commit 20de7e7c authored by Robbert Krebbers's avatar Robbert Krebbers

Strengthen some gmap lemmas by using Leibniz equality.

parent 72a05023
Pipeline #2125 passed with stage
...@@ -205,15 +205,12 @@ Qed. ...@@ -205,15 +205,12 @@ Qed.
Lemma singleton_valid i x : ({[ i := x ]} : gmap K A) x. Lemma singleton_valid i x : ({[ i := x ]} : gmap K A) x.
Proof. rewrite !cmra_valid_validN. by setoid_rewrite singleton_validN. Qed. Proof. rewrite !cmra_valid_validN. by setoid_rewrite singleton_validN. Qed.
Lemma insert_singleton_opN n m i x : Lemma insert_singleton_op m i x : m !! i = None <[i:=x]> m = {[ i := x ]} m.
m !! i = None <[i:=x]> m {n} {[ i := x ]} m.
Proof. Proof.
intros Hi j; destruct (decide (i = j)) as [->|]. intros Hi; apply map_eq=> j; destruct (decide (i = j)) as [->|].
- by rewrite lookup_op lookup_insert lookup_singleton Hi right_id. - by rewrite lookup_op lookup_insert lookup_singleton Hi right_id_L.
- by rewrite lookup_op lookup_insert_ne // lookup_singleton_ne // left_id. - by rewrite lookup_op lookup_insert_ne // lookup_singleton_ne // left_id_L.
Qed. Qed.
Lemma insert_singleton_op m i x : m !! i = None <[i:=x]> m {[ i := x ]} m.
Proof. rewrite !equiv_dist; naive_solver eauto using insert_singleton_opN. Qed.
Lemma core_singleton (i : K) (x : A) cx : Lemma core_singleton (i : K) (x : A) cx :
pcore x = Some cx core ({[ i := x ]} : gmap K A) = {[ i := cx ]}. pcore x = Some cx core ({[ i := x ]} : gmap K A) = {[ i := cx ]}.
...@@ -252,9 +249,9 @@ Proof. ...@@ -252,9 +249,9 @@ Proof.
* by rewrite Hi lookup_op lookup_singleton lookup_delete. * by rewrite Hi lookup_op lookup_singleton lookup_delete.
* by rewrite lookup_op lookup_singleton_ne // lookup_delete_ne // left_id. * by rewrite lookup_op lookup_singleton_ne // lookup_delete_ne // left_id.
Qed. Qed.
Lemma dom_op m1 m2 : dom (gset K) (m1 m2) dom _ m1 dom _ m2. Lemma dom_op m1 m2 : dom (gset K) (m1 m2) = dom _ m1 dom _ m2.
Proof. Proof.
apply elem_of_equiv; intros i; rewrite elem_of_union !elem_of_dom. apply elem_of_equiv_L=> i; rewrite elem_of_union !elem_of_dom.
unfold is_Some; setoid_rewrite lookup_op. unfold is_Some; setoid_rewrite lookup_op.
destruct (m1 !! i), (m2 !! i); naive_solver. destruct (m1 !! i), (m2 !! i); naive_solver.
Qed. Qed.
...@@ -303,8 +300,8 @@ Section freshness. ...@@ -303,8 +300,8 @@ Section freshness.
{ rewrite -not_elem_of_union -dom_op -not_elem_of_union; apply is_fresh. } { rewrite -not_elem_of_union -dom_op -not_elem_of_union; apply is_fresh. }
exists (<[i:=x]>m); split. exists (<[i:=x]>m); split.
{ by apply HQ; last done; apply not_elem_of_dom. } { by apply HQ; last done; apply not_elem_of_dom. }
rewrite insert_singleton_opN; last by apply not_elem_of_dom. rewrite insert_singleton_op; last by apply not_elem_of_dom.
rewrite -assoc -insert_singleton_opN; rewrite -assoc -insert_singleton_op;
last by apply not_elem_of_dom; rewrite dom_op not_elem_of_union. last by apply not_elem_of_dom; rewrite dom_op not_elem_of_union.
by apply insert_validN; [apply cmra_valid_validN|]. by apply insert_validN; [apply cmra_valid_validN|].
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