dist_later_intro fixes.

coq-actris.opam

@@ -8,7 +8,7 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/actris/issues"
 dev-repo: "git+https://gitlab.mpi-sws.org/iris/actris.git"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2023-03-07.0.16ec64da") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2023-03-07.1.7e127436") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]

theories/channel/proto_model.v

@@ -179,7 +179,7 @@ Global Instance proto_map_aux_contractive {V}
 Proof.
   intros n rec1 rec2 Hrec p. simpl. apply proto_elim_ne=> // a m1 m2 Hm.
   f_equiv=> v p' /=. do 2 f_equiv; [done|].
-  apply Next_contractive; by f_contractive_core n' Hn'.
+  apply Next_contractive; by dist_later_intro n' Hn'.
 Qed.
 
 Definition proto_map_aux_2 {V}
@@ -239,7 +239,7 @@ Proof.
   destruct (proto_case p) as [->|(a & m & ->)]; [by rewrite !proto_map_end|].
   rewrite !proto_map_message /=.
   apply proto_message_ne=> // v p' /=. f_equiv; [done|]. f_equiv.
-  apply Next_contractive; f_contractive_core n' Hn'; eauto using dist_le with lia.
+  apply Next_contractive; dist_later_intro n' Hn'; eauto using dist_le with lia.
 Qed.
 Lemma proto_map_ext {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
     (gn1 gn2 : PROPn' -n> PROPn) (g1 g2 : PROP -n> PROP') p :
@@ -255,7 +255,7 @@ Proof.
   induction (lt_wf n) as [n _ IH]=> PROPn ? PROP ? p /=.
   destruct (proto_case p) as [->|(a & m & ->)]; [by rewrite !proto_map_end|].
   rewrite !proto_map_message /=. apply proto_message_ne=> // v p' /=. f_equiv.
-  apply Next_contractive; f_contractive_core n' Hn'; auto.
+  apply Next_contractive; dist_later_intro n' Hn'; auto.
 Qed.
 Lemma proto_map_compose {V}
    `{Hcn:!Cofe PROPn, Hcn':!Cofe PROPn', Hcn'':!Cofe PROPn'',
@@ -270,7 +270,7 @@ Proof.
     PROP ? PROP' ? PROP'' ? gn1 gn2 g1 g2 p /=.
   destruct (proto_case p) as [->|(a & c & ->)]; [by rewrite !proto_map_end|].
   rewrite !proto_map_message /=. apply proto_message_ne=> // v p' /=.
-  do 3 f_equiv. apply Next_contractive; f_contractive_core n' Hn'; simpl; auto.
+  do 3 f_equiv. apply Next_contractive; dist_later_intro n' Hn'; simpl; auto.
 Qed.
 
 Program Definition protoOF (V : Type) (Fn F : oFunctor)
@@ -302,6 +302,6 @@ Global Instance protoOF_contractive (V : Type) (Fn F : oFunctor)
 Proof.
   intros HFn HF A1 ? A2 ? B1 ? B2 ? n f g Hfg p; simpl in *.
   apply proto_map_ne=> y //=.
-  + apply HFn. f_contractive_core n' Hn'. f_equiv; apply Hfg.
-  + apply HF. by f_contractive_core n' Hn'.
+  + apply HFn. dist_later_intro n' Hn'. f_equiv; apply Hfg.
+  + apply HF. by dist_later_intro n' Hn'.
 Qed.

theories/logrel/term_types.v

@@ -115,7 +115,7 @@ Section term_types.
   Proof.
     intros A A' ? B B' ?. apply Ltty_ne=> v. f_equiv=> w.
     f_equiv; [by f_contractive|].
-    apply (wp_contractive _ _ _ _ _)=> v'. f_contractive_core n' Hn'. by f_equiv.
+    apply (wp_contractive _ _ _ _ _)=> v'. dist_later_intro n' Hn'. by f_equiv.
   Qed.
   Global Instance lty_arr_ne `{heapGS Σ} : NonExpansive2 lty_arr.
   Proof. solve_proper. Qed.
@@ -135,7 +135,7 @@ Section term_types.
   Proof.
     intros F F' A. apply Ltty_ne=> w. f_equiv=> B.
     apply (wp_contractive _ _ _ _ _)=> u. specialize (A B).
-    f_contractive_core n' Hn'. by f_equiv.
+    dist_later_intro n' Hn'. by f_equiv.
   Qed.
   Global Instance lty_forall_ne `{heapGS Σ} k n :
     Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_forall Σ _ k).

theories/utils/cofe_solver_2.v

@@ -72,14 +72,14 @@ Section cofe_solver_2.
       rewrite -{2}(ofe_iso_12 T_result y). f_equiv.
       rewrite -(oFunctor_map_id (F _) (ofe_iso_2 T_result y))
               -!oFunctor_map_compose.
-      f_equiv; apply Fcontr; f_contractive_core n' Hn'; split=> x /=;
+      f_equiv; apply Fcontr; dist_later_intro n' Hn'; split=> x /=;
         rewrite ofe_iso_21 -{2}(oFunctor_map_id (F _) x)
           -!oFunctor_map_compose; do 2 f_equiv; split=> z /=; auto.
     - intros y. apply equiv_dist=> n. revert An Hcn A Hc y.
       induction (lt_wf n) as [n _ IH]; intros An ? A ? y.
       rewrite T_iso_fun_unfold_1 T_iso_fun_unfold_2 /= ofe_iso_21.
       rewrite -(oFunctor_map_id (F _) y) -!oFunctor_map_compose.
-      f_equiv; apply Fcontr; f_contractive_core n' Hn'; split=> x /=;
+      f_equiv; apply Fcontr; dist_later_intro n' Hn'; split=> x /=;
         rewrite -{2}(ofe_iso_12 T_result x); f_equiv;
         rewrite -{2}(oFunctor_map_id (F _) (ofe_iso_2 T_result x))
                 -!oFunctor_map_compose;