Documentation

VCVio.EvalDist.Defs.Instances

Monad Evaluation Semantics Instances #

This file defines various instances of evaluation semantics for different monads

source
@[implicit_reducible]
instance SetM.instHasEvalSet :
HasEvalSet SetM

Enable support notation for SetM (note the need for the monadic instance and not Set).

source
@[simp]
theorem SetM.support_eq_run {α : Type u} (s : SetM α) :
support s = s.run
source
@[implicit_reducible]
instance SPMF.instHasEvalSPMF :
HasEvalSPMF SPMF

Enable probability notation for SPMF, using identity as the SPMF embedding.

source
@[simp]
theorem SPMF.evalDist_def {α : Type u} (p : SPMF α) :
evalDist p = p
source
theorem SPMF.support_eq_support {α : Type u} (p : SPMF α) :
support p = p.support
source
theorem SPMF.probOutput_eq_apply {α : Type u} (p : SPMF α) (x : α) :
Pr[= x | p] = p x
source
theorem SPMF.evalDist_eq_iff {α : Type u} {m : Type u → Type u_1} [Monad m] [HasEvalSPMF m] (mx : m α) (p : SPMF α) :
evalDist mx = p ↔ ∀ (x : α), Pr[= x | mx] = p x
source
@[implicit_reducible]
noncomputable instance PMF.instHasEvalPMF :
HasEvalPMF PMF

Enable probability notation for PMF, using liftM as the SPMF embedding.

source
@[simp]
theorem PMF.evalDist_eq {α : Type u} (p : PMF α) :
evalDist p = liftM p
source
@[simp]
theorem PMF.probOutput_eq_apply {α : Type u} (p : PMF α) (x : α) :
Pr[= x | p] = p x
source
@[simp]
theorem SPMF.evalDist_liftM {α : Type u} (p : PMF α) :
evalDist (liftM p) = evalDist p
source
@[simp]
theorem SPMF.probOutput_liftM {α : Type u} (p : PMF α) (x : α) :
Pr[= x | liftM p] = Pr[= x | p]
source
@[simp]
theorem SPMF.probEvent_liftM {α : Type u} (p : PMF α) (e : α → Prop) :
probEvent (liftM p) e = probEvent p e
source
@[simp]
theorem SPMF.probFailure_liftM {α : Type u} (p : PMF α) :
Pr[⊥ | liftM p] = Pr[⊥ | p]
source
@[implicit_reducible]
noncomputable instance Id.instHasEvalPMF :
HasEvalPMF Id

The support of a computation in Id is the result being returned.

source
@[implicit_reducible]
instance Id.instHasEvalFinset :
HasEvalFinset Id
source
@[simp]
theorem Id.support_eq_singleton {α : Type u} (x : Id α) :
support x = {x.run}
source
@[simp]
theorem Id.finSupport_eq_singleton {α : Type u} [DecidableEq α] (x : Id α) :
finSupport x = {x.run}
source
@[simp]
theorem Id.probOutput_eq_ite {α : Type u} [DecidableEq α] (x : Id α) (y : α) :
Pr[= y | x] = if y = x.run then 1 else 0
source
@[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
source
theorem Id.probFailure_eq_zero {α : Type u} (x : Id α) :
Pr[⊥ | x] = 0