diff --git a/theories/prob/distribution.v b/theories/prob/distribution.v index cdf39a1a..06f9e091 100644 --- a/theories/prob/distribution.v +++ b/theories/prob/distribution.v @@ -661,6 +661,316 @@ Section monadic. End monadic. +Section probabilities. + Context `{Countable A}. + Implicit Types μ d : distr A. + + Definition prob (μ : distr A) (P : A → bool) : R := + SeriesC (λ a : A, if (P a) then μ a else 0). + + Lemma prob_le_1 (μ : distr A) (P : A → bool) : + prob μ P <= 1. + Proof. + transitivity (SeriesC μ); [|done]. + apply SeriesC_le; [|done]. + real_solver. + Qed. + + Lemma prob_ge_0 (μ : distr A) (P : A → bool) : + 0 <= prob μ P. + Proof. apply SeriesC_ge_0'=> a. real_solver. Qed. + +End probabilities. + +Section probability_lemmas. + Context `{Countable A}. + + Lemma prob_dret_true (a : A) (P : A → bool) : + P a = true → prob (dret a) P = 1. + Proof. + intro HP. + rewrite /prob/pmf/=/dret_pmf/=. + erewrite SeriesC_ext; [apply SeriesC_singleton|]. + real_solver. + Qed. + + Lemma prob_dret_false (a : A) (P : A → bool) : + P a = false → prob (dret a) P = 0. + Proof. + intro HP. + rewrite /prob/pmf/=/dret_pmf/=. + apply SeriesC_0. real_solver. + Qed. + + Lemma prob_dbind `{Countable B} (μ : distr A) (f : A → distr B) (P : B → bool) : + prob (dbind f μ) P = SeriesC (λ a, μ a * prob (f a) P). + Proof. + rewrite /prob{1}/pmf/=/dbind_pmf/=. + assert (∀ a, + (if P a then SeriesC (λ a0 : A, μ a0 * f a0 a) else 0) = + SeriesC (λ a0 : A, if P a then μ a0 * f a0 a else 0)) as Haux. + {intro a. destruct (P a); [done|]. rewrite SeriesC_0 //. } + setoid_rewrite Haux. + rewrite -(fubini_pos_seriesC (λ '(a, a0), if P a then μ a0 * f a0 a else 0)). + - apply SeriesC_ext=> a. + rewrite -SeriesC_scal_l. + apply SeriesC_ext; intro b. + real_solver. + - real_solver. + - intro b. + apply (ex_seriesC_le _ μ); [|done]. + real_solver. + - apply (ex_seriesC_le _ (λ a : B, SeriesC (λ b : A, μ b * f b a))). + + intro b; split. + * apply SeriesC_ge_0'. real_solver. + * apply SeriesC_le; [real_solver|]. + apply pmf_ex_seriesC_mult_fn. + exists 1. real_solver. + + apply (pmf_ex_seriesC (dbind f μ)). + Qed. + + Lemma union_bound (μ : distr A) (P Q : A → bool) : + prob μ (λ a, orb (P a) (Q a)) <= prob μ P + prob μ Q. + Proof. + rewrite /prob. + rewrite -SeriesC_plus. + - apply SeriesC_le. + + intro n. + pose proof (pmf_pos μ n). + destruct (P n); destruct (Q n); real_solver. + + apply (ex_seriesC_le _ (λ x, 2 * μ x)). + * intro n. + pose proof (pmf_pos μ n). + destruct (P n); destruct (Q n); real_solver. + * by apply ex_seriesC_scal_l. + - by apply ex_seriesC_filter_bool_pos. + - by apply ex_seriesC_filter_bool_pos. + Qed. + +End probability_lemmas. + + +Section probabilities_prop. + Context `{Countable A}. + Context (μ : distr A). + Context (P : A -> Prop). + Context `{forall a, Decision (P a)}. + + Definition probp : R := + SeriesC (λ a : A, if (bool_decide (P a)) then μ a else 0). + + Lemma probp_le_1 : + probp <= 1. + Proof. + transitivity (SeriesC μ); [|done]. + apply SeriesC_le; [|done]. + real_solver. + Qed. + + Lemma probp_ge_0 : + 0 <= probp. + Proof. apply SeriesC_ge_0'=> a. real_solver. Qed. + +End probabilities_prop. + +Section probability_prop_lemmas. + Context `{Countable A}. + + Lemma probp_dret_true (a : A) (P : A → Prop) `{forall a, Decision (P a)}: + P a → probp (dret a) P = 1. + Proof. + intro HP. + rewrite /probp/pmf/=/dret_pmf/=. + erewrite SeriesC_ext; [apply SeriesC_singleton|]. + real_solver. + Qed. + + Lemma probp_dret_false (a : A) (P : A → Prop) `{forall a, Decision (P a)}: + ¬ (P a) → probp (dret a) P = 0. + Proof. + intro HP. + rewrite /probp/pmf/=/dret_pmf/=. + apply SeriesC_0; real_solver. + Qed. + + Lemma probp_dbind `{Countable B} (μ : distr A) (f : A → distr B) (P : B → Prop) `{forall a, Decision (P a)}: + probp (dbind f μ) P = SeriesC (λ a, μ a * probp (f a) P). + Proof. + rewrite /probp{1}/pmf/=/dbind_pmf/=. + assert (∀ a, + (if (bool_decide (P a)) then SeriesC (λ a0 : A, μ a0 * f a0 a) else 0) = + SeriesC (λ a0 : A, if (bool_decide (P a)) then μ a0 * f a0 a else 0)) as Haux. + {intro a. case_bool_decide; [done|]. rewrite SeriesC_0 //. } + setoid_rewrite Haux. + rewrite -(fubini_pos_seriesC (λ '(a, a0), if (bool_decide (P a)) then μ a0 * f a0 a else 0)). + - apply SeriesC_ext=> a. + rewrite -SeriesC_scal_l. + apply SeriesC_ext; intro b. + real_solver. + - real_solver. + - intro b. + apply (ex_seriesC_le _ μ); [|done]. + real_solver. + - apply (ex_seriesC_le _ (λ a : B, SeriesC (λ b : A, μ b * f b a))). + + intro b; split. + * apply SeriesC_ge_0'. real_solver. + * apply SeriesC_le; [real_solver|]. + apply pmf_ex_seriesC_mult_fn. + exists 1. real_solver. + + apply (pmf_ex_seriesC (dbind f μ)). + Qed. + + Lemma union_bound_prop (μ : distr A) (P Q : A → Prop) `{forall a, Decision (P a)} `{forall a, Decision (Q a)} : + probp μ (λ a, (P a) \/ (Q a)) <= probp μ P + probp μ Q. + Proof. + rewrite /probp. + rewrite -SeriesC_plus. + - apply SeriesC_le. + + intro n. + pose proof (pmf_pos μ n). + do 3 case_bool_decide; try real_solver. + destruct_or?; done. + + apply (ex_seriesC_le _ (λ x, 2 * μ x)). + * intro n. + pose proof (pmf_pos μ n). + do 2 case_bool_decide; real_solver. + * by apply ex_seriesC_scal_l. + - by apply ex_seriesC_filter_bool_pos. + - by apply ex_seriesC_filter_bool_pos. + Qed. + +End probability_prop_lemmas. + + +Section subset_distribution. + Context `{Countable A}. + Context (P : A -> bool). + Implicit Types μ d : distr A. + + Definition ssd_pmf (μ : distr A) := + λ a : A, if P a then μ a else 0. + + Program Definition ssd (μ : distr A) := MkDistr (ssd_pmf μ) _ _ _. + Next Obligation. + move=> μ a. + rewrite /ssd_pmf. by (destruct (P a)). + Qed. + Next Obligation. + move=> μ. rewrite /ssd_pmf. + eapply (ex_seriesC_le _ μ); try done. + move=> n. split; by (destruct (P n)). + Qed. + Next Obligation. + move=> μ. + etrans. + - eapply (SeriesC_le _ μ); try done. rewrite /ssd_pmf. + split; by (destruct (P n)). + - done. + Qed. + +End subset_distribution. + + +Declare Scope predicate_scope. +Delimit Scope predicate_scope with P. +Notation "∽ K " := (λ a, negb (K a)) (at level 70, right associativity) : predicate_scope. + +Section subset_distribution_lemmas. + Context `{Countable A}. + Implicit Type P : A -> bool. + Implicit Types μ : distr A. + + Lemma ssd_ret_pos P μ (a : A) : ssd P μ a > 0 -> P a. + Proof. + rewrite /ssd /ssd_pmf /pmf. move=> H0. + destruct (P a); [done|lra]. + Qed. + + Lemma ssd_sum P μ (a : A) : μ a = ssd P μ a + ssd (∽ P)%P μ a. + Proof. + rewrite /ssd /ssd_pmf /pmf /=. + destruct (P a) => /=; lra. + Qed. + + Lemma ssd_remove P μ : (∀ a, negb (P a) -> μ a = 0) -> ssd P μ = μ. + Proof. + move=> H0. + apply distr_ext. move=> a. destruct (P a) eqn:H'. + - by rewrite /ssd{1}/pmf/ssd_pmf H'. + - rewrite /ssd{1}/pmf/ssd_pmf H'. rewrite H0; [done|by rewrite H']. + Qed. + +End subset_distribution_lemmas. + +Section bind_lemmas. + Context `{Countable A, Countable B}. + Implicit Types μ: distr A. + Implicit Types ν: A -> distr B. + + Lemma bind_split_sum (μ μ1 μ2 : distr A) ν: + (∀ a, μ a = μ1 a + μ2 a) -> + (∀ b, (μ ≫= λ a', ν a') b = (μ1 ≫= λ a', ν a') b + (μ2 ≫= λ a', ν a') b). + Proof. + move=> H1 b. + rewrite /pmf /= /dbind_pmf. + rewrite -SeriesC_plus; last first. + { eapply (ex_seriesC_le _ (λ a, μ2 a)); [intros n; split|apply pmf_ex_seriesC]. + - real_solver. + - rewrite <-Rmult_1_r. by apply Rmult_le_compat_l. + } + { eapply (ex_seriesC_le _ (λ a, μ1 a)); [intros n; split|apply pmf_ex_seriesC]. + - real_solver. + - rewrite <-Rmult_1_r. by apply Rmult_le_compat_l. + } + f_equal. apply functional_extensionality_dep => a. + replace (_*_+_*_) with ((μ1 a + μ2 a) * ν a b); last real_solver. + by rewrite -H1. + Qed. + + Lemma ssd_bind_split_sum μ ν P : + ∀ b, (μ ≫= λ a', ν a') b = (ssd P μ ≫= λ a', ν a') b + (ssd (∽ P)%P μ ≫= λ a', ν a')b. + Proof. + move=> b. + erewrite <-bind_split_sum; first done. + intros. apply ssd_sum. + Qed. + + + (** *strengthen following lemma? *) + Lemma ssd_bind_constant P μ ν (b : B) k: + (∀ a, P a = true -> ν a b = k) -> (ssd P μ ≫= λ a', ν a') b = k * SeriesC (ssd P μ). + Proof. + move=> H1. + rewrite {1}/pmf /= /dbind_pmf. + rewrite -SeriesC_scal_l. + f_equal. apply functional_extensionality_dep => a. + destruct (P a) eqn:H'. + - apply H1 in H'. rewrite H'. real_solver. + - rewrite /ssd /pmf /ssd_pmf H'. real_solver. + Qed. + + Lemma ssd_fix_value μ (v : A): + SeriesC (ssd (λ a, bool_decide (a = v)) μ) = μ v. + Proof. + erewrite <-(SeriesC_singleton v). + f_equal. + apply functional_extensionality_dep => a. + rewrite /ssd/pmf/ssd_pmf/pmf. case_bool_decide; eauto. + by rewrite H1. + Qed. + + + Lemma ssd_chain μ (P Q: A -> bool): + ssd P (ssd Q μ) = ssd (λ a, P a && Q a) μ. + Proof. + apply distr_ext => a. + rewrite /ssd/pmf/ssd_pmf/pmf. + destruct (P a) eqn:H1; destruct (Q a) eqn:H2; eauto. + Qed. + +End bind_lemmas. + + (** * Monadic map *) Definition dmap `{Countable A, Countable B} (f : A → B) (μ : distr A) : distr B := a ← μ; dret (f a). diff --git a/theories/program_logic/exec.v b/theories/program_logic/exec.v index 94eaa728..97573d1f 100644 --- a/theories/program_logic/exec.v +++ b/theories/program_logic/exec.v @@ -1,6 +1,7 @@ From Coq Require Import Reals Psatz. From Coquelicot Require Import Rcomplements Rbar Lim_seq. From stdpp Require Import relations. +From clutch.prob_lang Require Import lang. From clutch.program_logic Require Import language. From clutch.prob Require Import distribution couplings. @@ -52,7 +53,7 @@ Section exec. assert (S n = n + 1)%nat as -> by lia. rewrite exec_plus exec_1 //. Qed. - + Lemma exec_det_step n ρ e1 e2 σ1 σ2 : prim_step e1 σ1 (e2, σ2) = 1 → exec n ρ (e1, σ1) = 1 → @@ -113,6 +114,13 @@ Section exec_val. | None, S n => prim_step ρ.1 ρ.2 ≫= exec_val n end. + Fixpoint exec_cfg (n : nat) (ρ : cfg Λ) {struct n} : distr (cfg Λ) := + match to_val ρ.1, n with + | Some _, _ => dret ρ + | None, 0 => dzero + | None, S n => prim_step ρ.1 ρ.2 ≫= exec_cfg n + end. + Lemma exec_val_unfold (n : nat) : exec_val n = λ ρ, match to_val ρ.1, n with @@ -152,6 +160,42 @@ Section exec_val. by intros ? ? ->. Qed. + Lemma exec_cfg_is_val v e σ n : + to_val e = Some v → exec_cfg n (e, σ) = dret (of_val v, σ). + Proof. + intros. + apply of_to_val in H; subst. + destruct n; simpl; intros; by rewrite to_of_val. + Qed. + + Lemma exec_cfg_Sn (ρ : cfg Λ) (n: nat) : + exec_cfg (S n) ρ = prim_step_or_val ρ ≫= exec_cfg n. + Proof. + destruct ρ as [e σ]. + rewrite /prim_step_or_val /=. + destruct (to_val e) eqn:Hv=>/=; [|done]. + rewrite dret_id_left -/exec_cfg. + fold exec_cfg. + epose proof (exec_cfg_is_val _ _ _ _ Hv) as Hv'. + erewrite Hv'. + apply of_to_val in Hv. by subst. + Qed. + + Lemma exec_cfg_mon ρ n ρ': + exec_cfg n ρ ρ' <= exec_cfg (S n) ρ ρ'. + Proof. + apply refRcoupl_eq_elim. + move : ρ. + induction n. + - intros. + apply refRcoupl_from_leq. + intros w. rewrite /distr_le /=. + by case_match. + - intros; do 2 rewrite exec_cfg_Sn. + eapply refRcoupl_dbind; [|apply refRcoupl_eq_refl]. + by intros ? ? ->. + Qed. + Lemma exec_val_mon' ρ n m v : n ≤ m → exec_val n ρ v <= exec_val m ρ v. Proof. @@ -234,6 +278,9 @@ Section prim_exec_lim. Definition lim_exec_val (ρ : cfg Λ) : distr (val Λ):= lim_distr (λ n, exec_val n ρ) (exec_val_mon ρ). + Definition lim_exec_cfg (ρ : cfg Λ) : distr (cfg Λ) := + lim_distr (λ n, exec_cfg n ρ) (exec_cfg_mon ρ). + Lemma lim_exec_val_rw (ρ : cfg Λ) v : lim_exec_val ρ v = Sup_seq (λ n, (exec_val n ρ) v). Proof. @@ -299,6 +346,338 @@ Section prim_exec_lim. intros ??. apply IHn. Qed. + + (** * strengthen this lemma? *) + + Lemma lim_exec_bind_continuity_1 e σ ν v: + (lim_exec_cfg (e, σ) ≫= (λ s, ν s)) v = + Sup_seq (λ n, (exec_cfg n (e, σ) ≫= (λ s, ν s)) v). + Proof. + rewrite /pmf /= /dbind_pmf. + rewrite /lim_exec_cfg. + assert (SeriesC (λ a : cfg Λ, lim_distr (λ n : nat, exec_cfg n (e, σ)) (exec_cfg_mon (e, σ)) a * ν a v) = SeriesC (λ a : cfg Λ, Sup_seq (λ n : nat, exec_cfg n (e, σ) a) * ν a v)) as H by f_equal. + rewrite H. clear H. + pose (h := λ n a, exec_cfg n (e, σ) a * ν a v). + assert (SeriesC (λ a : cfg Λ, Sup_seq (λ n : nat, exec_cfg n (e, σ) a) * ν a v) = + SeriesC (λ a : cfg Λ, Sup_seq (λ n : nat, h n a))). + { f_equal. apply functional_extensionality_dep => s. rewrite /h. + rewrite Rmult_comm. apply eq_rbar_finite. rewrite rmult_finite rbar_finite_real_eq; last first. + { apply (is_finite_bounded 0 1). + - apply (Sup_seq_minor_le _ _ 0). apply pmf_pos. + - apply upper_bound_ge_sup => n. apply pmf_le_1. + } + rewrite -Sup_seq_scal_l; [|done]. + f_equal. apply functional_extensionality_dep => n. rewrite Rmult_comm. done. + } + rewrite H. clear H. + rewrite /h. clear h. + eapply MCT_seriesC; intros. + - by apply Rmult_le_pos. + - apply Rmult_le_compat_r; [done|apply exec_cfg_mon]. + - exists 1. intros. replace 1 with (1*1); [by apply Rmult_le_compat|lra]. + - apply SeriesC_correct. + eapply (ex_seriesC_le _ (λ a, exec_cfg n (e, σ) a)). + + intros; split; [by apply Rmult_le_pos|]. + rewrite <-Rmult_1_r. + by apply Rmult_le_compat_l. + + apply pmf_ex_seriesC. + - rewrite (Rbar_le_sandwich 0 1). + + eapply is_sup_seq_ext; last first. + { eapply Sup_seq_correct. } + intros => /=. done. + + eapply (Sup_seq_minor_le _ _ 0%nat). apply SeriesC_ge_0' => ?. + by apply Rmult_le_pos. + + apply upper_bound_ge_sup => n. + trans ((exec_cfg n (e, σ) ≫= λ a, ν a) v ). + -- by rewrite {3}/pmf. + -- apply pmf_le_1. + Qed. + + + (** * strengthen this lemma? *) + + Lemma lim_exec_bind_continuity_2 (μ : distr (cfg Λ)) v `{!LanguageCtx K}: + (μ ≫= (λ '(e, σ), lim_exec_val ((K e), σ) )) v = + Sup_seq (λ n, (μ ≫= (λ '(e, σ), exec_val n ((K e), σ))) v). + Proof. + rewrite {1}/pmf /= /dbind_pmf. + rewrite {3}/pmf /= /dbind_pmf. + rewrite /lim_exec_val. + assert (SeriesC + (λ a : expr Λ * state Λ, + μ a * + (let '(e, σ) := a in lim_distr (λ n : nat, exec_val n (K e, σ)) (exec_val_mon (K e, σ))) v) = + SeriesC + (λ a : expr Λ * state Λ, + μ a * + (let '(e, σ) := a in Sup_seq (λ n : nat, exec_val n (K e, σ) v) ) + )) as H. + { f_equal. apply functional_extensionality_dep => e. destruct e. f_equal. } + rewrite H. clear H. + assert (SeriesC + (λ a : expr Λ * state Λ, μ a * (let '(e, σ) := a in Sup_seq (λ n : nat, exec_val n (K e, σ) v)))= + SeriesC + (λ a : expr Λ * state Λ, Sup_seq (λ n : nat, μ a * (let '(e, σ) := a in exec_val n (K e, σ) v)))) as H. + { f_equal. apply functional_extensionality_dep => e. destruct e. + apply eq_rbar_finite. rewrite rmult_finite rbar_finite_real_eq; last first. + { apply (is_finite_bounded 0 1). + - apply (Sup_seq_minor_le _ _ 0). apply pmf_pos. + - apply upper_bound_ge_sup => n. apply pmf_le_1. + } + rewrite -Sup_seq_scal_l; [|done]. + f_equal. + } + rewrite H. clear H. + eapply MCT_seriesC; intros. + - destruct a. by apply Rmult_le_pos. + - apply Rmult_le_compat_l; [done|]. destruct a. apply exec_val_mon. + - exists 1. intros. destruct a. replace 1 with (1*1); [by apply Rmult_le_compat|lra]. + - apply SeriesC_correct. + pose (ν := λ a, let '(e, σ) := a in exec_val n (K e, σ) v). + assert (ex_seriesC (λ a : expr Λ * state Λ, μ a * (let '(e, σ) := a in exec_val n (K e, σ) v)) + = ex_seriesC (λ a : expr Λ * state Λ, μ a * ν a)) as H by f_equal. + rewrite H. + eapply pmf_ex_seriesC_mult_fn. exists 1. intros [e σ]. rewrite /ν. split; done. + - rewrite (Rbar_le_sandwich 0 1). + + eapply is_sup_seq_ext; last first. + { eapply Sup_seq_correct. } + intros. simpl. repeat f_equal. apply functional_extensionality_dep. by intros [e σ]. + + eapply (Sup_seq_minor_le _ _ 0%nat). apply SeriesC_ge_0' => ?. + apply Rmult_le_pos; done. + + apply upper_bound_ge_sup => n. + trans ((μ ≫= λ '(e, σ), exec_val n (K e, σ)) v). + -- by rewrite {3}/pmf /= /dbind_pmf. + -- apply pmf_le_1. + Qed. + + + Lemma lim_exec_val_context_bind `{!LanguageCtx K} e σ: + lim_exec_val (K e, σ) = + lim_exec_cfg (e, σ) ≫= λ '(e', σ'), lim_exec_val (K e', σ'). + Proof. + apply distr_le_antisym; rewrite /distr_le; intros v; + [unfold lim_exec_val|]; rewrite lim_distr_pmf; rewrite lim_exec_bind_continuity_1. + - apply Rbar_le_fin. + { apply Rbar_0_le_to_Rle. apply (Sup_seq_minor_le _ _ 0). apply pmf_pos. } + rewrite rbar_finite_real_eq; last first. + { eapply is_finite_bounded. + ++ apply (Sup_seq_minor_le _ _ 0). rewrite /lim_exec_val. apply pmf_pos. + ++ apply upper_bound_ge_sup => ?. apply pmf_le_1. + } + apply Sup_seq_le. + intros n; revert e σ v; induction n => e σ v/=. + ++ destruct (to_val e) eqn:H1; destruct (to_val (K e)) eqn:H2. + --- rewrite dret_id_left. rewrite /lim_exec_val lim_distr_pmf. + apply rbar_le_finite. + { apply (is_finite_bounded 0 1). + +++ apply (Sup_seq_minor_le _ _ 0). apply pmf_pos. + +++ apply upper_bound_ge_sup => n. apply pmf_le_1. + } + eapply (Sup_seq_minor_le _ _ 0). simpl; rewrite H2. lra. + --- replace (dzero v) with 0. + 2:{ done. } + apply pmf_pos. + --- apply fill_not_val in H1. rewrite H1 in H2. inversion H2. + --- replace (dzero v) with 0. + 2:{ done. } + apply pmf_pos. + ++ destruct (to_val e) eqn:H1; destruct (to_val (K e)) eqn:H2. + --- rewrite dret_id_left. rewrite /lim_exec_val lim_distr_pmf. + apply rbar_le_finite. + { apply (is_finite_bounded 0 1). + +++ apply (Sup_seq_minor_le _ _ 0). apply pmf_pos. + +++ apply upper_bound_ge_sup => ?. apply pmf_le_1. + } + eapply (Sup_seq_minor_le _ _ 0). simpl; rewrite H2. lra. + --- rewrite dret_id_left. rewrite -exec_val_Sn_not_val; last done. + unfold lim_exec_val. rewrite lim_distr_pmf. + eapply rbar_le_finite. + { apply (is_finite_bounded 0 1). + +++ apply (Sup_seq_minor_le _ _ 0). apply pmf_pos. + +++ apply upper_bound_ge_sup => ?. apply pmf_le_1. + } + eapply (Sup_seq_minor_le _ _ (S n)). done. + --- apply fill_not_val in H1. rewrite H1 in H2. inversion H2. + --- rewrite fill_dmap; last done. rewrite /dmap. + rewrite -!dbind_assoc -/exec_cfg -/exec_val. + revert v. apply distr_le_dbind. { apply distr_le_refl. } + intros [e' σ']. unfold distr_le. intros v. + rewrite dret_id_left. simpl. + apply IHn. + - apply Rbar_le_fin. + { apply Rbar_0_le_to_Rle. apply (Sup_seq_minor_le _ _ 0). apply pmf_pos. } + rewrite rbar_finite_real_eq; last first. + { eapply is_finite_bounded. + ++ by eapply (Sup_seq_minor_le _ _ 0). + ++ apply upper_bound_ge_sup => n. apply pmf_le_1. + } + pose (μ := λ n (s : cfg Λ), exec_cfg n s). + assert (Sup_seq (λ n : nat, (exec_cfg n (e, σ) ≫= (λ '(e', σ'), lim_exec_val (K e', σ'))) v) = + Sup_seq (λ n : nat, Sup_seq (λ m, ((μ n) (e, σ) ≫= (λ '(e', σ'), exec_val m (K e', σ'))) v))) as H. + { rewrite /μ. apply Sup_seq_ext => ?. + rewrite lim_exec_bind_continuity_2 rbar_finite_real_eq;[f_equal|]. + apply (is_finite_bounded 0 1). + ++ apply (Sup_seq_minor_le _ _ 0). apply pmf_pos. + ++ apply upper_bound_ge_sup => n. apply pmf_le_1. + } + rewrite H. + rewrite /μ. clear H μ. + pose (μ := λ '(n, m), ((exec_cfg n (e, σ) ≫= (λ '(e', σ'), exec_val m (K e', σ'))) v)). + assert (Sup_seq + (λ n : nat, Sup_seq (λ m : nat, (exec_cfg n (e, σ) ≫= (λ '(e', σ'), exec_val m (K e', σ'))) v)) = + Sup_seq + (λ n : nat, Sup_seq (λ m : nat, μ (n, m)) )) as -> by f_equal. + rewrite sup_seq_swap. + apply upper_bound_ge_sup => m. + replace (Sup_seq (λ n : nat, exec_val n (K e, σ) v)) with (Sup_seq (λ n : nat, exec_val (n+m) (K e, σ) v)); last first. + { apply sup_seq_eq_antisym => n; try by eexists _. + eexists n. apply exec_val_mon'. lia. + } + rewrite /μ. clear μ. + apply Sup_seq_le => n. revert e σ m v. + induction n => e σ m v. + ++ destruct (to_val e) eqn:H1; destruct (to_val (K e)) eqn:H2. + all: simpl; rewrite H1; try rewrite dret_id_left; try rewrite dbind_dzero; try rewrite H2. + all: done. + ++ destruct (to_val e) eqn:H1; destruct (to_val (K e)) eqn:H2. + all: simpl; rewrite H1; try rewrite dret_id_left; try rewrite H2. + --- erewrite exec_val_is_val; done. + --- rewrite -prim_step_or_val_no_val; [|done]. rewrite -exec_val_Sn. + apply exec_val_mon'. lia. + --- apply fill_not_val in H1. rewrite H1 in H2. inversion H2. + --- rewrite fill_dmap; last done. rewrite /dmap. + rewrite -!dbind_assoc -/exec_cfg -/exec_val. + revert v. apply distr_le_dbind. { apply distr_le_refl. } + intros [e' σ']. unfold distr_le. intros v. + rewrite dret_id_left. simpl. + apply IHn. + Qed. + + Lemma lim_exec_cfg_lim_exec_val_relate e σ v: SeriesC (λ σ', lim_exec_cfg (e, σ) (of_val v, σ')) = lim_exec_val (e, σ) v. + Proof. +assert ( (λ σ', lim_exec_cfg (e, σ) (of_val v, σ')) = (λ σ', Sup_seq (λ n, exec_cfg n (e, σ) (of_val v, σ')))). + { apply functional_extensionality_dep. by intros. } + rewrite H. + assert (SeriesC (λ σ', Sup_seq (λ n : nat, exec_cfg n (e, σ) (of_val v, σ'))) = Sup_seq (λ n, SeriesC (λ σ', exec_cfg n (e, σ) (of_val v, σ')))). + { eapply MCT_seriesC. + - by intros. + - intros. apply exec_cfg_mon. + - intros. + by exists 1. + - intros. apply SeriesC_correct. apply ex_distr_lmarg. + - rewrite (Rbar_le_sandwich 0 1). + + eapply is_sup_seq_ext; last first. + { eapply Sup_seq_correct. } + intros; done. + + eapply (Sup_seq_minor_le _ _ 0%nat). apply SeriesC_ge_0' => ?. done. + + apply upper_bound_ge_sup => n. + assert ((SeriesC (λ σ', exec_cfg n (e, σ) (of_val v, σ'))) = lmarg (exec_cfg n (e, σ)) (of_val v)). + { rewrite lmarg_pmf. done. } + rewrite H0. + apply pmf_le_1. + } + rewrite H0. clear H0 H. rewrite lim_exec_val_rw. + repeat f_equal. apply functional_extensionality_dep. + intros n. revert e σ. + induction n; intros. + - simpl. destruct (to_val e) eqn:H. + + apply of_to_val in H. + rewrite /dret/pmf/dret_pmf. + case_bool_decide. + -- assert ((λ σ', dret (e, σ) (of_val v, σ')) = (dret σ)). + { apply functional_extensionality_dep. intros. + unfold dret, pmf, dret_pmf. + repeat case_bool_decide; try done. + + inversion H1. done. + + subst. done. + } + rewrite H1. f_equal. apply dret_mass. + -- assert ( (λ σ', if bool_decide ((of_val v, σ') = (e, σ)) then 1 else 0) = dzero). + { apply functional_extensionality_dep. intros. case_bool_decide. + - inversion H1. subst. apply of_to_val_flip in H3. rewrite to_of_val in H3. + inversion H3. done. + - done. + } + rewrite H1. f_equal. apply dzero_mass. + + replace (dzero _) with 0; [|done]. + f_equal. eapply SeriesC_0. intros. done. + - destruct (to_val e) eqn:H. + + erewrite SeriesC_ext; last first. + { intros. simpl. rewrite H. done. } + simpl. rewrite H. + rewrite /dret/pmf/dret_pmf. + case_bool_decide. + -- subst. + assert ((λ n0 : state Λ, if bool_decide ((of_val v0, n0) = (e, σ)) then 1 else 0) = dret σ). + { apply functional_extensionality_dep. intros. + unfold dret, pmf, dret_pmf. + repeat case_bool_decide; try done. + + inversion H0. done. + + subst. apply of_to_val in H. by subst. + } + rewrite H0. f_equal. apply dret_mass. + -- assert ((λ n0 : state Λ, if bool_decide ((of_val v, n0) = (e, σ)) then 1 else 0) = dzero). + { apply functional_extensionality_dep. intros. case_bool_decide. + - inversion H1. subst. rewrite to_of_val in H. + inversion H. done. + - done. + } + rewrite H1. f_equal. apply dzero_mass. + + simpl. rewrite H. + rewrite /dbind/pmf/=/dbind_pmf. + assert (SeriesC (λ σ', SeriesC (λ a : cfg Λ, prim_step e σ a * exec_cfg n a (of_val v, σ'))) = + SeriesC (λ a: cfg Λ, SeriesC (λ σ', prim_step e σ a * exec_cfg n a (of_val v, σ')))). + { rewrite distr_double_swap_lmarg. f_equal. } + rewrite H0. clear H0. + assert (SeriesC (λ a : cfg Λ, SeriesC (λ σ', prim_step e σ a * exec_cfg n a (of_val v, σ'))) = + SeriesC (λ a : cfg Λ, prim_step e σ a * SeriesC (λ σ', exec_cfg n a (of_val v, σ')))). + { f_equal. apply functional_extensionality_dep. intros. rewrite SeriesC_scal_l. done. } + rewrite H0. clear H0. + repeat f_equal. apply functional_extensionality_dep. + intros []. f_equal. apply Rbar_finite_eq. apply IHn. + Qed. + + (** * strengthen lemma? *) + Lemma ssd_fix_value_lim_exec_val_lim_exec_cfg e σ (v : val Λ): + SeriesC (ssd (λ '(e', σ'), bool_decide (to_val e' = Some v)) (lim_exec_cfg (e, σ))) = + SeriesC (ssd (λ e' : val Λ, bool_decide (e' = v)) (lim_exec_val (e, σ))). + Proof. + rewrite {2}/ssd {2}/pmf/ssd_pmf. + pose (id := λ a: val Λ, a). + assert ( SeriesC (λ a : val Λ, if bool_decide (a = v) then lim_exec_val (e, σ) a else 0) = + (SeriesC (λ a : val Λ, if bool_decide (id a = v) then lim_exec_val (e, σ) v else 0))). + { f_equal. apply functional_extensionality_dep. + intros. rewrite /id. case_bool_decide; by subst. } + rewrite H. + rewrite SeriesC_singleton_inj; [|eauto]. clear H id. + + replace (SeriesC _) with + (SeriesC (λ σ', lim_exec_cfg (e, σ) (of_val v, σ'))); last first. + { erewrite <-(dmap_mass _ (λ s, s.2)). f_equal. + apply functional_extensionality_dep. + intros. + rewrite /dmap. + rewrite {2}/pmf/=/dbind_pmf. + replace (SeriesC _) with (SeriesC (λ s, if bool_decide (s = (of_val v, x)) then lim_exec_cfg (e, σ) (of_val v, x) else 0)). + 2: { f_equal. apply functional_extensionality_dep. intros []. + case_bool_decide; rewrite /ssd {2}/pmf/=/ssd_pmf; first case_bool_decide. + - inversion H. rewrite dret_1_1; [|done]. by rewrite Rmult_1_r. + - inversion H. subst. rewrite to_of_val in H0. done. + - rewrite /pmf. case_bool_decide. + + apply of_to_val in H0. rewrite H0 in H. + replace (dret_pmf _ _) with 0; [lra|]. + assert (s ≠ x); [intro; by subst|]. + rewrite /dret_pmf. case_bool_decide; [done|lra]. + + lra. + } + rewrite SeriesC_singleton_inj; eauto. + } + apply lim_exec_cfg_lim_exec_val_relate. +Qed. + + + + Lemma lim_exec_val_exec_det n ρ (v : val Λ) σ : exec n ρ (of_val v, σ) = 1 → lim_exec_val ρ = dret v. diff --git a/theories/typing/contextual_refinement_alt.v b/theories/typing/contextual_refinement_alt.v index b064f57b..a5f041c5 100644 --- a/theories/typing/contextual_refinement_alt.v +++ b/theories/typing/contextual_refinement_alt.v @@ -1,4 +1,4 @@ -From Coq Require Import Reals. +From Coq Require Import Reals Psatz. From Coquelicot Require Import Rcomplements Rbar Lim_seq. From clutch.program_logic Require Import language ectx_language exec. From clutch.prob_lang Require Import lang notation metatheory. @@ -121,3 +121,342 @@ Proof. - intros e. rewrite lim_exec_val_SeriesC_SeqV_true //. Qed. + + + +(*Other direction*) +Lemma ssd_is_value_lim_exec_cfg_same e σ : + (ssd (λ '(e', _), bool_decide (is_Some (to_val e'))) (lim_exec_cfg (e, σ))) = + lim_exec_cfg (e, σ). +Proof. + apply distr_ext. intros [e' σ']. + rewrite /ssd{1}/pmf/ssd_pmf. + case_bool_decide; eauto; simpl. + rewrite -eq_None_not_Some in H. + rewrite /lim_exec_cfg lim_distr_pmf. + symmetry. + rewrite <-sup_seq_const. do 2 f_equal. apply functional_extensionality_dep. + intros. revert e σ. induction x; intros; simpl; destruct (to_val e) eqn:H1; eauto. + - assert (e ≠ e'). + { intro. rewrite H0 in H1. by rewrite H in H1. } + rewrite /dret/pmf/dret_pmf; case_bool_decide; [|done]. + by inversion H2. + - assert (e ≠ e'). + { intro. rewrite H0 in H1. by rewrite H in H1. } + rewrite /dret/pmf/dret_pmf; case_bool_decide; [|done]. + by inversion H2. + - rewrite /dbind/pmf/dbind_pmf. + erewrite <-dzero_mass. do 2 f_equal. + apply functional_extensionality_dep. + intros [??]. + replace (dzero _) with 0; last done. + erewrite <-Rbar_finite_eq. rewrite rmult_finite. + rewrite IHx. apply Rbar_mult_0_r. +Qed. + + +Lemma ssd_not_value_lim_exec_cfg_dzero e σ : + ssd (λ a : expr * state, negb (let '(e', _) := a in bool_decide (is_Some (to_val e')))) + (lim_exec_cfg (e, σ)) = dzero. +Proof. + apply distr_ext. intros [e' σ']. + rewrite /dzero/ssd/pmf/ssd_pmf. + case_bool_decide; eauto; simpl. + rewrite -eq_None_not_Some in H. + rewrite /lim_exec_cfg lim_distr_pmf. + rewrite <-sup_seq_const. do 2 f_equal. apply functional_extensionality_dep. + intros. revert e σ. induction x; intros; simpl; destruct (to_val e) eqn:H1; eauto. + - assert (e ≠ e'). + { intro. rewrite H0 in H1. by rewrite H in H1. } + rewrite /dret/pmf/dret_pmf; case_bool_decide; [|done]. + by inversion H2. + - assert (e ≠ e'). + { intro. rewrite H0 in H1. by rewrite H in H1. } + rewrite /dret/pmf/dret_pmf; case_bool_decide; [|done]. + by inversion H2. + - rewrite /dbind/pmf/dbind_pmf. + erewrite <-dzero_mass. do 2 f_equal. + apply functional_extensionality_dep. + intros [??]. + replace (dzero _) with 0; last done. + erewrite <-Rbar_finite_eq. rewrite rmult_finite. + rewrite IHx. apply Rbar_mult_0_r. +Qed. + +(* first part *) +Lemma lim_exec_val_of_val_b_one e b σ: e = of_val #b -> lim_exec_val ((e = #b)%E, σ) #true = 1. +Proof. + intros ->. + rewrite lim_exec_val_rw. + rewrite mon_sup_succ. + - erewrite <-sup_seq_const. do 2 f_equal. apply functional_extensionality_dep. + intros n. simpl. rewrite head_prim_step_eq => /=. + 2: { eexists (_, _). destruct b; + eapply head_step_support_equiv_rel; + by econstructor. + } + destruct b => /=; try case_bool_decide; try done. + all: rewrite dret_id_left; destruct n => /=; by rewrite dret_1_1. + - intro. apply exec_val_mon. +Qed. + +Lemma lim_exec_val_of_val_not_b_zero e b σ: (is_Some (to_val e)) -> e ≠ of_val #b -> lim_exec_val ((e = #b)%E, σ) #true = 0. +Proof. + intros H H0. + rewrite lim_exec_val_rw. + erewrite <-sup_seq_const. do 2 f_equal. + apply functional_extensionality_dep. + intros []. + - by rewrite /pmf /=. + - simpl. destruct H. + apply of_to_val in H as H1. rewrite -H1. rewrite -H1 in H0. + clear H H1. + destruct x eqn:H2; rewrite head_prim_step_eq. + -- destruct b, l => /=; try (rewrite dret_id_left; destruct n => /=; done). + all: rewrite bool_decide_eq_false_2;[rewrite dret_id_left; by destruct n|]. + all: intro; apply H0; by rewrite H. + -- eexists (_,_). + eapply head_step_support_equiv_rel. + destruct l, b; by econstructor. + -- destruct b => /=; try (rewrite dret_id_left; destruct n => /=; done). + -- eexists (_,_). + eapply head_step_support_equiv_rel. + destruct b; by econstructor. + -- destruct b => /=; try (rewrite dret_id_left; destruct n => /=; done). + -- eexists (_,_). + eapply head_step_support_equiv_rel. + destruct b; by econstructor. + -- destruct v, b => /=; try (rewrite dret_id_left; destruct n => /=; done). + all: destruct l => /=; try (rewrite dret_id_left; destruct n => /=; done). + -- eexists (_,_). + eapply head_step_support_equiv_rel. + destruct v, b; try by econstructor. + all: destruct l; by econstructor. + -- destruct v, b => /=; try (rewrite dret_id_left; destruct n => /=; done). + all: destruct l => /=; try (rewrite dret_id_left; destruct n => /=; done). + -- eexists (_,_). + eapply head_step_support_equiv_rel. + destruct v, b; try by econstructor. + all: destruct l; by econstructor. +Qed. + + +Lemma lim_exec_val_is_b_test e σ (b:bool) : lim_exec_val (e, σ) #b = lim_exec_val ((e = #b)%E, σ) #true. +Proof. + replace ((e=#b)%E) with (fill_item (BinOpLCtx EqOp (#b)) e); last first. + { done. } + rewrite lim_exec_val_context_bind => /=. + pose (ν := λ '(e', σ'), lim_exec_val ((e' = #b)%E, σ')). + assert ((λ '(e', σ'), lim_exec_val ((e' = #b)%E, σ'))=(λ c, ν c)) as K. + { by apply functional_extensionality_dep. } + rewrite K. + erewrite (ssd_bind_split_sum _ _ (λ '(e', σ'), bool_decide (is_Some (to_val e')))). + rewrite ssd_not_value_lim_exec_cfg_dzero. + rewrite dbind_dzero /dzero {3}/pmf. rewrite Rplus_0_r. + erewrite (ssd_bind_split_sum _ _ (λ '(e', σ'), bool_decide (to_val e' = Some #b))). + erewrite (ssd_bind_constant _ _ _ _ 1); last first. + { intros [e' s] H. rewrite /ν. + apply lim_exec_val_of_val_b_one. + rewrite bool_decide_eq_true in H. + by apply of_to_val in H. + } + rewrite Rmult_1_l. + rewrite {1}ssd_is_value_lim_exec_cfg_same. + rewrite ssd_chain. + rewrite (ssd_bind_constant _ _ _ _ 0); last first. + { intros [??] H. + rewrite /ν. + rewrite andb_true_iff in H. destruct H as [H1 H2]. + rewrite negb_true_iff in H1. + rewrite bool_decide_eq_false in H1. + rewrite bool_decide_eq_true in H2. + apply lim_exec_val_of_val_not_b_zero; eauto. + intro. rewrite H in H1. simpl in H1. by apply H1. + } + rewrite Rmult_0_l Rplus_0_r. + rewrite ssd_fix_value_lim_exec_val_lim_exec_cfg. + by rewrite ssd_fix_value. +Qed. + + +(* second part *) + +Definition loop := App (RecV "f" "x" (App (Var "f") (Var "x"))) (#()). + +Lemma loop_zero_mass n σ x: exec_val n (loop, σ) x = 0. +Proof. + induction n as [n Hn] using (well_founded_induction lt_wf). + destruct n. + - simpl. destruct x; auto. + - rewrite /loop. simpl. rewrite head_prim_step_eq; last first. + -- eexists _. erewrite det_head_step_singleton; [|by econstructor]. simpl. + rewrite dret_1_1; [|done]. lra. + -- simpl. rewrite dret_id_left -/exec_val. apply Hn. lia. +Qed. + +Lemma lim_exec_val_of_val_true_one (e : expr) σ: e = #true -> lim_exec_val ((if: e then #() else loop)%E, σ) (#()) = 1. +Proof. +intros ->. + rewrite lim_exec_val_rw. + rewrite mon_sup_succ. + - erewrite <-sup_seq_const. do 2 f_equal. apply functional_extensionality_dep. + intros n. simpl. rewrite head_prim_step_eq => /=. + 2: { eexists (_, _). + eapply head_step_support_equiv_rel; + by econstructor. + } + rewrite dret_id_left; destruct n => /=; by rewrite dret_1_1. + - intro. apply exec_val_mon. +Qed. + +Lemma lim_exec_val_of_val_not_true_zero (e : expr) σ: (∃ v, e = of_val v) -> e ≠ #true -> lim_exec_val ((if: e then #() else loop)%E, σ) (#()) = 0. +Proof. + intros H H0. + rewrite lim_exec_val_rw. + erewrite <-sup_seq_const. do 2 f_equal. + apply functional_extensionality_dep. + intros []. + - by rewrite /pmf /=. + - simpl. destruct H. + rewrite H. rewrite H in H0. + clear H. + destruct x eqn:H2. + { destruct l. + 2: { destruct b; [exfalso; by apply H0|]. + rewrite head_prim_step_eq => /=; last first. + + eexists (_, _). + eapply head_step_support_equiv_rel; + by econstructor. + + rewrite dret_id_left -/ exec_val. rewrite loop_zero_mass. f_equal. + } + all: replace (_≫=_) with (dzero ≫= exec_val n); [by rewrite dbind_dzero|f_equal]. + all: apply distr_ext => s; replace (dzero s) with 0 by done. + all: rewrite /prim_step => /=; rewrite decomp_unfold => /=. + all: by rewrite dmap_dzero. + } + all: replace (_≫=_) with (dzero ≫= exec_val n); [by rewrite dbind_dzero|f_equal]. + all: apply distr_ext => s; replace (dzero s) with 0 by done. + all: rewrite /prim_step => /=; rewrite decomp_unfold => /=. + all: by rewrite dmap_dzero. +Qed. + +Lemma lim_exec_val_is_true_test e σ: + lim_exec_val ((if: e then #() else loop)%E, σ) #() = lim_exec_val (e,σ) (#true). +Proof. + replace (if: e then #() else loop)%E with (fill_item (IfCtx #() loop) e); last first. + { done. } + rewrite lim_exec_val_context_bind => /=. + pose (ν := λ '(e', σ'), lim_exec_val ((if: e' then #() else loop)%E, σ')). + assert ((λ '(e', σ'), lim_exec_val ((if: e' then #() else loop)%E, σ'))=(λ c, ν c)) as K. + { by apply functional_extensionality_dep. } + rewrite K. + erewrite (ssd_bind_split_sum _ _ (λ '(e', σ'), bool_decide (is_Some (to_val e')))). + rewrite ssd_not_value_lim_exec_cfg_dzero. + rewrite dbind_dzero /dzero {3}/pmf. rewrite Rplus_0_r. + erewrite (ssd_bind_split_sum _ _ (λ '(e', σ'), bool_decide (to_val e' = Some #true))). + erewrite (ssd_bind_constant _ _ _ _ 1); last first. + { intros [e' s] H. rewrite /ν. + apply lim_exec_val_of_val_true_one. + rewrite bool_decide_eq_true in H. + by apply of_to_val in H. + } + rewrite Rmult_1_l. + rewrite {1}ssd_is_value_lim_exec_cfg_same. + rewrite ssd_chain. + rewrite (ssd_bind_constant _ _ _ _ 0); last first. + { intros [??] H. + rewrite /ν. + rewrite andb_true_iff in H. destruct H as [H1 H2]. + rewrite negb_true_iff in H1. + rewrite bool_decide_eq_false in H1. + rewrite bool_decide_eq_true in H2. + apply lim_exec_val_of_val_not_true_zero. + - destruct H2. apply of_to_val in H. eauto. + - intro. rewrite H in H1. simpl in H1. by apply H1. + } + rewrite Rmult_0_l Rplus_0_r. + rewrite ssd_fix_value_lim_exec_val_lim_exec_cfg. + by rewrite ssd_fix_value. +Qed. + + +Lemma lim_exec_val_seriesc_return_value e σ: + SeriesC (lim_exec_val ((if: e then #() else loop)%E, σ)) = + lim_exec_val ((if: e then #() else loop)%E, σ) #(). +Proof. + rewrite -ssd_fix_value. + f_equal. f_equal. + apply distr_ext. intros v. + destruct (bool_decide (v=#())) eqn:H. + - by rewrite /ssd {2}/pmf /=/ssd_pmf H. + - rewrite /ssd {2}/pmf /=/ssd_pmf H. + rewrite bool_decide_eq_false in H. + rewrite lim_exec_val_rw. + rewrite <-sup_seq_const. do 2 f_equal. apply functional_extensionality_dep. + intros n. revert e σ. induction n. + + by intros. + + intros. simpl. + destruct (to_val e) eqn:H'. + -- apply of_to_val in H'; subst. destruct v0. + { destruct l. + 2: { destruct b; + rewrite head_prim_step_eq => /=; last first. + + eexists (_, _). + eapply head_step_support_equiv_rel; + by econstructor. + + rewrite dret_id_left -/ exec_val. rewrite loop_zero_mass. f_equal. + + eexists (_, _). + eapply head_step_support_equiv_rel; + by econstructor. + + rewrite dret_id_left -/ exec_val. + destruct n => /=; f_equal; by apply dret_0. + } + all: replace (_≫=_) with (dzero ≫= exec_val n); [by rewrite dbind_dzero|f_equal]. + all: apply distr_ext => s; replace (dzero s) with 0 by done. + all: rewrite /prim_step => /=; rewrite decomp_unfold => /=. + all: by rewrite dmap_dzero. + } + all: replace (_≫=_) with (dzero ≫= exec_val n); [by rewrite dbind_dzero|f_equal]. + all: apply distr_ext => s; replace (dzero s) with 0 by done. + all: rewrite /prim_step => /=; rewrite decomp_unfold => /=. + all: by rewrite dmap_dzero. + -- replace (if: _ then _ else _)%E with (fill [IfCtx (#()) loop] e); last done. + rewrite fill_prim_step_dbind; [|done]. + rewrite /dmap => /=. + rewrite -dbind_assoc -/exec_val. + rewrite {1}/dbind/pmf/dbind_pmf. + f_equal. apply SeriesC_0. intros [??]. + rewrite dret_id_left => /=. + replace (exec_val _ _ _) with 0; [lra|]. + do 2 f_equal. + rewrite <- Rbar_finite_eq. + by rewrite IHn. +Qed. + + +(*Combining both *) +Lemma alt_impl_ctx_refines_loop_lemma e (b:bool) σ: + lim_exec_val (e, σ) #b = SeriesC (lim_exec_val ((if: e = #b then #() else loop)%E, σ)). +Proof. + rewrite lim_exec_val_seriesc_return_value. + rewrite lim_exec_val_is_true_test. + apply lim_exec_val_is_b_test. +Qed. + +Lemma alt_impl_ctx_refines Γ e1 e2 τ : + ctx_refines_alt Γ e1 e2 τ -> (Γ ⊨ e1 ≤ctx≤ e2 : τ). +Proof. + intros H K σ0 b Hty. + destruct (bool_decide_reflect (lim_exec_val (fill_ctx K e1, σ0) #b <= lim_exec_val (fill_ctx K e2, σ0) #b)) as [|HC]; first done. + apply Rnot_le_gt in HC. + pose (K' := CTX_IfL (#()) loop :: CTX_BinOpL EqOp #b :: K). + assert (¬ SeriesC (lim_exec_val (fill_ctx K' e1, σ0)) <= SeriesC (lim_exec_val (fill_ctx K' e2, σ0))); last first. + - exfalso. eapply H0, H. + rewrite /K'. + econstructor. + 2:{ econstructor; eauto. econstructor; eauto. econstructor. econstructor. } + rewrite /loop. econstructor; tychk. + - apply Rlt_not_le, Rgt_lt. + rewrite /K' /=. + by do 2 rewrite -alt_impl_ctx_refines_loop_lemma. +Qed.