From fa3141d227c6d0ab75b9ff802418d18814a6db4a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 8 Dec 2016 14:46:21 +0100
Subject: [PATCH] add lemma about readucing ectxi-languages

---
 program_logic/ectxi_language.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/program_logic/ectxi_language.v b/program_logic/ectxi_language.v
index 4dc3bbfd7..ca0ea6816 100644
--- a/program_logic/ectxi_language.v
+++ b/program_logic/ectxi_language.v
@@ -86,4 +86,17 @@ Section ectxi_language.
   Global Instance ectxi_lang_ctx_item Ki :
     LanguageCtx (ectx_lang expr) (fill_item Ki).
   Proof. change (LanguageCtx _ (fill [Ki])). apply _. Qed.
+
+  Lemma step_is_head K e σ :
+    to_val e = None → (∀ Ki K e', e = fill (Ki::K) e' → ¬head_reducible e' σ) →
+    reducible (fill K e) σ → head_reducible e σ.
+  Proof.
+    intros Hnonval Hnondecomp (e'&σ''&ef&Hstep).
+    change fill with ectx_language.fill in Hstep.
+    apply fill_step_inv in Hstep; last done. destruct Hstep as (e2'&_&Hstep).
+    clear K. destruct Hstep as [K e1' e2'' ?? Hstep]. subst.
+    destruct K as [|K0 K].
+    { rewrite fill_empty in Hnonval. subst. eexists; eauto. }
+    exfalso. eapply Hnondecomp; first done. do 3 eexists. done.
+  Qed.
 End ectxi_language.
-- 
GitLab