From 3adf6cfd8b6ec134c5a79fd5dccdf85215cd204f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 22 Feb 2017 16:19:01 +0100
Subject: [PATCH] remove lft_ctx from subtype and eqtype
---
theories/typing/borrow.v | 2 +-
theories/typing/fixpoint.v | 54 ++++++++++----------
theories/typing/function.v | 10 ++--
theories/typing/own.v | 6 +--
theories/typing/product.v | 12 ++---
theories/typing/product_split.v | 4 +-
theories/typing/shr_bor.v | 8 +--
theories/typing/sum.v | 12 ++---
theories/typing/type.v | 44 ++++++++--------
theories/typing/type_context.v | 2 +-
theories/typing/uniq_bor.v | 6 +--
theories/typing/unsafe/cell.v | 6 +--
theories/typing/unsafe/refcell/ref.v | 10 ++--
theories/typing/unsafe/refcell/ref_code.v | 2 +-
theories/typing/unsafe/refcell/refcell.v | 12 ++---
theories/typing/unsafe/refcell/refmut.v | 6 +--
theories/typing/unsafe/refcell/refmut_code.v | 2 +-
theories/typing/unsafe/spawn.v | 2 +-
18 files changed, 100 insertions(+), 100 deletions(-)
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 5e87a0b0..90bda252 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -154,7 +154,7 @@ Section borrow.
iMod ("Hclose'" with "[H↦]") as "Htok1"; first by auto.
iMod ("Hclose" with "[Htok1 Htok2]") as "($ & $)"; first by iFrame.
rewrite tctx_interp_singleton tctx_hasty_val' //.
- by iApply (ty_shr_mono with "LFT Hincl' Hshr").
+ by iApply (ty_shr_mono with "Hincl' Hshr").
Qed.
Lemma type_deref_shr_uniq {E L} κ κ' x p e ty C T T' :
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index 4c9122e9..a248f6d5 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -58,7 +58,7 @@ Section fixpoint.
Lemma fixpoint_unfold_eqtype E L : eqtype E L (fixpoint T) (T (fixpoint T)).
Proof.
unfold eqtype, subtype, type_incl. setoid_rewrite <-fixpoint_unfold.
- split; iIntros "_ _ _"; (iSplit; first done); iSplit; iIntros "!#*$".
+ split; iIntros "_ _"; (iSplit; first done); iSplit; iIntros "!#*$".
Qed.
End fixpoint.
@@ -75,30 +75,30 @@ Section subtyping.
- by eexists _.
- intros. rewrite (fixpoint_unfold_eqtype T2). by apply H12.
- intros c Hc.
- assert (Hsz : lft_ctx -∗ lft_contexts.elctx_interp_0 E -∗
+ assert (Hsz : lft_contexts.elctx_interp_0 E -∗
⌜lft_contexts.llctx_interp_0 L⌠-∗
⌜(compl c).(ty_size) = (fixpoint T2).(ty_size)âŒ).
- { 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 -∗
+ { iIntros "HE HL". rewrite (conv_compl 0 c) /=.
+ iDestruct (Hc 0%nat with "HE HL") as "[$ _]". }
+ assert (Hown : 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 _]; 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 -∗
+ apply equiv_dist, uPred.entails_equiv_and. iIntros "HE HL".
+ iDestruct (Hc (S n) with "HE HL") as "[_ [$ _]]". }
+ assert (Hshr : lft_contexts.elctx_interp_0 E -∗
⌜lft_contexts.llctx_interp_0 L⌠-∗
□ (∀ κ 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]; 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].
- + iApply (Hsz with "LFT HE HL").
- + iApply (Hown with "LFT HE HL").
- + iApply (Hshr with "LFT HE HL").
+ apply equiv_dist, uPred.entails_equiv_and. iIntros "HE HL".
+ iDestruct (Hc n with "HE HL") as "[_ [_ $]]". }
+ iIntros "HE HL". iSplit; [|iSplit].
+ + iApply (Hsz with "HE HL").
+ + iApply (Hown with "HE HL").
+ + iApply (Hshr with "HE HL").
Qed.
Lemma fixpoint_proper T1 `{Contractive T1} T2 `{Contractive T2} :
@@ -110,30 +110,30 @@ Section subtyping.
- by eexists _.
- intros. rewrite (fixpoint_unfold_eqtype T2). by apply H12.
- intros c Hc. setoid_rewrite eqtype_unfold in Hc. rewrite eqtype_unfold.
- assert (Hsz : lft_ctx -∗ lft_contexts.elctx_interp_0 E -∗
+ assert (Hsz : lft_contexts.elctx_interp_0 E -∗
⌜lft_contexts.llctx_interp_0 L⌠-∗
⌜(compl c).(ty_size) = (fixpoint T2).(ty_size)âŒ).
- { 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 -∗
+ { iIntros "HE HL". rewrite (conv_compl 0 c) /=.
+ iDestruct (Hc 0%nat with "HE HL") as "[$ _]". }
+ assert (Hown : 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 _]; 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 -∗
+ apply equiv_dist, uPred.entails_equiv_and. iIntros "HE HL".
+ iDestruct (Hc (S n) with "HE HL") as "[_ [$ _]]". }
+ assert (Hshr : lft_contexts.elctx_interp_0 E -∗
⌜lft_contexts.llctx_interp_0 L⌠-∗
□ (∀ κ 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 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].
- + iApply (Hsz with "LFT HE HL").
- + iApply (Hown with "LFT HE HL").
- + iApply (Hshr with "LFT HE HL").
+ apply equiv_dist, uPred.entails_equiv_and. iIntros "HE HL".
+ iDestruct (Hc n with "HE HL") as "[_ [_ $]]". }
+ iIntros "HE HL". iSplit; [|iSplit].
+ + iApply (Hsz with "HE HL").
+ + iApply (Hown with "HE HL").
+ + iApply (Hshr with "HE HL").
Qed.
Lemma fixpoint_unfold_subtype_l ty T `{Contractive T} :
diff --git a/theories/typing/function.v b/theories/typing/function.v
index fefa3888..9731f5be 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -94,9 +94,9 @@ Section typing.
subtype E0 L0 (fn E' tys ty) (fn E tys' ty').
Proof.
intros HE Htys Hty. apply subtype_simple_type=>//= _ vl.
- iIntros "#LFT #HE0 #HL0 Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
+ iIntros "#HE0 #HL0 Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
iExists fb, kb, xb, e, _. iSplit. done. iSplit. done. iNext.
- rewrite /typed_body. iIntros "* !# * _ Htl HE HL HC HT".
+ rewrite /typed_body. iIntros "* !# * #LFT Htl HE HL HC HT".
iDestruct (elctx_interp_persist with "HE") as "#HEp".
iMod (HE with "HE0 HL0 HE") as (qE') "[HE' Hclose]". done.
iApply ("Hf" with "LFT Htl HE' HL [HC Hclose] [HT]").
@@ -110,7 +110,7 @@ Section typing.
iDestruct "HT" as (v) "[HP Hown]". iExists v. iFrame "HP".
assert (Hst : subtype (E0 ++ E x) L0 (box (ty x)) (box (ty' x)))
by by rewrite ->Hty.
- iDestruct (Hst with "LFT [HE0 HEp] HL0") as "(_ & Hty & _)".
+ iDestruct (Hst with "[HE0 HEp] HL0") as "(_ & Hty & _)".
{ rewrite /elctx_interp_0 big_sepL_app. by iSplit. }
by iApply "Hty".
- rewrite /tctx_interp
@@ -126,7 +126,7 @@ Section typing.
specialize (Htys x). eapply Forall2_lookup_lr in Htys; try done.
assert (Hst : subtype (E0 ++ E x) L0 (box ty2') (box ty1'))
by by rewrite ->Htys.
- iDestruct (Hst with "[] [] []") as "(_ & #Ho & _)"; [done| |done|].
+ iDestruct (Hst with "[] []") as "(_ & #Ho & _)"; [ |done|].
{ rewrite /elctx_interp_0 big_sepL_app. by iSplit. }
by iApply "Ho".
Qed.
@@ -177,7 +177,7 @@ Section typing.
subtype E0 L0 (fn (n:=n) E tys ty) (fn (E ∘ σ) (tys ∘ σ) (ty ∘ σ)).
Proof.
apply subtype_simple_type=>//= _ vl.
- iIntros "#LFT _ _ Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
+ iIntros "_ _ Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
iExists fb, kb, xb, e, _. iSplit. done. iSplit. done.
rewrite /typed_body. iNext. iIntros "*". iApply "Hf".
Qed.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 95f6ade8..473df8bf 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -86,14 +86,14 @@ Section own.
iNext. iMod "Hclose'" as "_". iMod ("Hclose" with "[]") as "_"; by eauto.
Qed.
Next Obligation.
- intros _ ty κ κ' tid l. iIntros "#LFT #Hκ #H".
+ intros _ ty κ κ' tid l. iIntros "#Hκ #H".
iDestruct "H" as (l') "[Hfb #Hvs]".
iExists l'. iSplit. by iApply (frac_bor_shorten with "[]"). iIntros "!# *% Htok".
iApply (step_fupd_mask_mono F _ _ (F∖↑shrN∖↑lftN)). set_solver. set_solver.
iMod (lft_incl_acc with "Hκ Htok") as (q') "[Htok Hclose]"; first set_solver.
iMod ("Hvs" with "[%] Htok") as "Hvs'". set_solver. iModIntro. iNext.
iMod "Hvs'" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
- by iApply (ty.(ty_shr_mono) with "LFT Hκ").
+ by iApply (ty.(ty_shr_mono) with "Hκ").
Qed.
Lemma own_type_incl n ty1 ty2 :
@@ -114,7 +114,7 @@ Section own.
Proper (ctx_eq E L ==> subtype E L ==> subtype E L) own_ptr.
Proof.
intros n1 n2 Hn12 ty1 ty2 Hincl. iIntros.
- iDestruct (Hn12 with "[] [] []") as %->; [done..|].
+ iDestruct (Hn12 with "[] []") as %->; [done..|].
iApply own_type_incl. iApply Hincl; done.
Qed.
Lemma own_mono' E L n1 n2 ty1 ty2 :
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 898338ae..6e7d1121 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -10,7 +10,7 @@ Section product.
{| ty_size := 0; ty_own tid vl := ⌜vl = []âŒ%I; ty_shr κ tid l := True%I |}.
Next Obligation. iIntros (tid vl) "%". by subst. Qed.
Next Obligation. by iIntros (??????) "_ _ $". Qed.
- Next Obligation. by iIntros (????) "_ _ $". Qed.
+ Next Obligation. by iIntros (????) "_ $". Qed.
Global Instance unit0_copy : Copy unit0.
Proof.
@@ -63,8 +63,8 @@ Section product.
iModIntro. iFrame "Htok". iFrame.
Qed.
Next Obligation.
- intros ty1 ty2 κ κ' tid l. iIntros "#LFT /= #H⊑ [H1 H2]".
- iSplitL "H1"; by iApply (ty_shr_mono with "LFT H⊑").
+ intros ty1 ty2 κ κ' tid l. iIntros "/= #H⊑ [H1 H2]".
+ iSplitL "H1"; by iApply (ty_shr_mono with "H⊑").
Qed.
Global Instance product2_ne n:
@@ -80,8 +80,8 @@ Section product.
Proper (subtype E L ==> subtype E L ==> subtype E L) product2.
Proof.
iIntros (ty11 ty12 H1 ty21 ty22 H2). iIntros.
- iDestruct (H1 with "[] [] []") as "(% & #Ho1 & #Hs1)"; [done..|]. clear H1.
- iDestruct (H2 with "[] [] []") as "(% & #Ho2 & #Hs2)"; [done..|]. clear H2.
+ iDestruct (H1 with "[] []") as "(% & #Ho1 & #Hs1)"; [done..|]. clear H1.
+ iDestruct (H2 with "[] []") as "(% & #Ho2 & #Hs2)"; [done..|]. clear H2.
iSplit; first by (iPureIntro; simpl; f_equal). iSplit; iAlways.
- iIntros (??) "H". iDestruct "H" as (vl1 vl2) "(% & Hown1 & Hown2)".
iExists _, _. iSplit. done. iSplitL "Hown1".
@@ -198,7 +198,7 @@ Section typing.
last iIntros (?); iIntros (??) "H").
- iDestruct "H" as (? ?) "(% & % & ?)". by subst.
- iDestruct "H" as "(? & ?)". rewrite shift_loc_0.
- iApply (ty_shr_mono with "[] []"); [done| | done].
+ iApply ty_shr_mono; last done.
iApply lft_incl_refl.
- iExists [], _. eauto.
- simpl. rewrite shift_loc_0. by iFrame.
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index bb7955a0..2d56f54e 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -73,7 +73,7 @@ Section product_split.
iClear "IH Htyl". iExists #l. rewrite product_nil. iSplitR; first done.
assert (eqtype E L (ptr ty) (ptr (product2 ty unit))) as [Hincl _].
{ rewrite right_id. done. }
- iDestruct (Hincl with "LFT HE' HL'") as "#(_ & #Heq & _)". by iApply "Heq". }
+ iDestruct (Hincl with "HE' HL'") as "#(_ & #Heq & _)". by iApply "Heq". }
iMod ("IH" with "[] HE HL [Htyl]") as "(HE & HL & Htyl)"; first done.
{ change (ty_size ty) with (0+ty_size ty)%nat at 1.
rewrite plus_comm -hasty_ptr_offsets_offset //. }
@@ -323,4 +323,4 @@ Hint Resolve tctx_extract_split_own_prod tctx_extract_split_uniq_prod tctx_extra
*)
Hint Resolve tctx_extract_merge_own_prod tctx_extract_merge_uniq_prod tctx_extract_merge_shr_prod
| 40 : lrust_typing_merge.
-Hint Unfold extract_tyl : lrust_typing.
\ No newline at end of file
+Hint Unfold extract_tyl : lrust_typing.
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index eac5bb84..87e26d67 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -20,9 +20,9 @@ Section shr_bor.
Proper (flip (lctx_lft_incl E L) ==> subtype E L ==> subtype E L) shr_bor.
Proof.
intros κ1 κ2 Hκ ty1 ty2 Hty. apply subtype_simple_type.
- iIntros (? [|[[]|][]]) "#LFT #HE #HL H"; try done.
- iDestruct (Hκ with "HE HL") as "#Hκ". iApply (ty2.(ty_shr_mono) with "LFT Hκ").
- iDestruct (Hty with "[] [] []") as "(_ & _ & #Hs1)"; [done..|clear Hty].
+ iIntros (? [|[[]|][]]) "#HE #HL H"; try done.
+ iDestruct (Hκ with "HE HL") as "#Hκ". iApply (ty2.(ty_shr_mono) with "Hκ").
+ iDestruct (Hty with "[] []") as "(_ & _ & #Hs1)"; [done..|clear Hty].
by iApply "Hs1".
Qed.
Global Instance shr_mono_flip E L :
@@ -69,7 +69,7 @@ Section typing.
iDestruct (Hκκ' with "HE' HL'") as "Hκκ'".
rewrite /tctx_interp big_sepL_singleton big_sepL_cons big_sepL_singleton.
iDestruct "H" as ([[]|]) "[% #Hshr]"; try done. iModIntro. iSplit.
- - iExists _. iSplit. done. by iApply (ty_shr_mono with "LFT Hκκ' Hshr").
+ - iExists _. iSplit. done. by iApply (ty_shr_mono with "Hκκ' Hshr").
- iExists _. auto.
Qed.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 69de6094..dd77079d 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -19,7 +19,7 @@ Section sum.
iMod (bor_acc with "LFT Hown Htok") as "[>H _]"; first done.
iDestruct "H" as (?) "[_ []]".
Qed.
- Next Obligation. iIntros (κ κ' tid l) "#LFT #Hord []". Qed.
+ Next Obligation. iIntros (κ κ' tid l) "#Hord []". Qed.
Global Instance emp_empty : Empty type := emp.
@@ -88,11 +88,11 @@ Section sum.
by iFrame.
Qed.
Next Obligation.
- iIntros (tyl κ κ' tid l) "#LFT #Hord H".
+ iIntros (tyl κ κ' tid l) "#Hord H".
iDestruct "H" as (i) "[Hown0 Hown]". iExists i.
iSplitL "Hown0".
- by iApply (frac_bor_shorten with "Hord").
- - iApply ((nth i tyl ∅).(ty_shr_mono) with "LFT Hord"); done.
+ - iApply ((nth i tyl ∅).(ty_shr_mono) with "Hord"); done.
Qed.
Global Instance sum_ne n: Proper (dist n ==> dist n) sum.
@@ -109,16 +109,16 @@ Section sum.
- 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.
+ repeat (rewrite EQsz || apply EQnth || f_equiv).
Qed.
Global Instance sum_mono E L :
Proper (Forall2 (subtype E L) ==> subtype E L) sum.
Proof.
- iIntros (tyl1 tyl2 Htyl) "#LFT #? %".
+ iIntros (tyl1 tyl2 Htyl) "#? %".
iAssert (⌜list_max (map ty_size tyl1) = list_max (map ty_size tyl2)âŒ%I) with "[#]" as %Hleq.
{ iInduction Htyl as [|???? Hsub] "IH"; first done.
- iDestruct (Hsub with "LFT [] []") as "(% & _ & _)"; [done..|].
+ iDestruct (Hsub with "[] []") as "(% & _ & _)"; [done..|].
iDestruct "IH" as %IH. iPureIntro. simpl. inversion_clear IH. by f_equal. }
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.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index e08feeca..1f69cae8 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -43,7 +43,7 @@ Record type `{typeG Σ} :=
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
+ κ' ⊑ κ -∗ ty_shr κ tid l -∗ ty_shr κ' tid l
}.
Existing Instance ty_shr_persistent.
Instance: Params (@ty_size) 2.
@@ -166,7 +166,7 @@ Section type.
- iExFalso. by iApply (lft_tok_dead with "Hκ").
Qed.
Next Obligation.
- intros st κ κ' tid l. iIntros "#LFT #Hord H".
+ intros st κ κ' tid l. iIntros "#Hord H".
iDestruct "H" as (vl) "[#Hf #Hown]".
iExists vl. iFrame "Hown". by iApply (frac_bor_shorten with "Hord").
Qed.
@@ -229,7 +229,7 @@ Section ofe.
(∀ 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).
+ (∀ κ κ' tid l, κ' ⊑ κ -∗ 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)).
@@ -346,10 +346,10 @@ Section subtyping.
Context (E : elctx) (L : llctx).
Definition subtype (ty1 ty2 : type) : Prop :=
- lft_ctx -∗ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌠-∗ type_incl ty1 ty2.
+ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌠-∗ type_incl ty1 ty2.
(* TODO RJ: I'd really like to get rid of this definition. *)
Definition ctx_eq {A} (x1 x2 : A) : Prop :=
- lft_ctx -∗ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌠-∗ ⌜x1 = x2âŒ.
+ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌠-∗ ⌜x1 = x2âŒ.
Lemma subtype_refl ty : subtype ty ty.
Proof. iIntros. iApply type_incl_refl. Qed.
@@ -363,21 +363,21 @@ Section subtyping.
Qed.
Lemma ctx_eq_refl {A} (x : A) : ctx_eq x x.
- Proof. by iIntros "_ _ _". Qed.
+ Proof. by iIntros "_ _". Qed.
Global Instance ctx_eq_equivalent {A} : Equivalence (@ctx_eq A).
Proof.
split.
- - by iIntros (?) "_ _ _".
- - iIntros (x y Hxy) "LFT HE HL". by iDestruct (Hxy with "LFT HE HL") as %->.
- - iIntros (x y z Hxy Hyz) "LFT HE HL".
- iDestruct (Hxy with "LFT HE HL") as %->. by iApply (Hyz with "LFT HE HL").
+ - by iIntros (?) "_ _".
+ - iIntros (x y Hxy) "HE HL". by iDestruct (Hxy with "HE HL") as %->.
+ - iIntros (x y z Hxy Hyz) "HE HL".
+ iDestruct (Hxy with "HE HL") as %->. by iApply (Hyz with "HE HL").
Qed.
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_subtype : Proper (subtype ==> ctx_eq) ty_size.
- Proof. iIntros (?? Hst) "LFT HE HL". iDestruct (Hst with "LFT HE HL") as "[$ ?]". Qed.
+ Proof. iIntros (?? Hst) "HE HL". iDestruct (Hst with "HE HL") as "[$ ?]". Qed.
Global Instance ty_size_subtype_flip : Proper (flip subtype ==> ctx_eq) ty_size.
Proof. by intros ?? ->. Qed.
Lemma ty_size_subtype' ty1 ty2 :
@@ -393,21 +393,21 @@ Section subtyping.
Lemma eqtype_unfold ty1 ty2 :
eqtype ty1 ty2 ↔
- (lft_ctx -∗ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌠-∗
+ (elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌠-∗
(⌜ty1.(ty_size) = ty2.(ty_size)⌠∗
(□ ∀ tid vl, ty1.(ty_own) tid vl ↔ ty2.(ty_own) tid vl) ∗
(□ ∀ κ tid l, ty1.(ty_shr) κ tid l ↔ ty2.(ty_shr) κ tid l))%I).
Proof.
split.
- - iIntros ([EQ1 EQ2]) "#LFT #HE #HL".
- iDestruct (EQ1 with "LFT HE HL") as "[#Hsz [#H1own #H1shr]]".
- iDestruct (EQ2 with "LFT HE HL") as "[_ [#H2own #H2shr]]".
+ - iIntros ([EQ1 EQ2]) "#HE #HL".
+ iDestruct (EQ1 with "HE HL") as "[#Hsz [#H1own #H1shr]]".
+ iDestruct (EQ2 with "HE HL") as "[_ [#H2own #H2shr]]".
iSplit; last iSplit.
+ done.
+ by iIntros "!#*"; iSplit; iIntros "H"; [iApply "H1own"|iApply "H2own"].
+ by iIntros "!#*"; iSplit; iIntros "H"; [iApply "H1shr"|iApply "H2shr"].
- - intros EQ. split; iIntros "#LFT #HE #HL"; (iSplit; last iSplit);
- iDestruct (EQ with "LFT HE HL") as "[% [#Hown #Hshr]]".
+ - intros EQ. split; iIntros "#HE #HL"; (iSplit; last iSplit);
+ iDestruct (EQ with "HE HL") as "[% [#Hown #Hshr]]".
+ done.
+ iIntros "!#* H". by iApply "Hown".
+ iIntros "!#* H". by iApply "Hshr".
@@ -438,15 +438,15 @@ Section subtyping.
Proof. by intros ?? [-> _]. Qed.
Lemma subtype_simple_type (st1 st2 : simple_type) :
- (∀ tid vl, lft_ctx -∗ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌠-∗
+ (∀ tid vl, elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌠-∗
st1.(st_own) tid vl -∗ st2.(st_own) tid vl) →
subtype st1 st2.
Proof.
intros Hst. iIntros. iSplit; first done. iSplit; iAlways.
- - iIntros. iApply (Hst with "[] [] []"); done.
+ - iIntros. iApply Hst; done.
- iIntros (???) "H".
iDestruct "H" as (vl) "[Hf Hown]". iExists vl. iFrame "Hf".
- by iApply (Hst with "[] [] []").
+ by iApply Hst.
Qed.
End subtyping.
@@ -457,8 +457,8 @@ Section weakening.
E1 ⊆+ E2 → L1 ⊆+ L2 →
subtype E1 L1 ty1 ty2 → subtype E2 L2 ty1 ty2.
Proof.
- iIntros (HE12 ? Hsub) "#LFT HE HL".
- iApply (Hsub with "LFT [HE] [HL]").
+ iIntros (HE12 ? Hsub) "HE HL".
+ iApply (Hsub with "[HE] [HL]").
- rewrite /elctx_interp_0. by iApply big_sepL_submseteq.
- iDestruct "HL" as %HL. iPureIntro. intros ??. apply HL.
eauto using elem_of_submseteq.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index c1eb0393..92ef13e3 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -238,7 +238,7 @@ Section type_context.
iDestruct (elctx_interp_persist with "HE") as "#HE'".
iDestruct (llctx_interp_persist with "HL") as "#HL'".
iFrame "HE HL". iDestruct "H" as (v) "[% H]". iExists _. iFrame "%".
- iDestruct (Hst with "[] [] []") as "(_ & #Ho & _)"; [done..|by iApply "Ho"].
+ iDestruct (Hst with "[] []") as "(_ & #Ho & _)"; [done..|by iApply "Ho"].
Qed.
(* Extracting from a type context. *)
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 581891b0..53e18448 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -42,7 +42,7 @@ Section uniq_bor.
iApply step_fupd_intro. set_solver. auto.
Qed.
Next Obligation.
- intros κ0 ty κ κ' tid l. iIntros "#LFT #Hκ #H".
+ intros κ0 ty κ κ' tid l. iIntros "#Hκ #H".
iDestruct "H" as (l') "[Hfb Hvs]". iAssert (κ0∪κ' ⊑ κ0∪κ)%I as "#Hκ0".
{ iApply lft_glb_mono. iApply lft_incl_refl. done. }
iExists l'. iSplit. by iApply (frac_bor_shorten with "[]").
@@ -51,14 +51,14 @@ Section uniq_bor.
iMod (lft_incl_acc with "Hκ0 Htok") as (q') "[Htok Hclose]"; first set_solver.
iMod ("Hvs" with "[%] Htok") as "Hvs'". set_solver. iModIntro. iNext.
iMod "Hvs'" as "[#Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
- by iApply (ty_shr_mono with "LFT Hκ0").
+ by iApply (ty_shr_mono with "Hκ0").
Qed.
Global Instance uniq_mono E L :
Proper (flip (lctx_lft_incl E L) ==> eqtype E L ==> subtype E L) uniq_bor.
Proof.
intros κ1 κ2 Hκ ty1 ty2 Hty%eqtype_unfold. iIntros. iSplit; first done.
- iDestruct (Hty with "[] [] []") as "(_ & #Ho & #Hs)"; [done..|clear Hty].
+ iDestruct (Hty with "[] []") as "(_ & #Ho & #Hs)"; [done..|clear Hty].
iDestruct (Hκ with "[] []") as "#Hκ"; [done..|]. iSplit; iAlways.
- iIntros (? [|[[]|][]]) "H"; try done.
iApply (bor_shorten with "Hκ"). iApply bor_iff; last done.
diff --git a/theories/typing/unsafe/cell.v b/theories/typing/unsafe/cell.v
index ba9d6f96..690f0f73 100644
--- a/theories/typing/unsafe/cell.v
+++ b/theories/typing/unsafe/cell.v
@@ -18,7 +18,7 @@ Section cell.
iIntros (ty E κ l tid q ?) "#LFT Hown $". by iApply (bor_na with "Hown").
Qed.
Next Obligation.
- iIntros (ty ?? tid l) "#LFT #H⊑ H". by iApply (na_bor_shorten with "H⊑").
+ iIntros (ty ?? tid l) "#H⊑ H". by iApply (na_bor_shorten with "H⊑").
Qed.
Global Instance cell_ne n : Proper (dist n ==> dist n) cell.
@@ -29,8 +29,8 @@ Section cell.
Global Instance cell_mono E L : Proper (eqtype E L ==> subtype E L) cell.
Proof.
- iIntros (?? EQ%eqtype_unfold) "#LFT #HE #HL".
- iDestruct (EQ with "LFT HE HL") as "(% & #Hown & #Hshr)".
+ iIntros (?? EQ%eqtype_unfold) "#HE #HL".
+ iDestruct (EQ with "HE HL") as "(% & #Hown & #Hshr)".
iSplit; [done|iSplit; iIntros "!# * H"].
- iApply ("Hown" with "H").
- iApply na_bor_iff; last done. iSplit; iIntros "!>!# H";
diff --git a/theories/typing/unsafe/refcell/ref.v b/theories/typing/unsafe/refcell/ref.v
index 0d8000a6..e524dd99 100644
--- a/theories/typing/unsafe/refcell/ref.v
+++ b/theories/typing/unsafe/refcell/ref.v
@@ -60,7 +60,7 @@ Section ref.
iMod (bor_na with "Hb") as "#Hb". done. eauto 20.
Qed.
Next Obligation.
- iIntros (??????) "#? #? H". iDestruct "H" as (ν q γ β ty' lv lrc) "H".
+ iIntros (??????) "#? H". iDestruct "H" as (ν q γ β ty' lv lrc) "H".
iExists _, _, _, _, _, _, _. iDestruct "H" as "#(? & ? & $ & $ & $ & ?)".
iSplit; last iSplit.
- by iApply lft_incl_trans.
@@ -80,20 +80,20 @@ Section ref.
Global Instance ref_mono E L :
Proper (flip (lctx_lft_incl E L) ==> subtype E L ==> subtype E L) ref.
Proof.
- iIntros (α1 α2 Hα ty1 ty2 Hty) "#LFT #HE #HL".
- iDestruct (Hty with "LFT HE HL") as "(%&#Ho&#Hs)".
+ iIntros (α1 α2 Hα ty1 ty2 Hty) "#HE #HL".
+ iDestruct (Hty with "HE HL") as "(%&#Ho&#Hs)".
iDestruct (Hα with "HE HL") as "Hα1α2".
iSplit; [|iSplit; iAlways].
- done.
- iIntros (tid [|[[]|][|[[]|][]]]) "H"; try done.
iDestruct "H" as (ν q γ β ty') "(#Hshr & #H⊑ & #Hinv & Htok & Hown)".
iExists ν, q, γ, β, ty'. iFrame "∗#". iSplit.
- + iApply ty_shr_mono; last by iApply "Hs". done.
+ + iApply ty_shr_mono; last by iApply "Hs".
iApply lft_glb_mono. done. iApply lft_incl_refl.
+ by iApply lft_incl_trans.
- iIntros (κ tid l) "H". iDestruct "H" as (ν q γ β ty' lv lrc) "H".
iExists ν, q, γ, β, ty', lv, lrc. iDestruct "H" as "#($&$&?&?&$&$)". iSplit.
- + iApply ty_shr_mono; last by iApply "Hs". done.
+ + iApply ty_shr_mono; last by iApply "Hs".
iApply lft_glb_mono. done. iApply lft_incl_refl.
+ by iApply lft_incl_trans.
Qed.
diff --git a/theories/typing/unsafe/refcell/ref_code.v b/theories/typing/unsafe/refcell/ref_code.v
index 69bc8bed..113af696 100644
--- a/theories/typing/unsafe/refcell/ref_code.v
+++ b/theories/typing/unsafe/refcell/ref_code.v
@@ -138,7 +138,7 @@ Section ref_functions.
[ x ◠box (uninit 1); #lv ◠&shr{α}ty]%TC with "[] LFT Hna [Hα Hβ Hαβ] HL Hk");
first last.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
- iFrame. iApply (ty_shr_mono with "LFT [] Hshr"). by iApply lft_incl_glb. }
+ iFrame. iApply (ty_shr_mono with "[] Hshr"). by iApply lft_incl_glb. }
{ rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
iApply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
diff --git a/theories/typing/unsafe/refcell/refcell.v b/theories/typing/unsafe/refcell/refcell.v
index 1f30af14..2101ab0c 100644
--- a/theories/typing/unsafe/refcell/refcell.v
+++ b/theories/typing/unsafe/refcell/refcell.v
@@ -58,13 +58,13 @@ Section refcell_inv.
Lemma refcell_inv_proper E L tid l γ α ty1 ty2 :
eqtype E L ty1 ty2 →
- lft_ctx -∗ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌠-∗
+ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌠-∗
refcell_inv tid l γ α ty1 -∗ refcell_inv tid l γ α ty2.
Proof.
(* TODO : this proof is essentially [solve_proper], but within the logic.
It would easily gain from some automation. *)
- iIntros (Hty%eqtype_unfold) "#LFT #HE #HL H". unfold refcell_inv.
- iDestruct (Hty with "LFT HE HL") as "(% & Hown & Hshr)".
+ iIntros (Hty%eqtype_unfold) "#HE #HL H". unfold refcell_inv.
+ iDestruct (Hty with "HE HL") as "(% & Hown & Hshr)".
iAssert (□ (&{α} shift_loc l 1 ↦∗: ty_own ty1 tid -∗
&{α} shift_loc l 1 ↦∗: ty_own ty2 tid))%I with "[]" as "#Hb".
{ iIntros "!# H". iApply bor_iff; last done.
@@ -144,7 +144,7 @@ Section refcell.
iIntros "!>!> _". iApply step_fupd_intro; auto.
Qed.
Next Obligation.
- iIntros (?????) "LFT #Hκ H". iDestruct "H" as (α γ) "[#??]".
+ iIntros (?????) "#Hκ H". iDestruct "H" as (α γ) "[#??]".
iExists _, _. iFrame. iApply lft_incl_trans; auto.
Qed.
@@ -160,8 +160,8 @@ Section refcell.
Proof.
(* TODO : this proof is essentially [solve_proper], but within the logic.
It would easily gain from some automation. *)
- iIntros (ty1 ty2 EQ) "#LFT #HE #HL". pose proof EQ as EQ'%eqtype_unfold.
- iDestruct (EQ' with "LFT HE HL") as "(% & #Hown & #Hshr)".
+ iIntros (ty1 ty2 EQ) "#HE #HL". pose proof EQ as EQ'%eqtype_unfold.
+ iDestruct (EQ' with "HE HL") as "(% & #Hown & #Hshr)".
iSplit; [|iSplit; iIntros "!# * H"].
- iPureIntro. simpl. congruence.
- destruct vl as [|[[]|]]; try done. iDestruct "H" as "[$ H]". by iApply "Hown".
diff --git a/theories/typing/unsafe/refcell/refmut.v b/theories/typing/unsafe/refcell/refmut.v
index df19723e..f619bdaa 100644
--- a/theories/typing/unsafe/refcell/refmut.v
+++ b/theories/typing/unsafe/refcell/refmut.v
@@ -75,7 +75,7 @@ Section refmut.
iApply step_fupd_intro. set_solver. auto.
Qed.
Next Obligation.
- iIntros (??????) "#? #? H". iDestruct "H" as (lv lrc) "[#Hf #H]".
+ iIntros (??????) "#? H". iDestruct "H" as (lv lrc) "[#Hf #H]".
iExists _, _. iSplit.
- by iApply frac_bor_shorten.
- iIntros "!# * % Htok".
@@ -98,9 +98,9 @@ Section refmut.
Global Instance refmut_mono E L :
Proper (flip (lctx_lft_incl E L) ==> eqtype E L ==> subtype E L) refmut.
Proof.
- iIntros (α1 α2 Hα ty1 ty2 Hty) "#LFT #HE #HL".
+ iIntros (α1 α2 Hα ty1 ty2 Hty) "#HE #HL".
pose proof Hty as Hty'%eqtype_unfold.
- iDestruct (Hty' with "LFT HE HL") as "(%&#Ho&#Hs)".
+ iDestruct (Hty' with "HE HL") as "(%&#Ho&#Hs)".
iDestruct (Hα with "HE HL") as "Hα1α2".
iSplit; [|iSplit; iAlways].
- done.
diff --git a/theories/typing/unsafe/refcell/refmut_code.v b/theories/typing/unsafe/refcell/refmut_code.v
index 3b67b964..0214e24d 100644
--- a/theories/typing/unsafe/refcell/refmut_code.v
+++ b/theories/typing/unsafe/refcell/refmut_code.v
@@ -46,7 +46,7 @@ Section refmut_functions.
iApply (type_type _ _ _ [ x ◠box (uninit 1); #lv ◠&shr{α}ty]%TC
with "[] LFT Hna [Hα1 Hα2 Hβ Hαβ] HL Hk"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
- iFrame. iApply (ty_shr_mono with "LFT [] Hshr'"). iApply lft_incl_glb; first done.
+ iFrame. iApply (ty_shr_mono with "[] Hshr'"). iApply lft_incl_glb; first done.
iApply lft_incl_refl. }
{ rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
iApply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
diff --git a/theories/typing/unsafe/spawn.v b/theories/typing/unsafe/spawn.v
index a0c782dc..ce5c0553 100644
--- a/theories/typing/unsafe/spawn.v
+++ b/theories/typing/unsafe/spawn.v
@@ -39,7 +39,7 @@ Section join_handle.
Global Instance join_handle_mono E L :
Proper (subtype E L ==> subtype E L) join_handle.
Proof.
- iIntros (ty1 ty2 Hsub) "#? #? #?". iApply join_handle_subtype.
+ iIntros (ty1 ty2 Hsub) "#? #?". iApply join_handle_subtype.
iApply Hsub; done.
Qed.
Global Instance join_handle_proper E L :
--
GitLab