Library iris.chan_lang.refine
From iris.algebra Require Import upred_big_op frac dec_agree.
From iris.program_logic Require Export invariants ghost_ownership refine_ectx_delay
refine_raw_adequacy nat_delayed_language.
From iris.program_logic Require Import ownership auth refine_raw ectx_lifting.
From iris.proofmode Require Import weakestpre.
From iris.chan_lang Require Export lang.
From iris.chan_lang Require Import tactics.
Import uPred.
Hint Resolve head_prim_reducible head_reducible_prim_step.
Section refine.
Context `{refineG Λ Σ (delayed_lang (chan_lang) Kd Fd) (S Kd × (Kd + 3))}.
Implicit Types P Q : iPropG Λ Σ.
Local Open Scope nat_scope.
From iris.program_logic Require Export invariants ghost_ownership refine_ectx_delay
refine_raw_adequacy nat_delayed_language.
From iris.program_logic Require Import ownership auth refine_raw ectx_lifting.
From iris.proofmode Require Import weakestpre.
From iris.chan_lang Require Export lang.
From iris.chan_lang Require Import tactics.
Import uPred.
Hint Resolve head_prim_reducible head_reducible_prim_step.
Section refine.
Context `{refineG Λ Σ (delayed_lang (chan_lang) Kd Fd) (S Kd × (Kd + 3))}.
Implicit Types P Q : iPropG Λ Σ.
Local Open Scope nat_scope.
Base axioms for core primitives of the language: Stateful reductions.
Lemma refine_alloc_pst' E σ K d d' i:
d ≤ Kd →
d' ≤ Kd →
(ownT i (Alloc) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (Pair (Lit $ LitLoc (fresh (dom _ σ)) cleft)
(Lit $ LitLoc (fresh (dom _ σ)) cright)) K d'
★ ownSP (<[fresh (dom _ σ):=([], [])]>σ) .
Proof.
iIntros (??) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; auto.
Qed.
Lemma refine_recv_left_pst E σ K d d' l l1 l2 v i:
d ≤ Kd →
d' ≤ Kd →
σ !! l = Some (l1, v :: l2) →
(ownT i (Recv (Lit (LitLoc l cleft))) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (Pair (Lit $ LitLoc l cleft) (of_val v)) K d'
★ ownSP (<[l := (l1, l2)]>σ).
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; auto.
Qed.
Lemma refine_recv_right_pst E σ K d d' l l1 l2 v i:
d ≤ Kd →
d' ≤ Kd →
σ !! l = Some (v :: l1, l2) →
(ownT i (Recv (Lit (LitLoc l cright))) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (Pair (Lit $ LitLoc l cright) (of_val v)) K d'
★ ownSP (<[l := (l1, l2)]>σ).
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; auto.
Qed.
Lemma refine_recv_right_miss_pst E σ K d d' l l2 i:
d ≤ Kd →
d' ≤ Kd →
σ !! l = Some ([], l2) →
(ownT i (Recv (Lit (LitLoc l cright))) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (Recv (Lit (LitLoc l cright))) K d'
★ ownSP σ.
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; eauto.
Qed.
Lemma refine_recv_left_miss_pst E σ K d d' l l1 i:
d ≤ Kd →
d' ≤ Kd →
σ !! l = Some (l1, []) →
(ownT i (Recv (Lit (LitLoc l cleft))) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (Recv (Lit (LitLoc l cleft))) K d'
★ ownSP σ.
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; eauto.
Qed.
Lemma refine_send_left_pst E σ K d d' l e v l1 l2 i :
d ≤ Kd →
d' ≤ Kd →
to_val e = Some v → σ !! l = Some (l1, l2) →
(ownT i (Send (Lit (LitLoc l cleft)) e) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (Lit $ LitLoc l cleft) K d'
★ ownSP (<[l:= (l1 ++ [v], l2)]>σ).
Proof.
iIntros (????) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; auto.
Qed.
Lemma refine_send_right_pst E σ K d d' l e v l1 l2 i :
d ≤ Kd →
d' ≤ Kd →
to_val e = Some v → σ !! l = Some (l1, l2) →
(ownT i (Send (Lit (LitLoc l cright)) e) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (Lit $ LitLoc l cright) K d'
★ ownSP (<[l:= (l1, l2 ++ [v])]>σ).
Proof.
iIntros (????) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; auto.
Qed.
Lemma refine_rcase_left_left_pst E σ K d d' l l1 l2 e1 e2 i:
d ≤ Kd →
d' ≤ Kd →
σ !! l = Some (l1, (InjLV $ LitV LitUnit) :: l2) →
(ownT i (RCase (Lit (LitLoc l cleft)) e1 e2) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (App e1 (Lit $ LitLoc l cleft)) K d'
★ ownSP (<[l := (l1, l2)]>σ).
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; auto.
Qed.
Lemma refine_rcase_left_right_pst E σ K d d' l l1 l2 e1 e2 i:
d ≤ Kd →
d' ≤ Kd →
σ !! l = Some (l1, (InjRV $ LitV LitUnit) :: l2) →
(ownT i (RCase (Lit (LitLoc l cleft)) e1 e2) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (App e2 (Lit $ LitLoc l cleft)) K d'
★ ownSP (<[l := (l1, l2)]>σ).
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; auto.
Qed.
Lemma refine_rcase_left_miss_pst E σ K d d' l l1 e1 e2 i:
d ≤ Kd →
d' ≤ Kd →
σ !! l = Some (l1, []) →
(ownT i (RCase (Lit (LitLoc l cleft)) e1 e2) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (RCase (Lit (LitLoc l cleft)) e1 e2) K d'
★ ownSP σ.
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; eauto.
Qed.
Lemma refine_rcase_right_left_pst E σ K d d' l l1 l2 e1 e2 i:
d ≤ Kd →
d' ≤ Kd →
σ !! l = Some ((InjLV $ LitV LitUnit) :: l1, l2) →
(ownT i (RCase (Lit (LitLoc l cright)) e1 e2) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (App e1 (Lit $ LitLoc l cright)) K d'
★ ownSP (<[l := (l1, l2)]>σ).
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; auto.
Qed.
Lemma refine_rcase_right_right_pst E σ K d d' l l1 l2 e1 e2 i:
d ≤ Kd →
d' ≤ Kd →
σ !! l = Some ((InjRV $ LitV LitUnit) :: l1, l2) →
(ownT i (RCase (Lit (LitLoc l cright)) e1 e2) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (App e2 (Lit $ LitLoc l cright)) K d'
★ ownSP (<[l := (l1, l2)]>σ).
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; auto.
Qed.
Lemma refine_rcase_right_miss_pst E σ K d d' l l2 e1 e2 i:
d ≤ Kd →
d' ≤ Kd →
σ !! l = Some ([], l2) →
(ownT i (RCase (Lit (LitLoc l cright)) e1 e2) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (RCase (Lit (LitLoc l cright)) e1 e2) K d'
★ ownSP σ.
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; eauto.
Qed.
Lemma refine_select_left_pst E σ K d d' l s l1 l2 i :
d ≤ Kd →
d' ≤ Kd →
σ !! l = Some (l1, l2) →
(ownT i (Select (Lit (LitLoc l cleft)) s) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (Lit $ LitLoc l cleft) K d'
★ ownSP (<[l:= (l1 ++ [label_to_sum s], l2)]>σ).
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; auto.
Qed.
Lemma refine_select_right_pst E σ K d d' l s l1 l2 i :
d ≤ Kd →
d' ≤ Kd →
σ !! l = Some (l1, l2) →
(ownT i (Select (Lit (LitLoc l cright)) s) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (Lit $ LitLoc l cright) K d'
★ ownSP (<[l:= (l1, l2 ++ [label_to_sum s])]>σ).
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; auto.
Qed.
d ≤ Kd →
d' ≤ Kd →
(ownT i (Alloc) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (Pair (Lit $ LitLoc (fresh (dom _ σ)) cleft)
(Lit $ LitLoc (fresh (dom _ σ)) cright)) K d'
★ ownSP (<[fresh (dom _ σ):=([], [])]>σ) .
Proof.
iIntros (??) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; auto.
Qed.
Lemma refine_recv_left_pst E σ K d d' l l1 l2 v i:
d ≤ Kd →
d' ≤ Kd →
σ !! l = Some (l1, v :: l2) →
(ownT i (Recv (Lit (LitLoc l cleft))) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (Pair (Lit $ LitLoc l cleft) (of_val v)) K d'
★ ownSP (<[l := (l1, l2)]>σ).
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; auto.
Qed.
Lemma refine_recv_right_pst E σ K d d' l l1 l2 v i:
d ≤ Kd →
d' ≤ Kd →
σ !! l = Some (v :: l1, l2) →
(ownT i (Recv (Lit (LitLoc l cright))) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (Pair (Lit $ LitLoc l cright) (of_val v)) K d'
★ ownSP (<[l := (l1, l2)]>σ).
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; auto.
Qed.
Lemma refine_recv_right_miss_pst E σ K d d' l l2 i:
d ≤ Kd →
d' ≤ Kd →
σ !! l = Some ([], l2) →
(ownT i (Recv (Lit (LitLoc l cright))) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (Recv (Lit (LitLoc l cright))) K d'
★ ownSP σ.
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; eauto.
Qed.
Lemma refine_recv_left_miss_pst E σ K d d' l l1 i:
d ≤ Kd →
d' ≤ Kd →
σ !! l = Some (l1, []) →
(ownT i (Recv (Lit (LitLoc l cleft))) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (Recv (Lit (LitLoc l cleft))) K d'
★ ownSP σ.
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; eauto.
Qed.
Lemma refine_send_left_pst E σ K d d' l e v l1 l2 i :
d ≤ Kd →
d' ≤ Kd →
to_val e = Some v → σ !! l = Some (l1, l2) →
(ownT i (Send (Lit (LitLoc l cleft)) e) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (Lit $ LitLoc l cleft) K d'
★ ownSP (<[l:= (l1 ++ [v], l2)]>σ).
Proof.
iIntros (????) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; auto.
Qed.
Lemma refine_send_right_pst E σ K d d' l e v l1 l2 i :
d ≤ Kd →
d' ≤ Kd →
to_val e = Some v → σ !! l = Some (l1, l2) →
(ownT i (Send (Lit (LitLoc l cright)) e) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (Lit $ LitLoc l cright) K d'
★ ownSP (<[l:= (l1, l2 ++ [v])]>σ).
Proof.
iIntros (????) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; auto.
Qed.
Lemma refine_rcase_left_left_pst E σ K d d' l l1 l2 e1 e2 i:
d ≤ Kd →
d' ≤ Kd →
σ !! l = Some (l1, (InjLV $ LitV LitUnit) :: l2) →
(ownT i (RCase (Lit (LitLoc l cleft)) e1 e2) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (App e1 (Lit $ LitLoc l cleft)) K d'
★ ownSP (<[l := (l1, l2)]>σ).
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; auto.
Qed.
Lemma refine_rcase_left_right_pst E σ K d d' l l1 l2 e1 e2 i:
d ≤ Kd →
d' ≤ Kd →
σ !! l = Some (l1, (InjRV $ LitV LitUnit) :: l2) →
(ownT i (RCase (Lit (LitLoc l cleft)) e1 e2) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (App e2 (Lit $ LitLoc l cleft)) K d'
★ ownSP (<[l := (l1, l2)]>σ).
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; auto.
Qed.
Lemma refine_rcase_left_miss_pst E σ K d d' l l1 e1 e2 i:
d ≤ Kd →
d' ≤ Kd →
σ !! l = Some (l1, []) →
(ownT i (RCase (Lit (LitLoc l cleft)) e1 e2) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (RCase (Lit (LitLoc l cleft)) e1 e2) K d'
★ ownSP σ.
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; eauto.
Qed.
Lemma refine_rcase_right_left_pst E σ K d d' l l1 l2 e1 e2 i:
d ≤ Kd →
d' ≤ Kd →
σ !! l = Some ((InjLV $ LitV LitUnit) :: l1, l2) →
(ownT i (RCase (Lit (LitLoc l cright)) e1 e2) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (App e1 (Lit $ LitLoc l cright)) K d'
★ ownSP (<[l := (l1, l2)]>σ).
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; auto.
Qed.
Lemma refine_rcase_right_right_pst E σ K d d' l l1 l2 e1 e2 i:
d ≤ Kd →
d' ≤ Kd →
σ !! l = Some ((InjRV $ LitV LitUnit) :: l1, l2) →
(ownT i (RCase (Lit (LitLoc l cright)) e1 e2) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (App e2 (Lit $ LitLoc l cright)) K d'
★ ownSP (<[l := (l1, l2)]>σ).
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; auto.
Qed.
Lemma refine_rcase_right_miss_pst E σ K d d' l l2 e1 e2 i:
d ≤ Kd →
d' ≤ Kd →
σ !! l = Some ([], l2) →
(ownT i (RCase (Lit (LitLoc l cright)) e1 e2) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (RCase (Lit (LitLoc l cright)) e1 e2) K d'
★ ownSP σ.
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; eauto.
Qed.
Lemma refine_select_left_pst E σ K d d' l s l1 l2 i :
d ≤ Kd →
d' ≤ Kd →
σ !! l = Some (l1, l2) →
(ownT i (Select (Lit (LitLoc l cleft)) s) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (Lit $ LitLoc l cleft) K d'
★ ownSP (<[l:= (l1 ++ [label_to_sum s], l2)]>σ).
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; auto.
Qed.
Lemma refine_select_right_pst E σ K d d' l s l1 l2 i :
d ≤ Kd →
d' ≤ Kd →
σ !! l = Some (l1, l2) →
(ownT i (Select (Lit (LitLoc l cright)) s) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (Lit $ LitLoc l cright) K d'
★ ownSP (<[l:= (l1, l2 ++ [label_to_sum s])]>σ).
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; auto.
Qed.
Base axioms for core primitives of the language: Stateless reductions.
Unfortunately, whereas the wp rules do not require physical state ownership,
the refinement monoid construction does require ownSP. Hence, we suffix them by pst
as in the above rules. Later, when we develop the heap monoid for the source language,
we prove versions without this ownership requirement.
Lemma refine_fork_pst E σ K d d' e i :
d ≤ Kd →
d' ≤ Kd →
(ownT i (Fork e) K d ★ ownSP σ) ⊢
|={E}=>> ∃ i', ownT i (Lit LitUnit) K d'
★ ownT i' e [] (fresh_delay chan_lang Fd e) ★ ownSP σ.
Proof.
iIntros (??) "Hown".
iApply ownT_ownSP_step_fork; last done; eauto.
eapply head_prim_step. econstructor; eauto.
Qed.
Lemma refine_rec_pst E σ K f x erec e1 e2 d d' i :
d ≤ Kd →
d' ≤ Kd →
e1 = Rec f x erec →
is_Some (to_val e2) →
Closed (f :b: x :b: []) erec →
(ownT i (App e1 e2) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (subst' x e2 (subst' f e1 erec)) K d' ★ ownSP σ.
Proof.
intros ?? → [v2 ?] ?.
iIntros "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto; rewrite //= ?right_id.
eapply head_prim_step.
inv_head_step; eauto.
econstructor; eauto using chan_lang.to_of_val.
Qed.
Lemma refine_un_op_pst E op σ K l l' d d' i:
d ≤ Kd →
d' ≤ Kd →
un_op_eval op l = Some l' →
(ownT i (UnOp op (Lit l)) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (Lit l') K d' ★ ownSP σ.
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; eauto.
Qed.
Lemma refine_bin_op_pst E op σ K l1 l2 l' d d' i:
d ≤ Kd →
d' ≤ Kd →
bin_op_eval op l1 l2 = Some l' →
(ownT i (BinOp op (Lit l1) (Lit l2)) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (Lit l') K d' ★ ownSP σ.
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; eauto.
Qed.
Lemma refine_if_true_pst E σ K e1 e2 d d' i :
d ≤ Kd →
d' ≤ Kd →
(ownT i (If (Lit (LitBool true)) e1 e2) K d ★ ownSP σ) ⊢
|={E}=>> ownT i e1 K d' ★ ownSP σ.
Proof.
iIntros (??) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; eauto.
Qed.
Lemma refine_if_false_pst E σ K e1 e2 d d' i :
d ≤ Kd →
d' ≤ Kd →
(ownT i (If (Lit (LitBool false)) e1 e2) K d ★ ownSP σ) ⊢
|={E}=>> ownT i e2 K d' ★ ownSP σ.
Proof.
iIntros (??) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; eauto.
Qed.
Lemma refine_letp_pst E σ K x y e1 v1 e2 v2 eb d d' i :
d ≤ Kd →
d' ≤ Kd →
to_val e1 = Some v1 → to_val e2 = Some v2 →
Closed (x :b: y :b: []) eb →
(ownT i (Letp x y (Pair e1 e2) eb) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (subst' y e2 (subst' x e1 eb)) K d' ★ ownSP σ.
Proof.
iIntros (?????) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto; rewrite //= ?right_id.
eapply head_prim_step.
inv_head_step; eauto.
econstructor; eauto using chan_lang.to_of_val.
Qed.
Lemma refine_case_inl_pst E σ K e0 v0 e1 e2 d d' i :
d ≤ Kd →
d' ≤ Kd →
to_val e0 = Some v0 →
(ownT i (Case (InjL e0) e1 e2) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (App e1 e0) K d' ★ ownSP σ.
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; eauto.
Qed.
Lemma refine_case_inr_pst E σ K e0 v0 e1 e2 d d' i :
d ≤ Kd →
d' ≤ Kd →
to_val e0 = Some v0 →
(ownT i (Case (InjR e0) e1 e2) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (App e2 e0) K d' ★ ownSP σ.
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; eauto.
Qed.
End refine.