Commit e29ce6f1 authored by Ralf Jung's avatar Ralf Jung Committed by Robbert Krebbers
Browse files

make cmra_update a rewritable relation

parent 22823e07
......@@ -331,7 +331,7 @@ Section lemmas.
Proof.
intros. induction m' as [|k v m' ? IH] using map_ind; decompose_map_disjoint.
{ rewrite big_opM_empty left_id_L right_id. done. }
etrans; first by apply IH.
rewrite IH //.
rewrite big_opM_insert // assoc.
apply cmra_update_op; last done.
rewrite -insert_union_l. apply (gmap_view_alloc _ k dq); last done.
......@@ -370,10 +370,9 @@ Section lemmas.
gmap_view_auth 1 m gmap_view_frag k (DfracOwn 1) v ~~>
gmap_view_auth 1 (<[k := v']> m) gmap_view_frag k (DfracOwn 1) v'.
Proof.
etrans; first by eapply gmap_view_delete. etrans.
- eapply (gmap_view_alloc _ k (DfracOwn 1) v'); last done.
rewrite lookup_delete //.
- rewrite insert_delete. done.
rewrite gmap_view_delete.
rewrite (gmap_view_alloc _ k (DfracOwn 1) v') //; last by rewrite lookup_delete.
rewrite insert_delete //.
Qed.
Lemma gmap_view_update_big m m0 m1 :
......
......@@ -59,6 +59,7 @@ Proof.
- intros x y z. rewrite !cmra_update_updateP.
eauto using cmra_updateP_compose with subst.
Qed.
Global Instance cmra_update_rewrite_relation : RewriteRelation (@cmra_update A) := {}.
Lemma cmra_updateP_op (P1 P2 Q : A Prop) x1 x2 :
x1 ~~>: P1 x2 ~~>: P2 ( y1 y2, P1 y1 P2 y2 Q (y1 y2))
......
Supports Markdown
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