From ba6832070dd10aa26071e9faaf290b415f8ee64e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 3 Jun 2023 12:25:23 +0200
Subject: [PATCH] update dependencies

---
 coq-lambda-rust.opam                |  2 +-
 theories/lang/heap.v                |  9 +++++----
 theories/lifetime/frac_borrow.v     |  3 +++
 theories/lifetime/lifetime_sig.v    | 12 ++++++------
 theories/lifetime/model/primitive.v | 18 ++++++++++--------
 theories/typing/lft_contexts.v      |  7 ++++---
 6 files changed, 29 insertions(+), 22 deletions(-)

diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index efa91425..9f7e2faf 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -13,7 +13,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2023-05-03.3.85295b18") | (= "dev") }
+  "coq-iris" { (= "dev.2023-06-02.4.80f55f7c") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index ef1051a5..c147dede 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -124,10 +124,11 @@ Section heap.
     AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q.
   Proof. split; first done. apply _. Qed.
 
-  Global Instance frame_mapsto p l v q1 q2 RES :
-    FrameFractionalHyps p (l ↦{q1} v) (λ q, l ↦{q} v)%I RES q1 q2 →
-    Frame p (l ↦{q1} v) (l ↦{q2} v) RES | 5.
-  Proof. apply: frame_fractional. Qed.
+  Global Instance frame_mapsto p l v q1 q2 q :
+    FrameFractionalQp q1 q2 q →
+    Frame p (l ↦{q1} v) (l ↦{q2} v) (l ↦{q} v) | 5.
+  (* FIXME: somehow Φ gets inferred wrong here. *)
+  Proof. apply: (frame_fractional _ _ _ (λ q, l ↦{q} v)%I). Qed.
 
   Global Instance heap_mapsto_vec_timeless l q vl : Timeless (l ↦∗{q} vl).
   Proof. rewrite /heap_mapsto_vec. apply _. Qed.
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index 6d1d6468..d1da97f0 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -160,6 +160,9 @@ Lemma frac_bor_lft_incl `{!invGS Σ, !lftGS Σ userE, !frac_borG Σ} κ κ' q:
 Proof.
   iIntros "#LFT#Hbor". iApply lft_incl_intro. iModIntro. iSplitR.
   - iIntros (q') "Hκ'".
+    (* FIXME we should probably have a lemma for this in Iris *)
+    assert (Fractional (λ q' : Qp, (q * q').[κ']))%I.
+    { intros ??. rewrite Qp.mul_add_distr_l lft_tok_fractional //. }
     iMod (frac_bor_acc with "LFT Hbor Hκ'") as (q'') "[>? Hclose]"; first done.
     iExists _. iFrame. iIntros "!>Hκ'". iApply "Hclose". auto.
   - iIntros "H†'".
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 1401bdcb..e3c8645f 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -89,16 +89,16 @@ Module Type lifetime_sig.
   Global Declare Instance lft_tok_fractional κ : Fractional (λ q, q.[κ])%I.
   Global Declare Instance lft_tok_as_fractional κ q :
     AsFractional q.[κ] (λ q, q.[κ])%I q.
-  Global Declare Instance frame_lft_tok p κ q1 q2 RES :
-    FrameFractionalHyps p q1.[κ] (λ q, q.[κ])%I RES q1 q2 →
-    Frame p q1.[κ] q2.[κ] RES | 5.
+  Global Declare Instance frame_lft_tok p κ q1 q2 q :
+    FrameFractionalQp q1 q2 q →
+    Frame p q1.[κ] q2.[κ] q.[κ] | 5.
 
   Global Declare Instance idx_bor_own_fractional i : Fractional (λ q, idx_bor_own q i)%I.
   Global Declare Instance idx_bor_own_as_fractional i q :
     AsFractional (idx_bor_own q i) (λ q, idx_bor_own q i)%I q.
-  Global Declare Instance frame_idx_bor_own p i q1 q2 RES :
-    FrameFractionalHyps p (idx_bor_own q1 i) (λ q, idx_bor_own q i)%I RES q1 q2 →
-    Frame p (idx_bor_own q1 i) (idx_bor_own q2 i) RES | 5.
+  Global Declare Instance frame_idx_bor_own p i q1 q2 q :
+    FrameFractionalQp q1 q2 q →
+    Frame p (idx_bor_own q1 i) (idx_bor_own q2 i) (idx_bor_own q i) | 5.
 
   Global Declare Instance positive_to_lft_inj : Inj eq eq positive_to_lft.
 
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 4c5d7294..edbf4174 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -321,10 +321,11 @@ Qed.
 Global Instance lft_tok_as_fractional κ q :
   AsFractional q.[κ] (λ q, q.[κ])%I q.
 Proof. split; first done. apply _. Qed.
-Global Instance frame_lft_tok p κ q1 q2 RES :
-  FrameFractionalHyps p q1.[κ] (λ q, q.[κ])%I RES q1 q2 →
-  Frame p q1.[κ] q2.[κ] RES | 5.
-Proof. apply: frame_fractional. Qed.
+Global Instance frame_lft_tok p κ q1 q2 q :
+    FrameFractionalQp q1 q2 q →
+    Frame p q1.[κ] q2.[κ] q.[κ] | 5.
+(* FIXME: somehow Φ gets inferred wrong here. *)
+Proof. apply: (frame_fractional _ _ _ (λ q, q.[κ])%I). Qed.
 
 Global Instance idx_bor_own_fractional i : Fractional (λ q, idx_bor_own q i)%I.
 Proof.
@@ -334,10 +335,11 @@ Qed.
 Global Instance idx_bor_own_as_fractional i q :
   AsFractional (idx_bor_own q i) (λ q, idx_bor_own q i)%I q.
 Proof. split; first done. apply _. Qed.
-Global Instance frame_idx_bor_own p i q1 q2 RES :
-  FrameFractionalHyps p (idx_bor_own q1 i) (λ q, idx_bor_own q i)%I RES q1 q2 →
-  Frame p (idx_bor_own q1 i) (idx_bor_own q2 i) RES | 5.
-Proof. apply: frame_fractional. Qed.
+Global Instance frame_idx_bor_own p i q1 q2 q :
+    FrameFractionalQp q1 q2 q →
+    Frame p (idx_bor_own q1 i) (idx_bor_own q2 i) (idx_bor_own q i) | 5.
+(* FIXME: somehow Φ gets inferred wrong here. *)
+Proof. apply: (frame_fractional _ _ _ (λ q, idx_bor_own q i)%I). Qed.
 
 (** Lifetime inclusion *)
 Lemma lft_incl_acc E κ κ' q :
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 949e0bcd..b5baaa41 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -96,9 +96,10 @@ Section lft_contexts.
   Global Instance llctx_interp_as_fractional qmax L q :
     AsFractional (llctx_interp_noend qmax L q) (llctx_interp_noend qmax L) q.
   Proof. split; first done. apply _. Qed.
-  Global Instance frame_llctx_interp p qmax L q1 q2 RES :
-    FrameFractionalHyps p (llctx_interp_noend qmax L q1) (llctx_interp_noend qmax L) RES q1 q2 →
-    Frame p (llctx_interp_noend qmax L q1) (llctx_interp_noend qmax L q2) RES | 5.
+  Global Instance frame_llctx_interp p qmax L q1 q2 q :
+    FrameFractionalQp q1 q2 q →
+    Frame p (llctx_interp_noend qmax L q1) (llctx_interp_noend qmax L q2)
+      (llctx_interp_noend qmax L q) | 5.
   Proof. apply: frame_fractional. Qed.
 
   Global Instance llctx_interp_permut qmax :
-- 
GitLab