From 54ebef8d8b24ff36c7a14600f6619259a70e1cf9 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Fri, 11 Dec 2020 16:56:50 +0100
Subject: [PATCH] WIP alternative contextual refinement definition

---
 theories/typing/contextual_refinement.v | 27 +++++++++++++++++++++++++
 1 file changed, 27 insertions(+)

diff --git a/theories/typing/contextual_refinement.v b/theories/typing/contextual_refinement.v
index 7003ace..cd25e7c 100644
--- a/theories/typing/contextual_refinement.v
+++ b/theories/typing/contextual_refinement.v
@@ -303,6 +303,33 @@ Proof.
   eapply typed_ctx_compose; eauto.
 Qed.
 
+(* Alternative formulation of contextual refinement
+without restricting to contexts of the ground type *)
+Definition ctx_refines_alt (Γ : stringmap type)
+    (e e' : expr) (τ : type) : Prop := ∀ K thp σ₀ σ₁ v1 τ',
+  typed_ctx K Γ τ ∅ τ' →
+  rtc erased_step ([fill_ctx K e], σ₀) (of_val v1 :: thp, σ₁) →
+  ∃ thp' σ₁' v2, rtc erased_step ([fill_ctx K e'], σ₀) (of_val v2 :: thp', σ₁').
+
+Lemma ctx_refines_impl_alt Γ e1 e2 τ :
+  (Γ ⊨ e1 ≤ctx≤ e2 : τ) →
+  ctx_refines_alt Γ e1 e2 τ.
+Proof.
+  intros H C thp σ0 σ1 v1 τ' HC Hstep.
+  pose (C' := (CTX_AppR (λ: <>, #true)%E)::C).
+  cut (∃ (thp' : list expr) σ₁',
+              rtc erased_step ([fill_ctx C' e2], σ0)
+                (of_val #true :: thp', σ₁')).
+  - unfold C'; simpl.
+    destruct 1 as (thp' & σ1' & Hstep').
+    exists thp', σ1'.
+    admit.
+  - eapply (H C' thp _ σ1 #true TBool).
+    + repeat econstructor; eauto.
+    + repeat econstructor; eauto.
+    + unfold C'. simpl.
+      admit.
+Admitted.
 
 Definition ctx_equiv Γ e1 e2 τ :=
   (Γ ⊨ e1 ≤ctx≤ e2 : τ) ∧ (Γ ⊨ e2 ≤ctx≤ e1 : τ).
-- 
GitLab