From e2ccbbc33f76b2310ffb75d30e0e86aeeaa77ca0 Mon Sep 17 00:00:00 2001
From: Simon Spies <simonspies@icloud.com>
Date: Tue, 7 Mar 2023 12:30:59 +0100
Subject: [PATCH] fixes for iris/iris!886 and iris/iris!896

---
 coq-lambda-rust.opam                          |  2 +-
 theories/lang/arc.v                           |  4 ++--
 theories/typing/fixpoint.v                    |  2 +-
 theories/typing/function.v                    |  8 +++----
 theories/typing/lib/arc.v                     |  6 +++---
 theories/typing/lib/mutex/mutex.v             |  2 +-
 theories/typing/lib/mutex/mutexguard.v        |  2 +-
 theories/typing/lib/rc/rc.v                   |  6 +++---
 theories/typing/lib/rc/weak.v                 |  2 +-
 theories/typing/lib/refcell/refcell.v         |  4 ++--
 theories/typing/lib/rwlock/rwlock.v           |  2 +-
 theories/typing/lib/rwlock/rwlockreadguard.v  |  2 +-
 theories/typing/lib/rwlock/rwlockwriteguard.v |  2 +-
 theories/typing/lib/spawn.v                   |  2 +-
 theories/typing/shr_bor.v                     |  2 +-
 theories/typing/sum.v                         |  2 +-
 theories/typing/type.v                        | 21 ++++++++++---------
 17 files changed, 36 insertions(+), 35 deletions(-)

diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index cf2dae91..cea1ed61 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -15,7 +15,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2022-08-17.0.f7475511") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2023-03-08.0.7eae77ac") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/arc.v b/theories/lang/arc.v
index 13bbf929..f30bbf1c 100644
--- a/theories/lang/arc.v
+++ b/theories/lang/arc.v
@@ -315,7 +315,7 @@ Section arc.
   Proof.
     repeat intro. subst. constructor => ?.
     rewrite /is_arc. apply view_inv_contractive.
-    destruct n; [done|by apply arc_inv_ne].
+    dist_later_intro; by apply arc_inv_ne.
   Qed.
 
   Global Instance is_arc_proper :
@@ -2211,7 +2211,7 @@ Section arc.
     iDestruct "VI" as (Vb) "[VI Hclose1]".
     iMod (arc_inv_split with "VI") as "((SMA & SDA & WUA) & IS & IW)".
 
