Commit cfe0535f authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'ralf/gmap-view' into 'master'

add big_op lemmas to gmap_view and use them in ghost_map

See merge request iris/iris!668
parents 45014bab 7d16a1d8
......@@ -26,6 +26,7 @@ Coq 8.11 is no longer supported in this version of Iris.
information.
* Demote the Camera structure on `list` to `iris_staging` since its composition
is not very well-behaved.
* Extend `gmap_view` with lemmas for "big" operations on maps.
**Changes in `proofmode`:**
......
......@@ -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.
......@@ -353,29 +353,49 @@ Section lemmas.
rewrite lookup_delete_ne //.
Qed.
Lemma gmap_view_delete_big m m' :
gmap_view_auth 1 m ([^op map] kv m', gmap_view_frag k (DfracOwn 1) v) ~~>
gmap_view_auth 1 (m m').
Proof.
induction m' as [|k v m' ? IH] using map_ind.
{ rewrite right_id_L big_opM_empty right_id //. }
rewrite big_opM_insert //.
rewrite [gmap_view_frag _ _ _ _]comm assoc IH gmap_view_delete.
rewrite -delete_difference. done.
Qed.
Lemma gmap_view_update m k v v' :
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.
apply view_update=>n bf Hrel j [df va] /=.
rewrite lookup_op. destruct (decide (j = k)) as [->|Hne].
- assert (bf !! k = None) as Hbf.
{ move: Hrel =>/view_rel_validN /(_ k).
rewrite lookup_op lookup_singleton.
destruct (bf !! k) as [[df' va']|] eqn:Hbf; last done.
rewrite Hbf. clear Hbf.
rewrite -Some_op -pair_op.
move=>[/= /dfrac_full_exclusive Hdf _]. done. }
rewrite Hbf right_id lookup_singleton. clear Hbf.
intros [= <- <-].
eexists. do 2 (split; first done).
rewrite lookup_insert. done.
- rewrite lookup_singleton_ne; last done.
rewrite left_id=>Hbf.
edestruct (Hrel j) as (v'' & ? & ? & Hm).
{ rewrite lookup_op lookup_singleton_ne // left_id. done. }
simpl in *. eexists. do 2 (split; first done).
rewrite lookup_insert_ne //.
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 :
dom (gset K) m0 = dom (gset K) m1
gmap_view_auth 1 m ([^op map] kv m0, gmap_view_frag k (DfracOwn 1) v) ~~>
gmap_view_auth 1 (m1 m) ([^op map] kv m1, gmap_view_frag k (DfracOwn 1) v).
Proof.
intros Hdom%eq_sym. revert m1 Hdom.
induction m0 as [|k v m0 Hnotdom IH] using map_ind; intros m1 Hdom.
{ rewrite dom_empty_L in Hdom.
apply dom_empty_inv_L in Hdom as ->.
rewrite left_id_L big_opM_empty. done. }
rewrite dom_insert_L in Hdom.
assert (k dom (gset K) m1) as Hindom by set_solver.
apply elem_of_dom in Hindom as [v' Hlookup].
rewrite big_opM_insert //.
rewrite [gmap_view_frag _ _ _ _]comm assoc.
rewrite (IH (delete k m1)); last first.
{ rewrite dom_delete_L Hdom.
apply not_elem_of_dom in Hnotdom. set_solver -Hdom. }
rewrite -assoc [_ gmap_view_frag _ _ _]comm assoc.
rewrite (gmap_view_update _ _ _ v').
rewrite (big_opM_delete _ m1 k v') // -assoc.
rewrite insert_union_r; last by rewrite lookup_delete.
rewrite union_delete_insert //.
Qed.
Lemma gmap_view_persist k dq v :
......
......@@ -52,6 +52,8 @@ Lemma cmra_update_exclusive `{!Exclusive x} y:
Proof. move=>??[z|]=>[/exclusiveN_l[]|_]. by apply cmra_valid_validN. Qed.
(** Updates form a preorder. *)
Global Instance cmra_update_rewrite_relation :
RewriteRelation (@cmra_update A) := {}.
Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
Proof.
split.
......@@ -59,6 +61,16 @@ Proof.
- intros x y z. rewrite !cmra_update_updateP.
eauto using cmra_updateP_compose with subst.
Qed.
Global Instance cmra_update_proper_update :
Proper (flip cmra_update ==> cmra_update ==> impl) (@cmra_update A).
Proof.
intros x1 x2 Hx y1 y2 Hy ?. etrans; [apply Hx|]. by etrans; [|apply Hy].
Qed.
Global Instance cmra_update_flip_proper_update :
Proper (cmra_update ==> flip cmra_update ==> flip impl) (@cmra_update A).
Proof.
intros x1 x2 Hx y1 y2 Hy ?. etrans; [apply Hx|]. by etrans; [|apply Hy].
Qed.
Lemma cmra_updateP_op (P1 P2 Q : A Prop) x1 x2 :
x1 ~~>: P1 x2 ~~>: P2 ( y1 y2, P1 y1 P2 y2 Q (y1 y2))
......@@ -80,6 +92,13 @@ Proof.
rewrite !cmra_update_updateP; eauto using cmra_updateP_op with congruence.
Qed.
Global Instance cmra_update_op_proper :
Proper (cmra_update ==> cmra_update ==> cmra_update) (op (A:=A)).
Proof. intros x1 x2 Hx y1 y2 Hy. by apply cmra_update_op. Qed.
Global Instance cmra_update_op_flip_proper :
Proper (flip cmra_update ==> flip cmra_update ==> flip cmra_update) (op (A:=A)).
Proof. intros x1 x2 Hx y1 y2 Hy. by apply cmra_update_op. Qed.
Lemma cmra_update_op_l x y : x y ~~> x.
Proof. intros n mz. rewrite comm cmra_op_opM_assoc. apply cmra_validN_op_r. Qed.
Lemma cmra_update_op_r x y : x y ~~> y.
......
......@@ -67,6 +67,15 @@ Section lemmas.
AsFractional (k [γ]{#q} v) (λ q, k [γ]{#q} v)%I q.
Proof. split; first done. apply _. Qed.
Local Lemma ghost_map_elems_unseal γ m dq :
([ map] k v m, k [γ]{dq} v) ==
own γ ([^op map] kv m, gmap_view_frag (V:=leibnizO V) k dq v).
Proof.
unseal. destruct (decide (m = )) as [->|Hne].
- rewrite !big_opM_empty. iIntros "_". iApply own_unit.
- rewrite big_opM_own //. iIntros "?". done.
Qed.
Lemma ghost_map_elem_valid k γ dq v : k [γ]{dq} v - ⌜✓ dq.
Proof.
unseal. iIntros "Helem".
......@@ -209,24 +218,20 @@ Section lemmas.
Lemma ghost_map_update {γ m k v} w :
ghost_map_auth γ 1 m - k [γ] v == ghost_map_auth γ 1 (<[k := w]> m) k [γ] w.
Proof.
iIntros "Hauth Hel". iMod (ghost_map_delete with "Hauth Hel") as "Hauth".
iMod (ghost_map_insert k with "Hauth").
{ rewrite lookup_delete. done. }
rewrite insert_delete. eauto.
unseal. apply bi.wand_intro_r. rewrite -!own_op.
apply own_update. apply: gmap_view_update.
Qed.
(** Derived big-op versions of above lemmas *)
(** Big-op versions of above lemmas *)
Lemma ghost_map_lookup_big {γ q m} m0 :
ghost_map_auth γ q m -
([ map] kv m0, k [γ] v) -
m0 m.
Proof.
iInduction m0 as [|k v m0 Hk IH] "IH" using map_ind.
{ iIntros "_ _". iPureIntro. apply map_empty_subseteq. }
rewrite big_sepM_insert //. iIntros "Hauth [Helem Hm0]".
iDestruct (ghost_map_lookup with "Hauth Helem") as %Helem.
iDestruct ("IH" with "Hauth Hm0") as %Hm0.
iPureIntro. apply insert_subseteq_l; done.
iIntros "Hauth Hfrag". rewrite map_subseteq_spec. iIntros (k v Hm0).
iDestruct (ghost_map_lookup with "Hauth [Hfrag]") as %->.
{ rewrite big_sepM_lookup; done. }
done.
Qed.
Lemma ghost_map_insert_big {γ m} m' :
......@@ -234,14 +239,8 @@ Section lemmas.
ghost_map_auth γ 1 m ==
ghost_map_auth γ 1 (m' m) ([ map] k v m', k [γ] v).
Proof.
iInduction m' as [|k v m' Hk] "IH" using map_ind forall (m); iIntros (Hdisj) "Hm".
{ rewrite left_id_L. auto. }
iMod ("IH" with "[] Hm") as "[Hm'm Hm']".
{ iPureIntro. by eapply map_disjoint_insert_l. }
decompose_map_disjoint.
rewrite !big_opM_insert // -insert_union_l //.
by iMod (ghost_map_insert with "Hm'm") as "($ & $)";
first by apply lookup_union_None.
unseal. intros ?. rewrite -big_opM_own_1 -own_op.
apply own_update. apply: gmap_view_alloc_big; done.
Qed.
Lemma ghost_map_insert_persist_big {γ m} m' :
m' ## m
......@@ -259,12 +258,9 @@ Section lemmas.
([ map] kv m0, k [γ] v) ==
ghost_map_auth γ 1 (m m0).
Proof.
iInduction m0 as [|k v m0 Hk IH] "IH" using map_ind.
{ iIntros "Hauth _". rewrite right_id_L //. }
rewrite big_sepM_insert //. iIntros "Hauth [Helem Hm0]".
iMod ("IH" with "Hauth Hm0") as "Hauth".
iMod (ghost_map_delete with "Hauth Helem") as "Hauth".
rewrite -delete_difference. done.
iIntros "Hauth Hfrag". iMod (ghost_map_elems_unseal with "Hfrag") as "Hfrag".
unseal. iApply (own_update_2 with "Hauth Hfrag").
apply: gmap_view_delete_big.
Qed.
Theorem ghost_map_update_big {γ m} m0 m1 :
......@@ -274,22 +270,10 @@ Section lemmas.
ghost_map_auth γ 1 (m1 m)
[ map] kv m1, k [γ] v.
Proof.
iIntros (Hdom%eq_sym) "Hauth Hm0".
iInduction m0 as [|k v m0 Hk] "IH" using map_ind forall (m m1 Hdom).
- rewrite dom_empty_L in Hdom.
apply dom_empty_inv_L in Hdom as ->.
rewrite left_id_L big_sepM_empty.
by iFrame.
- rewrite big_sepM_insert //.
iDestruct "Hm0" as "[Hl Hm0]".
rewrite dom_insert_L in Hdom.
assert (k dom (gset K) m1) as Hindom by set_solver.
apply elem_of_dom in Hindom as [v' Hlookup].
iMod (ghost_map_update v' with "Hauth Hl") as "[Hauth Hl]".
iMod ("IH" $! (<[k:=v']> m) (delete k m1) with "[%] Hauth Hm0") as "[Hauth Hm0]".
{ apply (not_elem_of_dom (D:=gset K)) in Hk. set_solver. }
rewrite union_delete_insert //. iFrame. iClear "#".
iApply big_sepM_delete; first done. by iFrame.
iIntros (?) "Hauth Hfrag". iMod (ghost_map_elems_unseal with "Hfrag") as "Hfrag".
unseal. rewrite -big_opM_own_1 -own_op.
iApply (own_update_2 with "Hauth Hfrag").
apply: gmap_view_update_big. done.
Qed.
End lemmas.
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