From 3e9074b9e58674cba91280507cfaa6c834be44e4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 28 Mar 2017 14:10:14 +0200
Subject: [PATCH] Misc big op tweaks.
---
theories/typing/int.v | 9 +++------
theories/typing/lib/spawn.v | 5 ++---
theories/typing/programs.v | 8 +++-----
3 files changed, 8 insertions(+), 14 deletions(-)
diff --git a/theories/typing/int.v b/theories/typing/int.v
index 93e879ce..ed6a41ae 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -39,8 +39,7 @@ Section typing.
Lemma type_plus_instr E L p1 p2 :
typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 + p2) int.
Proof.
- iIntros (tid) "_ _ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
- iIntros "[Hp1 Hp2]".
+ iIntros (tid) "_ _ $ $ [Hp1 [Hp2 _]]".
wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done.
wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try done.
wp_op. by rewrite tctx_interp_singleton tctx_hasty_val' //.
@@ -56,8 +55,7 @@ Section typing.
Lemma type_minus_instr E L p1 p2 :
typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 - p2) int.
Proof.
- iIntros (tid) "_ _ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
- iIntros "[Hp1 Hp2]".
+ iIntros (tid) "_ _ $ $ [Hp1 [Hp2 _]]".
wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done.
wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try done.
wp_op. by rewrite tctx_interp_singleton tctx_hasty_val' //.
@@ -73,8 +71,7 @@ Section typing.
Lemma type_le_instr E L p1 p2 :
typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 ≤ p2) bool.
Proof.
- iIntros (tid) "_ _ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
- iIntros "[Hp1 Hp2]".
+ iIntros (tid) "_ _ $ $ [Hp1 [Hp2 _]]".
wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done.
wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try done.
wp_op; intros _; by rewrite tctx_interp_singleton tctx_hasty_val' //.
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index d6a4140f..d0f1050f 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -81,9 +81,8 @@ Section spawn.
iApply (type_let _ _ _ _ ([f' ◁ _; env ◁ _]%TC)
(λ j, [j ◁ join_handle retty]%TC)); try solve_typing; [|].
{ (* The core of the proof: showing that spawn is safe. *)
- iIntros (tid) "#LFT #HE $ $".
- rewrite tctx_interp_cons tctx_interp_singleton.
- iIntros "[Hf' Henv]". iApply (spawn_spec _ (join_inv tid retty) with "[-]");
+ iIntros (tid) "#LFT #HE $ $ [Hf' [Henv _]]".
+ iApply (spawn_spec _ (join_inv tid retty) 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. }
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 372bb223..090e8cc5 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -99,8 +99,7 @@ Section typing_rules.
typed_body ((κ1 ⊑ κ2) :: (κ2 ⊑ κ1) :: E) L C T e →
typed_body E ((κ1 ⊑ [κ2]%list) :: L) C T e.
Proof.
- iIntros (He tid) "#LFT #HE Htl HL HC HT".
- rewrite /llctx_interp big_sepL_cons. iDestruct "HL" as "[Hκ HL]".
+ iIntros (He tid) "#LFT #HE Htl [Hκ HL] HC HT".
iMod (lctx_equalize_lft with "LFT Hκ") as "[Hκ1 Hκ2]".
iApply (He with "LFT [Hκ1 Hκ2 HE] Htl HL HC HT").
rewrite /elctx_interp /=. by iFrame.
@@ -163,8 +162,7 @@ Section typing_rules.
Closed [] e → UnblockTctx κ T1 T2 →
typed_body E L C T2 e -∗ typed_body E ((κ ⊑ κs) :: L) C T1 (Endlft ;; e).
Proof.
- iIntros (Hc Hub) "He". iIntros (tid) "#LFT #HE Htl".
- rewrite /llctx_interp big_sepL_cons. iIntros "[Hκ HL] HC HT".
+ iIntros (Hc Hub) "He". iIntros (tid) "#LFT #HE Htl [Hκ HL] HC HT".
iDestruct "Hκ" as (Λ) "(% & Htok & #Hend)".
iSpecialize ("Hend" with "Htok"). wp_bind Endlft.
iApply (wp_mask_mono (↑lftN)); first done.
@@ -176,7 +174,7 @@ Section typing_rules.
Lemma type_path_instr {E L} p ty :
typed_instruction_ty E L [p ◁ ty] p ty.
Proof.
- iIntros (?) "_ _ $$ ?". rewrite tctx_interp_singleton.
+ iIntros (?) "_ _ $$ [? _]".
iApply (wp_hasty with "[-]"). done. iIntros (v) "_ Hv".
rewrite tctx_interp_singleton. iExists v. iFrame. by rewrite eval_path_of_val.
Qed.
--
GitLab