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

Merge branch 'ralf/dom' into 'master'

port to dom D type being implicit

See merge request !795
parents dacf718e 9f0eb79d
Pipeline #65863 passed with stage
in 15 minutes and 59 seconds
...@@ -28,7 +28,7 @@ tags: [ ...@@ -28,7 +28,7 @@ tags: [
depends: [ depends: [
"coq" { (>= "8.13" & < "8.16~") | (= "dev") } "coq" { (>= "8.13" & < "8.16~") | (= "dev") }
"coq-stdpp" { (= "dev.2022-05-04.0.1aceb4c6") | (= "dev") } "coq-stdpp" { (= "dev.2022-05-13.0.53c9d7f7") | (= "dev") }
] ]
build: ["./make-package" "iris" "-j%{jobs}%"] build: ["./make-package" "iris" "-j%{jobs}%"]
......
...@@ -602,7 +602,7 @@ Proof. ...@@ -602,7 +602,7 @@ Proof.
Qed. Qed.
Lemma big_opM_dom `{Countable K} {A} (f : K M) (m : gmap K A) : Lemma big_opM_dom `{Countable K} {A} (f : K M) (m : gmap K A) :
([^o map] k_ m, f k) ([^o set] k dom _ m, f k). ([^o map] k_ m, f k) ([^o set] k dom m, f k).
Proof. Proof.
induction m as [|i x ?? IH] using map_ind. induction m as [|i x ?? IH] using map_ind.
{ by rewrite big_opM_eq big_opS_eq dom_empty_L. } { by rewrite big_opM_eq big_opS_eq dom_empty_L. }
......
...@@ -282,7 +282,7 @@ Section cmra. ...@@ -282,7 +282,7 @@ Section cmra.
intros [Hmap [Hinf Hdisj]]. intros [Hmap [Hinf Hdisj]].
(* Pick a fresh set disjoint from the existing tokens [Ef] and map [mf], (* Pick a fresh set disjoint from the existing tokens [Ef] and map [mf],
such that both that set [E1] and the remainder [E2] are infinite. *) such that both that set [E1] and the remainder [E2] are infinite. *)
edestruct (coPset_split_infinite ( (Ef (gset_to_coPset $ dom (gset _) mf)))) as edestruct (coPset_split_infinite ( (Ef (gset_to_coPset $ dom mf)))) as
(E1 & E2 & HEunion & HEdisj & HE1inf & HE2inf). (E1 & E2 & HEunion & HEdisj & HE1inf & HE2inf).
{ rewrite -difference_difference_L. { rewrite -difference_difference_L.
by apply difference_infinite, gset_to_coPset_finite. } by apply difference_infinite, gset_to_coPset_finite. }
...@@ -294,7 +294,7 @@ Section cmra. ...@@ -294,7 +294,7 @@ Section cmra.
- eapply set_infinite_subseteq, HE2inf. set_solver. - eapply set_infinite_subseteq, HE2inf. set_solver.
- intros i. rewrite left_id_L. destruct (Hdisj i) as [?|Hi]; first by left. - intros i. rewrite left_id_L. destruct (Hdisj i) as [?|Hi]; first by left.
destruct (mf !! i) as [p|] eqn:Hp; last by left. destruct (mf !! i) as [p|] eqn:Hp; last by left.
apply (elem_of_dom_2 (D:=gset _)), elem_of_gset_to_coPset in Hp. right. set_solver. apply elem_of_dom_2, elem_of_gset_to_coPset in Hp. right. set_solver.
Qed. Qed.
Lemma dyn_reservation_map_reserve' : Lemma dyn_reservation_map_reserve' :
ε ~~>: (λ x, E, set_infinite E x = dyn_reservation_map_token E). ε ~~>: (λ x, E, set_infinite E x = dyn_reservation_map_token E).
......
...@@ -96,7 +96,7 @@ Lemma insert_idN n m i x : ...@@ -96,7 +96,7 @@ Lemma insert_idN n m i x :
Proof. intros (y'&?&->)%dist_Some_inv_r'. by rewrite insert_id. Qed. Proof. intros (y'&?&->)%dist_Some_inv_r'. by rewrite insert_id. Qed.
Global Instance gmap_dom_ne n : Global Instance gmap_dom_ne n :
Proper (({n}@{gmap K A}) ==> (=)) (dom (gset K)). Proper (({n}@{gmap K A}) ==> (=)) dom.
Proof. intros m1 m2 Hm. apply set_eq=> k. by rewrite !elem_of_dom Hm. Qed. Proof. intros m1 m2 Hm. apply set_eq=> k. by rewrite !elem_of_dom Hm. Qed.
End ofe. End ofe.
...@@ -421,13 +421,13 @@ Proof. ...@@ -421,13 +421,13 @@ Proof.
- move: (Hm j). by rewrite !lookup_op lookup_delete_ne. - move: (Hm j). by rewrite !lookup_op lookup_delete_ne.
Qed. Qed.
Lemma dom_op m1 m2 : dom (gset K) (m1 m2) = dom _ m1 dom _ m2. Lemma dom_op m1 m2 : dom (m1 m2) = dom m1 dom m2.
Proof. Proof.
apply set_eq=> i; rewrite elem_of_union !elem_of_dom. apply set_eq=> 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.
Lemma dom_included m1 m2 : m1 m2 dom (gset K) m1 dom _ m2. Lemma dom_included m1 m2 : m1 m2 dom m1 dom m2.
Proof. Proof.
rewrite lookup_included=>? i; rewrite !elem_of_dom. by apply is_Some_included. rewrite lookup_included=>? i; rewrite !elem_of_dom. by apply is_Some_included.
Qed. Qed.
...@@ -442,15 +442,14 @@ Section freshness. ...@@ -442,15 +442,14 @@ Section freshness.
Proof. Proof.
move=> /(pred_infinite_set I (C:=gset K)) HP ? HQ. move=> /(pred_infinite_set I (C:=gset K)) HP ? HQ.
apply cmra_total_updateP. intros n mf Hm. apply cmra_total_updateP. intros n mf Hm.
destruct (HP (dom (gset K) (m mf))) as [i [Hi1 Hi2]]. destruct (HP (dom (m mf))) as [i [Hi1 Hi2]].
assert (m !! i = None). assert (m !! i = None).
{ eapply (not_elem_of_dom (D:=gset K)). revert Hi2. { eapply not_elem_of_dom. revert Hi2.
rewrite dom_op not_elem_of_union. naive_solver. } rewrite dom_op not_elem_of_union. naive_solver. }
exists (<[i:=f i]>m); split. exists (<[i:=f i]>m); split.
- by apply HQ. - by apply HQ.
- rewrite insert_singleton_op //. - rewrite insert_singleton_op //.
rewrite -assoc -insert_singleton_op; rewrite -assoc -insert_singleton_op; last by eapply not_elem_of_dom.
last by eapply (not_elem_of_dom (D:=gset K)).
apply insert_validN; [apply cmra_valid_validN|]; auto. apply insert_validN; [apply cmra_valid_validN|]; auto.
Qed. Qed.
Lemma alloc_updateP_strong (Q : gmap K A Prop) (I : K Prop) m x : Lemma alloc_updateP_strong (Q : gmap K A Prop) (I : K Prop) m x :
......
...@@ -379,7 +379,7 @@ Section lemmas. ...@@ -379,7 +379,7 @@ Section lemmas.
Qed. Qed.
Lemma gmap_view_update_big m m0 m1 : Lemma gmap_view_update_big m m0 m1 :
dom (gset K) m0 = dom (gset K) m1 dom m0 = dom m1
gmap_view_auth (DfracOwn 1) m ([^op map] kv m0, gmap_view_frag k (DfracOwn 1) v) ~~> gmap_view_auth (DfracOwn 1) m ([^op map] kv m0, gmap_view_frag k (DfracOwn 1) v) ~~>
gmap_view_auth (DfracOwn 1) (m1 m) ([^op map] kv m1, gmap_view_frag k (DfracOwn 1) v). gmap_view_auth (DfracOwn 1) (m1 m) ([^op map] kv m1, gmap_view_frag k (DfracOwn 1) v).
Proof. Proof.
...@@ -389,7 +389,7 @@ Section lemmas. ...@@ -389,7 +389,7 @@ Section lemmas.
apply dom_empty_iff_L in Hdom as ->. apply dom_empty_iff_L in Hdom as ->.
rewrite left_id_L big_opM_empty. done. } rewrite left_id_L big_opM_empty. done. }
rewrite dom_insert_L in Hdom. rewrite dom_insert_L in Hdom.
assert (k dom (gset K) m1) as Hindom by set_solver. assert (k dom m1) as Hindom by set_solver.
apply elem_of_dom in Hindom as [v' Hlookup]. apply elem_of_dom in Hindom as [v' Hlookup].
rewrite big_opM_insert //. rewrite big_opM_insert //.
rewrite [gmap_view_frag _ _ _ _]comm assoc. rewrite [gmap_view_frag _ _ _ _]comm assoc.
......
...@@ -108,7 +108,7 @@ Lemma slice_insert_empty E q f Q P : ...@@ -108,7 +108,7 @@ Lemma slice_insert_empty E q f Q P :
Proof. Proof.
iDestruct 1 as (Φ) "[#HeqP Hf]". iDestruct 1 as (Φ) "[#HeqP Hf]".
iMod (own_alloc_cofinite (E false E false, iMod (own_alloc_cofinite (E false E false,
Some (to_agree (Next Q))) (dom _ f)) Some (to_agree (Next Q))) (dom f))
as (γ) "[Hdom Hγ]"; first by (split; [apply auth_both_valid_discrete|]). as (γ) "[Hdom Hγ]"; first by (split; [apply auth_both_valid_discrete|]).
rewrite pair_split. iDestruct "Hγ" as "[[Hγ Hγ'] #HγQ]". rewrite pair_split. iDestruct "Hγ" as "[[Hγ Hγ'] #HγQ]".
iDestruct "Hdom" as % ?%not_elem_of_dom. iDestruct "Hdom" as % ?%not_elem_of_dom.
......
...@@ -98,7 +98,7 @@ Section definitions. ...@@ -98,7 +98,7 @@ Section definitions.
Definition gen_heap_interp (σ : gmap L V) : iProp Σ := m : gmap L gname, Definition gen_heap_interp (σ : gmap L V) : iProp Σ := m : gmap L gname,
(* The [⊆] is used to avoid assigning ghost information to the locations in (* The [⊆] is used to avoid assigning ghost information to the locations in
the initial heap (see [gen_heap_init]). *) the initial heap (see [gen_heap_init]). *)
dom _ m dom (gset L) σ dom m dom σ
ghost_map_auth (gen_heap_name hG) 1 σ ghost_map_auth (gen_heap_name hG) 1 σ
ghost_map_auth (gen_meta_name hG) 1 m. ghost_map_auth (gen_meta_name hG) 1 m.
...@@ -256,7 +256,7 @@ Section gen_heap. ...@@ -256,7 +256,7 @@ Section gen_heap.
iMod (own_alloc (reservation_map_token )) as (γm) "Hγm". iMod (own_alloc (reservation_map_token )) as (γm) "Hγm".
{ apply reservation_map_token_valid. } { apply reservation_map_token_valid. }
iMod (ghost_map_insert_persist l with "Hm") as "[Hm Hlm]". iMod (ghost_map_insert_persist l with "Hm") as "[Hm Hlm]".
{ move: Hσl. rewrite -!(not_elem_of_dom (D:=gset L)). set_solver. } { move: Hσl. rewrite -!not_elem_of_dom. set_solver. }
iModIntro. iFrame "Hl". iSplitL "Hσ Hm"; last by eauto with iFrame. iModIntro. iFrame "Hl". iSplitL "Hσ Hm"; last by eauto with iFrame.
iExists (<[l:=γm]> m). iFrame. iPureIntro. iExists (<[l:=γm]> m). iFrame. iPureIntro.
rewrite !dom_insert_L. set_solver. rewrite !dom_insert_L. set_solver.
...@@ -291,7 +291,7 @@ Section gen_heap. ...@@ -291,7 +291,7 @@ Section gen_heap.
iDestruct (ghost_map_lookup with "Hσ Hl") as %Hl. iDestruct (ghost_map_lookup with "Hσ Hl") as %Hl.
iMod (ghost_map_update with "Hσ Hl") as "[Hσ Hl]". iMod (ghost_map_update with "Hσ Hl") as "[Hσ Hl]".
iModIntro. iFrame "Hl". iExists m. iFrame. iModIntro. iFrame "Hl". iExists m. iFrame.
iPureIntro. apply (elem_of_dom_2 (D:=gset L)) in Hl. iPureIntro. apply elem_of_dom_2 in Hl.
rewrite dom_insert_L. set_solver. rewrite dom_insert_L. set_solver.
Qed. Qed.
End gen_heap. End gen_heap.
......
...@@ -266,7 +266,7 @@ Section lemmas. ...@@ -266,7 +266,7 @@ Section lemmas.
Qed. Qed.
Theorem ghost_map_update_big {γ m} m0 m1 : Theorem ghost_map_update_big {γ m} m0 m1 :
dom (gset K) m0 = dom (gset K) m1 dom m0 = dom m1
ghost_map_auth γ 1 m - ghost_map_auth γ 1 m -
([ map] kv m0, k [γ] v) == ([ map] kv m0, k [γ] v) ==
ghost_map_auth γ 1 (m1 m) ghost_map_auth γ 1 (m1 m)
......
...@@ -46,7 +46,7 @@ Section definitions. ...@@ -46,7 +46,7 @@ Section definitions.
Definition proph_map_interp pvs (ps : gset P) : iProp Σ := Definition proph_map_interp pvs (ps : gset P) : iProp Σ :=
R, proph_resolves_in_list R pvs R, proph_resolves_in_list R pvs
dom (gset _) R ps ghost_map_auth (proph_map_name pG) 1 R. dom R ps ghost_map_auth (proph_map_name pG) 1 R.
Definition proph_def (p : P) (vs : list V) : iProp Σ := Definition proph_def (p : P) (vs : list V) : iProp Σ :=
p [proph_map_name pG] vs. p [proph_map_name pG] vs.
...@@ -64,7 +64,7 @@ Section list_resolves. ...@@ -64,7 +64,7 @@ Section list_resolves.
Lemma resolves_insert pvs p R : Lemma resolves_insert pvs p R :
proph_resolves_in_list R pvs proph_resolves_in_list R pvs
p dom (gset _) R p dom R
proph_resolves_in_list (<[p := proph_list_resolves pvs p]> R) pvs. proph_resolves_in_list (<[p := proph_list_resolves pvs p]> R) pvs.
Proof. Proof.
intros Hinlist Hp q vs HEq. intros Hinlist Hp q vs HEq.
...@@ -109,7 +109,7 @@ Section proph_map. ...@@ -109,7 +109,7 @@ Section proph_map.
iIntros (Hp) "HR". iDestruct "HR" as (R) "[[% %] H●]". iIntros (Hp) "HR". iDestruct "HR" as (R) "[[% %] H●]".
rewrite proph_eq /proph_def. rewrite proph_eq /proph_def.
iMod (ghost_map_insert p (proph_list_resolves pvs p) with "H●") as "[H● H◯]". iMod (ghost_map_insert p (proph_list_resolves pvs p) with "H●") as "[H● H◯]".
{ apply (not_elem_of_dom (D:=gset P)). set_solver. } { apply not_elem_of_dom. set_solver. }
iModIntro. iFrame. iModIntro. iFrame.
iExists (<[p := proph_list_resolves pvs p]> R). iExists (<[p := proph_list_resolves pvs p]> R).
iFrame. iPureIntro. split. iFrame. iPureIntro. split.
...@@ -135,7 +135,7 @@ Section proph_map. ...@@ -135,7 +135,7 @@ Section proph_map.
* rewrite lookup_insert_ne in HEq; last done. * rewrite lookup_insert_ne in HEq; last done.
rewrite (Hres q ws HEq). rewrite (Hres q ws HEq).
simpl. rewrite decide_False; done. simpl. rewrite decide_False; done.
+ assert (p dom (gset P) R) by exact: elem_of_dom_2. + assert (p dom R) by exact: elem_of_dom_2.
rewrite dom_insert. set_solver. rewrite dom_insert. set_solver.
Qed. Qed.
End proph_map. End proph_map.
...@@ -146,7 +146,7 @@ Proof. ...@@ -146,7 +146,7 @@ Proof.
iMod (own_unit (gset_disjUR positive) disabled_name) as "HE". iMod (own_unit (gset_disjUR positive) disabled_name) as "HE".
iMod (own_updateP with "[$]") as "HE". iMod (own_updateP with "[$]") as "HE".
{ apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None φ i)). { apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None φ i)).
intros E. destruct (Hfresh (E dom _ I)) intros E. destruct (Hfresh (E dom I))
as (i & [? HIi%not_elem_of_dom]%not_elem_of_union & ?); eauto. } as (i & [? HIi%not_elem_of_dom]%not_elem_of_union & ?); eauto. }
iDestruct "HE" as (X) "[Hi HE]"; iDestruct "Hi" as %(i & -> & HIi & ?). iDestruct "HE" as (X) "[Hi HE]"; iDestruct "Hi" as %(i & -> & HIi & ?).
iMod (own_update with "Hw") as "[Hw HiP]". iMod (own_update with "Hw") as "[Hw HiP]".
...@@ -167,7 +167,7 @@ Proof. ...@@ -167,7 +167,7 @@ Proof.
iMod (own_unit (gset_disjUR positive) disabled_name) as "HD". iMod (own_unit (gset_disjUR positive) disabled_name) as "HD".
iMod (own_updateP with "[$]") as "HD". iMod (own_updateP with "[$]") as "HD".
{ apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None φ i)). { apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None φ i)).
intros E. destruct (Hfresh (E dom _ I)) intros E. destruct (Hfresh (E dom I))
as (i & [? HIi%not_elem_of_dom]%not_elem_of_union & ?); eauto. } as (i & [? HIi%not_elem_of_dom]%not_elem_of_union & ?); eauto. }
iDestruct "HD" as (X) "[Hi HD]"; iDestruct "Hi" as %(i & -> & HIi & ?). iDestruct "HD" as (X) "[Hi HD]"; iDestruct "Hi" as %(i & -> & HIi & ?).
iMod (own_update with "Hw") as "[Hw HiP]". iMod (own_update with "Hw") as "[Hw HiP]".
......
...@@ -1645,7 +1645,7 @@ Qed. ...@@ -1645,7 +1645,7 @@ Qed.
Lemma big_sepM_impl_dom_subseteq `{Countable K} {A B} Lemma big_sepM_impl_dom_subseteq `{Countable K} {A B}
(Φ : K A PROP) (Ψ : K B PROP) (m1 : gmap K A) (m2 : gmap K B) : (Φ : K A PROP) (Ψ : K B PROP) (m1 : gmap K A) (m2 : gmap K B) :
dom (gset _) m2 dom _ m1 dom m2 dom m1
([ map] kx m1, Φ k x) - ([ map] kx m1, Φ k x) -
( (k : K) (x : A) (y : B), ( (k : K) (x : A) (y : B),
m1 !! k = Some x m2 !! k = Some y m1 !! k = Some x m2 !! k = Some y
...@@ -1872,7 +1872,7 @@ Section map2. ...@@ -1872,7 +1872,7 @@ Section map2.
Lemma big_sepM2_dom Φ m1 m2 : Lemma big_sepM2_dom Φ m1 m2 :
([ map] ky1;y2 m1; m2, Φ k y1 y2) ([ map] ky1;y2 m1; m2, Φ k y1 y2)
dom (gset K) m1 = dom (gset K) m2 . dom m1 = dom m2 .
Proof. Proof.
rewrite big_sepM2_lookup_iff. apply pure_mono=>Hm. rewrite big_sepM2_lookup_iff. apply pure_mono=>Hm.
apply set_eq=> k. by rewrite !elem_of_dom. apply set_eq=> k. by rewrite !elem_of_dom.
...@@ -1993,7 +1993,7 @@ Section map2. ...@@ -1993,7 +1993,7 @@ Section map2.
Lemma big_sepM2_empty_r m2 Φ : ([ map] ky1;y2 ; m2, Φ k y1 y2) m2 = ∅⌝. Lemma big_sepM2_empty_r m2 Φ : ([ map] ky1;y2 ; m2, Φ k y1 y2) m2 = ∅⌝.
Proof. Proof.
rewrite big_sepM2_dom dom_empty_L. rewrite big_sepM2_dom dom_empty_L.
apply pure_mono=>?. eapply (dom_empty_iff_L (D:=gset K)). eauto. apply pure_mono=>?. eapply dom_empty_iff_L. eauto.
Qed. Qed.
Lemma big_sepM2_insert Φ m1 m2 i x1 x2 : Lemma big_sepM2_insert Φ m1 m2 i x1 x2 :
...@@ -2769,7 +2769,7 @@ Section gset. ...@@ -2769,7 +2769,7 @@ Section gset.
End gset. End gset.
Lemma big_sepM_dom `{Countable K} {A} (Φ : K PROP) (m : gmap K A) : Lemma big_sepM_dom `{Countable K} {A} (Φ : K PROP) (m : gmap K A) :
([ map] k_ m, Φ k) ([ set] k dom _ m, Φ k). ([ map] k_ m, Φ k) ([ set] k dom m, Φ k).
Proof. apply big_opM_dom. Qed. Proof. apply big_opM_dom. Qed.
(** ** Big ops over finite multisets *) (** ** Big ops over finite multisets *)
......
...@@ -741,14 +741,14 @@ Proof. ...@@ -741,14 +741,14 @@ Proof.
Qed. Qed.
Lemma alloc_fresh v n σ : Lemma alloc_fresh v n σ :
let l := fresh_locs (dom (gset loc) σ.(heap)) in let l := fresh_locs (dom σ.(heap)) in
(0 < n)%Z (0 < n)%Z
head_step (AllocN ((Val $ LitV $ LitInt $ n)) (Val v)) σ [] head_step (AllocN ((Val $ LitV $ LitInt $ n)) (Val v)) σ []
(Val $ LitV $ LitLoc l) (state_init_heap l n v σ) []. (Val $ LitV $ LitLoc l) (state_init_heap l n v σ) [].
Proof. Proof.
intros. intros.
apply AllocNS; first done. apply AllocNS; first done.
intros. apply (not_elem_of_dom (D := gset loc)). intros. apply not_elem_of_dom.
by apply fresh_locs_fresh. by apply fresh_locs_fresh.
Qed. Qed.
......
...@@ -714,7 +714,7 @@ Section interpret_ok. ...@@ -714,7 +714,7 @@ Section interpret_ok.
Qed. Qed.
Lemma state_wf_same_dom s f : Lemma state_wf_same_dom s f :
(dom (gset loc) (f s.(lang_state)).(heap) = dom _ s.(lang_state).(heap)) (dom (f s.(lang_state)).(heap) = dom s.(lang_state).(heap))
state_wf s state_wf s
state_wf (modify_lang_state f s). state_wf (modify_lang_state f s).
Proof. Proof.
......
...@@ -83,8 +83,7 @@ Proof. ...@@ -83,8 +83,7 @@ Proof.
Qed. Qed.
Lemma test_iRewrite_dom `{!BiInternalEq PROP} {A : ofe} (m1 m2 : gmap nat A) : Lemma test_iRewrite_dom `{!BiInternalEq PROP} {A : ofe} (m1 m2 : gmap nat A) :
m1 m2 @{PROP} m1 m2 @{PROP} dom m1 = dom m2 .
dom (gset nat) m1 = dom (gset nat) m2 .
Proof. iIntros "H". by iRewrite "H". Qed. Proof. iIntros "H". by iRewrite "H". Qed.
Check "test_iDestruct_and_emp". Check "test_iDestruct_and_emp".
......
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