-    iMod (GPS_SWRaw_SharedWriter_revert (strong_interp P1 (l >> 1) γi γw γsw) 
+    iMod (GPS_SWRaw_SharedWriter_revert (strong_interp P1 (l >> 1) γi γw γsw)
             with "SW SR IS") as "[SW IS]".
     iMod ("Hclose1" with "tok [SMA SDA WUA IW IS]") as "tok".
     { by iApply (arc_inv_join with "SMA SDA WUA IS IW"). }
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index 93ce1742..0389062d 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -12,7 +12,7 @@ Section fixpoint_def.
   Local Instance type_2_contractive : Contractive (Nat.iter 2 T).
   Proof using Type*.
     intros n ? **. simpl.
-    by apply dist_later_dist, type_dist2_dist_later, HT, HT, type_later_dist2_later.
+    by apply dist_later_S, type_dist2_dist_later, HT, HT, type_later_dist2_later.
   Qed.
 
   Definition type_fixpoint : type := fixpointK 2 T.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 03c0c62d..e225cedb 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -77,12 +77,12 @@ Section fn.
     Proper (pointwise_relation A (fn_params_rel (type_dist2_later n')) ==>
             type_dist2 n') fn.
   Proof.
-    intros fp1 fp2 Hfp. apply ty_of_st_type_ne. destruct n'; first done.
+    intros fp1 fp2 Hfp. apply ty_of_st_type_ne. dist_later_fin_intro.
     constructor; unfold ty_own; simpl.
     (* TODO: 'f_equiv' is slow here because reflexivity is slow. *)
     (* The clean way to do this would be to have a metric on type contexts. Oh well. *)
     intros tid vl. unfold typed_body.
-    do 12 f_equiv. f_contractive.
+    do 12 f_equiv. f_contractive_fin.
     do 18 ((eapply fp_E_proper; try reflexivity) || exact: Hfp || f_equiv).
     - rewrite !cctx_interp_singleton /=. do 5 f_equiv.
       rewrite !tctx_interp_singleton /tctx_elt_interp /=.
@@ -95,7 +95,7 @@ Section fn.
             end)%I).
       { intros Hprop. apply Hprop, list_fmap_ne; last first.
         - symmetry. eapply Forall2_impl; first apply Hfp. intros.
-          apply dist_later_dist, type_dist2_dist_later. done.
+          apply dist_later_S, type_dist2_dist_later. done.
         - solve_proper. }
       clear. intros n tid p i x y. rewrite list_dist_lookup=>/(_ i).
       case _ : (x !! i)=>[tyx|]; case  _ : (y !! i)=>[tyy|];
@@ -105,7 +105,7 @@ Section fn.
   Global Instance fn_ne n' :
     Proper (pointwise_relation A (fn_params_rel (dist n')) ==> dist n') fn.
   Proof.
-    intros ?? Hfp. apply dist_later_dist, type_dist2_dist_later.
+    intros ?? Hfp. apply dist_later_S, type_dist2_dist_later.
     apply fn_type_contractive=>u. split; last split.
     - eapply Forall2_impl; first apply Hfp. intros. simpl.
       apply type_dist_dist2. done.
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 9215c251..7c208d38 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -43,7 +43,7 @@ Section arc.
     - apply is_arc_contractive; eauto; [done|].
       solve_proper_core ltac:(fun _ => f_type_equiv || f_equiv).
     - solve_proper_core ltac:(fun _ => exact: type_dist2_S || exact: type_dist2_dist ||
-                                     f_type_equiv || f_contractive || f_equiv).
+                                     f_type_equiv || f_contractive_fin || f_equiv).
   Qed.
 
   Global Instance arc_persist_persistent tid ν γi γs γw γsw l ty :
@@ -227,7 +227,7 @@ Section arc.
   Proof.
     constructor=>/=; unfold arc, full_arc_own, shared_arc_own;
       solve_proper_core ltac:(fun _ => exact: type_dist2_S || exact: type_dist2_dist ||
-                                       f_type_equiv || f_contractive || f_equiv).
+                                       f_type_equiv || f_contractive_fin || f_equiv).
   Qed.
 
   Global Instance arc_ne : NonExpansive arc.
@@ -352,7 +352,7 @@ Section arc.
   Proof.
     constructor;
       solve_proper_core ltac:(fun _ => exact: type_dist2_S || exact: type_dist2_dist ||
-                                       f_type_equiv || f_contractive || f_equiv).
+                                       f_type_equiv || f_contractive_fin || f_equiv).
   Qed.
 
   Global Instance weak_ne : NonExpansive weak.
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index 980f71a0..8e9067d4 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -73,7 +73,7 @@ Section mutex.
   Proof.
     constructor;
       solve_proper_core ltac:(fun _ => exact: type_dist2_S ||
-                                              f_type_equiv || f_contractive || f_equiv).
+                                              f_type_equiv || f_contractive_fin || f_equiv).
   Qed.
 
   Global Instance mutex_ne : NonExpansive mutex.
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index c4fac885..9b2ac252 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -78,7 +78,7 @@ Section mguard.
   Global Instance mutexguard_type_contractive α : TypeContractive (mutexguard α).
   Proof.
     constructor;
-      solve_proper_core ltac:(fun _ => f_type_equiv || f_contractive || f_equiv
+      solve_proper_core ltac:(fun _ => f_type_equiv || f_contractive_fin || f_equiv
                                     || exact: type_dist2_S).
   Qed.
   Global Instance mutexguard_ne α : NonExpansive (mutexguard α).
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 2439c8f4..7cb63f0f 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -75,7 +75,7 @@ Section rc.
   Global Instance rc_inv_ne tid ν γ l n :
     Proper (type_dist2 n ==> dist n) (rc_inv tid ν γ l).
   Proof.
-    solve_proper_core ltac:(fun _ => f_type_equiv || f_contractive || f_equiv).
+    solve_proper_core ltac:(fun _ => f_type_equiv || f_contractive_fin || f_equiv).
   Qed.
 
   Definition rc_persist tid ν (γ : gname) (l : loc) (ty : type) : vProp Σ :=
@@ -94,7 +94,7 @@ Section rc.
     Proper (type_dist2 n ==> dist n) (rc_persist tid ν γ l).
   Proof.
     solve_proper_core ltac:(fun _ => exact: type_dist2_S || exact: type_dist2_dist ||
-                                     f_type_equiv || f_contractive || f_equiv).
+                                     f_type_equiv || f_contractive_fin || f_equiv).
   Qed.
 
   Lemma rc_persist_type_incl tid ν γ l ty1 ty2:
