Library iris.program_logic.nat_delayed_language
From iris.program_logic Require Import language.
From iris.prelude Require Import set irelations.
Section delayed_lang.
Context (L: language).
Context (max: nat).
Context (fdelay: nat).
Definition delayed_expr := (expr L × nat)%type.
Definition delayed_val := val L.
Definition delayed_state := state L.
Definition delayed_of_val (v: delayed_val) : delayed_expr := (@of_val L v, 0).
Definition delayed_to_val (e: delayed_expr): option delayed_val :=
match to_val (fst e), (snd e) with
| Some v, 0 ⇒ Some v
| _, _ ⇒ None
end.
Definition delayed_atomic (e: delayed_expr) : bool :=
match (snd e) with
| S O ⇒ match to_val (fst e) with
| Some _ ⇒ true
| _ ⇒ false
end
| _ ⇒ false
end.
Definition fresh_delay (e: expr L): nat :=
match to_val e with
| None ⇒ fdelay
| Some _ ⇒ 0
end.
Inductive delayed_prim_step:
delayed_expr → delayed_state → delayed_expr → delayed_state → option (delayed_expr) → Prop :=
| base_step e σ e' σ' ef:
prim_step e σ e' σ' ef →
delayed_prim_step (e, 0) σ (e', max) σ' (default None ef (λ e, Some (e, fresh_delay e)))
| delay_step e d σ: delayed_prim_step (e, S d) σ (e, d) σ None.
Lemma delayed_to_of_val: ∀ v, delayed_to_val (delayed_of_val v) = Some v.
Proof.
intros; rewrite /delayed_of_val /delayed_to_val // to_of_val //=.
Qed.
Lemma delayed_of_to_val: ∀ e v, delayed_to_val e = Some v → delayed_of_val v = e.
Proof.
rewrite /delayed_of_val /delayed_to_val.
destruct e as (?&?); simpl. intros v.
case_match; last congruence.
case_match; last congruence.
inversion 1. subst. f_equal.
by apply of_to_val.
Qed.
Lemma delayed_val_stuck:
∀ e σ e' σ' ef, delayed_prim_step e σ e' σ' ef → delayed_to_val e = None.
Proof.
induction 1 as [ e p σ e' p' σ' ef pf Hps | ? p ].
- rewrite /delayed_to_val //=. erewrite val_stuck; eauto.
- rewrite /delayed_to_val //=. case_match; auto.
Qed.
Lemma delayed_atomic_not_val:
∀ e, delayed_atomic e → delayed_to_val e = None.
Proof.
intros (?&?). destruct n; [intros; exfalso; auto|].
rewrite /delayed_to_val //=.
case_match; auto.
Qed.
Lemma delayed_atomic_step: ∀ e1 σ1 e2 σ2 ef,
delayed_atomic e1 →
delayed_prim_step e1 σ1 e2 σ2 ef →
is_Some (delayed_to_val e2).
Proof.
intros e1 σ1 e2 σ2 ef Hda Hdps.
inversion Hdps; subst.
- exfalso. unfold delayed_atomic in Hda; auto.
- destruct d.
× rewrite /delayed_to_val //=.
unfold delayed_atomic in Hda. simpl in ×.
destruct (to_val e); last (by exfalso); eauto.
× exfalso. unfold delayed_atomic in Hda; auto.
Qed.
Program Definition delayed_lang_aux : language := {|
expr := delayed_expr; val := delayed_val; state := delayed_state;
of_val := delayed_of_val; to_val := delayed_to_val;
prim_step := delayed_prim_step;
|}.
Solve Obligations with eauto using delayed_to_of_val, delayed_of_to_val,
delayed_val_stuck, delayed_atomic_not_val, delayed_atomic_step.
Canonical Structure delayed_lang : language := delayed_lang_aux.
Definition erase_expr (e: delayed_expr) := fst e.
Definition erase_cfg (c: cfg delayed_lang) : cfg L :=
(map erase_expr (c.1), c.2).
Lemma map_cons_inv {A B}:
∀ b (lb: list B) (l: list A) (f: A → B),
b :: lb = map f l → ∃ a la, l = a :: la ∧ f a = b ∧ map f la = lb.
Proof.
intros b lb l f. rewrite Tauto.map_simpl. destruct l as [| a la]; first congruence.
intros Heq. inversion Heq. ∃ a, la; split_and!; eauto.
Qed.
Lemma map_app_inv {A B}:
∀ (l1 l2: list B) (l: list A) (f: A → B),
l1 ++ l2 = map f l → ∃ l1a l2a, l = l1a ++ l2a ∧ map f l1a = l1 ∧ map f l2a = l2.
Proof.
induction l1 as [| b l1]; intros l2 l f.
- rewrite app_nil_l. intros; ∃ [], l.
split_and!; eauto.
- rewrite Tauto.map_simpl; simpl. destruct l as [| a l0]; first congruence.
intros Heq. inversion Heq.
edestruct IHl1 as (l1a&l2a&?&?&?); eauto.
∃ (a :: l1a), l2a. split_and!; auto.
× rewrite -app_comm_cons.
congruence.
× simpl.
congruence.
Qed.
Lemma reducible_erase e σ: reducible (erase_expr e) σ → reducible e σ.
Proof.
intros (e'&σ'&ef'&Hstep).
destruct e as (e&[|n]).
- do 3 eexists; econstructor; eauto.
- do 3 eexists; econstructor.
Qed.
Lemma enabled_erase: ∀ c i, enabled idx_step (erase_cfg c) i → enabled idx_step c i.
Proof.
rewrite /enabled. intros ec i (ec'&Hs).
rewrite idx_step_equiv in Hs ×.
cut (∀ ec ec', idx_step' i ec ec' → ∀ c, ec = erase_cfg c →
∃ y : cfg delayed_lang, idx_step' i c y).
{ intros Hcut Hs. edestruct Hcut; eauto. eexists.
rewrite idx_step_equiv; eauto. }
clear; induction 1.
- intros. destruct c. rewrite /erase_cfg in H0. simpl in ×.
inversion H0. subst. apply map_cons_inv in H2 as (?&?&?&?&?).
destruct x. simpl in ×. subst.
destruct ef. simpl in ×.
× destruct n.
** ∃ ((e2, max) :: x0 ++ option_list (Some (e, fresh_delay e)), σ2).
eapply (idx_step_alt_hd_atomic _ _ _ (σ2: state delayed_lang) _ _).
specialize (base_step e1 s e2 σ2 (Some e)); simpl; eauto.
** ∃ ((e1, n) :: x0 ++ option_list None, s).
eapply (idx_step_alt_hd_atomic _ _ _ (s: state delayed_lang) _ _).
econstructor.
× destruct n.
** ∃ ((e2, max) :: x0 ++ (option_list (None)), σ2).
eapply (idx_step_alt_hd_atomic _ _ _ (σ2: state delayed_lang) _ _).
specialize (base_step e1 s e2 σ2 None); simpl; eauto.
** ∃ ((e1, n) :: x0 ++ option_list None, s).
eapply (idx_step_alt_hd_atomic _ _ _ (s: state delayed_lang) _ _).
econstructor.
- intros. destruct c. inversion H0.
eapply map_cons_inv in H2 as (?&?&?&?&?).
subst. edestruct (IHidx_step' (x0, s)); eauto.
destruct x1.
eexists. econstructor. eauto.
Qed.
Definition idx_measure (c: cfg delayed_lang) i : nat :=
nth i (map snd (fst c)) 0.
Lemma erase_option_list ef p:
map erase_expr (option_list (default None ef (λ e : expr L, Some (e, p)))) =
option_list (default None ef Some).
Proof.
destruct ef; simpl; auto.
Qed.
Lemma estep_or_dec_plt_hd {c: cfg delayed_lang} (e: trace idx_step c):
match e with
| trace_step i c c' HR e' ⇒
(idx_measure c' i) < (idx_measure c i) ∨
idx_step i (erase_cfg c) (erase_cfg c')
end.
Proof.
destruct e as [i c c' HR e'].
revert e'. inversion HR as [? ? ? ? ? ? ? ? ? Hprim]. subst.
induction Hprim.
- right.
unfold erase_cfg.
simpl. repeat (rewrite ?map_app; simpl).
destruct ef; econstructor; eauto using map_length; simpl; auto.
- left. unfold idx_measure. rewrite ?map_app.
rewrite ?app_nth2; rewrite map_length; auto.
assert (length t1 - length t1 = 0) as Hz by omega. rewrite Hz.
simpl; auto.
Qed.
Lemma estep_or_dec_plt_hd_miss {c: cfg delayed_lang} (e: trace idx_step c) i:
match e with
| trace_step i' c c' HR e' ⇒
i ≠ i' → length (fst c) > i → idx_measure c' i = idx_measure c i
end.
Proof.
destruct e as [i' c c' HR e'].
revert e'. inversion HR as [? ? ? ? ? ? ? ? ? Hprim]. subst.
unfold idx_measure.
intros ? Hneq Htid_in_dom.
simpl. repeat (rewrite ?map_app; simpl).
assert (i < length t1 ∨ i > length t1) as [|] by omega.
- rewrite ?app_nth1; auto; rewrite map_length; auto.
- rewrite ?app_nth2; auto; rewrite map_length; try eauto with arith.
assert (i - length t1 = S (i - length t1 - 1)) as Heq by omega.
rewrite Heq. simpl. auto.
rewrite ?app_length //= in Htid_in_dom.
rewrite ?app_nth1; auto; rewrite map_length; auto.
rewrite Heq. simpl.
rewrite -minus_n_O.
apply lt_S_n.
rewrite -Heq. clear Heq.
eapply (plus_lt_reg_l _ _ (length t1)).
assert (length t1 + (i - length t1) = i) as Heq' by omega.
rewrite Heq'. auto.
Qed.
Lemma estep_or_dec_plt_k_miss {c: cfg delayed_lang} (e: trace idx_step c) i:
∀ k, snd (tr2fun e k) ≠ i →
length (fst (fst (tr2fun e k))) > i →
idx_measure (fst (tr2fun e (S k))) i = idx_measure (fst (tr2fun e k)) i.
Proof.
intros k. revert c e i; induction k; intros.
- specialize (estep_or_dec_plt_hd_miss e i).
destruct e. destruct e. auto.
- destruct e.
specialize (IHk _ e i).
destruct e. simpl in ×. eauto.
Qed.
Lemma length_cfg_S {c: cfg delayed_lang} (e: trace idx_step c):
∀ k, length (fst (fst (tr2fun e k))) ≤ length (fst (fst (tr2fun e (S k)))).
Proof.
intros k. revert c e. induction k.
- intros. simpl.
destruct e as [? ? ? HR ?]. destruct e. simpl.
eapply (length_cfg_idx_step _ _ _ HR).
- intros. simpl. destruct e. specialize (IHk _ e).
eauto.
Qed.
Lemma length_cfg_monotone {c: cfg delayed_lang} (e: trace idx_step c):
∀ k k', k < k' → length (fst (fst (tr2fun e k))) ≤ length (fst (fst (tr2fun e k'))).
Proof.
intros k k' Hlt. revert c e. induction Hlt.
- intros. eapply length_cfg_S.
- intros. etransitivity; first eapply IHHlt.
eapply length_cfg_S.
Qed.
Lemma idx_step_tid_in_dom:
∀ {L: language} (c c': cfg L) i, idx_step i c c' → length (fst c) > i.
Proof.
inversion 1. subst. rewrite ?app_length. simpl. omega.
Qed.
Lemma idx_step_tid_in_dom_k {c: cfg delayed_lang} (e: trace idx_step c):
∀ i k, snd (tr2fun e k) = i → length (fst (fst (tr2fun e k))) > i.
Proof.
intros i k.
- specialize (tr2fun_succ idx_step _ e k).
intros. eapply idx_step_tid_in_dom. subst. eauto.
Qed.
Lemma estep_or_dec_plt_k_1 {c: cfg delayed_lang} (e: trace idx_step c):
∀ i k, snd (tr2fun e k) = i →
(idx_measure (fst (tr2fun e (S k))) i) <
(idx_measure (fst (tr2fun e k)) i)
∨ ∃ k'', k ≤ k'' ∧ k'' < S k ∧
snd (tr2fun e k'') = i ∧
idx_step i (erase_cfg (fst (tr2fun e k'')))
(erase_cfg (fst (tr2fun e (S k'')))).
Proof.
intros i k.
revert c e i.
induction k; intros ? ? i <-.
× specialize (estep_or_dec_plt_hd e).
destruct e. destruct e. simpl.
intros [?|?].
** left; auto.
** right. ∃ 0. split_and!; auto.
× destruct e.
specialize (IHk _ e (snd (tr2fun e k))).
edestruct IHk as [|(k''&?&?&?&?)]; auto.
right. ∃ (S k''). split_and!; simpl; auto.
** omega.
** omega.
Qed.
Lemma estep_or_dec_plt {c: cfg delayed_lang} (e: trace idx_step c):
∀ i k k', k < k' → snd (tr2fun e k) = i →
(idx_measure (fst (tr2fun e k')) i) <
(idx_measure (fst (tr2fun e k)) i)
∨ ∃ k'', k ≤ k'' ∧ k'' < k' ∧
snd (tr2fun e k'') = i ∧
idx_step i (erase_cfg (fst (tr2fun e k'')))
(erase_cfg (fst (tr2fun e (S k'')))).
Proof.
intros i k k' Hlt.
revert c e i. induction Hlt; intros.
- eapply estep_or_dec_plt_k_1; eauto.
- case (decide (snd (tr2fun e m) = i)); intros.
× edestruct (estep_or_dec_plt_k_1 e i m) as [|(k''&?&?&?&?)]; eauto.
** edestruct (IHHlt) as [?|(k''&?&?&?&?)]; eauto.
*** left. omega.
*** right. ∃ k''. split_and!; eauto.
** right. ∃ k''. split_and!; eauto. omega.
× edestruct (IHHlt) as [?|(k''&?&?&?&?)]; eauto.
** left.
erewrite estep_or_dec_plt_k_miss; eauto.
eapply le_gt_trans; first eapply length_cfg_monotone; eauto.
eapply idx_step_tid_in_dom_k; eauto.
** right. ∃ k''. split_and!; eauto.
Qed.
Lemma delayed_ae_estep (c: cfg delayed_lang) (e: trace idx_step c) (i: nat):
ae_taken e i → ae_estep idx_step idx_step erase_cfg c e i.
Proof.
rewrite tr2fun_ae_taken. intros Hae.
unfold ae_estep, ev_estep'.
specialize
(tr2fun_al_ev_2 idx_step _ e (λ p y, i = snd p
∧ idx_step i (erase_cfg (fst p)) (erase_cfg y))).
intros Hal_ev.
simpl in Hal_ev; rewrite Hal_ev; clear Hal_ev.
intros k. destruct (Hae k) as (kinit & Hk).
remember (idx_measure (fst (tr2fun e kinit)) i) as p eqn:Hpeq.
revert kinit k Hk Hpeq.
induction p as [p IH] using (well_founded_induction lt_wf).
intros kinit k (?&?) →.
destruct (Hae (S kinit)) as (knext & ? & ?).
edestruct (estep_or_dec_plt e i kinit knext) as [|(k'' & ? & ? & ? & ?)]; auto.
- intros. edestruct IH as (k'' & ? & ? & ?); eauto.
∃ k''. split_and!; eauto.
omega.
- ∃ k''. split_and!; eauto.
omega.
Qed.
Fixpoint Pow (A: Type) (n: nat) :=
match n with
| O ⇒ A
| S n' ⇒ prod A (Pow A n')
end.
Definition pow_plt (n: nat) (x y: Pow nat n) : Prop.
Proof.
induction n as [|n' pow_plt].
- simpl in ×. apply (lt x y).
- simpl in ×. destruct x as (px, x'). destruct y as (py, y').
exact ((lt px py ∧ x' = y') ∨ (px = py ∧ pow_plt x' y')).
Defined.
Lemma pow_plt_S: ∀ n x y, pow_plt (S n) x y ↔
(Relation_Operators.symprod _ _ lt (pow_plt n)) x y.
Proof.
induction n; intros; simpl.
- split. destruct x, y.
× intros [(?&?)|(?&?)]; subst; econstructor; eauto.
× inversion 1; subst; auto.
- split. destruct x, y.
× intros [(?&?)|(?&?)]; subst; econstructor; eauto.
× inversion 1; subst; auto.
Qed.
Lemma wf_iff: ∀ {A: Type} (r1 r2: relation A), (∀ x y, r1 x y ↔ r2 x y) → wf r2 → wf r1.
Proof.
intros ? r1 r2 Hequiv Hwf. intro a.
induction a as [a IH] using (well_founded_induction Hwf).
econstructor.
intros. eapply IH. eapply Hequiv. eauto.
Qed.
Require Wellfounded.Lexicographic_Product.
Lemma pow_plt_wf (n: nat): wf (pow_plt n).
Proof.
induction n.
- apply lt_wf.
- eapply (wf_iff); first eapply pow_plt_S.
apply (Wellfounded.Lexicographic_Product.wf_symprod); eauto.
apply lt_wf.
Qed.
Fixpoint firstn_tuple {A: Type} (n:nat) (def: A) (l:list A) : Pow A n :=
match n with
| 0 ⇒ match l with
| nil ⇒ def
| a :: l ⇒ a
end
| S n ⇒ match l with
| nil ⇒ (def, (firstn_tuple n def nil))
| a::l ⇒ (a, (firstn_tuple n def l))
end
end.
Definition cfg_measure (c: cfg delayed_lang) (n: nat) : Pow nat n :=
firstn_tuple n 0 (map snd (fst c)).
Lemma pow_plt_app:
∀ t1 t2 t2' σ σ',
pow_plt (length t2')
(cfg_measure (t2, σ) (length t2'))
(cfg_measure (t2', σ') (length t2')) →
pow_plt (length (t1 ++ t2'))
(cfg_measure (t1 ++ t2, σ) (length (t1 ++ t2')))
(cfg_measure (t1 ++ t2', σ') (length (t1 ++ t2'))).
Proof.
induction t1; simpl; auto.
intros. right. split; auto.
eapply IHt1. eauto.
Qed.
Lemma pow_plt_hd:
∀ e e' t t' ts σ σ',
lt t t' →
pow_plt (S (length ts))
(cfg_measure ((e, t) :: ts, σ) (S (length ts)))
(cfg_measure ((e', t') :: ts, σ') (S (length ts))).
Proof.
intros. simpl. left. auto.
Qed.
Lemma estep_or_dec_pow_plt_hd {c: cfg delayed_lang} (e: trace idx_step c):
match e with
| trace_step i c c' HR e' ⇒
(pow_plt (length (fst c)) (cfg_measure c' (length (fst c))) (cfg_measure c (length (fst c)))
∧ length (fst c) = length (fst c'))
∨ idx_step i (erase_cfg c) (erase_cfg c')
end.
Proof.
destruct e as [i c c' HR e'].
revert e'. inversion HR as [? ? ? ? ? ? ? ? ? Hprim]. subst.
induction Hprim.
- right.
unfold erase_cfg.
simpl. repeat (rewrite ?map_app; simpl).
destruct ef; econstructor; eauto using map_length; simpl; eauto.
- left.
split; simpl; rewrite app_nil_r; auto.
× apply pow_plt_app. apply pow_plt_hd; auto.
× rewrite ?app_length. simpl; auto.
Qed.
Lemma delayed_some_ev_estep (c: cfg delayed_lang) (e: trace idx_step c):
∃ i, ev_estep idx_step idx_step erase_cfg c e i.
Proof.
destruct e as [i c c' HR e'].
remember (cfg_measure c (length (fst c))) as p eqn:Hpeq.
remember (length (c.1)) as n eqn:Hneq.
revert i c c' HR e' Hneq Hpeq.
induction p as [p IH] using (well_founded_induction (pow_plt_wf n)).
intros.
destruct (estep_or_dec_pow_plt_hd (trace_step i c c' HR e')) as [(?&?)|].
× subst. destruct e'. edestruct IH as (i' & ?); eauto.
∃ i'. eapply ev_estep_later.
eauto.
× ∃ i. econstructor. eauto.
Qed.
Lemma erase_trace:
∀ (c: cfg delayed_lang) (e: trace (idx_step) c),
∃ (e': trace (idx_step) (erase_cfg c)), fair_pres _ _ e e'.
Proof.
intros. eapply ae_ev_estep_yield_fun_fair.
- intros. eapply ClassicalEpsilon.excluded_middle_informative.
- intros. eapply enabled_erase; auto.
- intros i c1 c2 HR.
destruct (ClassicalEpsilon.excluded_middle_informative
(idx_step i (erase_cfg c1) (erase_cfg c2))) as [|Hn].
× left. auto.
× right. split; auto.
inversion HR as [? ? ? ? ? ? ? ? ? Hprim]. subst.
inversion Hprim; subst.
** exfalso. eapply Hn.
unfold erase_cfg. rewrite ?map_app. simpl;
econstructor; simpl; eauto using map_length.
repeat f_equal. rewrite map_app. f_equal.
destruct ef0; simpl; auto.
** unfold erase_cfg. repeat (simpl; f_equal; rewrite ?map_app).
rewrite app_nil_r. auto.
- apply ae_ev_estep_intro_all; eauto using delayed_ae_estep, delayed_some_ev_estep.
Qed.
Lemma delayed_lang_dec:
(∀ (e: expr L) σ, { t | prim_step e σ (fst (fst t)) (snd (fst t)) (snd t)} +
{¬ ∃ e' σ' ef', prim_step e σ e' σ' ef'}) →
(∀ (e: expr (delayed_lang)) σ, { t | prim_step e σ (fst (fst t)) (snd (fst t)) (snd t)} +
{¬ ∃ e' σ' ef', prim_step e σ e' σ' ef'}).
Proof.
intros Hdec e σ. destruct e as (e&[|d]).
× edestruct (Hdec e σ) as [(t&Hstep)|Hn].
** left. destruct t as ((e'&σ')&ef').
∃ ((e', max), σ', (default None ef' (λ e, Some (e, fresh_delay e)))).
econstructor; eauto.
** right. intros (e'&σ'&ef'&Hstep).
inversion Hstep. eapply Hn. do 3 eexists. eauto.
× left. ∃ ((e, d), σ, None). simpl. econstructor.
Qed.
Lemma delayed_lang_det:
(∀ (e: expr L) σ e1' σ1' ef1' e2' σ2' ef2',
prim_step e σ e1' σ1' ef1' →
prim_step e σ e2' σ2' ef2' →
e1' = e2' ∧ σ1' = σ2' ∧ ef1' = ef2') →
(∀ (e: expr (delayed_lang)) σ e1' σ1' ef1' e2' σ2' ef2',
prim_step e σ e1' σ1' ef1' →
prim_step e σ e2' σ2' ef2' →
e1' = e2' ∧ σ1' = σ2' ∧ ef1' = ef2').
Proof.
intros Hdet e σ e1' σ1' ef1' e2' σ2' ef2'.
inversion 1 as [????? Hbstep1|]. subst.
- inversion 1 as [????? Hbstep2|]. subst.
edestruct (Hdet _ _ _ _ _ _ _ _ Hbstep1 Hbstep2) as (->&->&->); eauto.
- inversion 1.
subst; auto.
Qed.
Lemma delayed_erase_isteps:
∀ l c1 c2, isteps idx_step l c1 c2 →
∃ l', isteps idx_step l' (erase_cfg c1) (erase_cfg c2).
Proof.
induction 1 as [| i ? ? x' y' Hs His IH].
- ∃ []; econstructor.
- inversion Hs.
inversion H1.
× edestruct IH as (l'&?).
∃ (i :: l').
econstructor; eauto.
econstructor; eauto.
** rewrite H. rewrite /erase_cfg ?map_app //=.
repeat f_equal. subst. eauto.
** rewrite H0. rewrite /erase_cfg ?map_app //=.
repeat f_equal. subst. eauto.
rewrite map_app. destruct ef0; simpl in *; subst; simpl; auto.
** rewrite map_length. auto.
× assert (erase_cfg x = erase_cfg x') as →.
{ subst. rewrite /erase_cfg; f_equal.
rewrite ?map_app //= app_nil_r; f_equal. }
eauto.
Qed.
Lemma delayed_to_val_0 (e: expr L):
delayed_to_val (e, 0) = to_val e.
Proof.
rewrite /delayed_to_val //=. case_match; auto.
Qed.
Lemma delayed_lang_safe_refine {ΛT} R (e: expr ΛT) (σ: state ΛT) (e': expr L) σ' d:
@safe_refine ΛT (delayed_lang) R e σ (e', d) σ' →
@safe_refine ΛT L R e σ e' σ'.
Proof.
intros (HR1&HR2&HR3).
split_and!; eauto.
- intros.
edestruct HR2 as (?&?&?&?&?&Hcase); eauto.
edestruct delayed_erase_isteps as (l'&Hesteps); eauto.
do 4 eexists; split; eauto.
× rewrite /erase_cfg in Hesteps. simpl in ×. eauto.
× destruct Hcase as [(ebad&Hin&Hnr&?)|(Hvals&(v&?&?))].
** left. ∃ (erase_expr ebad).
split_and!; auto.
*** clear -Hin. induction x1; set_solver.
*** intros Hred. apply Hnr.
eapply reducible_erase; eauto.
*** destruct ebad as (ebad&n).
destruct n as [| n'].
**** simpl in ×.
rewrite -delayed_to_val_0; auto.
**** exfalso; eapply Hnr.
do 3 eexists; econstructor.
** right. split; auto.
**** clear -Hvals. induction Hvals as [| x ? Hx IH]; first econstructor.
simpl. econstructor; eauto.
destruct x as (x' & ?). simpl.
rewrite /to_val //= /delayed_to_val //= in Hx.
case_match; eauto.
**** ∃ v. split; auto. destruct x0.
simpl in ×. unfold delayed_to_val in ×.
case_match; simpl in *; last congruence.
case_match; simpl in *; auto; congruence.
- intros. edestruct HR3; eauto.
edestruct (erase_trace ([(e', d)], σ')); eauto.
Qed.
End delayed_lang.
From iris.prelude Require Import set irelations.
Section delayed_lang.
Context (L: language).
Context (max: nat).
Context (fdelay: nat).
Definition delayed_expr := (expr L × nat)%type.
Definition delayed_val := val L.
Definition delayed_state := state L.
Definition delayed_of_val (v: delayed_val) : delayed_expr := (@of_val L v, 0).
Definition delayed_to_val (e: delayed_expr): option delayed_val :=
match to_val (fst e), (snd e) with
| Some v, 0 ⇒ Some v
| _, _ ⇒ None
end.
Definition delayed_atomic (e: delayed_expr) : bool :=
match (snd e) with
| S O ⇒ match to_val (fst e) with
| Some _ ⇒ true
| _ ⇒ false
end
| _ ⇒ false
end.
Definition fresh_delay (e: expr L): nat :=
match to_val e with
| None ⇒ fdelay
| Some _ ⇒ 0
end.
Inductive delayed_prim_step:
delayed_expr → delayed_state → delayed_expr → delayed_state → option (delayed_expr) → Prop :=
| base_step e σ e' σ' ef:
prim_step e σ e' σ' ef →
delayed_prim_step (e, 0) σ (e', max) σ' (default None ef (λ e, Some (e, fresh_delay e)))
| delay_step e d σ: delayed_prim_step (e, S d) σ (e, d) σ None.
Lemma delayed_to_of_val: ∀ v, delayed_to_val (delayed_of_val v) = Some v.
Proof.
intros; rewrite /delayed_of_val /delayed_to_val // to_of_val //=.
Qed.
Lemma delayed_of_to_val: ∀ e v, delayed_to_val e = Some v → delayed_of_val v = e.
Proof.
rewrite /delayed_of_val /delayed_to_val.
destruct e as (?&?); simpl. intros v.
case_match; last congruence.
case_match; last congruence.
inversion 1. subst. f_equal.
by apply of_to_val.
Qed.
Lemma delayed_val_stuck:
∀ e σ e' σ' ef, delayed_prim_step e σ e' σ' ef → delayed_to_val e = None.
Proof.
induction 1 as [ e p σ e' p' σ' ef pf Hps | ? p ].
- rewrite /delayed_to_val //=. erewrite val_stuck; eauto.
- rewrite /delayed_to_val //=. case_match; auto.
Qed.
Lemma delayed_atomic_not_val:
∀ e, delayed_atomic e → delayed_to_val e = None.
Proof.
intros (?&?). destruct n; [intros; exfalso; auto|].
rewrite /delayed_to_val //=.
case_match; auto.
Qed.
Lemma delayed_atomic_step: ∀ e1 σ1 e2 σ2 ef,
delayed_atomic e1 →
delayed_prim_step e1 σ1 e2 σ2 ef →
is_Some (delayed_to_val e2).
Proof.
intros e1 σ1 e2 σ2 ef Hda Hdps.
inversion Hdps; subst.
- exfalso. unfold delayed_atomic in Hda; auto.
- destruct d.
× rewrite /delayed_to_val //=.
unfold delayed_atomic in Hda. simpl in ×.
destruct (to_val e); last (by exfalso); eauto.
× exfalso. unfold delayed_atomic in Hda; auto.
Qed.
Program Definition delayed_lang_aux : language := {|
expr := delayed_expr; val := delayed_val; state := delayed_state;
of_val := delayed_of_val; to_val := delayed_to_val;
prim_step := delayed_prim_step;
|}.
Solve Obligations with eauto using delayed_to_of_val, delayed_of_to_val,
delayed_val_stuck, delayed_atomic_not_val, delayed_atomic_step.
Canonical Structure delayed_lang : language := delayed_lang_aux.
Definition erase_expr (e: delayed_expr) := fst e.
Definition erase_cfg (c: cfg delayed_lang) : cfg L :=
(map erase_expr (c.1), c.2).
Lemma map_cons_inv {A B}:
∀ b (lb: list B) (l: list A) (f: A → B),
b :: lb = map f l → ∃ a la, l = a :: la ∧ f a = b ∧ map f la = lb.
Proof.
intros b lb l f. rewrite Tauto.map_simpl. destruct l as [| a la]; first congruence.
intros Heq. inversion Heq. ∃ a, la; split_and!; eauto.
Qed.
Lemma map_app_inv {A B}:
∀ (l1 l2: list B) (l: list A) (f: A → B),
l1 ++ l2 = map f l → ∃ l1a l2a, l = l1a ++ l2a ∧ map f l1a = l1 ∧ map f l2a = l2.
Proof.
induction l1 as [| b l1]; intros l2 l f.
- rewrite app_nil_l. intros; ∃ [], l.
split_and!; eauto.
- rewrite Tauto.map_simpl; simpl. destruct l as [| a l0]; first congruence.
intros Heq. inversion Heq.
edestruct IHl1 as (l1a&l2a&?&?&?); eauto.
∃ (a :: l1a), l2a. split_and!; auto.
× rewrite -app_comm_cons.
congruence.
× simpl.
congruence.
Qed.
Lemma reducible_erase e σ: reducible (erase_expr e) σ → reducible e σ.
Proof.
intros (e'&σ'&ef'&Hstep).
destruct e as (e&[|n]).
- do 3 eexists; econstructor; eauto.
- do 3 eexists; econstructor.
Qed.
Lemma enabled_erase: ∀ c i, enabled idx_step (erase_cfg c) i → enabled idx_step c i.
Proof.
rewrite /enabled. intros ec i (ec'&Hs).
rewrite idx_step_equiv in Hs ×.
cut (∀ ec ec', idx_step' i ec ec' → ∀ c, ec = erase_cfg c →
∃ y : cfg delayed_lang, idx_step' i c y).
{ intros Hcut Hs. edestruct Hcut; eauto. eexists.
rewrite idx_step_equiv; eauto. }
clear; induction 1.
- intros. destruct c. rewrite /erase_cfg in H0. simpl in ×.
inversion H0. subst. apply map_cons_inv in H2 as (?&?&?&?&?).
destruct x. simpl in ×. subst.
destruct ef. simpl in ×.
× destruct n.
** ∃ ((e2, max) :: x0 ++ option_list (Some (e, fresh_delay e)), σ2).
eapply (idx_step_alt_hd_atomic _ _ _ (σ2: state delayed_lang) _ _).
specialize (base_step e1 s e2 σ2 (Some e)); simpl; eauto.
** ∃ ((e1, n) :: x0 ++ option_list None, s).
eapply (idx_step_alt_hd_atomic _ _ _ (s: state delayed_lang) _ _).
econstructor.
× destruct n.
** ∃ ((e2, max) :: x0 ++ (option_list (None)), σ2).
eapply (idx_step_alt_hd_atomic _ _ _ (σ2: state delayed_lang) _ _).
specialize (base_step e1 s e2 σ2 None); simpl; eauto.
** ∃ ((e1, n) :: x0 ++ option_list None, s).
eapply (idx_step_alt_hd_atomic _ _ _ (s: state delayed_lang) _ _).
econstructor.
- intros. destruct c. inversion H0.
eapply map_cons_inv in H2 as (?&?&?&?&?).
subst. edestruct (IHidx_step' (x0, s)); eauto.
destruct x1.
eexists. econstructor. eauto.
Qed.
Definition idx_measure (c: cfg delayed_lang) i : nat :=
nth i (map snd (fst c)) 0.
Lemma erase_option_list ef p:
map erase_expr (option_list (default None ef (λ e : expr L, Some (e, p)))) =
option_list (default None ef Some).
Proof.
destruct ef; simpl; auto.
Qed.
Lemma estep_or_dec_plt_hd {c: cfg delayed_lang} (e: trace idx_step c):
match e with
| trace_step i c c' HR e' ⇒
(idx_measure c' i) < (idx_measure c i) ∨
idx_step i (erase_cfg c) (erase_cfg c')
end.
Proof.
destruct e as [i c c' HR e'].
revert e'. inversion HR as [? ? ? ? ? ? ? ? ? Hprim]. subst.
induction Hprim.
- right.
unfold erase_cfg.
simpl. repeat (rewrite ?map_app; simpl).
destruct ef; econstructor; eauto using map_length; simpl; auto.
- left. unfold idx_measure. rewrite ?map_app.
rewrite ?app_nth2; rewrite map_length; auto.
assert (length t1 - length t1 = 0) as Hz by omega. rewrite Hz.
simpl; auto.
Qed.
Lemma estep_or_dec_plt_hd_miss {c: cfg delayed_lang} (e: trace idx_step c) i:
match e with
| trace_step i' c c' HR e' ⇒
i ≠ i' → length (fst c) > i → idx_measure c' i = idx_measure c i
end.
Proof.
destruct e as [i' c c' HR e'].
revert e'. inversion HR as [? ? ? ? ? ? ? ? ? Hprim]. subst.
unfold idx_measure.
intros ? Hneq Htid_in_dom.
simpl. repeat (rewrite ?map_app; simpl).
assert (i < length t1 ∨ i > length t1) as [|] by omega.
- rewrite ?app_nth1; auto; rewrite map_length; auto.
- rewrite ?app_nth2; auto; rewrite map_length; try eauto with arith.
assert (i - length t1 = S (i - length t1 - 1)) as Heq by omega.
rewrite Heq. simpl. auto.
rewrite ?app_length //= in Htid_in_dom.
rewrite ?app_nth1; auto; rewrite map_length; auto.
rewrite Heq. simpl.
rewrite -minus_n_O.
apply lt_S_n.
rewrite -Heq. clear Heq.
eapply (plus_lt_reg_l _ _ (length t1)).
assert (length t1 + (i - length t1) = i) as Heq' by omega.
rewrite Heq'. auto.
Qed.
Lemma estep_or_dec_plt_k_miss {c: cfg delayed_lang} (e: trace idx_step c) i:
∀ k, snd (tr2fun e k) ≠ i →
length (fst (fst (tr2fun e k))) > i →
idx_measure (fst (tr2fun e (S k))) i = idx_measure (fst (tr2fun e k)) i.
Proof.
intros k. revert c e i; induction k; intros.
- specialize (estep_or_dec_plt_hd_miss e i).
destruct e. destruct e. auto.
- destruct e.
specialize (IHk _ e i).
destruct e. simpl in ×. eauto.
Qed.
Lemma length_cfg_S {c: cfg delayed_lang} (e: trace idx_step c):
∀ k, length (fst (fst (tr2fun e k))) ≤ length (fst (fst (tr2fun e (S k)))).
Proof.
intros k. revert c e. induction k.
- intros. simpl.
destruct e as [? ? ? HR ?]. destruct e. simpl.
eapply (length_cfg_idx_step _ _ _ HR).
- intros. simpl. destruct e. specialize (IHk _ e).
eauto.
Qed.
Lemma length_cfg_monotone {c: cfg delayed_lang} (e: trace idx_step c):
∀ k k', k < k' → length (fst (fst (tr2fun e k))) ≤ length (fst (fst (tr2fun e k'))).
Proof.
intros k k' Hlt. revert c e. induction Hlt.
- intros. eapply length_cfg_S.
- intros. etransitivity; first eapply IHHlt.
eapply length_cfg_S.
Qed.
Lemma idx_step_tid_in_dom:
∀ {L: language} (c c': cfg L) i, idx_step i c c' → length (fst c) > i.
Proof.
inversion 1. subst. rewrite ?app_length. simpl. omega.
Qed.
Lemma idx_step_tid_in_dom_k {c: cfg delayed_lang} (e: trace idx_step c):
∀ i k, snd (tr2fun e k) = i → length (fst (fst (tr2fun e k))) > i.
Proof.
intros i k.
- specialize (tr2fun_succ idx_step _ e k).
intros. eapply idx_step_tid_in_dom. subst. eauto.
Qed.
Lemma estep_or_dec_plt_k_1 {c: cfg delayed_lang} (e: trace idx_step c):
∀ i k, snd (tr2fun e k) = i →
(idx_measure (fst (tr2fun e (S k))) i) <
(idx_measure (fst (tr2fun e k)) i)
∨ ∃ k'', k ≤ k'' ∧ k'' < S k ∧
snd (tr2fun e k'') = i ∧
idx_step i (erase_cfg (fst (tr2fun e k'')))
(erase_cfg (fst (tr2fun e (S k'')))).
Proof.
intros i k.
revert c e i.
induction k; intros ? ? i <-.
× specialize (estep_or_dec_plt_hd e).
destruct e. destruct e. simpl.
intros [?|?].
** left; auto.
** right. ∃ 0. split_and!; auto.
× destruct e.
specialize (IHk _ e (snd (tr2fun e k))).
edestruct IHk as [|(k''&?&?&?&?)]; auto.
right. ∃ (S k''). split_and!; simpl; auto.
** omega.
** omega.
Qed.
Lemma estep_or_dec_plt {c: cfg delayed_lang} (e: trace idx_step c):
∀ i k k', k < k' → snd (tr2fun e k) = i →
(idx_measure (fst (tr2fun e k')) i) <
(idx_measure (fst (tr2fun e k)) i)
∨ ∃ k'', k ≤ k'' ∧ k'' < k' ∧
snd (tr2fun e k'') = i ∧
idx_step i (erase_cfg (fst (tr2fun e k'')))
(erase_cfg (fst (tr2fun e (S k'')))).
Proof.
intros i k k' Hlt.
revert c e i. induction Hlt; intros.
- eapply estep_or_dec_plt_k_1; eauto.
- case (decide (snd (tr2fun e m) = i)); intros.
× edestruct (estep_or_dec_plt_k_1 e i m) as [|(k''&?&?&?&?)]; eauto.
** edestruct (IHHlt) as [?|(k''&?&?&?&?)]; eauto.
*** left. omega.
*** right. ∃ k''. split_and!; eauto.
** right. ∃ k''. split_and!; eauto. omega.
× edestruct (IHHlt) as [?|(k''&?&?&?&?)]; eauto.
** left.
erewrite estep_or_dec_plt_k_miss; eauto.
eapply le_gt_trans; first eapply length_cfg_monotone; eauto.
eapply idx_step_tid_in_dom_k; eauto.
** right. ∃ k''. split_and!; eauto.
Qed.
Lemma delayed_ae_estep (c: cfg delayed_lang) (e: trace idx_step c) (i: nat):
ae_taken e i → ae_estep idx_step idx_step erase_cfg c e i.
Proof.
rewrite tr2fun_ae_taken. intros Hae.
unfold ae_estep, ev_estep'.
specialize
(tr2fun_al_ev_2 idx_step _ e (λ p y, i = snd p
∧ idx_step i (erase_cfg (fst p)) (erase_cfg y))).
intros Hal_ev.
simpl in Hal_ev; rewrite Hal_ev; clear Hal_ev.
intros k. destruct (Hae k) as (kinit & Hk).
remember (idx_measure (fst (tr2fun e kinit)) i) as p eqn:Hpeq.
revert kinit k Hk Hpeq.
induction p as [p IH] using (well_founded_induction lt_wf).
intros kinit k (?&?) →.
destruct (Hae (S kinit)) as (knext & ? & ?).
edestruct (estep_or_dec_plt e i kinit knext) as [|(k'' & ? & ? & ? & ?)]; auto.
- intros. edestruct IH as (k'' & ? & ? & ?); eauto.
∃ k''. split_and!; eauto.
omega.
- ∃ k''. split_and!; eauto.
omega.
Qed.
Fixpoint Pow (A: Type) (n: nat) :=
match n with
| O ⇒ A
| S n' ⇒ prod A (Pow A n')
end.
Definition pow_plt (n: nat) (x y: Pow nat n) : Prop.
Proof.
induction n as [|n' pow_plt].
- simpl in ×. apply (lt x y).
- simpl in ×. destruct x as (px, x'). destruct y as (py, y').
exact ((lt px py ∧ x' = y') ∨ (px = py ∧ pow_plt x' y')).
Defined.
Lemma pow_plt_S: ∀ n x y, pow_plt (S n) x y ↔
(Relation_Operators.symprod _ _ lt (pow_plt n)) x y.
Proof.
induction n; intros; simpl.
- split. destruct x, y.
× intros [(?&?)|(?&?)]; subst; econstructor; eauto.
× inversion 1; subst; auto.
- split. destruct x, y.
× intros [(?&?)|(?&?)]; subst; econstructor; eauto.
× inversion 1; subst; auto.
Qed.
Lemma wf_iff: ∀ {A: Type} (r1 r2: relation A), (∀ x y, r1 x y ↔ r2 x y) → wf r2 → wf r1.
Proof.
intros ? r1 r2 Hequiv Hwf. intro a.
induction a as [a IH] using (well_founded_induction Hwf).
econstructor.
intros. eapply IH. eapply Hequiv. eauto.
Qed.
Require Wellfounded.Lexicographic_Product.
Lemma pow_plt_wf (n: nat): wf (pow_plt n).
Proof.
induction n.
- apply lt_wf.
- eapply (wf_iff); first eapply pow_plt_S.
apply (Wellfounded.Lexicographic_Product.wf_symprod); eauto.
apply lt_wf.
Qed.
Fixpoint firstn_tuple {A: Type} (n:nat) (def: A) (l:list A) : Pow A n :=
match n with
| 0 ⇒ match l with
| nil ⇒ def
| a :: l ⇒ a
end
| S n ⇒ match l with
| nil ⇒ (def, (firstn_tuple n def nil))
| a::l ⇒ (a, (firstn_tuple n def l))
end
end.
Definition cfg_measure (c: cfg delayed_lang) (n: nat) : Pow nat n :=
firstn_tuple n 0 (map snd (fst c)).
Lemma pow_plt_app:
∀ t1 t2 t2' σ σ',
pow_plt (length t2')
(cfg_measure (t2, σ) (length t2'))
(cfg_measure (t2', σ') (length t2')) →
pow_plt (length (t1 ++ t2'))
(cfg_measure (t1 ++ t2, σ) (length (t1 ++ t2')))
(cfg_measure (t1 ++ t2', σ') (length (t1 ++ t2'))).
Proof.
induction t1; simpl; auto.
intros. right. split; auto.
eapply IHt1. eauto.
Qed.
Lemma pow_plt_hd:
∀ e e' t t' ts σ σ',
lt t t' →
pow_plt (S (length ts))
(cfg_measure ((e, t) :: ts, σ) (S (length ts)))
(cfg_measure ((e', t') :: ts, σ') (S (length ts))).
Proof.
intros. simpl. left. auto.
Qed.
Lemma estep_or_dec_pow_plt_hd {c: cfg delayed_lang} (e: trace idx_step c):
match e with
| trace_step i c c' HR e' ⇒
(pow_plt (length (fst c)) (cfg_measure c' (length (fst c))) (cfg_measure c (length (fst c)))
∧ length (fst c) = length (fst c'))
∨ idx_step i (erase_cfg c) (erase_cfg c')
end.
Proof.
destruct e as [i c c' HR e'].
revert e'. inversion HR as [? ? ? ? ? ? ? ? ? Hprim]. subst.
induction Hprim.
- right.
unfold erase_cfg.
simpl. repeat (rewrite ?map_app; simpl).
destruct ef; econstructor; eauto using map_length; simpl; eauto.
- left.
split; simpl; rewrite app_nil_r; auto.
× apply pow_plt_app. apply pow_plt_hd; auto.
× rewrite ?app_length. simpl; auto.
Qed.
Lemma delayed_some_ev_estep (c: cfg delayed_lang) (e: trace idx_step c):
∃ i, ev_estep idx_step idx_step erase_cfg c e i.
Proof.
destruct e as [i c c' HR e'].
remember (cfg_measure c (length (fst c))) as p eqn:Hpeq.
remember (length (c.1)) as n eqn:Hneq.
revert i c c' HR e' Hneq Hpeq.
induction p as [p IH] using (well_founded_induction (pow_plt_wf n)).
intros.
destruct (estep_or_dec_pow_plt_hd (trace_step i c c' HR e')) as [(?&?)|].
× subst. destruct e'. edestruct IH as (i' & ?); eauto.
∃ i'. eapply ev_estep_later.
eauto.
× ∃ i. econstructor. eauto.
Qed.
Lemma erase_trace:
∀ (c: cfg delayed_lang) (e: trace (idx_step) c),
∃ (e': trace (idx_step) (erase_cfg c)), fair_pres _ _ e e'.
Proof.
intros. eapply ae_ev_estep_yield_fun_fair.
- intros. eapply ClassicalEpsilon.excluded_middle_informative.
- intros. eapply enabled_erase; auto.
- intros i c1 c2 HR.
destruct (ClassicalEpsilon.excluded_middle_informative
(idx_step i (erase_cfg c1) (erase_cfg c2))) as [|Hn].
× left. auto.
× right. split; auto.
inversion HR as [? ? ? ? ? ? ? ? ? Hprim]. subst.
inversion Hprim; subst.
** exfalso. eapply Hn.
unfold erase_cfg. rewrite ?map_app. simpl;
econstructor; simpl; eauto using map_length.
repeat f_equal. rewrite map_app. f_equal.
destruct ef0; simpl; auto.
** unfold erase_cfg. repeat (simpl; f_equal; rewrite ?map_app).
rewrite app_nil_r. auto.
- apply ae_ev_estep_intro_all; eauto using delayed_ae_estep, delayed_some_ev_estep.
Qed.
Lemma delayed_lang_dec:
(∀ (e: expr L) σ, { t | prim_step e σ (fst (fst t)) (snd (fst t)) (snd t)} +
{¬ ∃ e' σ' ef', prim_step e σ e' σ' ef'}) →
(∀ (e: expr (delayed_lang)) σ, { t | prim_step e σ (fst (fst t)) (snd (fst t)) (snd t)} +
{¬ ∃ e' σ' ef', prim_step e σ e' σ' ef'}).
Proof.
intros Hdec e σ. destruct e as (e&[|d]).
× edestruct (Hdec e σ) as [(t&Hstep)|Hn].
** left. destruct t as ((e'&σ')&ef').
∃ ((e', max), σ', (default None ef' (λ e, Some (e, fresh_delay e)))).
econstructor; eauto.
** right. intros (e'&σ'&ef'&Hstep).
inversion Hstep. eapply Hn. do 3 eexists. eauto.
× left. ∃ ((e, d), σ, None). simpl. econstructor.
Qed.
Lemma delayed_lang_det:
(∀ (e: expr L) σ e1' σ1' ef1' e2' σ2' ef2',
prim_step e σ e1' σ1' ef1' →
prim_step e σ e2' σ2' ef2' →
e1' = e2' ∧ σ1' = σ2' ∧ ef1' = ef2') →
(∀ (e: expr (delayed_lang)) σ e1' σ1' ef1' e2' σ2' ef2',
prim_step e σ e1' σ1' ef1' →
prim_step e σ e2' σ2' ef2' →
e1' = e2' ∧ σ1' = σ2' ∧ ef1' = ef2').
Proof.
intros Hdet e σ e1' σ1' ef1' e2' σ2' ef2'.
inversion 1 as [????? Hbstep1|]. subst.
- inversion 1 as [????? Hbstep2|]. subst.
edestruct (Hdet _ _ _ _ _ _ _ _ Hbstep1 Hbstep2) as (->&->&->); eauto.
- inversion 1.
subst; auto.
Qed.
Lemma delayed_erase_isteps:
∀ l c1 c2, isteps idx_step l c1 c2 →
∃ l', isteps idx_step l' (erase_cfg c1) (erase_cfg c2).
Proof.
induction 1 as [| i ? ? x' y' Hs His IH].
- ∃ []; econstructor.
- inversion Hs.
inversion H1.
× edestruct IH as (l'&?).
∃ (i :: l').
econstructor; eauto.
econstructor; eauto.
** rewrite H. rewrite /erase_cfg ?map_app //=.
repeat f_equal. subst. eauto.
** rewrite H0. rewrite /erase_cfg ?map_app //=.
repeat f_equal. subst. eauto.
rewrite map_app. destruct ef0; simpl in *; subst; simpl; auto.
** rewrite map_length. auto.
× assert (erase_cfg x = erase_cfg x') as →.
{ subst. rewrite /erase_cfg; f_equal.
rewrite ?map_app //= app_nil_r; f_equal. }
eauto.
Qed.
Lemma delayed_to_val_0 (e: expr L):
delayed_to_val (e, 0) = to_val e.
Proof.
rewrite /delayed_to_val //=. case_match; auto.
Qed.
Lemma delayed_lang_safe_refine {ΛT} R (e: expr ΛT) (σ: state ΛT) (e': expr L) σ' d:
@safe_refine ΛT (delayed_lang) R e σ (e', d) σ' →
@safe_refine ΛT L R e σ e' σ'.
Proof.
intros (HR1&HR2&HR3).
split_and!; eauto.
- intros.
edestruct HR2 as (?&?&?&?&?&Hcase); eauto.
edestruct delayed_erase_isteps as (l'&Hesteps); eauto.
do 4 eexists; split; eauto.
× rewrite /erase_cfg in Hesteps. simpl in ×. eauto.
× destruct Hcase as [(ebad&Hin&Hnr&?)|(Hvals&(v&?&?))].
** left. ∃ (erase_expr ebad).
split_and!; auto.
*** clear -Hin. induction x1; set_solver.
*** intros Hred. apply Hnr.
eapply reducible_erase; eauto.
*** destruct ebad as (ebad&n).
destruct n as [| n'].
**** simpl in ×.
rewrite -delayed_to_val_0; auto.
**** exfalso; eapply Hnr.
do 3 eexists; econstructor.
** right. split; auto.
**** clear -Hvals. induction Hvals as [| x ? Hx IH]; first econstructor.
simpl. econstructor; eauto.
destruct x as (x' & ?). simpl.
rewrite /to_val //= /delayed_to_val //= in Hx.
case_match; eauto.
**** ∃ v. split; auto. destruct x0.
simpl in ×. unfold delayed_to_val in ×.
case_match; simpl in *; last congruence.
case_match; simpl in *; auto; congruence.
- intros. edestruct HR3; eauto.
edestruct (erase_trace ([(e', d)], σ')); eauto.
Qed.
End delayed_lang.