Merge branch 'robbert/new_contractive' into 'master'

Alternative fixes for iris!886 that do not rely on backwards compatibility layer

See merge request iris/actris!29

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}%"]

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.

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.