Use the new LimitPreserving stuff.

It is still not as nice as it could be; we need more automation to
prove Propers.

theories/typing/fixpoint.v

@@ -36,15 +36,14 @@ Section fixpoint.
     - exists bool. apply _.
     - done.
     - (* If Copy was an Iris assertion, this would be trivial -- we'd just
-         use entails_lim once.  However, on the Coq side, it is more convenient
-         as a record -- so this is where we pay. *)
-      intros c Hc. split.
-      + intros tid vl. rewrite /PersistentP. entails_lim c; [solve_proper..|].
-        intros. apply (Hc n).
-      + intros κ tid E F l q ? ?. entails_lim c; first solve_proper.
-        * solve_proper_core ltac:(fun _ => eapply ty_size_ne || f_equiv).
-        * intros n. apply (Hc n); first done. erewrite ty_size_ne; first done.
-          rewrite conv_compl. done.
+         use limit_preserving_and directly. However, on the Coq side, it is
+         more convenient as a record -- so this is where we pay. *)
+      eapply (limit_preserving_ext (λ _, _ ∧ _)).
+      { split; (intros [H1 H2]; split; [apply H1|apply H2]). }
+      apply limit_preserving_and; repeat (apply limit_preserving_forall=> ?).
+      { apply uPred.limit_preserving_PersistentP; solve_proper. }
+      apply limit_preserving_impl, uPred.limit_preserving_entails;
+        solve_proper_core ltac:(fun _ => eapply ty_size_ne || f_equiv).
   Qed.
 
   Global Instance fixpoint_send :
@@ -55,7 +54,8 @@ Section fixpoint.
     - apply send_equiv.
     - exists bool. apply _.
     - done.
-    - intros c Hc ???. entails_lim c; [solve_proper..|]. intros n. apply Hc.
+    - repeat (apply limit_preserving_forall=> ?).
+      apply uPred.limit_preserving_entails; solve_proper.
   Qed.
 
   Global Instance fixpoint_sync :
@@ -66,7 +66,8 @@ Section fixpoint.
     - apply sync_equiv.
     - exists bool. apply _.
     - done.
-    - intros c Hc ????. entails_lim c; [solve_proper..|]. intros n. apply Hc.
+    - repeat (apply limit_preserving_forall=> ?).
+      apply uPred.limit_preserving_entails; solve_proper.
   Qed.
 
   Lemma fixpoint_unfold_eqtype E L : eqtype E L (type_fixpoint T) (T (type_fixpoint T)).
@@ -90,8 +91,8 @@ Section subtyping.
     - intros ?? EQ ?. etrans; last done. by apply equiv_subtype.
     - by eexists _.
     - intros. setoid_rewrite (fixpoint_unfold_eqtype T2). by apply H12.
-    - intros c Hc. rewrite /subtype. entails_lim c; [solve_proper..|].
-      intros n. apply Hc.
+    - repeat (apply limit_preserving_forall=> ?).
+      apply uPred.limit_preserving_entails; solve_proper.
   Qed.
 
   Lemma fixpoint_proper T1 `{TypeContractive T1} T2 `{TypeContractive T2} :
@@ -103,8 +104,8 @@ Section subtyping.
     - intros ?? EQ ?. etrans; last done. by apply equiv_eqtype.
     - by eexists _.
     - intros. setoid_rewrite (fixpoint_unfold_eqtype T2). by apply H12.
-    - intros c Hc. split; rewrite /subtype; (entails_lim c; [solve_proper..|]);
-      intros n; apply Hc.
+    - apply limit_preserving_and; repeat (apply limit_preserving_forall=> ?);
+        apply uPred.limit_preserving_entails; solve_proper.
   Qed.
 
   Lemma fixpoint_unfold_subtype_l ty T `{TypeContractive T} :

theories/typing/type.v

@@ -152,23 +152,16 @@ Section ofe.
 
   Global Instance type_cofe : Cofe typeC.
   Proof.
-    apply: (iso_cofe_subtype P type_pack type_unpack).
+    apply (iso_cofe_subtype' P type_pack type_unpack).
+    - by intros [].
     - split; [by destruct 1|by intros [[??] ?]; constructor].
     - by intros [].
-    - intros ? c. rewrite /P /=. split_and!.
-      (* TODO: Can we do these proofs without effectively going into the model? *)
-      + intros κ tid l. apply uPred.entails_equiv_and, equiv_dist=>n.
-        setoid_rewrite conv_compl; simpl.
-        apply equiv_dist, uPred.entails_equiv_and, ty_shr_persistent.
-      + intros tid vl. apply uPred.entails_equiv_and, equiv_dist=>n.
-        repeat setoid_rewrite conv_compl at 1. simpl.
-        apply equiv_dist, uPred.entails_equiv_and, ty_size_eq.
-      + intros E κ l tid q ?. apply uPred.entails_equiv_and, equiv_dist=>n.
-        setoid_rewrite conv_compl; simpl.
-        by apply equiv_dist, uPred.entails_equiv_and, ty_share.
-      + intros κ κ' tid l. apply uPred.entails_equiv_and, equiv_dist=>n.
-        setoid_rewrite conv_compl; simpl.
-        apply equiv_dist, uPred.entails_equiv_and, ty_shr_mono.
+    - (* TODO: automate this *)
+      repeat apply limit_preserving_and; repeat (apply limit_preserving_forall; intros ?).
+      + apply uPred.limit_preserving_PersistentP=> n ty1 ty2 Hty; apply Hty.
+      + apply uPred.limit_preserving_entails=> n ty1 ty2 Hty. apply Hty. by rewrite Hty.
+      + apply uPred.limit_preserving_entails=> n ty1 ty2 Hty; repeat f_equiv; apply Hty.
+      + apply uPred.limit_preserving_entails=> n ty1 ty2 Hty; repeat f_equiv; apply Hty.
   Qed.
 
   Inductive st_equiv' (ty1 ty2 : simple_type) : Prop :=