From 0b4679758667aa6a19f2d7ea5d5dc287f1be6c28 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 11 May 2020 16:40:43 +0200
Subject: [PATCH] tweak proof
---
theories/program_logic/ectx_language.v | 10 +++++-----
1 file changed, 5 insertions(+), 5 deletions(-)
diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 4968ecc2a..0e0c1475e 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -169,11 +169,11 @@ Section ectx_language.
K = comp_ectx K' empty_ectx ∧ e = e'.
Proof.
intros Heq (κ & e2 & σ2 & efs & Hred) (κ' & e2' & σ2' & efs' & Hred').
- edestruct (step_by_val K' K e' e) as [K'' HK]; try done.
- { exact: val_head_stuck. }
- subst K. move: Heq. rewrite -fill_comp=> /fill_inj He'.
- subst e'. edestruct (head_ctx_step_val _ _ _ _ _ _ _ Hred') as [Hval|HK''].
- { erewrite val_head_stuck in Hval; last done. destruct Hval. done. }
+ edestruct (step_by_val K' K e' e) as [K'' HK];
+ [by eauto using val_head_stuck..|].
+ subst K. move: Heq. rewrite -fill_comp. intros <-%(inj (fill _)).
+ destruct (head_ctx_step_val _ _ _ _ _ _ _ Hred') as [[]%not_eq_None_Some|HK''].
+ { by eapply val_head_stuck. }
subst K''. rewrite fill_empty. done.
Qed.
--
GitLab