Library iris.program_logic.delayed_language
From iris.program_logic Require Import language.
From iris.prelude Require Import set irelations.
Section delayed_lang.
Context (L: language).
Context (P: Set) (plt: relation P) `{StrictOrder P plt}.
Context `{IN: Inhabited P}.
Context (P_fin: {l : list P | ∀ x : P, x ∈ l }).
Context (plt_dec: ∀ x y, {plt x y} + {¬ plt x y }).
Context (plt_trans: ∀ x y z, plt x y → plt y z → plt x z).
Context (plt_wf: well_founded plt).
Definition minimal x := ¬ (∃ x', plt x' x).
Lemma minimal_dec: ∀ x, sumbool (∃ x', plt x' x) (¬ ∃ x', plt x' x).
Proof.
destruct P_fin as (l & Hl).
intros x.
assert (∀ x' : P, x' ∈ l ∨ ¬ plt x' x) as Hl'; eauto.
clear Hl. revert x Hl'.
induction l; intros x Hl'.
× right. intros (x'&Hplt).
specialize (Hl' x'). destruct Hl' as [HlIn | Hnplt ]; eauto.
inversion HlIn.
× destruct (plt_dec a x); first (left; eauto).
eapply IHl. intros.
specialize (Hl' x'). destruct Hl' as [HlIn | Hnplt ]; eauto.
inversion HlIn; subst; auto.
Qed.
Lemma minimal_dec': ∀ x, {x' | plt x' x} + {minimal x}.
Proof.
destruct P_fin as (l & Hl).
intros x.
assert (∀ x' : P, x' ∈ l ∨ ¬ plt x' x) as Hl'; eauto.
clear Hl. revert x Hl'.
induction l; intros x Hl'.
× right. intros (x'&Hplt).
specialize (Hl' x'). destruct Hl' as [HlIn | Hnplt ]; eauto.
inversion HlIn.
× destruct (plt_dec a x); first (left; eauto).
eapply IHl. intros.
specialize (Hl' x'). destruct Hl' as [HlIn | Hnplt ]; eauto.
inversion HlIn; subst; auto.
Qed.
Definition mini : {x : P | minimal x }.
Proof.
destruct IN as [p].
induction p using (well_founded_induction plt_wf).
destruct (minimal_dec' p) as [(?&?)|].
- eapply H0; eauto.
- ∃ p. eauto.
Qed.
Definition delayed_expr := (expr L × P)%type.
Inductive delayed_val : Type :=
| delayed_val_minimal: ∀ (v: val L) (p: P), ¬ (∃ p', plt p' p) → delayed_val.
Definition delayed_state := state L.
Definition delayed_of_val (v: delayed_val) : delayed_expr :=
match v with
| delayed_val_minimal v p _ ⇒ (of_val v, p)
end.
Definition delayed_to_val (e: delayed_expr): option delayed_val :=
match to_val (fst e), minimal_dec (snd e) with
| Some v', right Pf ⇒ Some (delayed_val_minimal v' (snd e) Pf)
| _, _ ⇒ None
end.
Inductive delayed_atomic': delayed_expr → Prop :=
| delayed_succ_minimal_atomic:
∀ v p, (∃ p', plt p' p) →
(∀ p', plt p' p → minimal p') →
delayed_atomic' (of_val v, p).
Require ClassicalEpsilon.
Definition delayed_atomic: delayed_expr → bool.
Proof.
intros e.
destruct (ClassicalEpsilon.excluded_middle_informative (delayed_atomic' e)).
- exact true.
- exact false.
Defined.
Inductive delayed_prim_step:
delayed_expr → delayed_state → delayed_expr → delayed_state → option (delayed_expr) → Prop :=
| base_step e p σ e' p' σ' ef pf: prim_step e σ e' σ' ef →
delayed_prim_step (e, p) σ (e', p') σ'
(default None ef (λ e, Some (e, pf)))
| delay_step (e: expr L) p σ e p': plt p' p → delayed_prim_step (e, p) σ (e, p') σ None.
Lemma delayed_to_of_val: ∀ v, delayed_to_val (delayed_of_val v) = Some v.
Proof.
induction v.
- simpl. unfold delayed_to_val. simpl.
rewrite to_of_val. destruct (minimal_dec p); first exfalso; eauto.
repeat f_equal. apply proof_irrelevance.
Qed.
Lemma delayed_of_to_val: ∀ e v, delayed_to_val e = Some v → delayed_of_val v = e.
Proof.
induction v as [v p Pf].
destruct e as (e, p').
unfold delayed_to_val. simpl.
generalize (of_to_val e).
destruct (to_val e); auto.
- destruct (minimal_dec p'); first congruence.
intros Hofv Heq.
inversion Heq. subst.
rewrite Hofv; eauto.
- intros. congruence.
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 ].
- unfold delayed_to_val. simpl.
generalize (val_stuck e σ e' σ' ef) as Hvs.
destruct (to_val e); auto; intros.
eapply Hvs in Hps. congruence.
- unfold delayed_to_val. simpl.
destruct (minimal_dec p); destruct to_val; auto.
exfalso; eauto.
Qed.
Lemma delayed_atomic_not_val:
∀ e, delayed_atomic e → delayed_to_val e = None.
Proof.
intros e DA. unfold delayed_atomic in DA.
destruct (ClassicalEpsilon.excluded_middle_informative) as [d | nd]; last (exfalso; auto).
induction d as [v p Hpred].
unfold delayed_to_val.
simpl. rewrite to_of_val. destruct (minimal_dec p); auto.
exfalso; eauto.
Qed.
Lemma delayed_atomic_equiv:
∀ e, delayed_atomic e = true → delayed_atomic' e.
Proof.
intros e. unfold delayed_atomic.
destruct (ClassicalEpsilon.excluded_middle_informative) as [d | nd];
last (intros; congruence).
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.
- unfold delayed_atomic in Hda.
destruct (ClassicalEpsilon.excluded_middle_informative) as [Hda' | nd];
last (exfalso; auto).
inversion Hda' as [v p'' Hnm Hpred].
subst. exfalso.
assert (to_val (of_val v) = None) as HtoNone.
{ eapply val_stuck. eauto. }
rewrite to_of_val in HtoNone; congruence.
- unfold delayed_atomic in Hda.
destruct (ClassicalEpsilon.excluded_middle_informative) as [Hda' | nd];
last (exfalso; auto).
inversion Hda' as [v p'' Hnm Hpred]. subst.
unfold delayed_to_val. rewrite to_of_val.
destruct minimal_dec; simpl; eauto.
simpl in ×. exfalso. eapply Hpred; eauto.
Qed.
Program Definition delayed_lang : 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.
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 erase_prim_step e e' ef' s s':
prim_step (erase_expr e) s (erase_expr e') s' (default None ef' (λ ef, Some (erase_expr ef))) →
delayed_prim_step e s e' s' ef'.
Proof.
destruct e as (e & p).
destruct e' as (e' & p').
destruct ef' as [(ef&pf)|]; simpl; intros.
- specialize (base_step e p s e' p' s' (Some ef) pf); auto.
- specialize (base_step e p s e' p' s' None p); auto.
Qed.
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 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 H1. simpl in ×.
inversion H1. subst. apply map_cons_inv in H3 as (?&?&?&?&?).
destruct x. simpl in ×. subst.
destruct ef. simpl in ×.
∃ ((e2, p) :: x0 ++ option_list (Some (e, p)), σ2).
eapply (idx_step_alt_hd_atomic _ _ _ (σ2: state delayed_lang) _ _).
specialize (base_step e1 p s e2 p σ2 (Some e) p); simpl; eauto.
∃ ((e2, p) :: x0 ++ option_list None, σ2).
eapply (idx_step_alt_hd_atomic _ _ _ (σ2: state delayed_lang) _ _).
specialize (base_step e1 p s e2 p σ2 None p); simpl; eauto.
- intros. destruct c. inversion H0.
eapply map_cons_inv in H2 as (?&?&?&?&?).
subst. edestruct (IHi0 i0 (x0, s)); eauto.
destruct x1.
eexists. econstructor. eauto.
Qed.
Definition idx_measure (c: cfg delayed_lang) i : P :=
nth i (map snd (fst c)) (proj1_sig mini).
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' ⇒
plt (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).
rewrite erase_option_list.
econstructor; eauto using map_length.
destruct ef; 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 →
plt (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 →
plt (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.
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 plt_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 P n) : Prop.
Proof.
induction n as [|n' pow_plt].
- simpl in ×. apply (plt x y).
- simpl in ×. destruct x as (px, x'). destruct y as (py, y').
exact ((plt 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 _ _ plt (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.
- eauto.
- eapply (wf_iff); first eapply pow_plt_S.
apply (Wellfounded.Lexicographic_Product.wf_symprod); eauto.
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 P n :=
firstn_tuple n (proj1_sig mini) (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 σ σ',
plt 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).
rewrite erase_option_list.
econstructor; eauto using map_length.
destruct ef; auto.
- 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.
rewrite erase_option_list. destruct ef0; 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.
End delayed_lang.
From iris.prelude Require Import set irelations.
Section delayed_lang.
Context (L: language).
Context (P: Set) (plt: relation P) `{StrictOrder P plt}.
Context `{IN: Inhabited P}.
Context (P_fin: {l : list P | ∀ x : P, x ∈ l }).
Context (plt_dec: ∀ x y, {plt x y} + {¬ plt x y }).
Context (plt_trans: ∀ x y z, plt x y → plt y z → plt x z).
Context (plt_wf: well_founded plt).
Definition minimal x := ¬ (∃ x', plt x' x).
Lemma minimal_dec: ∀ x, sumbool (∃ x', plt x' x) (¬ ∃ x', plt x' x).
Proof.
destruct P_fin as (l & Hl).
intros x.
assert (∀ x' : P, x' ∈ l ∨ ¬ plt x' x) as Hl'; eauto.
clear Hl. revert x Hl'.
induction l; intros x Hl'.
× right. intros (x'&Hplt).
specialize (Hl' x'). destruct Hl' as [HlIn | Hnplt ]; eauto.
inversion HlIn.
× destruct (plt_dec a x); first (left; eauto).
eapply IHl. intros.
specialize (Hl' x'). destruct Hl' as [HlIn | Hnplt ]; eauto.
inversion HlIn; subst; auto.
Qed.
Lemma minimal_dec': ∀ x, {x' | plt x' x} + {minimal x}.
Proof.
destruct P_fin as (l & Hl).
intros x.
assert (∀ x' : P, x' ∈ l ∨ ¬ plt x' x) as Hl'; eauto.
clear Hl. revert x Hl'.
induction l; intros x Hl'.
× right. intros (x'&Hplt).
specialize (Hl' x'). destruct Hl' as [HlIn | Hnplt ]; eauto.
inversion HlIn.
× destruct (plt_dec a x); first (left; eauto).
eapply IHl. intros.
specialize (Hl' x'). destruct Hl' as [HlIn | Hnplt ]; eauto.
inversion HlIn; subst; auto.
Qed.
Definition mini : {x : P | minimal x }.
Proof.
destruct IN as [p].
induction p using (well_founded_induction plt_wf).
destruct (minimal_dec' p) as [(?&?)|].
- eapply H0; eauto.
- ∃ p. eauto.
Qed.
Definition delayed_expr := (expr L × P)%type.
Inductive delayed_val : Type :=
| delayed_val_minimal: ∀ (v: val L) (p: P), ¬ (∃ p', plt p' p) → delayed_val.
Definition delayed_state := state L.
Definition delayed_of_val (v: delayed_val) : delayed_expr :=
match v with
| delayed_val_minimal v p _ ⇒ (of_val v, p)
end.
Definition delayed_to_val (e: delayed_expr): option delayed_val :=
match to_val (fst e), minimal_dec (snd e) with
| Some v', right Pf ⇒ Some (delayed_val_minimal v' (snd e) Pf)
| _, _ ⇒ None
end.
Inductive delayed_atomic': delayed_expr → Prop :=
| delayed_succ_minimal_atomic:
∀ v p, (∃ p', plt p' p) →
(∀ p', plt p' p → minimal p') →
delayed_atomic' (of_val v, p).
Require ClassicalEpsilon.
Definition delayed_atomic: delayed_expr → bool.
Proof.
intros e.
destruct (ClassicalEpsilon.excluded_middle_informative (delayed_atomic' e)).
- exact true.
- exact false.
Defined.
Inductive delayed_prim_step:
delayed_expr → delayed_state → delayed_expr → delayed_state → option (delayed_expr) → Prop :=
| base_step e p σ e' p' σ' ef pf: prim_step e σ e' σ' ef →
delayed_prim_step (e, p) σ (e', p') σ'
(default None ef (λ e, Some (e, pf)))
| delay_step (e: expr L) p σ e p': plt p' p → delayed_prim_step (e, p) σ (e, p') σ None.
Lemma delayed_to_of_val: ∀ v, delayed_to_val (delayed_of_val v) = Some v.
Proof.
induction v.
- simpl. unfold delayed_to_val. simpl.
rewrite to_of_val. destruct (minimal_dec p); first exfalso; eauto.
repeat f_equal. apply proof_irrelevance.
Qed.
Lemma delayed_of_to_val: ∀ e v, delayed_to_val e = Some v → delayed_of_val v = e.
Proof.
induction v as [v p Pf].
destruct e as (e, p').
unfold delayed_to_val. simpl.
generalize (of_to_val e).
destruct (to_val e); auto.
- destruct (minimal_dec p'); first congruence.
intros Hofv Heq.
inversion Heq. subst.
rewrite Hofv; eauto.
- intros. congruence.
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 ].
- unfold delayed_to_val. simpl.
generalize (val_stuck e σ e' σ' ef) as Hvs.
destruct (to_val e); auto; intros.
eapply Hvs in Hps. congruence.
- unfold delayed_to_val. simpl.
destruct (minimal_dec p); destruct to_val; auto.
exfalso; eauto.
Qed.
Lemma delayed_atomic_not_val:
∀ e, delayed_atomic e → delayed_to_val e = None.
Proof.
intros e DA. unfold delayed_atomic in DA.
destruct (ClassicalEpsilon.excluded_middle_informative) as [d | nd]; last (exfalso; auto).
induction d as [v p Hpred].
unfold delayed_to_val.
simpl. rewrite to_of_val. destruct (minimal_dec p); auto.
exfalso; eauto.
Qed.
Lemma delayed_atomic_equiv:
∀ e, delayed_atomic e = true → delayed_atomic' e.
Proof.
intros e. unfold delayed_atomic.
destruct (ClassicalEpsilon.excluded_middle_informative) as [d | nd];
last (intros; congruence).
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.
- unfold delayed_atomic in Hda.
destruct (ClassicalEpsilon.excluded_middle_informative) as [Hda' | nd];
last (exfalso; auto).
inversion Hda' as [v p'' Hnm Hpred].
subst. exfalso.
assert (to_val (of_val v) = None) as HtoNone.
{ eapply val_stuck. eauto. }
rewrite to_of_val in HtoNone; congruence.
- unfold delayed_atomic in Hda.
destruct (ClassicalEpsilon.excluded_middle_informative) as [Hda' | nd];
last (exfalso; auto).
inversion Hda' as [v p'' Hnm Hpred]. subst.
unfold delayed_to_val. rewrite to_of_val.
destruct minimal_dec; simpl; eauto.
simpl in ×. exfalso. eapply Hpred; eauto.
Qed.
Program Definition delayed_lang : 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.
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 erase_prim_step e e' ef' s s':
prim_step (erase_expr e) s (erase_expr e') s' (default None ef' (λ ef, Some (erase_expr ef))) →
delayed_prim_step e s e' s' ef'.
Proof.
destruct e as (e & p).
destruct e' as (e' & p').
destruct ef' as [(ef&pf)|]; simpl; intros.
- specialize (base_step e p s e' p' s' (Some ef) pf); auto.
- specialize (base_step e p s e' p' s' None p); auto.
Qed.
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 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 H1. simpl in ×.
inversion H1. subst. apply map_cons_inv in H3 as (?&?&?&?&?).
destruct x. simpl in ×. subst.
destruct ef. simpl in ×.
∃ ((e2, p) :: x0 ++ option_list (Some (e, p)), σ2).
eapply (idx_step_alt_hd_atomic _ _ _ (σ2: state delayed_lang) _ _).
specialize (base_step e1 p s e2 p σ2 (Some e) p); simpl; eauto.
∃ ((e2, p) :: x0 ++ option_list None, σ2).
eapply (idx_step_alt_hd_atomic _ _ _ (σ2: state delayed_lang) _ _).
specialize (base_step e1 p s e2 p σ2 None p); simpl; eauto.
- intros. destruct c. inversion H0.
eapply map_cons_inv in H2 as (?&?&?&?&?).
subst. edestruct (IHi0 i0 (x0, s)); eauto.
destruct x1.
eexists. econstructor. eauto.
Qed.
Definition idx_measure (c: cfg delayed_lang) i : P :=
nth i (map snd (fst c)) (proj1_sig mini).
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' ⇒
plt (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).
rewrite erase_option_list.
econstructor; eauto using map_length.
destruct ef; 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 →
plt (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 →
plt (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.
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 plt_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 P n) : Prop.
Proof.
induction n as [|n' pow_plt].
- simpl in ×. apply (plt x y).
- simpl in ×. destruct x as (px, x'). destruct y as (py, y').
exact ((plt 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 _ _ plt (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.
- eauto.
- eapply (wf_iff); first eapply pow_plt_S.
apply (Wellfounded.Lexicographic_Product.wf_symprod); eauto.
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 P n :=
firstn_tuple n (proj1_sig mini) (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 σ σ',
plt 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).
rewrite erase_option_list.
econstructor; eauto using map_length.
destruct ef; auto.
- 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.
rewrite erase_option_list. destruct ef0; 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.
End delayed_lang.