From cf7f147f0d6700bb54ac3c1411dea05b33b4bfef Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 24 Feb 2023 15:23:47 +0100
Subject: [PATCH] Fixes for iris!886.

---
 coq-actris.opam                |  2 +-
 theories/channel/proto_model.v | 18 +++++++++---------
 theories/utils/cofe_solver_2.v | 10 +++++-----
 3 files changed, 15 insertions(+), 15 deletions(-)

diff --git a/coq-actris.opam b/coq-actris.opam
index 44f1429..463852a 100644
--- a/coq-actris.opam
+++ b/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.2022-11-29.1.c44ce4c9") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2023-03-07.0.16ec64da") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/channel/proto_model.v b/theories/channel/proto_model.v
index 0a9bf8d..b331300 100644
--- a/theories/channel/proto_model.v
+++ b/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; destruct n as [|n]=> //=.
+  apply Next_contractive; by f_contractive_core n' Hn'.
 Qed.
 
 Definition proto_map_aux_2 {V}
@@ -211,8 +211,7 @@ Proof.
   induction (lt_wf n) as [n _ IH]=>
     PROPn Hcn PROPn' Hcn' PROP Hc PROP' Hc' gn g p.
   etrans; [apply equiv_dist, (fixpoint_unfold (proto_map_aux_2 gn g))|].
-  apply proto_map_aux_contractive; destruct n as [|n]; [done|]; simpl.
-  symmetry. apply: IH. lia.
+  apply proto_map_aux_contractive; constructor=> n' ?. symmetry. apply: IH. lia.
 Qed.
 Lemma proto_map_end {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
     (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
@@ -240,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; destruct n as [|n]=> //=; auto using dist_S with lia.
+  apply Next_contractive; f_contractive_core 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 :
@@ -256,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; destruct n as [|n]=> //=; auto.
+  apply Next_contractive; f_contractive_core n' Hn'; auto.
 Qed.
 Lemma proto_map_compose {V}
    `{Hcn:!Cofe PROPn, Hcn':!Cofe PROPn', Hcn'':!Cofe PROPn'',
@@ -271,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; destruct n as [|n]=> //=; auto.
+  do 3 f_equiv. apply Next_contractive; f_contractive_core n' Hn'; simpl; auto.
 Qed.
 
 Program Definition protoOF (V : Type) (Fn F : oFunctor)
@@ -301,7 +300,8 @@ Global Instance protoOF_contractive (V : Type) (Fn F : oFunctor)
   oFunctorContractive Fn → oFunctorContractive F → 
   oFunctorContractive (protoOF V Fn F).
 Proof.
-  intros ?? A1 ? A2 ? B1 ? B2 ? n f g Hfg p; simpl in *.
-  apply proto_map_ne=> //= y;
-    [destruct n; [|destruct Hfg]; by apply oFunctor_map_contractive..].
+  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'.
 Qed.
diff --git a/theories/utils/cofe_solver_2.v b/theories/utils/cofe_solver_2.v
index 91b37df..fb649ae 100644
--- a/theories/utils/cofe_solver_2.v
+++ b/theories/utils/cofe_solver_2.v
@@ -72,15 +72,15 @@ 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; destruct n as [|n]; simpl; [done|].
-      split => x /=; rewrite ofe_iso_21 -{2}(oFunctor_map_id (F _) x)
-        -!oFunctor_map_compose; do 2 f_equiv; split=> z /=; auto.
+      f_equiv; apply Fcontr; f_contractive_core 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; destruct n as [|n]; simpl; [done|].
-      split => x /=; rewrite -{2}(ofe_iso_12 T_result x); f_equiv;
+      f_equiv; apply Fcontr; f_contractive_core 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;
         do 2 f_equiv; split=> z /=; auto.
-- 
GitLab