Monad Evaluation Semantics Instances

This file defines various instances of evaluation semantics for different monads

@[simp]

theorem SetM.support_eq_run {α : Type u} (s : SetM α) : support s = s.run

@[simp]

theorem SPMF.evalDist_def {α : Type u} (p : SPMF α) : 𝒟[p] = p

theorem SPMF.support_eq_support {α : Type u} (p : SPMF α) : support p = p.support

theorem SPMF.probOutput_eq_apply {α : Type u} (p : SPMF α) (x : α) : Pr[= x | p] = p x

theorem SPMF.evalDist_eq_iff {α : Type u} {m : Type u → Type u_1} [Monad m] [MonadLiftT m SPMF] (mx : m α) (p : SPMF α) : 𝒟[mx] = p ↔ ∀ (x : α), Pr[= x | mx] = p x

@[simp]

theorem PMF.evalDist_eq {α : Type u} (p : PMF α) : 𝒟[p] = liftM p

@[simp]

theorem PMF.probOutput_eq_apply {α : Type u} (p : PMF α) (x : α) : Pr[= x | p] = p x

@[simp]

theorem SPMF.evalDist_liftM {α : Type u} (p : PMF α) : 𝒟[liftM p] = 𝒟[p]

@[simp]

theorem SPMF.probOutput_liftM {α : Type u} (p : PMF α) (x : α) : Pr[= x | liftM p] = Pr[= x | p]

@[simp]

theorem SPMF.probEvent_liftM {α : Type u} (p : PMF α) (e : α → Prop) : probEvent (liftM p) e = probEvent p e

@[simp]

theorem SPMF.probFailure_liftM {α : Type u} (p : PMF α) : Pr[⊥ | liftM p] = Pr[⊥ | p]

@[implicit_reducible]

noncomputable instance Id.instMonadLiftPMF_vCVio : MonadLift Id PMF

Lift Id into PMF (a pure of the result), giving Id the canonical total denotation.

instance Id.instLawfulMonadLiftPMF_vCVio : LawfulMonadLift Id PMF

@[implicit_reducible]

instance Id.instHasEvalFinset : HasEvalFinset Id

@[simp]

theorem Id.support_eq_singleton {α : Type u} (x : Id α) : support x = {x.run}

@[simp]

theorem Id.finSupport_eq_singleton {α : Type u} [DecidableEq α] (x : Id α) : finSupport x = {x.run}

@[simp]

theorem Id.probOutput_eq_ite {α : Type u} [DecidableEq α] (x : Id α) (y : α) : Pr[= y | x] = if y = x.run then 1 else 0

@[simp]

theorem Id.probEvent_eq_ite {α : Type u} (x : Id α) (p : α → Prop) [DecidablePred p] : probEvent x p = if p x.run then 1 else 0

theorem Id.probFailure_eq_zero {α : Type u} (x : Id α) : Pr[⊥ | x] = 0