Alternative def. of ctx ref

theories/typing/contextual_refinement.v

@@ -311,6 +311,82 @@ Definition ctx_refines_alt (Γ : stringmap type)
   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 erased_step_ectx (e e' : expr) tp' σ σ' K : *)
+(*   erased_step ([e], σ) (e' :: tp', σ') → *)
+(*   erased_step ([fill K e], σ) (fill K e' :: tp', σ'). *)
+(* Proof. *)
+(*   intros [κ Hst]. inversion Hst; simplify_eq/=. *)
+(*   symmetry in H. apply app_singleton in H. *)
+(*   assert (t1 = [] ∧ e1 = e ∧ t2 = []) as (->&->&->). *)
+(*   { naive_solver. } *)
+(*   assert (e2 = e' ∧ tp' = efs) as [-> ->]. *)
+(*   { naive_solver. } *)
+(*   eapply fill_prim_step in H1. simpl in H1. *)
+(*   econstructor. eapply step_atomic with (t1 := []); eauto. *)
+(* Qed. *)
+
+Lemma erased_step_ectx (e e' : expr) tp tp' σ σ' K :
+  erased_step (e :: tp, σ) (e' :: tp', σ') →
+  erased_step ((fill K e) :: tp, σ) (fill K e' :: tp', σ').
+Proof.
+  intros [κ Hst]. inversion Hst; simplify_eq/=.
+  destruct t1 as [|h1 t1]; simplify_eq/=.
+  { simplify_eq/=.
+    eapply fill_prim_step in H1. simpl in H1.
+    econstructor. eapply step_atomic with (t1 := []); eauto. }
+  econstructor. econstructor; eauto.
+  + rewrite app_comm_cons. reflexivity.
+  + rewrite app_comm_cons. reflexivity.
+Qed.
+
+
+Local Definition ffill (K : list ectx_item) :
+  (list expr * state) → (list expr * state) :=
+  fun x => match x with
+           | (e :: tp, σ) => (fill K e :: tp, σ)
+           | ([], σ) => ([], σ)
+           end.
+
+Lemma erased_step_nonempty  (tp : list expr) σ tp' σ'  :
+  erased_step (tp, σ) (tp', σ') → tp' ≠ [].
+Proof.
+  intros [? Hs].
+  destruct Hs as [e1 σ1' e2 σ2' efs tp1 tp2 ?? Hstep]; simplify_eq/=.
+  intros [_ HH]%app_eq_nil. by inversion HH.
+Qed.
+
+Lemma rtc_erased_step_nonempty (tp : list expr) σ tp' σ'  :
+  rtc erased_step (tp, σ) (tp', σ') → tp ≠ [] → tp' ≠ [].
+Proof.
+  pose (P := λ (x y : list expr * state), x.1 ≠ [] → y.1 ≠ []).
+  eapply (rtc_ind_r_weak P).
+  - intros [tp2 σ2]. unfold P. naive_solver.
+  - intros [tp1 σ1] [tp2 σ2] [tp3 σ3]. unfold P; simpl.
+    intros ? ?%erased_step_nonempty. naive_solver.
+Qed.
+
+Lemma rtc_erased_step_ectx (e e' : expr) tp tp' σ σ' K :
+  rtc erased_step (e :: tp, σ) (e' :: tp', σ') →
+  rtc erased_step (fill K e :: tp, σ) (fill K e' :: tp', σ').
+Proof.
+  change (rtc erased_step (fill K e :: tp, σ) (fill K e' :: tp', σ'))
+    with (rtc erased_step (ffill K (e :: tp, σ)) (ffill K (e' :: tp', σ'))).
+  eapply (rtc_congruence (ffill K) erased_step).
+  clear e e' tp tp' σ σ'.
+  intros [tp σ] [tp' σ'].
+  destruct tp as [|e tp].
+  - inversion 1. inversion H0. exfalso.
+    simplify_eq/=. by eapply app_cons_not_nil.
+  - intros Hstep1.
+    assert (tp' ≠ []).
+    { eapply (rtc_erased_step_nonempty (e::tp)).
+      econstructor; naive_solver.
+      naive_solver. }
+    destruct tp' as [|e' tp']; first naive_solver.
+    simpl.
+    by eapply erased_step_ectx.
+Qed.
+
 Lemma ctx_refines_impl_alt Γ e1 e2 τ :
   (Γ ⊨ e1 ≤ctx≤ e2 : τ) →
   ctx_refines_alt Γ e1 e2 τ.
@@ -328,7 +404,16 @@ Proof.
     + repeat econstructor; eauto.
     + repeat econstructor; eauto.
     + unfold C'. simpl.
-      admit.
+      trans (((of_val v1) ;; #true)%E :: thp, σ1); last first.
+      { econstructor.
+        - econstructor.
+          eapply (step_atomic) with (t1 := []); try reflexivity.
+          admit.
+        - admit. }
+      pose (K := [AppRCtx (λ: <>, #true)%E]).
+      change (fill_ctx C e1;; #true)%E with (fill K (fill_ctx C e1)).
+      change (v1;; #true)%E with (fill K (of_val v1)).
+      by eapply rtc_erased_step_ectx.
 Admitted.
 
 Definition ctx_equiv Γ e1 e2 τ :=