From 9f0eb79d2ec4aa632b9b0e27a1b08fcacf6fed64 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 13 May 2022 09:04:20 +0200
Subject: [PATCH] bump std++; port to dom D type being implicit
---
coq-iris.opam | 2 +-
iris/algebra/big_op.v | 2 +-
iris/algebra/dyn_reservation_map.v | 4 ++--
iris/algebra/gmap.v | 13 ++++++-------
iris/algebra/lib/gmap_view.v | 4 ++--
iris/base_logic/lib/boxes.v | 2 +-
iris/base_logic/lib/gen_heap.v | 6 +++---
iris/base_logic/lib/ghost_map.v | 2 +-
iris/base_logic/lib/proph_map.v | 8 ++++----
iris/base_logic/lib/wsat.v | 4 ++--
iris/bi/big_op.v | 8 ++++----
iris_heap_lang/lang.v | 4 ++--
iris_staging/heap_lang/interpreter.v | 2 +-
tests/proofmode.v | 3 +--
14 files changed, 31 insertions(+), 33 deletions(-)
diff --git a/coq-iris.opam b/coq-iris.opam
index d423ea99b..33d8d0dd0 100644
--- a/coq-iris.opam
+++ b/coq-iris.opam
@@ -28,7 +28,7 @@ tags: [
depends: [
"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}%"]
diff --git a/iris/algebra/big_op.v b/iris/algebra/big_op.v
index de29ac48c..0fdcaa4c0 100644
--- a/iris/algebra/big_op.v
+++ b/iris/algebra/big_op.v
@@ -602,7 +602,7 @@ Proof.
Qed.
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.
induction m as [|i x ?? IH] using map_ind.
{ by rewrite big_opM_eq big_opS_eq dom_empty_L. }
diff --git a/iris/algebra/dyn_reservation_map.v b/iris/algebra/dyn_reservation_map.v
index 51d5affda..2cdb59ba0 100644
--- a/iris/algebra/dyn_reservation_map.v
+++ b/iris/algebra/dyn_reservation_map.v
@@ -282,7 +282,7 @@ Section cmra.
intros [Hmap [Hinf Hdisj]].
(* 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. *)
- 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).
{ rewrite -difference_difference_L.
by apply difference_infinite, gset_to_coPset_finite. }
@@ -294,7 +294,7 @@ Section cmra.
- eapply set_infinite_subseteq, HE2inf. set_solver.
- intros i. rewrite left_id_L. destruct (Hdisj i) as [?|Hi]; first 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.
Lemma dyn_reservation_map_reserve' :
ε ~~>: (λ x, ∃ E, set_infinite E ∧ x = dyn_reservation_map_token E).
diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index fb51e5a04..1857deabf 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -96,7 +96,7 @@ Lemma insert_idN n m i x :
Proof. intros (y'&?&->)%dist_Some_inv_r'. by rewrite insert_id. Qed.
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.
End ofe.
@@ -421,13 +421,13 @@ Proof.
- move: (Hm j). by rewrite !lookup_op lookup_delete_ne.
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.
apply set_eq=> i; rewrite elem_of_union !elem_of_dom.
unfold is_Some; setoid_rewrite lookup_op.
destruct (m1 !! i), (m2 !! i); naive_solver.
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.
rewrite lookup_included=>? i; rewrite !elem_of_dom. by apply is_Some_included.
Qed.
@@ -442,15 +442,14 @@ Section freshness.
Proof.
move=> /(pred_infinite_set I (C:=gset K)) HP ? HQ.
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).
- { 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. }
exists (<[i:=f i]>m); split.
- by apply HQ.
- rewrite insert_singleton_op //.
- rewrite -assoc -insert_singleton_op;
- last by eapply (not_elem_of_dom (D:=gset K)).
+ rewrite -assoc -insert_singleton_op; last by eapply not_elem_of_dom.
apply insert_validN; [apply cmra_valid_validN|]; auto.
Qed.
Lemma alloc_updateP_strong (Q : gmap K A → Prop) (I : K → Prop) m x :
diff --git a/iris/algebra/lib/gmap_view.v b/iris/algebra/lib/gmap_view.v
index 3109af96a..abff73761 100644
--- a/iris/algebra/lib/gmap_view.v
+++ b/iris/algebra/lib/gmap_view.v
@@ -379,7 +379,7 @@ Section lemmas.
Qed.
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] k↦v ∈ m0, gmap_view_frag k (DfracOwn 1) v) ~~>
gmap_view_auth (DfracOwn 1) (m1 ∪ m) ⋅ ([^op map] k↦v ∈ m1, gmap_view_frag k (DfracOwn 1) v).
Proof.
@@ -389,7 +389,7 @@ Section lemmas.
apply dom_empty_iff_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.
+ assert (k ∈ dom 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.
diff --git a/iris/base_logic/lib/boxes.v b/iris/base_logic/lib/boxes.v
index 252446481..baf6635d5 100644
--- a/iris/base_logic/lib/boxes.v
+++ b/iris/base_logic/lib/boxes.v
@@ -108,7 +108,7 @@ Lemma slice_insert_empty E q f Q P :
Proof.
iDestruct 1 as (Φ) "[#HeqP Hf]".
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|]).
rewrite pair_split. iDestruct "Hγ" as "[[Hγ Hγ'] #HγQ]".
iDestruct "Hdom" as % ?%not_elem_of_dom.
diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v
index 7aa2d54cb..c9f28145a 100644
--- a/iris/base_logic/lib/gen_heap.v
+++ b/iris/base_logic/lib/gen_heap.v
@@ -98,7 +98,7 @@ Section definitions.
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 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_meta_name hG) 1 m.
@@ -256,7 +256,7 @@ Section gen_heap.
iMod (own_alloc (reservation_map_token ⊤)) as (γm) "Hγm".
{ apply reservation_map_token_valid. }
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.
iExists (<[l:=γm]> m). iFrame. iPureIntro.
rewrite !dom_insert_L. set_solver.
@@ -291,7 +291,7 @@ Section gen_heap.
iDestruct (ghost_map_lookup with "Hσ Hl") as %Hl.
iMod (ghost_map_update with "Hσ Hl") as "[Hσ Hl]".
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.
Qed.
End gen_heap.
diff --git a/iris/base_logic/lib/ghost_map.v b/iris/base_logic/lib/ghost_map.v
index a64159b00..c0897fbdd 100644
--- a/iris/base_logic/lib/ghost_map.v
+++ b/iris/base_logic/lib/ghost_map.v
@@ -266,7 +266,7 @@ Section lemmas.
Qed.
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 -∗
([∗ map] k↦v ∈ m0, k ↪[γ] v) ==∗
ghost_map_auth γ 1 (m1 ∪ m) ∗
diff --git a/iris/base_logic/lib/proph_map.v b/iris/base_logic/lib/proph_map.v
index e4e14cf2a..f44547106 100644
--- a/iris/base_logic/lib/proph_map.v
+++ b/iris/base_logic/lib/proph_map.v
@@ -46,7 +46,7 @@ Section definitions.
Definition proph_map_interp pvs (ps : gset P) : iProp Σ :=
∃ 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 Σ :=
p ↪[proph_map_name pG] vs.
@@ -64,7 +64,7 @@ Section list_resolves.
Lemma resolves_insert pvs p R :
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.
Proof.
intros Hinlist Hp q vs HEq.
@@ -109,7 +109,7 @@ Section proph_map.
iIntros (Hp) "HR". iDestruct "HR" as (R) "[[% %] Hâ—]".
rewrite proph_eq /proph_def.
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.
iExists (<[p := proph_list_resolves pvs p]> R).
iFrame. iPureIntro. split.
@@ -135,7 +135,7 @@ Section proph_map.
* rewrite lookup_insert_ne in HEq; last done.
rewrite (Hres q ws HEq).
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.
Qed.
End proph_map.
diff --git a/iris/base_logic/lib/wsat.v b/iris/base_logic/lib/wsat.v
index e6e9e1e81..9c821c1b3 100644
--- a/iris/base_logic/lib/wsat.v
+++ b/iris/base_logic/lib/wsat.v
@@ -146,7 +146,7 @@ Proof.
iMod (own_unit (gset_disjUR positive) disabled_name) as "HE".
iMod (own_updateP with "[$]") as "HE".
{ 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. }
iDestruct "HE" as (X) "[Hi HE]"; iDestruct "Hi" as %(i & -> & HIi & ?).
iMod (own_update with "Hw") as "[Hw HiP]".
@@ -167,7 +167,7 @@ Proof.
iMod (own_unit (gset_disjUR positive) disabled_name) as "HD".
iMod (own_updateP with "[$]") as "HD".
{ 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. }
iDestruct "HD" as (X) "[Hi HD]"; iDestruct "Hi" as %(i & -> & HIi & ?).
iMod (own_update with "Hw") as "[Hw HiP]".
diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 3ec0cdccf..3eb8e2750 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -1645,7 +1645,7 @@ Qed.
Lemma big_sepM_impl_dom_subseteq `{Countable K} {A 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] k↦x ∈ m1, Φ k x) -∗
□ (∀ (k : K) (x : A) (y : B),
⌜m1 !! k = Some x⌠→ ⌜m2 !! k = Some y⌠→
@@ -1872,7 +1872,7 @@ Section map2.
Lemma big_sepM2_dom Φ m1 m2 :
([∗ map] k↦y1;y2 ∈ m1; m2, Φ k y1 y2) ⊢
- ⌜ dom (gset K) m1 = dom (gset K) m2 âŒ.
+ ⌜ dom m1 = dom m2 âŒ.
Proof.
rewrite big_sepM2_lookup_iff. apply pure_mono=>Hm.
apply set_eq=> k. by rewrite !elem_of_dom.
@@ -1993,7 +1993,7 @@ Section map2.
Lemma big_sepM2_empty_r m2 Φ : ([∗ map] k↦y1;y2 ∈ ∅; m2, Φ k y1 y2) ⊢ ⌜m2 = ∅âŒ.
Proof.
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.
Lemma big_sepM2_insert Φ m1 m2 i x1 x2 :
@@ -2769,7 +2769,7 @@ Section gset.
End gset.
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.
(** ** Big ops over finite multisets *)
diff --git a/iris_heap_lang/lang.v b/iris_heap_lang/lang.v
index 49c537d76..54e771682 100644
--- a/iris_heap_lang/lang.v
+++ b/iris_heap_lang/lang.v
@@ -741,14 +741,14 @@ Proof.
Qed.
Lemma alloc_fresh v n σ :
- let l := fresh_locs (dom (gset loc) σ.(heap)) in
+ let l := fresh_locs (dom σ.(heap)) in
(0 < n)%Z →
head_step (AllocN ((Val $ LitV $ LitInt $ n)) (Val v)) σ []
(Val $ LitV $ LitLoc l) (state_init_heap l n v σ) [].
Proof.
intros.
apply AllocNS; first done.
- intros. apply (not_elem_of_dom (D := gset loc)).
+ intros. apply not_elem_of_dom.
by apply fresh_locs_fresh.
Qed.
diff --git a/iris_staging/heap_lang/interpreter.v b/iris_staging/heap_lang/interpreter.v
index 2e773ca47..eca5ef424 100644
--- a/iris_staging/heap_lang/interpreter.v
+++ b/iris_staging/heap_lang/interpreter.v
@@ -714,7 +714,7 @@ Section interpret_ok.
Qed.
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 (modify_lang_state f s).
Proof.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 5c1740448..963f2986a 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -83,8 +83,7 @@ Proof.
Qed.
Lemma test_iRewrite_dom `{!BiInternalEq PROP} {A : ofe} (m1 m2 : gmap nat A) :
- m1 ≡ m2 ⊢@{PROP}
- ⌜ dom (gset nat) m1 = dom (gset nat) m2 âŒ.
+ m1 ≡ m2 ⊢@{PROP} ⌜ dom m1 = dom m2 âŒ.
Proof. iIntros "H". by iRewrite "H". Qed.
Check "test_iDestruct_and_emp".
--
GitLab