From 30da7ea34fec696e1b04e835b3e0a182f66c7b4e Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Thu, 6 Jun 2024 09:23:05 +0200
Subject: [PATCH] Adapt to iris/stdpp!555

---
 iris/algebra/cmra.v                   | 11 +++++------
 iris/algebra/gmap.v                   | 14 +++++++-------
 iris/algebra/lib/gmap_view.v          |  8 ++++----
 iris/algebra/list.v                   |  8 ++++----
 iris/algebra/ofe.v                    |  6 +++---
 iris/base_logic/lib/gen_inv_heap.v    |  2 +-
 iris/base_logic/lib/ghost_map.v       |  8 +++++---
 iris_unstable/heap_lang/interpreter.v |  6 +++---
 tests/algebra.v                       |  2 +-
 9 files changed, 33 insertions(+), 32 deletions(-)

diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index 203e73dc6..381572fcc 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -1320,12 +1320,11 @@ Global Instance prod_map_cmra_morphism {A A' B B' : cmra} (f : A → A') (g : B
 Proof.
   split; first apply _.
   - by intros n x [??]; split; simpl; apply cmra_morphism_validN.
-  - intros x. etrans; last apply (reflexivity (mbind _ _)).
-    etrans; first apply (reflexivity (_ <$> mbind _ _)). simpl.
-    assert (Hf := cmra_morphism_pcore f (x.1)).
-    destruct (pcore (f (x.1))), (pcore (x.1)); inversion_clear Hf=>//=.
-    assert (Hg := cmra_morphism_pcore g (x.2)).
-    destruct (pcore (g (x.2))), (pcore (x.2)); inversion_clear Hg=>//=.
+  - intros [x1 x2]. rewrite /= !pair_pcore. simpl.
+    pose proof (Hf := cmra_morphism_pcore f (x1)).
+    destruct (pcore (f (x1))), (pcore (x1)); inversion_clear Hf=>//=.
+    pose proof (Hg := cmra_morphism_pcore g (x2)).
+    destruct (pcore (g (x2))), (pcore (x2)); inversion_clear Hg=>//=.
     by setoid_subst.
   - intros. by rewrite /prod_map /= !cmra_morphism_op.
 Qed.
diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index e250a628f..1f416c8a9 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -113,7 +113,7 @@ Global Arguments gmapO _ {_ _} _.
 (** Non-expansiveness of higher-order map functions and big-ops *)
 Global Instance merge_ne `{Countable K} {A B C : ofe} n :
   Proper ((dist (A:=option A) n ==> dist (A:=option B) n ==> dist (A:=option C) n) ==>
-          dist n ==> dist n ==> dist n) (merge (M:=gmap K)).
+          dist n ==> dist n ==> dist n) (merge (MA:=gmap K A)).
 Proof.
   intros ?? Hf ?? Hm1 ?? Hm2 i. rewrite !lookup_merge.
   destruct (Hm1 i), (Hm2 i); try apply Hf; by constructor.
@@ -126,7 +126,7 @@ Proof.
   by do 2 destruct 1; first [apply Hf | constructor].
 Qed.
 Global Instance map_fmap_ne `{Countable K} {A B : ofe} (f : A → B) n :
-  Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (fmap (M:=gmap K) f).
+  Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (fmap (MA:=gmap K A) f).
 Proof. intros ? m m' ? k; rewrite !lookup_fmap. by repeat f_equiv. Qed.
 Global Instance map_zip_with_ne `{Countable K} {A B C : ofe} (f : A → B → C) n :
   Proper (dist n ==> dist n ==> dist n) f →
@@ -714,7 +714,7 @@ End unital_properties.
 
 (** Functor *)
 Global Instance gmap_fmap_ne `{Countable K} {A B : ofe} (f : A → B) n :
-  Proper (dist n ==> dist n) f → Proper (dist n ==>dist n) (fmap (M:=gmap K) f).
+  Proper (dist n ==> dist n) f → Proper (dist n ==>dist n) (fmap (MA:=gmap K A) f).
 Proof. by intros ? m m' Hm k; rewrite !lookup_fmap; apply option_fmap_ne. Qed.
 Lemma gmap_fmap_ne_ext `{Countable K}
   {A : Type} {B : ofe} (f1 f2 : A → B) (m : gmap K A) n :
@@ -752,11 +752,11 @@ Next Obligation.
 Qed.
 Next Obligation.
   intros K ?? F A ? B ? x. rewrite /= -{2}(map_fmap_id x).
-  apply map_fmap_equiv_ext=>y ??; apply oFunctor_map_id.
+  apply: map_fmap_equiv_ext=>y ??; apply oFunctor_map_id.
 Qed.
 Next Obligation.
   intros K ?? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -map_fmap_compose.
-  apply map_fmap_equiv_ext=>y ??; apply oFunctor_map_compose.
+  apply: map_fmap_equiv_ext=>y ??; apply oFunctor_map_compose.
 Qed.
 Global Instance gmapOF_contractive K `{Countable K} F :
   oFunctorContractive F → oFunctorContractive (gmapOF K F).
@@ -773,11 +773,11 @@ Next Obligation.
 Qed.
 Next Obligation.
   intros K ?? F A ? B ? x. rewrite /= -{2}(map_fmap_id x).
-  apply map_fmap_equiv_ext=>y ??; apply rFunctor_map_id.
+  apply: map_fmap_equiv_ext=>y ??; apply rFunctor_map_id.
 Qed.
 Next Obligation.
   intros K ?? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -map_fmap_compose.
-  apply map_fmap_equiv_ext=>y ??; apply rFunctor_map_compose.
+  apply: map_fmap_equiv_ext=>y ??; apply rFunctor_map_compose.
 Qed.
 Global Instance gmapURF_contractive K `{Countable K} F :
   rFunctorContractive F → urFunctorContractive (gmapURF K F).
diff --git a/iris/algebra/lib/gmap_view.v b/iris/algebra/lib/gmap_view.v
index 390acb80b..519e1eb9f 100644
--- a/iris/algebra/lib/gmap_view.v
+++ b/iris/algebra/lib/gmap_view.v
@@ -639,10 +639,10 @@ Next Obligation.
   intros K ?? F A ? B ? x; simpl in *. rewrite -{2}(view_map_id x).
   apply (view_map_ext _ _ _ _)=> y.
   - rewrite /= -{2}(map_fmap_id y).
-    apply map_fmap_equiv_ext=>k ??.
+    apply: map_fmap_equiv_ext=>k ??.
     apply rFunctor_map_id.
   - rewrite /= -{2}(map_fmap_id y).
-    apply map_fmap_equiv_ext=>k [df va] ?.
+    apply: map_fmap_equiv_ext=>k [df va] ?.
     split; first done. simpl.
     apply rFunctor_map_id.
 Qed.
@@ -651,10 +651,10 @@ Next Obligation.
   rewrite -view_map_compose.
   apply (view_map_ext _ _ _ _)=> y.
   - rewrite /= -map_fmap_compose.
-    apply map_fmap_equiv_ext=>k ??.
+    apply: map_fmap_equiv_ext=>k ??.
     apply rFunctor_map_compose.
   - rewrite /= -map_fmap_compose.
-    apply map_fmap_equiv_ext=>k [df va] ?.
+    apply: map_fmap_equiv_ext=>k [df va] ?.
     split; first done. simpl.
     apply rFunctor_map_compose.
 Qed.
diff --git a/iris/algebra/list.v b/iris/algebra/list.v
index 3e081e416..3327138d8 100644
--- a/iris/algebra/list.v
+++ b/iris/algebra/list.v
@@ -125,10 +125,10 @@ Global Arguments listO : clear implicits.
 
 (** Non-expansiveness of higher-order list functions and big-ops *)
 Global Instance list_fmap_ne {A B : ofe} n :
-  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (fmap (M:=list) (A:=A) (B:=B)).
+  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (fmap (MA:=list A) (MB:=list B)).
 Proof. intros f1 f2 Hf l1 l2 Hl; by eapply Forall2_fmap, Forall2_impl; eauto. Qed.
 Global Instance list_omap_ne {A B : ofe} n :
-  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (omap (M:=list) (A:=A) (B:=B)).
+  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (omap (MA:=list A) (MB:=list B)).
 Proof.
   intros f1 f2 Hf. induction 1 as [|x1 x2 l1 l2 Hx Hl]; csimpl; [constructor|].
   destruct (Hf _ _ Hx); [f_equiv|]; auto.
@@ -143,9 +143,9 @@ Proof.
 Qed.
 Global Instance list_bind_ne {A B : ofe} n :
   Proper ((dist n ==> dist n) ==> dist n ==> dist n)
-         (mbind (M:=list) (A:=A) (B:=B)).
+         (mbind (A:=A) (MA:=list A) (MB:=list B)).
 Proof. intros f1 f2 Hf. induction 1; csimpl; [constructor|f_equiv; auto]. Qed.
-Global Instance list_join_ne {A : ofe} : NonExpansive (mjoin (M:=list) (A:=A)).
+Global Instance list_join_ne {A : ofe} : NonExpansive (mjoin (MA:=list A)).
 Proof. induction 1; simpl; [constructor|solve_proper]. Qed.
 Global Instance zip_with_ne {A B C : ofe} n :
   Proper ((dist n ==> dist n ==> dist n) ==> dist n ==> dist n ==> dist n)
diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index a6555c3f8..002c881ee 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -1295,13 +1295,13 @@ Global Typeclasses Opaque option_dist.
 Global Arguments optionO : clear implicits.
 
 Global Instance option_fmap_ne {A B : ofe} n:
-  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@fmap option _ A B).
+  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@fmap A B (option A) (option B) _).
 Proof. intros f f' Hf ?? []; constructor; auto. Qed.
 Global Instance option_mbind_ne {A B : ofe} n:
-  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@mbind option _ A B).
+  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@mbind A (option A) (option B) _).
 Proof. destruct 2; simpl; auto. Qed.
 Global Instance option_mjoin_ne {A : ofe} n:
-  Proper (dist n ==> dist n) (@mjoin option _ A).
+  Proper (dist n ==> dist n) (@mjoin (option A) (option (option A)) _).
 Proof. destruct 1 as [?? []|]; simpl; by constructor. Qed.
 
 Global Instance option_fmap_dist_inj {A B : ofe} (f : A → B) n :
diff --git a/iris/base_logic/lib/gen_inv_heap.v b/iris/base_logic/lib/gen_inv_heap.v
index 7923ffd12..d9b592286 100644
--- a/iris/base_logic/lib/gen_inv_heap.v
+++ b/iris/base_logic/lib/gen_inv_heap.v
@@ -85,7 +85,7 @@ Section to_inv_heap.
   Implicit Types (h : gmap L (V * (V -d> PropO))).
 
   Lemma to_inv_heap_valid h : ✓ to_inv_heap h.
-  Proof. intros l. rewrite lookup_fmap. by case (h !! l). Qed.
+  Proof. intros l. rewrite lookup_fmap. by case: (h !! l). Qed.
 
   Lemma to_inv_heap_singleton l v I :
     to_inv_heap {[l := (v, I)]} =@{inv_heap_mapUR L V} {[l := (Excl' v, to_agree I)]}.
diff --git a/iris/base_logic/lib/ghost_map.v b/iris/base_logic/lib/ghost_map.v
index d1dd18258..e76b96a91 100644
--- a/iris/base_logic/lib/ghost_map.v
+++ b/iris/base_logic/lib/ghost_map.v
@@ -99,7 +99,7 @@ Section lemmas.
     done.
   Qed.
 
-  Global Instance ghost_map_elem_combine_gives γ k v1 dq1 v2 dq2 : 
+  Global Instance ghost_map_elem_combine_gives γ k v1 dq1 v2 dq2 :
     CombineSepGives (k ↪[γ]{dq1} v1) (k ↪[γ]{dq2} v2) ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝.
   Proof.
     rewrite /CombineSepGives. iIntros "[H1 H2]".
@@ -115,7 +115,7 @@ Section lemmas.
   Qed.
 
   Global Instance ghost_map_elem_combine_as k γ dq1 dq2 v1 v2 :
-    CombineSepAs (k ↪[γ]{dq1} v1) (k ↪[γ]{dq2} v2) (k ↪[γ]{dq1 ⋅ dq2} v1) | 60. 
+    CombineSepAs (k ↪[γ]{dq1} v1) (k ↪[γ]{dq2} v2) (k ↪[γ]{dq1 ⋅ dq2} v1) | 60.
     (* higher cost than the Fractional instance [combine_sep_fractional_bwd],
        which kicks in for #qs *)
   Proof.
@@ -204,7 +204,9 @@ Section lemmas.
     ghost_map_auth γ q1 m1 -∗ ghost_map_auth γ q2 m2 -∗ ⌜(q1 + q2 ≤ 1)%Qp ∧ m1 = m2⌝.
   Proof.
     unseal. iIntros "H1 H2".
-    iCombine "H1 H2" gives %[? ?%(inj _)]%gmap_view_auth_dfrac_op_valid.
+    (* We need to explicitly specify the Inj instances instead of
+    using inj _ since we need to specify [leibnizO] for [to_agree_inj]. *)
+    iCombine "H1 H2" gives %[? ?%(map_fmap_equiv_inj _ (to_agree_inj (A:=(leibnizO _))))]%gmap_view_auth_dfrac_op_valid.
     iPureIntro. split; first done. by fold_leibniz.
   Qed.
   Lemma ghost_map_auth_agree γ q1 q2 m1 m2 :
diff --git a/iris_unstable/heap_lang/interpreter.v b/iris_unstable/heap_lang/interpreter.v
index f9f793ab7..05c597ff5 100644
--- a/iris_unstable/heap_lang/interpreter.v
+++ b/iris_unstable/heap_lang/interpreter.v
@@ -151,7 +151,7 @@ Module interp_monad.
   Proof. by inversion 1. Qed.
 
   Lemma mret_inv {A} (v: A) s v' s' :
-    mret (M:=InterpretM) v s = (inl v', s') → v = v' ∧ s = s'.
+    mret (MA:=InterpretM A) v s = (inl v', s') → v = v' ∧ s = s'.
   Proof. by inversion 1. Qed.
 
   Lemma interp_bind_inv A B (x: InterpretM A) (f: A → InterpretM B) r s s' :
@@ -176,7 +176,7 @@ Module interp_monad.
   Qed.
 
   Lemma interp_fmap_inv {A B} (f: A → B) x s v s' :
-    (fmap (M:=InterpretM) f x) s = (inl v, s') →
+    (fmap (MA:=InterpretM A) f x) s = (inl v, s') →
     ∃ v0, v = f v0 ∧ x s = (inl v0, s').
   Proof.
     rewrite /fmap /interp_fmap.
@@ -240,7 +240,7 @@ Module interp_monad.
   Qed.
 
   Lemma interp_fmap_inr_inv {A B} (f: A → B) (x: InterpretM A) s e s' :
-    (f <$> x) s = (inr e, s') →
+    (fmap (MB := InterpretM B) f x) s = (inr e, s') →
     x s = (inr e, s').
   Proof.
     rewrite /fmap /interp_fmap.
diff --git a/tests/algebra.v b/tests/algebra.v
index 16c917581..082f6e9e7 100644
--- a/tests/algebra.v
+++ b/tests/algebra.v
@@ -92,5 +92,5 @@ Proof. apply _. Qed.
 
 (** Regression test for https://gitlab.mpi-sws.org/iris/iris/-/issues/577 *)
 Lemma list_bind_ne_test {A B : ofe} (f : A → list B) :
-  NonExpansive f → NonExpansive (mbind (M:=list) f).
+  NonExpansive f → NonExpansive (mbind (MA:=list A) f).
 Proof. apply _. Qed.
-- 
GitLab