@@ -207,7 +207,7 @@ Section rc.
   Proof.
     constructor;
       solve_proper_core ltac:(fun _ => exact: type_dist2_S || exact: type_dist2_dist ||
-                                       f_type_equiv || f_contractive || f_equiv).
+                                       f_type_equiv || f_contractive_fin || f_equiv).
   Qed.
 
   Global Instance rc_ne : NonExpansive rc.
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 38ce5368..2970101e 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -77,7 +77,7 @@ Section weak.
   Proof.
     constructor;
       solve_proper_core ltac:(fun _ => exact: type_dist2_S || exact: type_dist2_dist ||
-                                       f_type_equiv || f_contractive || f_equiv).
+                                       f_type_equiv || f_contractive_fin || f_equiv).
   Qed.
 
   Global Instance weak_ne : NonExpansive weak.
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index 6a3cc8ce..8afd3112 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -58,7 +58,7 @@ Section refcell_inv.
     Proper (type_dist2 n ==> dist n) (refcell_inv tid l γ α).
   Proof.
     solve_proper_core
-      ltac:(fun _ => exact: type_dist2_S || f_type_equiv || f_contractive || f_equiv).
+      ltac:(fun _ => exact: type_dist2_S || f_type_equiv || f_contractive_fin || f_equiv).
   Qed.
 
   Global Instance refcell_inv_ne tid l γ α : NonExpansive (refcell_inv tid l γ α).
@@ -171,7 +171,7 @@ Section refcell.
   Proof.
     constructor;
       solve_proper_core ltac:(fun _ => exact: type_dist2_S || (eapply refcell_inv_type_ne; try reflexivity) ||
-                                              f_type_equiv || f_contractive || f_equiv).
+                                              f_type_equiv || f_contractive_fin || f_equiv).
   Qed.
 
   Global Instance refcell_ne : NonExpansive refcell.
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 48d62737..fcc9a5c7 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -218,7 +218,7 @@ Section rwlock_inv.
   Proof.
     move => ???.
     apply bi.sep_ne; [|apply bi.sep_ne]; [..|done];
-      f_contractive;
+      f_contractive_fin;
       apply bi.intuitionistically_ne.
     - apply bi.iff_ne; [done|]. apply bi.exist_ne => ?.
       apply bi.sep_ne; [done|by apply ty_own_type_dist].
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 42ee0b62..7a1855d7 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -69,7 +69,7 @@ Section rwlockreadguard.
   Proof.
     constructor;
       solve_proper_core ltac:(fun _ => exact: type_dist2_S || (eapply rwlock_proto_type_ne; try reflexivity) ||
-                                              f_type_equiv || f_contractive || f_equiv).
+                                              f_type_equiv || f_contractive_fin || f_equiv).
   Qed.
   Global Instance rwlockreadguard_ne α : NonExpansive (rwlockreadguard α).
   Proof. apply type_contractive_ne, _. Qed.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index 68196e98..57432632 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -72,7 +72,7 @@ Section rwlockwriteguard.
   Proof.
     constructor;
       solve_proper_core ltac:(fun _ => exact: type_dist2_S || (eapply rwlock_proto_type_ne; try reflexivity) ||
-                                              f_type_equiv || f_contractive || f_equiv).
+                                              f_type_equiv || f_contractive_fin || f_equiv).
   Qed.
   Global Instance rwlockwriteguard_ne α : NonExpansive (rwlockwriteguard α).
   Proof. apply type_contractive_ne, _. Qed.
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index b71c434e..d8887092 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -52,7 +52,7 @@ Section join_handle.
   Proof.
     constructor;
       solve_proper_core ltac:(fun _ => progress unfold join_inv ||
-          exact: type_dist2_dist || f_type_equiv || f_contractive || f_equiv).
+          exact: type_dist2_dist || f_type_equiv || f_contractive_fin || f_equiv).
   Qed.
   Global Instance join_handle_ne : NonExpansive join_handle.
   Proof. apply type_contractive_ne, _. Qed.
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index bc2b4eae..7ee32d3f 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -46,7 +46,7 @@ Section shr_bor.
 
   Global Instance shr_type_contractive κ : TypeContractive (shr_bor κ).
   Proof.
