diff --git a/opam.pins b/opam.pins
index 5c7302b34a1e97280d08790970e644cefb751a4f..dbf958d081b063ab955462c8b3bb10b663a3c0e3 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 34eefd91027b10f99c930cbc15999fb7175a4168
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq fb1712dd9da4d05ca2c919748633801934369d0d
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index d8de200fc9c3a36bb5e32ad378100c321fa5f28d..841ac12e746b6eecef9842d0130dc6821f4b715a 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -16,10 +16,16 @@ Section frac_bor.
Context `{invG Σ, lftG Σ, frac_borG Σ}.
Implicit Types E : coPset.
- Global Instance frac_bor_proper :
+ Global Instance frac_bor_contractive κ n :
+ Proper (pointwise_relation _ (dist_later n) ==> dist n) (frac_bor κ).
+ Proof. solve_contractive. Qed.
+ Global Instance frac_bor_ne κ n :
+ Proper (pointwise_relation _ (dist n) ==> dist n) (frac_bor κ).
+ Proof. solve_proper. Qed.
+ Global Instance frac_bor_proper κ :
Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (frac_bor κ).
Proof. solve_proper. Qed.
- Global Instance frac_bor_persistent : PersistentP (&frac{κ}Φ) := _.
+ Global Instance frac_bor_persistent κ : PersistentP (&frac{κ}Φ) := _.
Lemma bor_fracture φ E κ :
↑lftN ⊆ E → lft_ctx -∗ &{κ}(φ 1%Qp) ={E}=∗ &frac{κ}φ.
diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index 70f0b33d1d0e01c236499cb6341b661b52592549..16ae3d6943febf8c86dd2cd9592ff1553a70b74b 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -13,12 +13,15 @@ Section na_bor.
Context `{invG Σ, lftG Σ, na_invG Σ}
(tid : na_inv_pool_name) (N : namespace) (P : iProp Σ).
- Global Instance na_bor_persistent κ : PersistentP (&na{κ,tid,N} P) := _.
- Global Instance na_bor_proper κ :
+ Global Instance na_bor_ne κ tid N n :
+ Proper (dist n ==> dist n) (na_bor κ tid N).
+ Proof. solve_proper. Qed.
+ Global Instance na_bor_contractive κ tid N : Contractive (na_bor κ tid N).
+ Proof. solve_contractive. Qed.
+ Global Instance na_bor_proper κ tid N :
Proper ((⊣⊢) ==> (⊣⊢)) (na_bor κ tid N).
- Proof.
- intros P1 P2 EQ. apply uPred.exist_proper. intros i. by rewrite EQ.
- Qed.
+ Proof. solve_proper. Qed.
+ Global Instance na_bor_persistent κ : PersistentP (&na{κ,tid,N} P) := _.
Lemma bor_na κ E : ↑lftN ⊆ E → &{κ}P ={E}=∗ &na{κ,tid,N}P.
Proof.
diff --git a/theories/lifetime/shr_borrow.v b/theories/lifetime/shr_borrow.v
index f31b4a095f5d55ece99ed4c3c7b9d7322421c7c2..0df3676db4532358eb5731f343c4bb8ccddc9732 100644
--- a/theories/lifetime/shr_borrow.v
+++ b/theories/lifetime/shr_borrow.v
@@ -11,8 +11,11 @@ Notation "&shr{ κ } P" := (shr_bor κ P)
Section shared_bors.
Context `{invG Σ, lftG Σ} (P : iProp Σ).
- Global Instance shr_bor_proper :
- Proper ((⊣⊢) ==> (⊣⊢)) (shr_bor κ).
+ Global Instance shr_bor_ne κ n : Proper (dist n ==> dist n) (shr_bor κ).
+ Proof. solve_proper. Qed.
+ Global Instance shr_bor_contractive κ : Contractive (shr_bor κ).
+ Proof. solve_contractive. Qed.
+ Global Instance shr_bor_proper : Proper ((⊣⊢) ==> (⊣⊢)) (shr_bor κ).
Proof. solve_proper. Qed.
Global Instance shr_bor_persistent : PersistentP (&shr{κ} P) := _.
diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index 4a2aca3903b00501b8011cb1156c9e58026df70c..7a494cc5201ff63095165a649264db81b0f025f1 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -42,6 +42,30 @@ Section cont_context.
Proper ((≡ₚ) ==> (⊣⊢)) (cctx_interp tid).
Proof. solve_proper. Qed.
+ Lemma cctx_interp_cons tid x T :
+ cctx_interp tid (x :: T) ≡ (cctx_elt_interp tid x ∧ cctx_interp tid T)%I.
+ Proof.
+ iSplit.
+ - iIntros "H". iSplit; [|iIntros (??)]; iApply "H"; rewrite elem_of_cons; auto.
+ - iIntros "H". iIntros (? Hin). revert Hin. rewrite elem_of_cons=>-[->|?].
+ + by iDestruct "H" as "[H _]".
+ + iDestruct "H" as "[_ H]". by iApply "H".
+ Qed.
+
+ Lemma cctx_interp_nil tid : cctx_interp tid [] ≡ True%I.
+ Proof. iSplit; first by auto. iIntros "_". iIntros (? Hin). inversion Hin. Qed.
+
+ Lemma cctx_interp_app tid T1 T2 :
+ cctx_interp tid (T1 ++ T2) ≡ (cctx_interp tid T1 ∧ cctx_interp tid T2)%I.
+ Proof.
+ induction T1 as [|?? IH]; first by rewrite /= cctx_interp_nil left_id.
+ by rewrite /= !cctx_interp_cons IH assoc.
+ Qed.
+
+ Lemma cctx_interp_singleton tid x :
+ cctx_interp tid [x] ≡ cctx_elt_interp tid x.
+ Proof. rewrite cctx_interp_cons cctx_interp_nil right_id //. Qed.
+
Lemma fupd_cctx_interp tid C :
(|={⊤}=> cctx_interp tid C) -∗ cctx_interp tid C.
Proof.
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index 89a466d8c57bbe88640062f612230374bd6416e5..a601779a9da3592de6188fe88c28e56bf3907d6a 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -28,13 +28,11 @@ Section fixpoint.
+ intros κ tid E F l q ? ?.
apply uPred.entails_equiv_and, equiv_dist=>n. etrans.
{ apply equiv_dist, uPred.entails_equiv_and, (copy_shr_acc κ tid E F)=>//.
- by rewrite -conv_compl. }
- do 2 f_equiv; first by rewrite conv_compl. do 8 (f_contractive || f_equiv).
- * by rewrite -conv_compl.
- * destruct n. done. by setoid_rewrite conv_compl.
- * by rewrite -conv_compl.
- * f_equiv. f_contractive. unfold dist_later. destruct n=>//.
- by setoid_rewrite conv_compl.
+ by rewrite -conv_compl. }
+ symmetry. (* FIXME : this is too slow *)
+ do 2 f_equiv; first by rewrite conv_compl. set (cn:=c n).
+ repeat (apply (conv_compl n c) || f_contractive || f_equiv);
+ by rewrite conv_compl.
Qed.
Global Instance fixpoint_send :
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 87d4099009e3a70d632116db785897899a21d29c..c5a5ff50c46cade25e289d20f4889df2ebcf0b5a 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -1,16 +1,14 @@
From iris.base_logic Require Import big_op.
From iris.proofmode Require Import tactics.
+From iris.algebra Require Import vector.
From lrust.lifetime Require Import borrow.
From lrust.typing Require Export type.
From lrust.typing Require Import programs.
-(* TODO : prove contractiveness.
- Prerequisite : cofe structure on lists and vectors. *)
-
Section fn.
- Context `{typeG Σ}.
+ Context `{typeG Σ} {A : Type} {n : nat}.
- Program Definition fn {A n} (E : A → elctx)
+ Program Definition fn (E : A → elctx)
(tys : A → vec type n) (ty : A → type) : type :=
{| st_own tid vl := (∃ fb kb xb e H,
⌜vl = [@RecV fb (kb::xb) e H]⌠∗ ⌜length xb = n⌠∗
@@ -20,11 +18,47 @@ Section fn.
(zip_with (TCtx_hasty ∘ of_val) xl (tys x))
(subst_v (fb::kb::xb) (RecV fb (kb::xb) e:::k:::xl) e))%I |}.
Next Obligation.
- iIntros (A n E tys ty tid vl) "H". iDestruct "H" as (fb kb xb e ?) "[% _]". by subst.
+ iIntros (E tys ty tid vl) "H". iDestruct "H" as (fb kb xb e ?) "[% _]". by subst.
Qed.
- Global Instance fn_send {A n} E tys ty : Send (@fn A n E tys ty).
+ Global Instance fn_send E tys ty : Send (fn E tys ty).
Proof. iIntros (tid1 tid2 vl). done. Qed.
+
+ Global Instance fn_contractive n' E :
+ Proper (pointwise_relation A (dist_later n') ==>
+ pointwise_relation A (dist_later n') ==> dist n') (fn E).
+ Proof.
+ intros ?? Htys ?? Hty. unfold fn. f_equiv. rewrite st_dist_unfold /=.
+ f_contractive=>tid vl. unfold typed_body.
+ do 13 f_equiv. f_contractive. do 17 f_equiv.
+ - rewrite !cctx_interp_singleton /=. do 5 f_equiv.
+ rewrite !tctx_interp_singleton /tctx_elt_interp. do 3 f_equiv. apply Hty.
+ - rewrite /tctx_interp !big_sepL_zip_with /=. do 3 f_equiv.
+ assert (Hprop : ∀ n tid p i, Proper (dist (S n) ==> dist n)
+ (λ (l : list _), ∀ ty, ⌜l !! i = Some ty⌠→ tctx_elt_interp tid (p ◠ty))%I);
+ last by apply Hprop, Htys.
+ clear. intros n tid p i x y. rewrite list_dist_lookup=>Hxy.
+ specialize (Hxy i). destruct (x !! i) as [tyx|], (y !! i) as [tyy|];
+ inversion_clear Hxy; last done.
+ transitivity (tctx_elt_interp tid (p â— tyx));
+ last transitivity (tctx_elt_interp tid (p â— tyy)); last 2 first.
+ + unfold tctx_elt_interp. do 3 f_equiv. by apply ty_own_ne.
+ + apply equiv_dist. iSplit.
+ * iIntros "H * #EQ". by iDestruct "EQ" as %[=->].
+ * iIntros "H". by iApply "H".
+ + apply equiv_dist. iSplit.
+ * iIntros "H". by iApply "H".
+ * iIntros "H * #EQ". by iDestruct "EQ" as %[=->].
+ Qed.
+
+ Global Instance fn_ne n' E :
+ Proper (pointwise_relation A (dist n') ==>
+ pointwise_relation A (dist n') ==> dist n') (fn E).
+ Proof.
+ intros ?? H1 ?? H2.
+ apply fn_contractive=>u; destruct n'; try done; apply dist_S.
+ by apply (H1 u). by apply (H2 u).
+ Qed.
End fn.
Section typing.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index c4b8bdb69b98c8b8a1557134ecd4affd4aa7115b..c57ba87f990a6fee4ddf04654755d25203ca5da8 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -1,10 +1,8 @@
From iris.proofmode Require Import tactics.
+From iris.algebra Require Import list.
From lrust.lifetime Require Import borrow frac_borrow.
From lrust.typing Require Export type.
-(* TODO : prove contractiveness.
- Prerequisite : cofe structure on lists and vectors. *)
-
Section product.
Context `{typeG Σ}.
@@ -74,8 +72,7 @@ Section product.
Proof.
intros ?? EQ1 ?? EQ2. split; [split|]; simpl.
- by rewrite EQ1 EQ2.
- - f_contractive. destruct n=>// tid vl.
- by setoid_rewrite EQ1; setoid_rewrite EQ2.
+ - f_contractive=>tid vl. by setoid_rewrite EQ1; setoid_rewrite EQ2.
- intros ???. by rewrite EQ1 EQ2.
Qed.
@@ -150,12 +147,14 @@ Section product.
Definition product := foldr product2 unit.
+ Global Instance product_ne n: Proper (dist n ==> dist n) product.
+ Proof. intros ??. induction 1=>//=. by f_equiv. Qed.
Global Instance product_mono E L:
Proper (Forall2 (subtype E L) ==> subtype E L) product.
- Proof. intros ??. induction 1. done. by simpl; f_equiv. Qed.
+ Proof. intros ??. induction 1=>//=. by f_equiv. Qed.
Global Instance product_proper E L:
Proper (Forall2 (eqtype E L) ==> eqtype E L) product.
- Proof. intros ??. induction 1. done. by simpl; f_equiv. Qed.
+ Proof. intros ??. induction 1=>//=. by f_equiv. Qed.
Global Instance product_copy tys : LstCopy tys → Copy (product tys).
Proof. induction 1; apply _. Qed.
Global Instance product_send tys : LstSend tys → Send (product tys).
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 3496590a3450e04ff322a1f3fd76dc4a42dc8b85..ac6617e070389103e918b40b6372d71cfa37e8fb 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -32,9 +32,8 @@ Section shr_bor.
Global Instance shr_contractive κ : Contractive (shr_bor κ).
Proof.
- intros n ?? EQ. apply ty_of_st_ne. apply Next_contractive.
- destruct n=>// tid vl /=. apply uPred.exist_ne.
- repeat (apply EQ || f_contractive || f_equiv).
+ intros n ?? EQ. unfold shr_bor. f_equiv. rewrite st_dist_unfold.
+ f_contractive=> /= tid vl. repeat f_equiv. apply EQ.
Qed.
Global Instance shr_ne κ n : Proper (dist n ==> dist n) (shr_bor κ).
Proof. apply contractive_ne, _. Qed.
@@ -85,5 +84,4 @@ Section typing.
{ iExists _. iFrame "∗#". }
iMod ("Hclose" with "Hκ") as "[$ $]". iExists _. auto.
Qed.
-
End typing.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index d261ffebbd96bf2fbf45cc91290a637a3c3c093d..c3e1b0c4fc9e88f408f80a6ae7bf4a2006c33394 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -1,11 +1,9 @@
From iris.proofmode Require Import tactics.
+From iris.algebra Require Import list.
From iris.base_logic Require Import fractional.
From lrust.lifetime Require Import borrow frac_borrow.
From lrust.typing Require Export type.
-(* TODO : prove contractiveness.
- Prerequisite : cofe structure on lists and vectors. *)
-
Section sum.
Context `{typeG Σ}.
@@ -106,6 +104,23 @@ Section sum.
- iApply ((nth i tyl ∅).(ty_shr_mono) with "LFT Hord"); done.
Qed.
+ Global Instance sum_ne n: Proper (dist n ==> dist n) sum.
+ Proof.
+ intros x y EQ.
+ assert (EQmax : list_max (map ty_size x) = list_max (map ty_size y)).
+ { induction EQ as [|???? EQ _ IH]=>//=.
+ rewrite IH. f_equiv. apply EQ. }
+ assert (EQnth :∀ i, nth i x ∅ ≡{n}≡ nth i y ∅).
+ { clear EQmax. induction EQ as [|???? EQ _ IH]=>-[|i] //=. }
+ split; [split|]; simpl.
+ - by rewrite EQmax.
+ - f_contractive=>tid vl. rewrite EQmax. by setoid_rewrite EQnth.
+ - intros κ tid l. unfold is_pad. rewrite EQmax.
+ assert (EQsz : ∀ i, (nth i x ∅).(ty_size) = (nth i y ∅).(ty_size))
+ by (intros; apply EQnth).
+ repeat (rewrite EQsz || f_equiv). apply EQnth.
+ Qed.
+
Global Instance sum_mono E L :
Proper (Forall2 (subtype E L) ==> subtype E L) sum.
Proof.
@@ -117,7 +132,7 @@ Section sum.
iAssert (∀ i, type_incl (nth i tyl1 ∅) (nth i tyl2 ∅))%I with "[#]" as "#Hty".
{ iIntros (i). edestruct (nth_lookup_or_length tyl1 i) as [Hl1|Hl]; last first.
{ rewrite nth_overflow // nth_overflow; first by iApply type_incl_refl.
- by erewrite <-Forall2_length. }
+ by erewrite <-Forall2_length. }
edestruct @Forall2_lookup_l as (ty2 & Hl2 & Hty2); [done..|].
rewrite (nth_lookup_Some tyl2 _ _ ty2) //.
by iApply (Hty2 with "* [] []"). }
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 9e77427f4e7f4add1503f4c41484bd41fd9a80e4..004b4433c70545c2f394ed2f3fd29fd75ab9bd9b 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -230,9 +230,9 @@ Section ofe.
Canonical Structure typeC : ofeT := OfeT type type_ofe_mixin.
Instance st_equiv : Equiv simple_type := λ st1 st2,
- @Next (_ -c> _ -c> _) st1.(st_own) ≡ Next st2.(st_own).
+ @Next (_ -c> _ -c> _) st1.(st_own) ≡ @Next (_ -c> _ -c> _) st2.(st_own).
Instance st_dist : Dist simple_type := λ n st1 st2,
- @Next (_ -c> _ -c> _) st1.(st_own) ≡{n}≡ Next st2.(st_own).
+ @Next (_ -c> _ -c> _) st1.(st_own) ≡{n}≡ @Next (_ -c> _ -c> _) st2.(st_own).
Definition st_ofe_mixin : OfeMixin simple_type.
Proof.
@@ -247,6 +247,11 @@ Section ofe.
Canonical Structure simple_typeC : ofeT := OfeT simple_type st_ofe_mixin.
End def.
+ Lemma st_dist_unfold n (x y : simple_type) :
+ x ≡{n}≡ y ↔
+ @Next (_ -c> _ -c> _) x.(st_own) ≡{n}≡ @Next (_ -c> _ -c> _) y.(st_own).
+ Proof. done. Qed.
+
Global Instance ty_size_proper_d n:
Proper (dist n ==> eq) ty_size.
Proof. intros ?? EQ. apply EQ. Qed.
@@ -309,30 +314,7 @@ Section ofe.
Qed.
Next Obligation.
intros n c. split; [split|]; simpl; try by rewrite conv_compl.
- f_contractive. destruct n; first done. rewrite /= conv_compl //.
- Qed.
-
- Global Program Instance simple_type_cofe : Cofe simple_typeC :=
- {| compl c :=
- let 'Next st_own := compl
- {| chain_car := Next ∘ (st_own : _ -> _ -c> _ -c> _) ∘ c |} in
- {| st_own := st_own |}
- |}.
- Next Obligation. intros [c Hc]. apply Hc. Qed.
- Next Obligation.
- simpl. intros c own [=->] tid vl.
- apply uPred.entails_equiv_and, equiv_dist=>n.
- rewrite (λ c, conv_compl (A:=_ -c> _ -c> _) n c tid vl) /=.
- apply equiv_dist, uPred.entails_equiv_and, st_size_eq.
- Qed.
- Next Obligation.
- simpl. intros c own [=->] tid vl.
- apply uPred.equiv_entails, equiv_dist=>n.
- by rewrite (λ c, conv_compl (A:=_ -c> _ -c> _) n c tid vl) /=
- uPred.always_always.
- Qed.
- Next Obligation.
- intros n c. apply Next_contractive. destruct n=>//=. rewrite conv_compl //.
+ set (c n). f_contractive. rewrite conv_compl //.
Qed.
Global Instance ty_of_st_ne n : Proper (dist n ==> dist n) ty_of_st.