clutch.meas_lang.exec_lang
(* TODO move into metatheory.v ? *)
From Stdlib Require Export Reals Psatz.
From clutch.meas_lang Require Import lang.
(*
Lemma exec_det_step_ctx K `{!LanguageCtx K} n ρ (e1 e2 : expr) σ1 σ2 :
prim_step e1 σ1 (e2, σ2) = 1R →
pexec (S n) ρ (K e2, σ2) = 1nsteps_inv_r Hdet.
specialize (IHn _ _ m Hsteps Hdet).
rewrite -plus_n_Sm.
eapply exec_det_step_ctx; done| |done.
apply Hpstep.
Qed.
Lemma stepN_det_step_ctx K `{!LanguageCtx K} n ρ (e1 e2 : expr) σ1 σ2 :
prim_step e1 σ1 (e2, σ2) = 1R →
stepN (S n) ρ (K e2, σ2) = 1nsteps_inv_r Hdet.
specialize (IHn _ _ m Hsteps Hdet).
rewrite -plus_n_Sm.
eapply stepN_det_step_ctx; done| |done.
apply Hpstep.
Qed.
*)
From Stdlib Require Export Reals Psatz.
From clutch.meas_lang Require Import lang.
(*
Lemma exec_det_step_ctx K `{!LanguageCtx K} n ρ (e1 e2 : expr) σ1 σ2 :
prim_step e1 σ1 (e2, σ2) = 1R →
pexec (S n) ρ (K e2, σ2) = 1nsteps_inv_r Hdet.
specialize (IHn _ _ m Hsteps Hdet).
rewrite -plus_n_Sm.
eapply exec_det_step_ctx; done| |done.
apply Hpstep.
Qed.
Lemma stepN_det_step_ctx K `{!LanguageCtx K} n ρ (e1 e2 : expr) σ1 σ2 :
prim_step e1 σ1 (e2, σ2) = 1R →
stepN (S n) ρ (K e2, σ2) = 1nsteps_inv_r Hdet.
specialize (IHn _ _ m Hsteps Hdet).
rewrite -plus_n_Sm.
eapply stepN_det_step_ctx; done| |done.
apply Hpstep.
Qed.
*)