From 166449ecb3e90db8e582881ad091d0a0629cc022 Mon Sep 17 00:00:00 2001
From: Amin Timany <amintimany@gmail.com>
Date: Sun, 19 Jan 2020 14:17:44 -0600
Subject: [PATCH] clean up

---
 theories/demo.v | 22 ++++++++++------------
 1 file changed, 10 insertions(+), 12 deletions(-)

diff --git a/theories/demo.v b/theories/demo.v
index e20738b..80b04cb 100644
--- a/theories/demo.v
+++ b/theories/demo.v
@@ -156,12 +156,16 @@ End semtyp.
 Notation "Γ ⊨ e : A" := (sem_typed Γ e A)
   (at level 74, e, A at next level).
 
-Lemma sem_type_safety `{!heapPreG Σ} e σ es σ' e' τ :
-  (∀ `{!heapG Σ}, ∅ ⊨ e : τ) →
-  rtc erased_step ([e], σ) (es, σ') → e' ∈ es →
-  is_Some (to_val e') ∨ reducible e' σ'.
+Definition safe (e : expr) :=
+  ∀ σ es' e' σ',
+    rtc erased_step ([e], σ) (es', σ') →
+    e' ∈ es' →
+    is_Some (to_val e') ∨ reducible e' σ'.
+
+Lemma sem_type_safety `{!heapPreG Σ} e τ :
+  (∀ `{!heapG Σ}, ∅ ⊨ e : τ) → safe e.
 Proof.
-  intros Hty.
+  intros Hty σ es' e' σ'.
   apply (heap_adequacy Σ NotStuck e σ (λ _, True))=> // ?.
   iDestruct (Hty $! ∅) as "#He".
   rewrite subst_map_empty. iApply (wp_wand with "(He [])").
@@ -169,14 +173,8 @@ Proof.
   auto.
 Qed.
 
-Lemma type_safety e σ es σ' e' τ :
-  (∅ ⊢ₜ e : τ) →
-  rtc erased_step ([e], σ) (es, σ') → e' ∈ es →
-  is_Some (to_val e') ∨ reducible e' σ'.
+Lemma type_safety e τ : ∅ ⊢ₜ e : τ → safe e.
 Proof.
   intros Hty. eapply (sem_type_safety (Σ:=heapΣ))=> ?.
   by apply fundamental.
 Qed.
-
-(*  LocalWords:  Robbert
- *)
-- 
GitLab