From 6d36b8cfbe2e7dbeda13889b17ef4b168d6953cf Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 13 Feb 2017 22:52:49 +0100
Subject: [PATCH] Bump iris. Simplify some proofs.
---
opam.pins | 2 +-
theories/typing/bool.v | 5 +--
theories/typing/borrow.v | 18 ++++-----
theories/typing/int.v | 20 ++++------
theories/typing/own.v | 26 ++++++-------
theories/typing/product_split.v | 39 ++++++++-----------
theories/typing/shr_bor.v | 17 +++-----
theories/typing/sum.v | 14 ++-----
theories/typing/type_sum.v | 9 ++---
theories/typing/uniq_bor.v | 20 +++++-----
theories/typing/unsafe/cell.v | 5 +--
theories/typing/unsafe/refcell/ref.v | 6 +--
theories/typing/unsafe/refcell/ref_code.v | 8 ++--
theories/typing/unsafe/refcell/refcell_code.v | 19 ++++-----
theories/typing/unsafe/refcell/refmut.v | 2 +-
theories/typing/unsafe/refcell/refmut_code.v | 8 ++--
theories/typing/unsafe/spawn.v | 10 ++---
17 files changed, 92 insertions(+), 136 deletions(-)
diff --git a/opam.pins b/opam.pins
index 221e0a3f..9db15430 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq f1b30a2eb12d38bffd8a0aa541c90e3675af2a29
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq ea64fd148b56e1c38c08c2954e76bfa2e75b4db9
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index eecf25ec..5806a9ee 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -13,7 +13,7 @@ Section bool.
| [ #(LitInt (0|1))] => True
| _ => False
end%I |}.
- Next Obligation. intros ? [|[[| |[|[]|]]|] []]; try iIntros "[]"; auto. Qed.
+ Next Obligation. intros ? [|[[| |[|[]|]]|] []]; iStartProof; auto. Qed.
Next Obligation. intros ? [|[[| |[|[]|]]|] []]; apply _. Qed.
Global Instance bool_send : Send bool.
@@ -46,8 +46,7 @@ Section typing.
iIntros (Hp He1 He2) "!#". iIntros (tid qE) "#LFT Htl HE HL HC HT".
iDestruct (big_sepL_elem_of _ _ _ Hp with "HT") as "#Hp".
wp_bind p. iApply (wp_hasty with "Hp").
- iIntros ([[| |[|[]|]]|]) "_ H1"; try iDestruct "H1" as "[]";
- (iApply wp_case; [done..|iNext]).
+ iIntros ([[| |[|[]|]]|]) "_ H1"; try done; (iApply wp_case; [done..|iNext]).
- iApply (He2 with "LFT Htl HE HL HC HT").
- iApply (He1 with "LFT Htl HE HL HC HT").
Qed.
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 1ea3d962..3c697b63 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -17,8 +17,8 @@ Section borrow.
Proof.
iIntros (tid ??) "#LFT $ $ H".
rewrite /tctx_interp big_sepL_singleton big_sepL_cons big_sepL_singleton.
- iDestruct "H" as ([[]|]) "[% Hown]"; try iDestruct "Hown" as "[]".
- iDestruct "Hown" as "[Hmt ?]". iMod (bor_create with "LFT Hmt") as "[Hbor Hext]". done.
+ iDestruct "H" as ([[]|]) "[% Hown]"; try done. iDestruct "Hown" as "[Hmt ?]".
+ iMod (bor_create with "LFT Hmt") as "[Hbor Hext]". done.
iModIntro. iSplitL "Hbor".
- iExists _. auto.
- iExists _. iSplit. done. by iFrame.
@@ -50,8 +50,7 @@ Section borrow.
iIntros (Hκ) "!#". iIntros (tid qE) "#LFT $ HE HL Hp".
rewrite tctx_interp_singleton.
iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
- wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown";
- (try iDestruct "Hown" as "[]").
+ wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
iMod (bor_acc_cons with "LFT Hown Htok") as "[H↦ Hclose']". done.
iDestruct "H↦" as ([|[[|l'|]|][]]) "[>H↦ Hown]"; try iDestruct "Hown" as ">[]".
iDestruct "Hown" as "[Hown H†]". rewrite heap_mapsto_vec_singleton -wp_fupd. wp_read.
@@ -83,8 +82,8 @@ Section borrow.
iIntros (Hκ) "!#". iIntros (tid qE) "#LFT $ HE HL Hp".
rewrite tctx_interp_singleton.
iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first set_solver.
- wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown";
- (try iDestruct "Hown" as "[]"). iDestruct "Hown" as (l') "#[H↦b #Hown]".
+ wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
+ iDestruct "Hown" as (l') "#[H↦b #Hown]".
iMod (frac_bor_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
iApply (wp_fupd_step _ (_∖_) with "[Hown Htok2]"); try done.
- iApply ("Hown" with "[%] Htok2"). set_solver+.
@@ -113,8 +112,7 @@ Section borrow.
iPoseProof (Hincl with "[#] [#]") as "Hincl".
{ by iApply elctx_interp_persist. } { by iApply llctx_interp_persist. }
iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
- wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown";
- try iDestruct "Hown" as "[]".
+ wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
iMod (bor_exists with "LFT Hown") as (vl) "Hbor". done.
iMod (bor_sep with "LFT Hbor") as "[H↦ Hbor]". done.
destruct vl as [|[[]|][]];
@@ -149,8 +147,8 @@ Section borrow.
iPoseProof (Hincl with "[#] [#]") as "Hincl".
{ by iApply elctx_interp_persist. } { by iApply llctx_interp_persist. }
iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first set_solver.
- wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hshr";
- try iDestruct "Hshr" as "[]". iDestruct "Hshr" as (l') "[H↦ Hown]".
+ wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hshr"; try done.
+ iDestruct "Hshr" as (l') "[H↦ Hown]".
iMod (frac_bor_acc with "LFT H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
iAssert (κ ⊑ κ' ∪ κ)%I as "#Hincl'".
{ iApply (lft_incl_glb with "Hincl []"). iApply lft_incl_refl. }
diff --git a/theories/typing/int.v b/theories/typing/int.v
index fc156b3c..af9b3615 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -12,7 +12,7 @@ Section int.
| [ #(LitInt z)] => True
| _ => False
end%I |}.
- Next Obligation. intros ? [|[[]|] []]; try iIntros "[]". auto. Qed.
+ Next Obligation. intros ? [|[[]|] []]; iStartProof; auto. Qed.
Next Obligation. intros ? [|[[]|] []]; apply _. Qed.
Global Instance int_send : Send int.
@@ -42,10 +42,8 @@ Section typing.
Proof.
iAlways. iIntros (tid qE) "_ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
iIntros "[Hp1 Hp2]".
- wp_bind p1. iApply (wp_hasty with "Hp1").
- iIntros ([[]|]) "_ H1"; try iDestruct "H1" as "[]".
- wp_bind p2. iApply (wp_hasty with "Hp2").
- iIntros ([[]|]) "_ H2"; try iDestruct "H2" as "[]".
+ wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done.
+ wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try done.
wp_op. by rewrite tctx_interp_singleton tctx_hasty_val' //.
Qed.
@@ -63,10 +61,8 @@ Section typing.
Proof.
iAlways. iIntros (tid qE) "_ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
iIntros "[Hp1 Hp2]".
- wp_bind p1. iApply (wp_hasty with "Hp1").
- iIntros ([[]|]) "_ H1"; try iDestruct "H1" as "[]".
- wp_bind p2. iApply (wp_hasty with "Hp2").
- iIntros ([[]|]) "_ H2"; try iDestruct "H2" as "[]".
+ wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done.
+ wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try done.
wp_op. by rewrite tctx_interp_singleton tctx_hasty_val' //.
Qed.
@@ -84,10 +80,8 @@ Section typing.
Proof.
iAlways. iIntros (tid qE) "_ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
iIntros "[Hp1 Hp2]".
- wp_bind p1. iApply (wp_hasty with "Hp1").
- iIntros ([[]|]) "_ H1"; try iDestruct "H1" as "[]".
- wp_bind p2. iApply (wp_hasty with "Hp2").
- iIntros ([[]|]) "_ H2"; try iDestruct "H2" as "[]".
+ wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done.
+ wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try done.
wp_op; intros _; by rewrite tctx_interp_singleton tctx_hasty_val' //.
Qed.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 32a9fa29..e1786c94 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -62,7 +62,7 @@ Section own.
(∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ∗
□ (∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[κ] ={F,F∖↑shrN∖↑lftN}▷=∗ ty.(ty_shr) κ tid l' ∗ q.[κ]))%I
|}.
- Next Obligation. by iIntros (q ty tid [|[[]|][]]) "H"; try iDestruct "H" as "[]". Qed.
+ Next Obligation. by iIntros (q ty tid [|[[]|][]]) "H". Qed.
Next Obligation.
move=>n ty N κ l tid ?? /=. iIntros "#LFT Hshr Htok".
iMod (bor_exists with "LFT Hshr") as (vl) "Hb". set_solver.
@@ -102,7 +102,7 @@ Section own.
type_incl ty1 ty2 -∗ type_incl (own_ptr n ty1) (own_ptr n ty2).
Proof.
iIntros "(#Hsz & #Ho & #Hs)". iSplit; first done. iSplit; iAlways.
- - iIntros (?[|[[| |]|][]]) "H"; try iDestruct "H" as "[]". simpl.
+ - iIntros (?[|[[| |]|][]]) "H"; try done. simpl.
iDestruct "H" as "[Hmt H†]". iDestruct "Hmt" as (vl') "[Hmt Hown]". iNext.
iDestruct ("Ho" with "Hown") as "Hown". iDestruct ("Hsz") as %<-.
iFrame. iExists _. iFrame.
@@ -168,17 +168,15 @@ Section typing.
Lemma write_own {E L} ty ty' n :
ty.(ty_size) = ty'.(ty_size) → typed_write E L (own_ptr n ty') ty (own_ptr n ty).
Proof.
- iIntros (Hsz) "!#". iIntros ([[]|] tid F qE qL ?) "_ $ $ Hown";
- try iDestruct "Hown" as "[]". rewrite /= Hsz. iDestruct "Hown" as "[H↦ $]".
- iDestruct "H↦" as (vl) "[>H↦ Hown]". iDestruct (ty_size_eq with "Hown") as "#>%".
- iExists _, _. iFrame "H↦". auto.
+ iIntros (Hsz) "!#". iIntros ([[]|] tid F qE qL ?) "_ $ $ Hown"; try done.
+ rewrite /= Hsz. iDestruct "Hown" as "[H↦ $]". iDestruct "H↦" as (vl) "[>H↦ Hown]".
+ iDestruct (ty_size_eq with "Hown") as "#>%". iExists _, _. iFrame "H↦". auto.
Qed.
Lemma read_own_copy E L ty n :
Copy ty → typed_read E L (own_ptr n ty) ty (own_ptr n ty).
Proof.
- iIntros (Hsz) "!#". iIntros ([[]|] tid F qE qL ?) "_ $ $ $ Hown";
- try iDestruct "Hown" as "[]".
+ iIntros (Hsz) "!#". iIntros ([[]|] tid F qE qL ?) "_ $ $ $ Hown"; try done.
iDestruct "Hown" as "[H↦ H†]". iDestruct "H↦" as (vl) "[>H↦ #Hown]".
iExists l, _, _. iFrame "∗#". iSplitR; first done. iIntros "!> Hl !>".
iExists _. auto.
@@ -187,8 +185,7 @@ Section typing.
Lemma read_own_move E L ty n :
typed_read E L (own_ptr n ty) ty (own_ptr n $ uninit ty.(ty_size)).
Proof.
- iAlways. iIntros ([[]|] tid F qE qL ?) "_ $ $ $ Hown";
- try iDestruct "Hown" as "[]".
+ iAlways. iIntros ([[]|] tid F qE qL ?) "_ $ $ $ Hown"; try done.
iDestruct "Hown" as "[H↦ H†]". iDestruct "H↦" as (vl) "[>H↦ Hown]".
iDestruct (ty_size_eq with "Hown") as "#>%".
iExists l, vl, _. iFrame "∗#". iSplitR; first done. iIntros "!> Hl !> !>".
@@ -233,11 +230,10 @@ Section typing.
typed_instruction E L [p ◠box ty] (delete [ #n; p])%E (λ _, []).
Proof.
iIntros (<-) "!#". iIntros (tid eq) "#LFT $ $ $ Hp". rewrite tctx_interp_singleton.
- wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown";
- try iDestruct "Hown" as "[]". iDestruct "Hown" as "[H↦∗: >H†]".
- iDestruct "H↦∗:" as (vl) "[>H↦ Hown]". rewrite tctx_interp_nil.
- iDestruct (ty_size_eq with "Hown") as "#>EQ". iDestruct "EQ" as %<-.
- iApply (wp_delete with "[-]"); try (by auto); [].
+ wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
+ iDestruct "Hown" as "[H↦∗: >H†]". iDestruct "H↦∗:" as (vl) "[>H↦ Hown]".
+ rewrite tctx_interp_nil. iDestruct (ty_size_eq with "Hown") as "#>EQ".
+ iDestruct "EQ" as %<-. iApply (wp_delete with "[-]"); auto; [].
rewrite freeable_sz_full. by iFrame.
Qed.
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 4e90676d..bb7955a0 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -90,7 +90,7 @@ Section product_split.
Proof.
iIntros (tid q1 q2) "#LFT $ $ H".
rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
- iDestruct "H" as ([[]|]) "[#Hp H]"; try iDestruct "H" as "[]".
+ iDestruct "H" as ([[]|]) "[#Hp H]"; try done.
iDestruct "H" as "[H >H†]". iDestruct "H" as (vl) "[>H↦ H]".
iDestruct "H" as (vl1 vl2) "(>% & H1 & H2)". subst.
rewrite heap_mapsto_vec_app -freeable_sz_split.
@@ -108,15 +108,15 @@ Section product_split.
Proof.
iIntros (tid q1 q2) "#LFT $ $ H".
rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
- iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "(Hp1 & H1)";
- try iDestruct "H1" as "[]". iDestruct "H1" as "(H↦1 & H†1)".
+ iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "(Hp1 & H1)"; try done.
+ iDestruct "H1" as "(H↦1 & H†1)".
iDestruct "H2" as (v2) "(Hp2 & H2)". simpl. iDestruct "Hp1" as %HÏ1.
rewrite HÏ1. iDestruct "Hp2" as %[=<-]. iDestruct "H2" as "[H↦2 H†2]".
iExists #l. iSplitR; first done. rewrite /= -freeable_sz_split. iFrame.
iDestruct "H↦1" as (vl1) "[H↦1 H1]". iDestruct "H↦2" as (vl2) "[H↦2 H2]".
iExists (vl1 ++ vl2). rewrite heap_mapsto_vec_app. iFrame.
iDestruct (ty_size_eq with "H1") as "#>EQ". iDestruct "EQ" as %->.
- iFrame. iExists vl1, vl2. iFrame. auto 10.
+ auto 10 with iFrame.
Qed.
Lemma tctx_split_own_prod E L n tyl p :
@@ -124,7 +124,7 @@ Section product_split.
Proof.
apply tctx_split_ptr_prod.
- intros. apply tctx_split_own_prod2.
- - intros ??[|[[]|][]]; try iIntros "[]". eauto.
+ - iIntros (??[|[[]|][]]) "?"; eauto.
Qed.
Lemma tctx_merge_own_prod E L n tyl :
@@ -135,7 +135,7 @@ Section product_split.
intros. apply tctx_merge_ptr_prod; try done.
- apply _.
- intros. apply tctx_merge_own_prod2.
- - intros ??[|[[]|][]]; try iIntros "[]". eauto.
+ - iIntros (??[|[[]|][]]) "?"; eauto.
Qed.
(** Unique borrows *)
@@ -145,7 +145,7 @@ Section product_split.
Proof.
iIntros (tid q1 q2) "#LFT $ $ H".
rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
- iDestruct "H" as ([[]|]) "[Hp H]"; try iDestruct "H" as "[]". iDestruct "Hp" as %Hp.
+ iDestruct "H" as ([[]|]) "[Hp H]"; try done. iDestruct "Hp" as %Hp.
rewrite /= split_prod_mt. iMod (bor_sep with "LFT H") as "[H1 H2]".
set_solver. rewrite /tctx_elt_interp /=.
iSplitL "H1"; iExists _; (iSplitR; first by rewrite Hp); auto.
@@ -157,18 +157,15 @@ Section product_split.
Proof.
iIntros (tid q1 q2) "#LFT $ $ H".
rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
- iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "[Hp1 H1]";
- try iDestruct "H1" as "[]". iDestruct "Hp1" as %Hp1.
- iDestruct "H2" as (v2) "(Hp2 & H2)". rewrite /= Hp1. iDestruct "Hp2" as %[=<-].
- iExists #l. iFrame "%". iMod (bor_combine with "LFT H1 H2") as "H". set_solver.
- by rewrite /= split_prod_mt.
+ iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "[Hp1 H1]"; try done.
+ iDestruct "Hp1" as %Hp1. iDestruct "H2" as (v2) "(Hp2 & H2)". rewrite /= Hp1.
+ iDestruct "Hp2" as %[=<-]. iExists #l. iFrame "%".
+ iMod (bor_combine with "LFT H1 H2") as "H". set_solver. by rewrite /= split_prod_mt.
Qed.
Lemma uniq_is_ptr κ ty tid (vl : list val) :
ty_own (&uniq{κ} ty) tid vl -∗ ⌜∃ l : loc, vl = [(#l) : val]âŒ.
- Proof.
- iIntros "H". destruct vl as [|[[]|][]]; try iDestruct "H" as "[]". eauto.
- Qed.
+ Proof. iIntros "H". destruct vl as [|[[]|][]]; eauto. Qed.
Lemma tctx_split_uniq_prod E L κ tyl p :
tctx_incl E L [p ◠&uniq{κ} product tyl]
@@ -208,18 +205,14 @@ Section product_split.
Proof.
iIntros (tid q1 q2) "#LFT $ $ H".
rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
- iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "[Hp1 Hown1]";
- try iDestruct "Hown1" as "[]". iDestruct "Hp1" as %Hp1.
- iDestruct "H2" as ([[]|]) "[Hp2 Hown2]"; try iDestruct "Hown2" as "[]".
- rewrite /= Hp1. iDestruct "Hp2" as %[=<-].
- iExists #l. by iFrame.
+ iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "[Hp1 Hown1]"; try done.
+ iDestruct "Hp1" as %Hp1. iDestruct "H2" as ([[]|]) "[Hp2 Hown2]"; try done.
+ rewrite /= Hp1. iDestruct "Hp2" as %[=<-]. iExists #l. by iFrame.
Qed.
Lemma shr_is_ptr κ ty tid (vl : list val) :
ty_own (&shr{κ} ty) tid vl -∗ ⌜∃ l : loc, vl = [(#l) : val]âŒ.
- Proof.
- iIntros "H". destruct vl as [|[[]|][]]; try iDestruct "H" as "[]". eauto.
- Qed.
+ Proof. iIntros "H". destruct vl as [|[[]|][]]; eauto. Qed.
Lemma tctx_split_shr_prod E L κ tyl p :
tctx_incl E L [p ◠&shr{κ} product tyl]
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index a0c649a9..8ed4d937 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -13,16 +13,14 @@ Section shr_bor.
| [ #(LitLoc l) ] => ty.(ty_shr) κ tid l
| _ => False
end%I |}.
- Next Obligation.
- iIntros (κ ty tid [|[[]|][]]) "H"; try iDestruct "H" as "[]". done.
- Qed.
+ Next Obligation. by iIntros (κ ty tid [|[[]|][]]) "H". Qed.
Next Obligation. intros κ ty tid [|[[]|][]]; apply _. Qed.
Global Instance shr_mono E L :
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 iDestruct "H" as "[]".
+ 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].
by iApply "Hs1".
@@ -44,9 +42,7 @@ Section shr_bor.
Global Instance shr_send κ ty :
Sync ty → Send (shr_bor κ ty).
- Proof.
- iIntros (Hsync tid1 tid2 [|[[]|][]]) "H"; try iDestruct "H" as "[]". by iApply Hsync.
- Qed.
+ Proof. by iIntros (Hsync tid1 tid2 [|[[]|][]]) "H"; try iApply Hsync. Qed.
End shr_bor.
Notation "&shr{ κ } ty" := (shr_bor κ ty)
@@ -72,8 +68,7 @@ Section typing.
iDestruct (llctx_interp_persist with "HL") as "#HL'". iFrame "HE HL".
iDestruct (Hκκ' with "HE' HL'") as "Hκκ'".
rewrite /tctx_interp big_sepL_singleton big_sepL_cons big_sepL_singleton.
- iDestruct "H" as ([[]|]) "[% #Hshr]"; try iDestruct "Hshr" as "[]".
- iModIntro. iSplit.
+ iDestruct "H" as ([[]|]) "[% #Hshr]"; try done. iModIntro. iSplit.
- iExists _. iSplit. done. by iApply (ty_shr_mono with "LFT Hκκ' Hshr").
- iExists _. auto.
Qed.
@@ -81,8 +76,8 @@ Section typing.
Lemma read_shr E L κ ty :
Copy ty → lctx_lft_alive E L κ → typed_read E L (&shr{κ}ty) ty (&shr{κ}ty).
Proof.
- iIntros (Hcopy Halive) "!#". iIntros ([[]|] tid F qE qL ?) "#LFT Htl HE HL #Hshr";
- try iDestruct "Hshr" as "[]".
+ iIntros (Hcopy Halive) "!#".
+ iIntros ([[]|] tid F qE qL ?) "#LFT Htl HE HL #Hshr"; try done.
iMod (Halive with "HE HL") as (q) "[Hκ Hclose]"; first set_solver.
assert (↑shrN ⊆ (↑lrustN : coPset)) by solve_ndisj. (* set_solver needs some help. *)
iMod (copy_shr_acc with "LFT Hshr Htl Hκ") as (q') "(Htl & H↦ & Hcl)".
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 0c28c7f3..2b7b157d 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -19,17 +19,12 @@ 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) "#LFT #Hord []". Qed.
Global Instance emp_empty : Empty type := emp.
Global Instance emp_copy : Copy ∅.
- Proof.
- split; first by apply _.
- iIntros (????????) "? []".
- Qed.
+ Proof. split; first by apply _. iIntros (????????) "? []". Qed.
Global Instance emp_send : Send ∅.
Proof. iIntros (???) "[]". Qed.
@@ -168,9 +163,8 @@ Section sum.
- iIntros (??) "[]".
- iIntros (κ tid l) "[]".
- iIntros (??) "H". iDestruct "H" as (i vl' vl'') "(% & % & Hown)".
- rewrite nth_empty. by iDestruct "Hown" as "[]".
- - iIntros (???) "H". iDestruct "H" as (i) "(_ & Hshr)".
- rewrite nth_empty. by iDestruct "Hshr" as "[]".
+ by rewrite nth_empty.
+ - iIntros (???) "H". iDestruct "H" as (i) "(_ & Hshr)". by rewrite nth_empty.
Qed.
Global Instance sum_copy tyl : LstCopy tyl → Copy (sum tyl).
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 7fa40e16..1cc5221c 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -17,9 +17,8 @@ Section case.
Proof.
iIntros (Hel) "!#". iIntros (tid qE) "#LFT Hna HE HL HC HT". wp_bind p.
rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
- iApply (wp_hasty with "Hp"). iIntros ([[]|] Hv) "Hp";
- try iDestruct "Hp" as "[]". iDestruct "Hp" as "[H↦ Hf]".
- iDestruct "H↦" as (vl) "[H↦ Hown]".
+ iApply (wp_hasty with "Hp"). iIntros ([[]|] Hv) "Hp"; try done.
+ iDestruct "Hp" as "[H↦ Hf]". iDestruct "H↦" as (vl) "[H↦ Hown]".
iDestruct "Hown" as (i vl' vl'') "(>% & >EQlen & Hown)". subst.
simpl ty_size. iDestruct "EQlen" as %[=EQlen]. rewrite -EQlen. simpl length.
rewrite -Nat.add_1_l app_length -!freeable_sz_split
@@ -116,12 +115,12 @@ Section case.
Proof.
iIntros (Halive Hel) "!#". iIntros (tid qE) "#LFT Hna HE HL HC HT". wp_bind p.
rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
- iApply (wp_hasty with "Hp"). iIntros ([[]|] Hv) "Hp"; try iDestruct "Hp" as "[]".
+ iApply (wp_hasty with "Hp"). iIntros ([[]|] Hv) "Hp"; try done.
iDestruct "Hp" as (i) "[#Hb Hshr]".
iMod (Halive with "HE HL") as (q) "[Htok Hclose]". done.
iMod (frac_bor_acc with "LFT Hb Htok") as (q') "[[H↦i H↦vl''] Hclose']". done.
rewrite nth_lookup.
- destruct (tyl !! i) as [ty|] eqn:EQty; last iDestruct "Hshr" as "[]".
+ destruct (tyl !! i) as [ty|] eqn:EQty; last done.
edestruct @Forall2_lookup_l as (e & He & Hety); eauto.
wp_read. iApply wp_case; [lia|by rewrite Nat2Z.id|]. iNext.
iMod ("Hclose'" with "[$H↦i $H↦vl'']") as "Htok".
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 52e708ff..88055127 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -21,9 +21,7 @@ Section uniq_bor.
□ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[κ∪κ']
={F, F∖↑shrN∖↑lftN}▷=∗ ty.(ty_shr) (κ∪κ') tid l' ∗ q.[κ∪κ'])%I
|}.
- Next Obligation.
- iIntros (q ty tid [|[[]|][]]) "H"; try iDestruct "H" as "[]". done.
- Qed.
+ Next Obligation. by iIntros (q ty tid [|[[]|][]]) "H". Qed.
Next Obligation.
move=> κ ty N κ' l tid ??/=. iIntros "#LFT Hshr Htok".
iMod (bor_exists with "LFT Hshr") as ([|[[|l'|]|][]]) "Hb"; first set_solver;
@@ -63,7 +61,7 @@ Section uniq_bor.
intros κ1 κ2 Hκ ty1 ty2 Hty%eqtype_unfold. iIntros. iSplit; first done.
iDestruct (Hty with "[] [] []") as "(_ & #Ho & #Hs)"; [done..|clear Hty].
iDestruct (Hκ with "[] []") as "#Hκ"; [done..|]. iSplit; iAlways.
- - iIntros (? [|[[]|][]]) "H"; try iDestruct "H" as "[]".
+ - iIntros (? [|[[]|][]]) "H"; try done.
iApply (bor_shorten with "Hκ"). iApply bor_iff; last done.
iSplit; iIntros "!>!# H"; iDestruct "H" as (vl) "[??]";
iExists vl; iFrame; by iApply "Ho".
@@ -95,7 +93,7 @@ Section uniq_bor.
Global Instance uniq_send κ ty :
Send ty → Send (uniq_bor κ ty).
Proof.
- iIntros (Hsend tid1 tid2 [|[[]|][]]) "H"; try iDestruct "H" as "[]".
+ iIntros (Hsend tid1 tid2 [|[[]|][]]) "H"; try done.
iApply bor_iff; last done. iNext. iAlways. iApply uPred.equiv_iff.
do 3 f_equiv. iSplit; iIntros "."; by iApply Hsend.
Qed.
@@ -130,7 +128,7 @@ Section typing.
iIntros (Hκ ???) "#LFT HE HL Huniq".
iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; [try done..|].
rewrite !tctx_interp_singleton /=.
- iDestruct "Huniq" as ([[]|]) "[% Huniq]"; try iDestruct "Huniq" as "[]".
+ iDestruct "Huniq" as ([[]|]) "[% Huniq]"; try done.
iMod (ty.(ty_share) with "LFT Huniq Htok") as "[Hown Htok]"; [solve_ndisj|].
iMod ("Hclose" with "Htok") as "[$ $]". iExists _. by iFrame "%∗".
Qed.
@@ -144,7 +142,7 @@ Section typing.
iDestruct (llctx_interp_persist with "HL") as "#HL'". iFrame "HE HL".
iDestruct (Hκκ' with "HE' HL'") as "Hκκ'".
rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
- iDestruct "H" as ([[]|]) "[% Hb]"; try iDestruct "Hb" as "[]".
+ iDestruct "H" as ([[]|]) "[% Hb]"; try done.
iMod (rebor with "LFT Hκκ' Hb") as "[Hb Hext]". done. iModIntro.
iSplitL "Hb"; iExists _; auto.
Qed.
@@ -191,8 +189,8 @@ Section typing.
Lemma read_uniq E L κ ty :
Copy ty → lctx_lft_alive E L κ → typed_read E L (&uniq{κ}ty) ty (&uniq{κ}ty).
Proof.
- iIntros (Hcopy Halive) "!#". iIntros ([[]|] tid F qE qL ?) "#LFT Htl HE HL Hown";
- try iDestruct "Hown" as "[]".
+ iIntros (Hcopy Halive) "!#".
+ iIntros ([[]|] tid F qE qL ?) "#LFT Htl HE HL Hown"; try done.
iMod (Halive with "HE HL") as (q) "[Hκ Hclose]"; first set_solver.
iMod (bor_acc with "LFT Hown Hκ") as "[H↦ Hclose']"; first set_solver.
iDestruct "H↦" as (vl) "[>H↦ #Hown]".
@@ -205,8 +203,8 @@ Section typing.
Lemma write_uniq E L κ ty :
lctx_lft_alive E L κ → typed_write E L (&uniq{κ}ty) ty (&uniq{κ}ty).
Proof.
- iIntros (Halive) "!#". iIntros ([[]|] tid F qE qL ?) "#LFT HE HL Hown";
- try iDestruct "Hown" as "[]".
+ iIntros (Halive) "!#".
+ iIntros ([[]|] tid F qE qL ?) "#LFT HE HL Hown"; try done.
iMod (Halive with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
iMod (bor_acc with "LFT Hown Htok") as "[H↦ Hclose']". set_solver.
iDestruct "H↦" as (vl) "[>H↦ Hown]". rewrite ty.(ty_size_eq).
diff --git a/theories/typing/unsafe/cell.v b/theories/typing/unsafe/cell.v
index 0371a1dc..9b4474d3 100644
--- a/theories/typing/unsafe/cell.v
+++ b/theories/typing/unsafe/cell.v
@@ -155,9 +155,8 @@ Section typing.
rewrite 3!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iIntros "(Hr & Hc & #Hc' & Hx)".
rewrite {1}/elctx_interp big_opL_singleton /=.
- destruct c' as [[|c'|]|]; try iDestruct "Hc'" as "[]".
- destruct x as [[|x|]|]; try iDestruct "Hx" as "[]".
- destruct r as [[|r|]|]; try iDestruct "Hr" as "[]".
+ destruct c' as [[|c'|]|]; try done. destruct x as [[|x|]|]; try done.
+ destruct r as [[|r|]|]; try done.
iMod (na_bor_acc with "LFT Hc' HE Htl") as "(Hc'↦ & Htl & Hclose)"; [solve_ndisj..|].
iDestruct "Hc'↦" as (vc') "[>Hc'↦ Hc'own]".
iDestruct (ty_size_eq with "Hc'own") as "#>%".
diff --git a/theories/typing/unsafe/refcell/ref.v b/theories/typing/unsafe/refcell/ref.v
index d3ccd14b..93e7cf56 100644
--- a/theories/typing/unsafe/refcell/ref.v
+++ b/theories/typing/unsafe/refcell/ref.v
@@ -27,9 +27,7 @@ Section ref.
▷ ty.(ty_shr) (α ∪ ν) tid lv ∗
▷ (α ⊑ β) ∗ ▷ &na{β, tid, refcell_invN}(refcell_inv tid lrc γ β ty') ∗
&na{κ, tid, refcell_refN}(own γ (◯ reading_st q ν)) |}%I.
- Next Obligation.
- iIntros (???[|[[]|][|[[]|][]]]); try iIntros "[]"; auto.
- Qed.
+ Next Obligation. iIntros (???[|[[]|][|[[]|][]]]) "?"; auto. Qed.
Next Obligation.
iIntros (α ty E κ l tid q ?) "#LFT Hb Htok".
iMod (bor_exists with "LFT Hb") as (vl) "Hb". done.
@@ -79,7 +77,7 @@ Section ref.
iDestruct (Hα with "HE HL") as "Hα1α2".
iSplit; [|iSplit; iAlways].
- done.
- - iIntros (tid [|[[]|][|[[]|][]]]); try iIntros "[]". iIntros "H".
+ - 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.
diff --git a/theories/typing/unsafe/refcell/ref_code.v b/theories/typing/unsafe/refcell/ref_code.v
index 8eb9adc2..1ff52542 100644
--- a/theories/typing/unsafe/refcell/ref_code.v
+++ b/theories/typing/unsafe/refcell/ref_code.v
@@ -63,8 +63,7 @@ Section ref_functions.
eapply type_deref; [solve_typing..|by apply read_own_move|done|]=>x'.
iIntros "!# * #LFT Hna HE HL Hk HT". simpl_subst.
rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
- iDestruct "HT" as "[Hx Hx']".
- destruct x' as [[|lx'|]|]; try iDestruct "Hx'" as "[]".
+ iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
iDestruct "Hx'" as (ν q γ δ ty' lv lrc) "#(Hαν & Hfrac & Hshr & Hβδ & Hinv & H◯inv)".
wp_op. rewrite {1}/elctx_interp big_sepL_cons big_sepL_singleton.
iDestruct "HE" as "[[Hα1 Hα2] Hβ]".
@@ -129,8 +128,7 @@ Section ref_functions.
eapply type_deref; [solve_typing..|by apply read_own_move|done|]=>x'.
iIntros "!# * #LFT Hna HE HL Hk HT". simpl_subst.
rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
- iDestruct "HT" as "[Hx Hx']".
- destruct x' as [[|lx'|]|]; try iDestruct "Hx'" as "[]".
+ iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
iDestruct "Hx'" as (ν q γ δ ty' lv lrc) "#(Hαν & Hfrac & Hshr & Hx')".
rewrite {1}/elctx_interp 2!big_sepL_cons big_sepL_singleton.
iDestruct "HE" as "(Hα & Hβ & #Hαβ)".
@@ -166,7 +164,7 @@ Section ref_functions.
eapply type_fn; [solve_typing..|]=>- /= α ret arg. inv_vec arg=>x. simpl_subst.
iIntros "!# * #LFT Hna Hα HL Hk Hx".
rewrite {1}/elctx_interp big_sepL_singleton tctx_interp_singleton tctx_hasty_val.
- destruct x as [[|lx|]|]; try iDestruct "Hx" as "[]". iDestruct "Hx" as "[Hx Hx†]".
+ destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
iDestruct "Hx" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Hx"; try iDestruct "Hx" as "[_ >[]]".
rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iDestruct "Hx" as "[[Hx↦1 Hx↦2] Hx]". wp_op. wp_read. wp_let.
diff --git a/theories/typing/unsafe/refcell/refcell_code.v b/theories/typing/unsafe/refcell/refcell_code.v
index 1dc95b9c..231edb06 100644
--- a/theories/typing/unsafe/refcell/refcell_code.v
+++ b/theories/typing/unsafe/refcell/refcell_code.v
@@ -28,10 +28,9 @@ Section refcell_functions.
iIntros (r) "!# * #LFT Hna HE HL Hk HT". simpl_subst.
rewrite (Nat2Z.id (S ty.(ty_size))) tctx_interp_cons
tctx_interp_singleton !tctx_hasty_val.
- iDestruct "HT" as "[Hr Hx]".
- destruct x as [[|lx|]|]; try iDestruct "Hx" as "[]". iDestruct "Hx" as "[Hx Hx†]".
- iDestruct "Hx" as (vl) "[Hx↦ Hx]".
- destruct r as [[|lr|]|]; try iDestruct "Hr" as "[]". iDestruct "Hr" as "[Hr Hr†]".
+ iDestruct "HT" as "[Hr Hx]". destruct x as [[|lx|]|]; try done.
+ iDestruct "Hx" as "[Hx Hx†]". iDestruct "Hx" as (vl) "[Hx↦ Hx]".
+ destruct r as [[|lr|]|]; try done. iDestruct "Hr" as "[Hr Hr†]".
iDestruct "Hr" as (vl') "Hr". rewrite uninit_own.
iDestruct "Hr" as "[Hr↦ >SZ]". destruct vl' as [|]; iDestruct "SZ" as %[=].
rewrite heap_mapsto_vec_cons. iDestruct "Hr↦" as "[Hr↦0 Hr↦1]". wp_op.
@@ -64,10 +63,10 @@ Section refcell_functions.
iIntros (r) "!# * #LFT Hna HE HL Hk HT". simpl_subst.
rewrite (Nat2Z.id (ty.(ty_size))) tctx_interp_cons
tctx_interp_singleton !tctx_hasty_val.
- iDestruct "HT" as "[Hr Hx]". destruct x as [[|lx|]|]; try iDestruct "Hx" as "[]".
+ iDestruct "HT" as "[Hr Hx]". destruct x as [[|lx|]|]; try done.
iDestruct "Hx" as "[Hx Hx†]".
iDestruct "Hx" as ([|[[]|]vl]) "[Hx↦ Hx]"; try iDestruct "Hx" as ">[]".
- destruct r as [[|lr|]|]; try iDestruct "Hr" as "[]". iDestruct "Hr" as "[Hr Hr†]".
+ destruct r as [[|lr|]|]; try done. iDestruct "Hr" as "[Hr Hr†]".
iDestruct "Hr" as (vl') "Hr". rewrite uninit_own heap_mapsto_vec_cons.
iDestruct "Hr" as "[Hr↦ >%]". iDestruct "Hx↦" as "[Hx↦0 Hx↦1]". wp_op.
iDestruct "Hx" as "[% Hx]". iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
@@ -107,7 +106,7 @@ Section refcell_functions.
rewrite heap_mapsto_vec_cons.
iDestruct "H" as "[H1 H2]". iDestruct "H↦" as "[H↦1 H↦2]".
iSplitL "H1 H↦1"; eauto. iExists _. iFrame. }
- destruct x as [[|lx|]|]; try iDestruct "Hx" as "[]". iDestruct "Hx" as "[Hx Hx†]".
+ destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
iDestruct "Hx" as (vl) "[Hx↦ Hx]". rewrite uninit_own. wp_op.
iApply (type_type _ _ _
[ #lx ◠box (uninit 1); #(shift_loc lx' 1) ◠&uniq{α}ty]%TC
@@ -152,8 +151,7 @@ Section refcell_functions.
eapply type_deref; [solve_typing..|apply read_own_copy, _|done|].
iIntros (x') "!# * #LFT Hna HE HL Hk HT". simpl_subst.
rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
- iDestruct "HT" as "(Hx & Hx' & Hr)".
- destruct x' as [[|lx|]|]; try iDestruct "Hx'" as "[]".
+ iDestruct "HT" as "(Hx & Hx' & Hr)". destruct x' as [[|lx|]|]; try done.
iDestruct "Hx'" as (β γ) "#[Hαβ Hinv]".
rewrite {1}/elctx_interp big_sepL_singleton.
iMod (lft_incl_acc with "Hαβ HE") as (qβ) "[[Hβtok1 Hβtok2] Hclose]". done.
@@ -259,8 +257,7 @@ Section refcell_functions.
eapply type_deref; [solve_typing..|apply read_own_copy, _|done|].
iIntros (x') "!# * #LFT Hna HE HL Hk HT". simpl_subst.
rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
- iDestruct "HT" as "(Hx & Hx' & Hr)".
- destruct x' as [[|lx|]|]; try iDestruct "Hx'" as "[]".
+ iDestruct "HT" as "(Hx & Hx' & Hr)". destruct x' as [[|lx|]|]; try done.
iDestruct "Hx'" as (β γ) "#[Hαβ Hinv]".
rewrite {1}/elctx_interp big_sepL_singleton.
iMod (lft_incl_acc with "Hαβ HE") as (qβ) "[Hβtok Hclose]". done.
diff --git a/theories/typing/unsafe/refcell/refmut.v b/theories/typing/unsafe/refcell/refmut.v
index db6c45d0..3817d1ad 100644
--- a/theories/typing/unsafe/refcell/refmut.v
+++ b/theories/typing/unsafe/refcell/refmut.v
@@ -95,7 +95,7 @@ Section refmut.
iDestruct (Hα with "HE HL") as "Hα1α2".
iSplit; [|iSplit; iAlways].
- done.
- - iIntros (tid [|[[]|][|[[]|][]]]); try iIntros "[]". iIntros "H".
+ - iIntros (tid [|[[]|][|[[]|][]]]) "H"; try done.
iDestruct "H" as (ν γ β ty') "(Hb & #H⊑ & #Hinv & Hν & Hown)".
iExists ν, γ, β, ty'. iFrame "∗#". iSplit.
+ iApply bor_shorten; last iApply bor_iff; last done.
diff --git a/theories/typing/unsafe/refcell/refmut_code.v b/theories/typing/unsafe/refcell/refmut_code.v
index 04e083f8..cfb17aa0 100644
--- a/theories/typing/unsafe/refcell/refmut_code.v
+++ b/theories/typing/unsafe/refcell/refmut_code.v
@@ -30,8 +30,7 @@ Section refmut_functions.
eapply type_deref; [solve_typing..|by apply read_own_move|done|]=>x'.
iIntros "!# * #LFT Hna HE HL Hk HT". simpl_subst.
rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
- iDestruct "HT" as "[Hx Hx']".
- destruct x' as [[|lx'|]|]; try iDestruct "Hx'" as "[]".
+ iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
iDestruct "Hx'" as (lv lrc) "#(Hfrac & #Hshr)".
rewrite {1}/elctx_interp 2!big_sepL_cons big_sepL_singleton.
iDestruct "HE" as "([Hα1 Hα2] & Hβ & #Hαβ)".
@@ -74,8 +73,7 @@ Section refmut_functions.
rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iDestruct "HT" as "[Hx Hx']".
rewrite {1}/elctx_interp 2!big_sepL_cons big_sepL_singleton.
- iDestruct "HE" as "(Hα & Hβ & #Hαβ)".
- destruct x' as [[|lx'|]|]; try iDestruct "Hx'" as "[]".
+ iDestruct "HE" as "(Hα & Hβ & #Hαβ)". destruct x' as [[|lx'|]|]; try done.
iMod (bor_exists with "LFT Hx'") as (vl) "H". done.
iMod (bor_sep with "LFT H") as "[H↦ H]". done.
destruct vl as [|[[|lv|]|][|[[|lrc|]|][]]];
@@ -125,7 +123,7 @@ Section refmut_functions.
eapply type_fn; [solve_typing..|]. move=>/= α ret arg. inv_vec arg=>x. simpl_subst.
iIntros "!# * #LFT Hna Hα HL Hk Hx".
rewrite {1}/elctx_interp big_sepL_singleton tctx_interp_singleton tctx_hasty_val.
- destruct x as [[|lx|]|]; try iDestruct "Hx" as "[]". iDestruct "Hx" as "[Hx Hx†]".
+ destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
iDestruct "Hx" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Hx"; try iDestruct "Hx" as "[_ >[]]".
rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iDestruct "Hx" as "[[Hx↦1 Hx↦2] Hx]". wp_op. wp_read. wp_let.
diff --git a/theories/typing/unsafe/spawn.v b/theories/typing/unsafe/spawn.v
index 56a50af5..656a167d 100644
--- a/theories/typing/unsafe/spawn.v
+++ b/theories/typing/unsafe/spawn.v
@@ -22,7 +22,7 @@ Section join_handle.
| _ => False
end%I;
ty_shr κ tid l := True%I |}.
- Next Obligation. by iIntros (ty tid [|[[]|][]]) "H"; try iDestruct "H" as "[]". Qed.
+ Next Obligation. by iIntros (ty tid [|[[]|][]]) "H". Qed.
Next Obligation. iIntros "* _ _ _ $". auto. Qed.
Next Obligation. iIntros (?) "**"; auto. Qed.
@@ -30,7 +30,7 @@ Section join_handle.
type_incl ty1 ty2 -∗ type_incl (join_handle ty1) (join_handle ty2).
Proof.
iIntros "#Hincl". iSplit; first done. iSplit; iAlways.
- - iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try by iDestruct "Hvl" as "[]".
+ - iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
iDestruct "Hvl" as (ty) "[Hincl' ?]". iExists ty. iFrame.
iApply (type_incl_trans with "Hincl'"). done.
- iIntros "* _". auto.
@@ -73,7 +73,8 @@ Section spawn.
{ (* The core of the proof: showing that spawn is safe. *)
iAlways. iIntros (tid qE) "#LFT $ $ $".
rewrite tctx_interp_cons tctx_interp_singleton.
- iIntros "[Hf' Henv]". iApply (spawn_spec _ (join_inv retty tid) with "[-]"); first solve_to_val; last first; last simpl_subst.
+ iIntros "[Hf' Henv]". iApply (spawn_spec _ (join_inv retty tid) with "[-]");
+ first solve_to_val; last first; last simpl_subst.
{ iIntros "!> *". rewrite tctx_interp_singleton tctx_hasty_val.
iIntros "?". iExists retty. iFrame. iApply type_incl_refl. }
iIntros (c) "Hfin". iMod na_alloc as (tid') "Htl". wp_let. wp_let.
@@ -119,8 +120,7 @@ Section spawn.
(T2 := λ r, [r ◠box retty]%TC); try solve_typing; [|].
{ iAlways. iIntros (tid qE) "#LFT $ $ $".
rewrite tctx_interp_singleton tctx_hasty_val. iIntros "Hc'".
- destruct c' as [[|c'|]|]; try by iDestruct "Hc'" as "[]".
- iDestruct "Hc'" as (ty') "[#Hsub Hc']".
+ destruct c' as [[|c'|]|]; try done. iDestruct "Hc'" as (ty') "[#Hsub Hc']".
iApply (join_spec with "Hc'"). iIntros "!> * Hret".
rewrite tctx_interp_singleton tctx_hasty_val.
iPoseProof "Hsub" as "Hsz". iDestruct "Hsz" as "[% _]".
--
GitLab