From 05bd12cd6acfd970ba42e03268bd38245c2f814e Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 12 Jan 2017 10:33:42 +0100
Subject: [PATCH] Simplify proof of soundness/adequacy.
---
theories/typing/adequacy.v | 6 ++----
1 file changed, 2 insertions(+), 4 deletions(-)
diff --git a/theories/typing/adequacy.v b/theories/typing/adequacy.v
index 7b4eff80..674fdaa2 100644
--- a/theories/typing/adequacy.v
+++ b/theories/typing/adequacy.v
@@ -44,17 +44,15 @@ Section type_soundness.
{ by rewrite /elctx_interp big_sepL_nil. }
{ by rewrite /llctx_interp big_sepL_nil. }
{ by rewrite tctx_interp_nil. }
- clear Hrtc Hmain main. iIntros (main) "(Htl & _ & _ & Hmain)".
+ clear Hrtc Hmain main. iIntros (main) "(Htl & HE & HL & Hmain)".
rewrite tctx_interp_singleton. iDestruct "Hmain" as (?) "[EQ Hmain]".
rewrite eval_path_of_val. iDestruct "EQ" as %[= <-].
iDestruct "Hmain" as (f k x e ?) "(EQ & % & Hmain)". iDestruct "EQ" as %[= ->].
destruct x; try done.
iApply (wp_rec _ _ _ _ _ _ [exit_cont]%E); [done| |by simpl_subst|iNext].
{ repeat econstructor. apply to_of_val. }
- iApply ("Hmain" $! () exit_cont [#] tid 1%Qp with "HEAP LFT Htl [] [] []");
+ iApply ("Hmain" $! () exit_cont [#] tid 1%Qp with "HEAP LFT Htl HE HL []");
last by rewrite tctx_interp_nil.
- { by rewrite /elctx_interp big_sepL_nil. }
- { by rewrite /llctx_interp big_sepL_nil. }
iIntros "_". rewrite cctx_interp_singleton. simpl. iIntros (args) "_ _".
inv_vec args. iIntros (x) "_". by wp_seq.
Qed.
--
GitLab