diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index c13c52b5d8b17af1744e7e493ea5b9e8ce34ad25..4c9122e99b738c411c07dc49182313ab59d2fb91 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -13,7 +13,7 @@ Section fixpoint.
(∀ `(!Copy ty), Copy (T ty)) → Copy (fixpoint T).
Proof.
intros ?. apply fixpoint_ind.
- - intros ??[[EQsz%leibniz_equiv EQown]EQshr].
+ - intros ??[EQsz%leibniz_equiv EQown EQshr].
specialize (λ tid vl, EQown tid vl). specialize (λ κ tid l, EQshr κ tid l).
simpl in *=>-[Hp Hsh]; (split; [intros ??|intros ???]).
+ revert Hp. by rewrite /PersistentP -EQown.
@@ -27,10 +27,10 @@ Section fixpoint.
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. }
- symmetry. (* FIXME : this is too slow *)
+ symmetry.
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.
+ by rewrite conv_compl. (* slow, FIXME *)
Qed.
Global Instance fixpoint_send :
@@ -78,12 +78,13 @@ Section subtyping.
assert (Hsz : lft_ctx -∗ lft_contexts.elctx_interp_0 E -∗
⌜lft_contexts.llctx_interp_0 L⌠-∗
⌜(compl c).(ty_size) = (fixpoint T2).(ty_size)âŒ).
- { iIntros "LFT HE HL". iDestruct (Hc 0%nat with "LFT HE HL") as "[$ _]". }
+ { iIntros "LFT HE HL". rewrite (conv_compl 0 c) /=.
+ iDestruct (Hc 0%nat with "LFT HE HL") as "[$ _]". }
assert (Hown : lft_ctx -∗ lft_contexts.elctx_interp_0 E -∗
⌜lft_contexts.llctx_interp_0 L⌠-∗
□ (∀ tid vl, (compl c).(ty_own) tid vl -∗ (fixpoint T2).(ty_own) tid vl)).
{ apply uPred.entails_equiv_and, equiv_dist=>n.
- destruct (conv_compl (S n) c) as [[_ Heq] _]. setoid_rewrite (λ tid vl, Heq tid vl).
+ destruct (conv_compl (S n) c) as [_ Heq _]; simpl in *. setoid_rewrite Heq.
apply equiv_dist, uPred.entails_equiv_and. iIntros "LFT HE HL".
iDestruct (Hc (S n) with "LFT HE HL") as "[_ [$ _]]". }
assert (Hshr : lft_ctx -∗ lft_contexts.elctx_interp_0 E -∗
@@ -91,7 +92,7 @@ Section subtyping.
□ (∀ κ tid l,
(compl c).(ty_shr) κ tid l -∗ (fixpoint T2).(ty_shr) κ tid l)).
{ apply uPred.entails_equiv_and, equiv_dist=>n.
- destruct (conv_compl n c) as [_ Heq]. setoid_rewrite (λ κ tid l, Heq κ tid l).
+ destruct (conv_compl n c) as [_ _ Heq]; simpl in *. setoid_rewrite Heq.
apply equiv_dist, uPred.entails_equiv_and. iIntros "LFT HE HL".
iDestruct (Hc n with "LFT HE HL") as "[_ [_ $]]". }
iIntros "LFT HE HL". iSplit; [|iSplit].
@@ -112,12 +113,13 @@ Section subtyping.
assert (Hsz : lft_ctx -∗ lft_contexts.elctx_interp_0 E -∗
⌜lft_contexts.llctx_interp_0 L⌠-∗
⌜(compl c).(ty_size) = (fixpoint T2).(ty_size)âŒ).
- { iIntros "LFT HE HL". iDestruct (Hc 0%nat with "LFT HE HL") as "[$ _]". }
+ { iIntros "LFT HE HL". rewrite (conv_compl 0 c) /=.
+ iDestruct (Hc 0%nat with "LFT HE HL") as "[$ _]". }
assert (Hown : lft_ctx -∗ lft_contexts.elctx_interp_0 E -∗
⌜lft_contexts.llctx_interp_0 L⌠-∗
□ (∀ tid vl, (compl c).(ty_own) tid vl ↔ (fixpoint T2).(ty_own) tid vl)).
{ apply uPred.entails_equiv_and, equiv_dist=>n.
- destruct (conv_compl (S n) c) as [[_ Heq] _]. setoid_rewrite (λ tid vl, Heq tid vl).
+ destruct (conv_compl (S n) c) as [_ Heq _]; simpl in *. setoid_rewrite Heq.
apply equiv_dist, uPred.entails_equiv_and. iIntros "LFT HE HL".
iDestruct (Hc (S n) with "LFT HE HL") as "[_ [$ _]]". }
assert (Hshr : lft_ctx -∗ lft_contexts.elctx_interp_0 E -∗
@@ -125,7 +127,7 @@ Section subtyping.
□ (∀ κ tid l,
(compl c).(ty_shr) κ tid l ↔ (fixpoint T2).(ty_shr) κ tid l)).
{ apply uPred.entails_equiv_and, equiv_dist=>n.
- destruct (conv_compl n c) as [_ Heq]. setoid_rewrite (λ κ tid l, Heq κ tid l).
+ destruct (conv_compl n c) as [_ _ Heq]. setoid_rewrite Heq.
apply equiv_dist, uPred.entails_equiv_and. iIntros "LFT HE HL".
iDestruct (Hc n with "LFT HE HL") as "[_ [_ $]]". }
iIntros "LFT HE HL". iSplit; [|iSplit].
diff --git a/theories/typing/function.v b/theories/typing/function.v
index b7dee7711a717f20745a921b43ff01c2490707af..6cecb4cf2c49dac7345475680368101e3beb36cf 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -29,17 +29,17 @@ Section fn.
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.
+ intros ?? Htys ?? Hty. apply ty_of_st_ne; constructor.
+ intros tid vl. destruct n' as [|n']; simpl; [done|]. unfold typed_body.
do 12 f_equiv. f_contractive. do 17 f_equiv.
- rewrite !cctx_interp_singleton /=. do 5 f_equiv.
rewrite !tctx_interp_singleton /tctx_elt_interp /=. repeat f_equiv. apply Hty.
- by rewrite (ty_size_proper_d _ _ _ (Hty _)).
+ by rewrite (ty_size_ne _ _ _ (Hty _)).
- rewrite /tctx_interp !big_sepL_zip_with /=. do 3 f_equiv.
cut (∀ n tid p i, Proper (dist (S n) ==> dist n)
(λ (l : list _), ∀ ty, ⌜l !! i = Some ty⌠→ tctx_elt_interp tid (p ◠ty))%I).
{ intros Hprop. apply Hprop, list_fmap_ne, Htys. intros ty1 ty2 Hty12.
- rewrite (ty_size_proper_d _ _ _ Hty12). by rewrite Hty12. }
+ rewrite (ty_size_ne _ _ _ Hty12). by rewrite Hty12. }
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.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index b3707114cc5a1550482ec178eee88b82204aa590..0bb33dda2d6ecdbe40b462bb9b583d071c94534f 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -131,7 +131,7 @@ Section own.
Global Instance own_contractive n : Contractive (own_ptr n).
Proof.
- intros m ?? EQ. split; [split|]; simpl.
+ intros m ?? EQ. constructor; simpl.
- done.
- destruct m=>// tid vl /=. repeat (apply EQ || f_contractive || f_equiv).
- intros κ tid l. repeat (apply EQ || f_contractive || f_equiv).
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 6a43961ebc49b0b84ae9c6fef49f7f2a516429e5..898338ae1567c91cd8ad9d0c95c095d38ab5c748 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -70,10 +70,10 @@ Section product.
Global Instance product2_ne n:
Proper (dist n ==> dist n ==> dist n) product2.
Proof.
- intros ?? EQ1 ?? EQ2. split; [split|]; simpl.
+ intros ?? EQ1 ?? EQ2. constructor; simpl.
- by rewrite EQ1 EQ2.
- - f_contractive=>tid vl. by setoid_rewrite EQ1; setoid_rewrite EQ2.
- - intros ???. by rewrite EQ1 EQ2.
+ - intros tid vs. destruct n as [|n]=>//=. by setoid_rewrite EQ1; setoid_rewrite EQ2.
+ - intros ???. by rewrite EQ1 EQ2. (* slow, FIXME *)
Qed.
Global Instance product2_mono E L:
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 8ed4d9371c95fa47f05421849fa575288e8b84d4..eac5bb844efa4c684468a1a44672cc9537d69a26 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -34,8 +34,8 @@ Section shr_bor.
Global Instance shr_contractive κ : Contractive (shr_bor κ).
Proof.
- intros n ?? EQ. unfold shr_bor. f_equiv. rewrite st_dist_unfold.
- f_contractive=> /= tid vl. repeat f_equiv. apply EQ.
+ intros n ?? EQ. apply ty_of_st_ne; constructor=> //=.
+ intros tid vl. destruct n as [n|]=>//=. repeat f_equiv. apply EQ.
Qed.
Global Instance shr_ne κ n : Proper (dist n ==> dist n) (shr_bor κ).
Proof. apply contractive_ne, _. Qed.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 2b7b157df5c2484ad63e18ef7d74ca06af442e98..69de6094161cc24fba701ec705a658d7cc3ece9c 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -103,9 +103,9 @@ Section sum.
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.
+ constructor; simpl.
- by rewrite EQmax.
- - f_contractive=>tid vl. rewrite EQmax. by setoid_rewrite EQnth.
+ - intros tid vl. destruct n as [|n]=> //=. 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).
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 86459792ec338a3c416864e91d748bfbf26560e8..e08feeca0f55b09318422fcc78ff10fa884c74b1 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -16,40 +16,50 @@ Definition lftE := ↑lftN.
Definition lrustN := nroot .@ "lrust".
Definition shrN := lrustN .@ "shr".
+Definition thread_id := na_inv_pool_name.
+
+Record type `{typeG Σ} :=
+ { ty_size : nat;
+ ty_own : thread_id → list val → iProp Σ;
+ ty_shr : lft → thread_id → loc → iProp Σ;
+
+ ty_shr_persistent κ tid l : PersistentP (ty_shr κ tid l);
+
+ ty_size_eq tid vl : ty_own tid vl -∗ ⌜length vl = ty_sizeâŒ;
+ (* The mask for starting the sharing does /not/ include the
+ namespace N, for allowing more flexibility for the user of
+ this type (typically for the [own] type). AFAIK, there is no
+ fundamental reason for this.
+ This should not be harmful, since sharing typically creates
+ invariants, which does not need the mask. Moreover, it is
+ more consistent with thread-local tokens, which we do not
+ give any.
+
+ The lifetime token is needed (a) to make the definition of simple types
+ nicer (they would otherwise require a "∨ □|=>[†κ]"), and (b) so that
+ we can have emp == sum [].
+ *)
+ ty_share E κ l tid q : lftE ⊆ E →
+ lft_ctx -∗ &{κ} (l ↦∗: ty_own tid) -∗ q.[κ] ={E}=∗
+ ty_shr κ tid l ∗ q.[κ];
+ ty_shr_mono κ κ' tid l :
+ lft_ctx -∗ κ' ⊑ κ -∗ ty_shr κ tid l -∗ ty_shr κ' tid l
+ }.
+Existing Instance ty_shr_persistent.
+Instance: Params (@ty_size) 2.
+Instance: Params (@ty_own) 2.
+Instance: Params (@ty_shr) 2.
+
+Record simple_type `{typeG Σ} :=
+ { st_own : thread_id → list val → iProp Σ;
+ st_size_eq tid vl : st_own tid vl -∗ ⌜length vl = 1%natâŒ;
+ st_own_persistent tid vl : PersistentP (st_own tid vl) }.
+Existing Instance st_own_persistent.
+Instance: Params (@st_own) 2.
+
Section type.
Context `{typeG Σ}.
- Definition thread_id := na_inv_pool_name.
-
- Record type :=
- { ty_size : nat;
- ty_own : thread_id → list val → iProp Σ;
- ty_shr : lft → thread_id → loc → iProp Σ;
-
- ty_shr_persistent κ tid l : PersistentP (ty_shr κ tid l);
-
- ty_size_eq tid vl : ty_own tid vl -∗ ⌜length vl = ty_sizeâŒ;
- (* The mask for starting the sharing does /not/ include the
- namespace N, for allowing more flexibility for the user of
- this type (typically for the [own] type). AFAIK, there is no
- fundamental reason for this.
- This should not be harmful, since sharing typically creates
- invariants, which does not need the mask. Moreover, it is
- more consistent with thread-local tokens, which we do not
- give any.
-
- The lifetime token is needed (a) to make the definition of simple types
- nicer (they would otherwise require a "∨ □|=>[†κ]"), and (b) so that
- we can have emp == sum [].
- *)
- ty_share E κ l tid q : lftE ⊆ E →
- lft_ctx -∗ &{κ} (l ↦∗: ty_own tid) -∗ q.[κ] ={E}=∗
- ty_shr κ tid l ∗ q.[κ];
- ty_shr_mono κ κ' tid l :
- lft_ctx -∗ κ' ⊑ κ -∗ ty_shr κ tid l -∗ ty_shr κ' tid l
- }.
- Global Existing Instances ty_shr_persistent.
-
(** Copy types *)
Fixpoint shr_locsE (l : loc) (n : nat) : coPset :=
match n with
@@ -135,17 +145,6 @@ Section type.
Sync ty → LstSync tys → LstSync (ty::tys) := List.Forall_cons _ _ _.
(** Simple types *)
- (* We are repeating the typeclass parameter here just to make sure
- that simple_type does depend on it. Otherwise, the coercion defined
- bellow will not be acceptable by Coq. *)
- Record simple_type `{typeG Σ} :=
- { st_own : thread_id → list val → iProp Σ;
-
- st_size_eq tid vl : st_own tid vl -∗ ⌜length vl = 1%natâŒ;
- st_own_persistent tid vl : PersistentP (st_own tid vl) }.
-
- Global Existing Instance st_own_persistent.
-
Program Definition ty_of_st (st : simple_type) : type :=
{| ty_size := 1; ty_own := st.(st_own);
@@ -162,10 +161,9 @@ Section type.
iMod (bor_exists with "LFT Hmt") as (vl) "Hmt". set_solver.
iMod (bor_sep with "LFT Hmt") as "[Hmt Hown]". set_solver.
iMod (bor_persistent with "LFT Hown") as "[Hown|#H†]". set_solver.
- - iFrame "Hκ". iMod (bor_fracture with "LFT [Hmt]") as "Hfrac"; last first.
- { iExists vl. iFrame. auto. }
- done. set_solver.
- - iExFalso. iApply (lft_tok_dead with "Hκ"). done.
+ - iFrame "Hκ".
+ iMod (bor_fracture with "LFT [Hmt]") as "Hfrac"; by eauto with iFrame.
+ - iExFalso. by iApply (lft_tok_dead with "Hκ").
Qed.
Next Obligation.
intros st κ κ' tid l. iIntros "#LFT #Hord H".
@@ -175,25 +173,25 @@ Section type.
Global Program Instance ty_of_st_copy st : Copy (ty_of_st st).
Next Obligation.
- intros st κ tid E ? l q ? HF. iIntros "#LFT #Hshr Htok Hlft".
+ iIntros (st κ tid E ? l q ? HF) "#LFT #Hshr Htok Hlft".
iDestruct (na_own_acc with "Htok") as "[$ Htok]"; first set_solver+.
iDestruct "Hshr" as (vl) "[Hf Hown]".
iMod (frac_bor_acc with "LFT Hf Hlft") as (q') "[Hmt Hclose]"; first set_solver.
- iModIntro. iExists _. iDestruct "Hmt" as "[Hmt1 Hmt2]". iSplitL "Hmt1".
- - iNext. iExists _. by iFrame.
- - iIntros "Htok2 Hmt1". iDestruct "Hmt1" as (vl') "[Hmt1 #Hown']".
- iDestruct ("Htok" with "Htok2") as "$".
- iAssert (â–· ⌜length vl = length vl'âŒ)%I as ">%".
- { iNext. iDestruct (st_size_eq with "Hown") as %->.
- iDestruct (st_size_eq with "Hown'") as %->. done. }
- iCombine "Hmt1" "Hmt2" as "Hmt". rewrite heap_mapsto_vec_op // Qp_div_2.
- iDestruct "Hmt" as "[>% Hmt]". subst. by iApply "Hclose".
+ iModIntro. iExists _. iDestruct "Hmt" as "[Hmt1 Hmt2]".
+ iSplitL "Hmt1"; first by auto with iFrame.
+ iIntros "Htok2 Hmt1". iDestruct "Hmt1" as (vl') "[Hmt1 #Hown']".
+ iDestruct ("Htok" with "Htok2") as "$".
+ iAssert (â–· ⌜length vl = length vl'âŒ)%I as ">%".
+ { iNext. iDestruct (st_size_eq with "Hown") as %->.
+ iDestruct (st_size_eq with "Hown'") as %->. done. }
+ iCombine "Hmt1" "Hmt2" as "Hmt". rewrite heap_mapsto_vec_op // Qp_div_2.
+ iDestruct "Hmt" as "[>% Hmt]". subst. by iApply "Hclose".
Qed.
Global Instance ty_of_st_sync st :
Send (ty_of_st st) → Sync (ty_of_st st).
Proof.
- iIntros (Hsend κ tid1 tid2 l) "H". iDestruct "H" as (vl) "[Hm Hown]".
+ iIntros (Hsend κ tid1 tid2 l). iDestruct 1 as (vl) "[Hm Hown]".
iExists vl. iFrame "Hm". iNext. by iApply Hsend.
Qed.
End type.
@@ -207,123 +205,119 @@ Bind Scope lrust_type_scope with type.
Section ofe.
Context `{typeG Σ}.
- (* TODO: Use the ofe_iso infrastructure from Iris. *)
- Section def.
- Definition tuple_of_type (ty : type) : prodC (prodC _ _) _ :=
- (ty.(ty_size),
- Next (ty.(ty_own) : _ -c> _ -c> _),
- ty.(ty_shr) : _ -c> _ -c> _ -c> _).
-
- Instance type_equiv : Equiv type := λ ty1 ty2,
- tuple_of_type ty1 ≡ tuple_of_type ty2.
- Instance type_dist : Dist type := λ n ty1 ty2,
- tuple_of_type ty1 ≡{n}≡ tuple_of_type ty2.
-
- Definition type_ofe_mixin : OfeMixin type.
- Proof.
- split; [|split|]; unfold equiv, dist, type_equiv, type_dist.
- - intros. apply equiv_dist.
- - by intros ?.
- - by intros ???.
- - by intros ???->.
- - by intros ????; apply dist_S.
- Qed.
-
- Canonical Structure typeC : ofeT := OfeT type type_ofe_mixin.
-
- Instance st_equiv : Equiv simple_type := λ st1 st2,
- @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 (_ -c> _ -c> _) st2.(st_own).
-
- Definition st_ofe_mixin : OfeMixin simple_type.
- Proof.
- split; [|split|]; unfold equiv, dist, st_equiv, st_dist.
- - intros. apply equiv_dist.
- - by intros ?.
- - by intros ???.
- - by intros ???->.
- - by intros ????; apply dist_S.
- Qed.
-
- 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.
+ Inductive type_equiv' (ty1 ty2 : type) : Prop :=
+ Type_equiv :
+ ty1.(ty_size) = ty2.(ty_size) →
+ (∀ tid vs, ty1.(ty_own) tid vs ≡ ty2.(ty_own) tid vs) →
+ (∀ κ tid l, ty1.(ty_shr) κ tid l ≡ ty2.(ty_shr) κ tid l) →
+ type_equiv' ty1 ty2.
+ Instance type_equiv : Equiv type := type_equiv'.
+ Inductive type_dist' (n : nat) (ty1 ty2 : type) : Prop :=
+ Type_dist :
+ ty1.(ty_size) = ty2.(ty_size) →
+ (∀ tid vs, dist_later n (ty1.(ty_own) tid vs) (ty2.(ty_own) tid vs)) →
+ (∀ κ tid l, ty1.(ty_shr) κ tid l ≡{n}≡ ty2.(ty_shr) κ tid l) →
+ type_dist' n ty1 ty2.
+ Instance type_dist : Dist type := type_dist'.
+
+ Let T := prodC
+ (prodC natC (thread_id -c> list val -c> laterC (iProp Σ)))
+ (lft -c> thread_id -c> loc -c> iProp Σ).
+ Let P (x : T) : Prop :=
+ (∀ κ tid l, PersistentP (x.2 κ tid l)) ∧
+ (∀ tid vl, (later_car (x.1.2 tid vl) : iProp Σ) -∗ ⌜length vl = x.1.1âŒ) ∧
+ (∀ E κ l tid q, lftE ⊆ E →
+ lft_ctx -∗ &{κ} (l ↦∗: λ vs, later_car (x.1.2 tid vs)) -∗
+ q.[κ] ={E}=∗ x.2 κ tid l ∗ q.[κ]) ∧
+ (∀ κ κ' tid l, lft_ctx -∗ κ' ⊑ κ -∗ x.2 κ tid l -∗ x.2 κ' tid l).
+
+ Definition type_unpack (ty : type) : T :=
+ (ty.(ty_size), λ tid vl, Next (ty.(ty_own) tid vl), ty.(ty_shr)).
+ Program Definition type_pack (x : T) (H : P x) : type :=
+ {| ty_size := x.1.1; ty_own tid vl := later_car (x.1.2 tid vl); ty_shr := x.2 |}.
+ Solve Obligations with by intros [[??] ?] (?&?&?&?).
+
+ Definition type_ofe_mixin : OfeMixin type.
+ Proof.
+ apply (iso_ofe_mixin type_unpack).
+ - split; [by destruct 1|by intros [[??] ?]; constructor].
+ - split; [by destruct 1|by intros [[??] ?]; constructor].
+ Qed.
+ Canonical Structure typeC : ofeT := OfeT type type_ofe_mixin.
+
+ Global Instance ty_size_ne n : Proper (dist n ==> eq) ty_size.
Proof. intros ?? EQ. apply EQ. Qed.
- Global Instance ty_size_proper_e :
- Proper ((≡) ==> eq) ty_size.
+ Global Instance ty_size_proper : Proper ((≡) ==> eq) ty_size.
Proof. intros ?? EQ. apply EQ. Qed.
Global Instance ty_own_ne n:
Proper (dist (S n) ==> eq ==> eq ==> dist n) ty_own.
Proof. intros ?? EQ ??-> ??->. apply EQ. Qed.
- Global Instance ty_own_proper_e:
- Proper ((≡) ==> eq ==> eq ==> (≡)) ty_own.
+ Global Instance ty_own_proper : Proper ((≡) ==> eq ==> eq ==> (≡)) ty_own.
Proof. intros ?? EQ ??-> ??->. apply EQ. Qed.
- Global Instance ty_shr_ne n:
+ Global Instance ty_shr_ne n :
Proper (dist n ==> eq ==> eq ==> eq ==> dist n) ty_shr.
Proof. intros ?? EQ ??-> ??-> ??->. apply EQ. Qed.
- Global Instance ty_shr_proper_e :
+ Global Instance ty_shr_proper :
Proper ((≡) ==> eq ==> eq ==> eq ==> (≡)) ty_shr.
Proof. intros ?? EQ ??-> ??-> ??->. apply EQ. Qed.
- Global Instance st_own_ne n:
- Proper (dist (S n) ==> eq ==> eq ==> dist n) st_own.
- Proof. intros ?? EQ ??-> ??->. apply EQ. Qed.
- Global Instance st_own_proper_e :
- Proper ((≡) ==> eq ==> eq ==> (≡)) st_own.
- Proof. intros ?? EQ ??-> ??->. apply EQ. Qed.
- Global Program Instance type_cofe : Cofe typeC :=
- {| compl c :=
- let '(ty_size, Next ty_own, ty_shr) :=
- compl {| chain_car := tuple_of_type ∘ c |}
- in
- {| ty_size := ty_size; ty_own := ty_own; ty_shr := ty_shr |}
- |}.
- Next Obligation. intros [c Hc]. apply Hc. Qed.
- Next Obligation.
- simpl. intros c _ _ shr [=_ _ ->] κ tid l.
- apply uPred.equiv_entails, equiv_dist=>n.
- by rewrite (λ c, conv_compl (A:=_ -c> _ -c> _ -c> _) n c κ tid l) /=
- uPred.always_always.
- Qed.
- Next Obligation.
- simpl. intros c sz own _ [=-> -> _] tid vl.
- apply uPred.entails_equiv_and, equiv_dist=>n.
- rewrite (λ c, conv_compl (A:=_ -c> _ -c> _) n c tid vl) /= conv_compl /=.
- apply equiv_dist, uPred.entails_equiv_and, ty_size_eq.
- Qed.
- Next Obligation.
- simpl. intros c _ own shr [=_ -> ->] E κ l tid q ?.
- apply uPred.entails_equiv_and, equiv_dist=>n.
- rewrite (λ c, conv_compl (A:=_ -c> _ -c> _ -c> _) n c κ tid l) /=.
- setoid_rewrite (λ c vl, conv_compl (A:=_ -c> _ -c> _) n c tid vl). simpl.
- etrans. { by apply equiv_dist, uPred.entails_equiv_and, (c n).(ty_share). }
- simpl. destruct n; repeat (simpl; (f_contractive || f_equiv)).
- rewrite (c.(chain_cauchy) (S n) (S (S n))) //. lia.
- Qed.
- Next Obligation.
- simpl. intros c _ _ shr [=_ _ ->] κ κ' tid l.
- apply uPred.entails_equiv_and, equiv_dist=>n.
- rewrite !(λ c, conv_compl (A:=_ -c> _ -c> _ -c> _) n c _ tid l) /=.
- apply equiv_dist, uPred.entails_equiv_and. apply ty_shr_mono.
+ Global Instance type_cofe : Cofe typeC.
+ Proof.
+ apply: (iso_cofe_subtype P type_pack type_unpack).
+ - split; [by destruct 1|by intros [[??] ?]; constructor].
+ - by intros [].
+ - intros ? c. rewrite /P /=. split_and!.
+ + 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.
+ rewrite !conv_compl /=.
+ 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.
+ rewrite -(c.(chain_cauchy) n (S n)); last lia.
+ 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.
Qed.
- Next Obligation.
- intros n c. split; [split|]; simpl; try by rewrite conv_compl.
- set (c n). f_contractive. rewrite conv_compl //.
+
+ Inductive st_equiv' (ty1 ty2 : simple_type) : Prop :=
+ St_equiv :
+ (∀ tid vs, ty1.(ty_own) tid vs ≡ ty2.(ty_own) tid vs) →
+ st_equiv' ty1 ty2.
+ Instance st_equiv : Equiv simple_type := st_equiv'.
+ Inductive st_dist' (n : nat) (ty1 ty2 : simple_type) : Prop :=
+ St_dist :
+ (∀ tid vs, dist_later n (ty1.(ty_own) tid vs) (ty2.(ty_own) tid vs)) →
+ st_dist' n ty1 ty2.
+ Instance st_dist : Dist simple_type := st_dist'.
+
+ Definition st_unpack (ty : simple_type) : thread_id -c> list val -c> laterC (iProp Σ) :=
+ λ tid vl, Next (ty.(ty_own) tid vl).
+
+ Definition st_ofe_mixin : OfeMixin simple_type.
+ Proof.
+ apply (iso_ofe_mixin st_unpack).
+ - split; [by destruct 1|by constructor].
+ - split; [by destruct 1|by constructor].
Qed.
+ Canonical Structure stC : ofeT := OfeT simple_type st_ofe_mixin.
+
+ Global Instance st_own_ne n :
+ Proper (dist (S n) ==> eq ==> eq ==> dist n) st_own.
+ Proof. intros ?? EQ ??-> ??->. apply EQ. Qed.
+ Global Instance st_own_proper : Proper ((≡) ==> eq ==> eq ==> (≡)) st_own.
+ Proof. intros ?? EQ ??-> ??->. apply EQ. Qed.
- Global Instance ty_of_st_ne n : Proper (dist n ==> dist n) ty_of_st.
+ Global Instance ty_of_st_ne : NonExpansive ty_of_st.
Proof.
- intros [][]EQ. split;[split|]=>//= κ tid l.
- repeat (f_contractive || f_equiv). apply EQ.
+ intros n ?? EQ. constructor. done. simpl.
+ - intros tid l. apply EQ.
+ - simpl. intros; repeat (f_contractive || f_equiv). apply EQ.
Qed.
+ Global Instance ty_of_st_proper : Proper ((≡) ==> (≡)) ty_of_st.
+ Proof. apply (ne_proper _). Qed.
End ofe.
Section subtyping.
@@ -382,16 +376,16 @@ Section subtyping.
Lemma equiv_subtype ty1 ty2 : ty1 ≡ ty2 → subtype ty1 ty2.
Proof. unfold subtype, type_incl=>EQ. setoid_rewrite EQ. apply subtype_refl. Qed.
- Global Instance ty_size_proper : Proper (subtype ==> ctx_eq) ty_size.
+ Global Instance ty_size_subtype : Proper (subtype ==> ctx_eq) ty_size.
Proof. iIntros (?? Hst) "LFT HE HL". iDestruct (Hst with "LFT HE HL") as "[$ ?]". Qed.
- Global Instance ty_size_proper_flip : Proper (flip subtype ==> ctx_eq) ty_size.
+ Global Instance ty_size_subtype_flip : Proper (flip subtype ==> ctx_eq) ty_size.
Proof. by intros ?? ->. Qed.
- Lemma ty_size_proper' ty1 ty2 :
+ Lemma ty_size_subtype' ty1 ty2 :
subtype ty1 ty2 → ctx_eq (ty_size ty1) (ty_size ty2).
- Proof. apply ty_size_proper. Qed.
- Lemma ty_size_proper_flip' ty1 ty2 :
+ Proof. apply ty_size_subtype. Qed.
+ Lemma ty_size_subtype_flip' ty1 ty2 :
subtype ty2 ty1 → ctx_eq (ty_size ty1) (ty_size ty2).
- Proof. apply ty_size_proper_flip. Qed.
+ Proof. apply ty_size_subtype_flip. Qed.
(* TODO: The prelude should have a symmetric closure. *)
Definition eqtype (ty1 ty2 : type) : Prop :=
@@ -471,6 +465,6 @@ Section weakening.
Qed.
End weakening.
-Hint Resolve subtype_refl eqtype_refl ctx_eq_refl ty_size_proper'
- ty_size_proper_flip': lrust_typing.
-Hint Opaque ctx_eq subtype eqtype : lrust_typing.
\ No newline at end of file
+Hint Resolve subtype_refl eqtype_refl ctx_eq_refl ty_size_subtype'
+ ty_size_subtype_flip': lrust_typing.
+Hint Opaque ctx_eq subtype eqtype : lrust_typing.
diff --git a/theories/typing/uninit.v b/theories/typing/uninit.v
index b437c900db310d351d0877a83b0604e30c602f85..294fb3721164eff16ac29a7041e4ed8fb3fa584d 100644
--- a/theories/typing/uninit.v
+++ b/theories/typing/uninit.v
@@ -43,7 +43,7 @@ Section uninit.
Lemma uninit_uninit0_eqtype E L n :
eqtype E L (uninit0 n) (uninit n).
- Proof. apply equiv_eqtype; (split; first split)=>//=. apply uninit0_sz. Qed.
+ Proof. apply equiv_eqtype; constructor=>//=. apply uninit0_sz. Qed.
Lemma uninit_product_subtype_cons {E L} (n : nat) ty tyl :
ty.(ty_size) ≤ n →
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index e5792895343245cd7e94533e53a9d6dc4f83e8e3..581891b02d0c352b1b47b5b2d06704d91a658e3f 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -81,8 +81,7 @@ Section uniq_bor.
Global Instance uniq_contractive κ : Contractive (uniq_bor κ).
Proof.
- intros n ?? EQ. split; [split|]; simpl.
- - done.
+ intros n ?? EQ. constructor=> //=.
- destruct n=>// tid vl /=. repeat (apply EQ || f_contractive || f_equiv).
- intros κ' tid l. repeat (apply EQ || f_contractive || f_equiv).
Qed.
diff --git a/theories/typing/unsafe/cell.v b/theories/typing/unsafe/cell.v
index 554c95ef47b1bc862085f670ba129c7ad851fba1..2bcbc1906370a38801102528fdf5c82f2bf23850 100644
--- a/theories/typing/unsafe/cell.v
+++ b/theories/typing/unsafe/cell.v
@@ -23,7 +23,7 @@ Section cell.
Global Instance cell_ne n : Proper (dist n ==> dist n) cell.
Proof.
- intros ?? EQ. split; [split|]; simpl; try apply EQ.
+ intros ?? EQ. constructor; simpl; try apply EQ.
intros κ tid l. repeat (apply EQ || f_contractive || f_equiv).
Qed.
diff --git a/theories/typing/unsafe/refcell/ref.v b/theories/typing/unsafe/refcell/ref.v
index 93e7cf567fcdc21c8b32e5301754a2eb106d6461..9e9f8c0afc53e9e71a3ea7970cfd97f05365ff48 100644
--- a/theories/typing/unsafe/refcell/ref.v
+++ b/theories/typing/unsafe/refcell/ref.v
@@ -62,8 +62,8 @@ Section ref.
Global Instance ref_contractive α : Contractive (ref α).
Proof.
- intros n ?? EQ. unfold ref. split; [split|]=>//=.
- - f_contractive=>tid vl. repeat (f_contractive || f_equiv). apply EQ.
+ intros n ?? EQ. unfold ref. constructor=>//=.
+ - intros tid vl. destruct n as [|n]=>//=. repeat (f_contractive || f_equiv). apply EQ.
- intros κ tid l. repeat (f_contractive || f_equiv). apply EQ.
Qed.
Global Instance ref_ne n α : Proper (dist n ==> dist n) (ref α).
diff --git a/theories/typing/unsafe/refcell/refcell.v b/theories/typing/unsafe/refcell/refcell.v
index 31a8afee7b6b4aac7653121b6d9eeda4d3450cd6..0eb1bb4deec190ecfa221bddd3f94e31d946efbe 100644
--- a/theories/typing/unsafe/refcell/refcell.v
+++ b/theories/typing/unsafe/refcell/refcell.v
@@ -143,9 +143,9 @@ Section refcell.
Global Instance refcell_ne n : Proper (dist n ==> dist n) refcell.
Proof.
- move=>ty1 ty2 Hty. split; [split|]; simpl.
+ move=>ty1 ty2 Hty. constructor; simpl.
- f_equiv. apply Hty.
- - f_contractive=>tid vl. repeat f_equiv. apply Hty.
+ - intros tid vl. destruct n as [|n]=>//=. repeat f_equiv. apply Hty.
- intros κ tid l. by repeat f_equiv.
Qed.
diff --git a/theories/typing/unsafe/refcell/refmut.v b/theories/typing/unsafe/refcell/refmut.v
index 1c7b2b00fe2bc8622c70e145f4cba9dbd70967c0..36a86ad35098fe05ccc1638eaa6f1e23d9106bd6 100644
--- a/theories/typing/unsafe/refcell/refmut.v
+++ b/theories/typing/unsafe/refcell/refmut.v
@@ -78,8 +78,8 @@ Section refmut.
Global Instance refmut_contractive α : Contractive (refmut α).
Proof.
- intros n ?? EQ. unfold refmut. split; [split|]=>//=.
- - f_contractive=>tid vl. repeat (f_contractive || f_equiv). apply EQ.
+ intros n ?? EQ. unfold refmut. constructor=>//=.
+ - intros tid vl. destruct n as [|n]=>//=. repeat (f_contractive || f_equiv). apply EQ.
- intros κ tid l. repeat (f_contractive || f_equiv). apply EQ.
Qed.
Global Instance refmut_ne n α : Proper (dist n ==> dist n) (refmut α).