From 01c96d5f6bc859c3c6ce2fb69332aec19021a755 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Mon, 4 Jan 2021 19:23:48 +0100
Subject: [PATCH] Getting rid of admits in contextual_refinement.v

---
 theories/typing/contextual_refinement.v | 64 ++++++++++++++++++-------
 1 file changed, 47 insertions(+), 17 deletions(-)

diff --git a/theories/typing/contextual_refinement.v b/theories/typing/contextual_refinement.v
index 85cc050..5f47dae 100644
--- a/theories/typing/contextual_refinement.v
+++ b/theories/typing/contextual_refinement.v
@@ -388,22 +388,52 @@ Proof.
     by eapply erased_step_ectx.
 Qed.
 
-Lemma rtc_erased_step_smart_ctx (e : expr) σ0 σ1 tp0 tp1 :
-  rtc erased_step ((e ;; #true)%E :: tp0, σ0) (of_val #true :: tp1, σ1) →
-  ∃ (v : val), rtc erased_step (e :: tp0, σ0) (of_val v :: tp1, σ1).
+Lemma nice_ctx_lemma K tp1 tp2 e ρ1 ρ2 v :
+  rtc erased_step ρ1 ρ2 →
+  ρ1.1 = (fill K e) :: tp1 →
+  ρ2.1 = of_val v :: tp2 →
+  ∃ tp2' σ' w,
+    rtc erased_step (e :: tp1, ρ1.2) (of_val w :: tp2', σ').
 Proof.
-  pose (P := λ (s1 s2 : list expr * state),
-             match s1, s2 with
-             | ((Seq e #true)%E :: tp0, σ0), (of_val #true :: tp1, σ1) =>
-               ∃ (v : val), rtc erased_step (e :: tp0, σ0) (of_val v :: tp1, σ1)
-             | _,_ => True
-             end).
-  (* eapply (rtc_ind _ P); clear tp0 tp1 σ0 σ1. *)
-  (* - intros [tp σ]. unfold P. *)
-  (*   destruct tp as [|e' tp]; first done. *)
-  (*   repeat (case_match; eauto). *)
-  admit.
-Admitted.
+  intros Hsteps.
+  revert tp1 e.
+  induction Hsteps as [ρ|ρ1 ρ2 ρ3 Hstep Hsteps IH]; intros tp1 e Hρ1 Hρ2.
+  { destruct (to_val e) as [w|] eqn:He.
+    - apply of_to_val in He as <-.
+      exists tp1, ρ.2, w. reflexivity.
+    - assert (to_val (fill K e) = None) by auto using fill_not_val.
+      destruct ρ as [ρ1 ρ2]. simplify_eq/=.
+      assert (of_val v = fill K e) as ?%of_to_val_flip; naive_solver. }
+  destruct Hstep as [κs [e1 σ1 e2 σ2 efs t1 t2 -> -> Hstep]]; simpl in *.
+  destruct t1 as [|h1 t1]; simplify_eq/=.
+  - destruct (to_val e) as [w|] eqn:He.
+    + apply of_to_val in He as <-.
+      eexists _, _, w. reflexivity.
+    + apply fill_step_inv in Hstep as (e2'&->&Hstep); last done.
+      specialize (IH (tp1++efs) e2').
+      assert (fill K e2' :: tp1 ++ efs = fill K e2' :: tp1 ++ efs) as H1 by done.
+      specialize (IH H1 Hρ2).
+      destruct IH as (tp2'&σ'&w&Hsteps1).
+      eexists _,_,w. eapply rtc_l, Hsteps1.
+      exists κs. by eapply step_atomic with (t1:=[]).
+  - specialize (IH (t1 ++ e2 :: t2 ++ efs) e).
+    assert (fill K e :: t1 ++ e2 :: t2 ++ efs = fill K e :: t1 ++ e2 :: t2 ++ efs) as H1 by done.
+    specialize (IH H1 Hρ2).
+    destruct IH as (tp2'&σ'&w&Hsteps1).
+    eexists _,_,w. eapply rtc_l, Hsteps1.
+    exists κs. econstructor; rewrite ?app_comm_cons; done.
+Qed.
+
+Lemma nice_ctx_lemma' K tp1 tp2 e σ1 σ2 v :
+  rtc erased_step ((fill K e) :: tp1, σ1) (of_val v :: tp2, σ2) →
+  ∃ tp2' σ' w,
+    rtc erased_step (e :: tp1, σ1) (of_val w :: tp2', σ').
+Proof.
+  pose (ρ1:=((fill K e) :: tp1, σ1)).
+  pose (ρ2:=(of_val v :: tp2, σ2)).
+  fold ρ1 ρ2. intros Hρ.
+  change σ1 with ρ1.2. eapply nice_ctx_lemma; eauto.
+Qed.
 
 Lemma ctx_refines_impl_alt Γ e1 e2 τ :
   (Γ ⊨ e1 ≤ctx≤ e2 : τ) →
@@ -416,8 +446,8 @@ Proof.
                 (of_val #true :: thp', σ₁')).
   - unfold C'; simpl.
     destruct 1 as (thp' & σ1' & Hstep').
-    exists thp', σ1'.
-    eapply rtc_erased_step_smart_ctx. done.
+    eapply (nice_ctx_lemma' [AppRCtx (λ: <>, #true)] []).
+    eapply Hstep'.
   - eapply (H C' thp _ σ1 #true TBool).
     + repeat econstructor; eauto.
     + repeat econstructor; eauto.
-- 
GitLab