-    intros n ???. apply: ty_of_st_type_ne. destruct n; first done.
+    intros n ???. apply: ty_of_st_type_ne. dist_later_fin_intro.
     solve_type_proper.
   Qed.
 
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index e5f5b3ac..19d9cb58 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -99,7 +99,7 @@ Section sum.
     { clear EQmax. induction EQ as [|???? EQ _ IH]=>-[|i] //=. }
     constructor; simpl.
     - by rewrite EQmax.
-    - intros tid vl. destruct n as [|n]=> //=. rewrite /ty_own /= EQmax.
+    - intros tid vl. dist_later_fin_intro. rewrite /ty_own /= EQmax.
       solve_proper_core ltac:(fun _ => exact:EQnth || f_type_equiv || f_equiv).
     - intros κ tid l. unfold is_pad. rewrite EQmax.
       solve_proper_core ltac:(fun _ => exact:EQnth || f_type_equiv || f_equiv).
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 14289e38..8d7789d0 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -300,13 +300,14 @@ Section type_dist2.
   Proof. intros EQ. split; intros; try apply dist_dist_later; apply EQ. Qed.
   Lemma type_dist2_dist_later n ty1 ty2 : type_dist2 n ty1 ty2 → dist_later n ty1 ty2.
   Proof.
-    intros EQ. destruct n; first done. split; intros; try apply EQ.
+    intros EQ. eapply dist_later_fin_iff. destruct n; first done.
+    split; intros; try apply EQ; try si_solver.
     apply dist_S, EQ.
   Qed.
   Lemma type_later_dist2_later n ty1 ty2 : dist_later n ty1 ty2 → type_dist2_later n ty1 ty2.
-  Proof. destruct n; first done. exact: type_dist_dist2. Qed.
+  Proof. destruct n; first done. rewrite dist_later_fin_iff. exact: type_dist_dist2.  Qed.
   Lemma type_dist2_dist n ty1 ty2 : type_dist2 (S n) ty1 ty2 → dist n ty1 ty2.
-  Proof. move=>/type_dist2_dist_later. done. Qed.
+  Proof. move=>/type_dist2_dist_later. rewrite dist_later_fin_iff. done. Qed.
   Lemma type_dist2_S n ty1 ty2 : type_dist2 (S n) ty1 ty2 → type_dist2 n ty1 ty2.
   Proof. intros. apply type_dist_dist2, type_dist2_dist. done. Qed.
 
@@ -314,7 +315,7 @@ Section type_dist2.
   Proof. intros ?? EQ. apply EQ. Qed.
   Lemma ty_own_type_dist n:
     Proper (type_dist2 (S n) ==> eq ==> eq ==> dist n) ty_own.
-  Proof. intros ?? EQ ??-> ??->. apply EQ. Qed.
+  Proof. intros ?? EQ ??-> ??->. apply EQ. si_solver. Qed.
   Lemma ty_shr_type_dist n :
     Proper (type_dist2 n ==> eq ==> eq ==> eq ==> dist n) ty_shr.
   Proof. intros ?? EQ ??-> ??-> ??->. apply EQ. Qed.
@@ -357,22 +358,22 @@ Section type_contractive.
   Lemma type_contractive_type_ne T :
     TypeContractive T → TypeNonExpansive T.
   Proof.
-    intros HT ? ???. apply type_dist_dist2, dist_later_dist, type_dist2_dist_later, HT. done.
+    intros HT ? ???. eapply type_dist_dist2, dist_later_S, type_dist2_dist_later, HT. done.
   Qed.
 
   Lemma type_contractive_ne T :
     TypeContractive T → NonExpansive T.
   Proof.
-    intros HT ? ???. apply dist_later_dist, type_dist2_dist_later, HT, type_dist_dist2. done.
+    intros HT ? ???. apply dist_later_S, type_dist2_dist_later, HT, type_dist_dist2. done.
   Qed.
 
   (* Simple types *)
   Global Instance ty_of_st_type_ne n :
     Proper (dist_later n ==> type_dist2 n) ty_of_st.
   Proof.
-    intros ???. constructor.
+    intros ?? Hdst. constructor.
     - done.
-    - intros. destruct n; first done; simpl. f_equiv. done.
+    - intros. dist_later_intro. eapply Hdst.
     - intros. solve_contractive.
   Qed.
 End type_contractive.
@@ -381,11 +382,11 @@ End type_contractive.
 Ltac f_type_equiv :=
   first [ ((eapply ty_size_type_dist || eapply ty_shr_type_dist || eapply ty_own_type_dist); try reflexivity) |
           match goal with | |- @dist_later ?A _ ?n ?x ?y =>
-                            destruct n as [|n]; [exact I|change (@dist A _ n x y)]
+                            eapply dist_later_fin_iff; destruct n as [|n]; [exact I|change (@dist A _ n x y)]
           end ].
 Ltac solve_type_proper :=
   constructor;
-  solve_proper_core ltac:(fun _ => f_type_equiv || f_contractive || f_equiv).
+  solve_proper_core ltac:(fun _ => f_type_equiv || f_contractive_fin || f_equiv).
 
 
 Fixpoint shr_locsE (l : loc) (n : nat) : coPset :=
-- 
GitLab