Monad Evaluation Semantics Instances

This file defines various instances of evaluation semantics for different monads

instance SetM.instHasEvalSet : HasEvalSet SetM

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

Equations

• SetM.instHasEvalSet = { toSet := MonadHom.id SetM }

@[simp]

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

instance SPMF.instHasEvalSPMF : HasEvalSPMF SPMF

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SPMF.evalDist_def {α : Type u} (p : SPMF α) : evalDist 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] [HasEvalSPMF m] (mx : m α) (p : SPMF α) : evalDist mx = p ↔ ∀ (x : α), Pr[=x | mx] = p x

noncomputable instance PMF.instHasEvalPMF : HasEvalPMF PMF

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PMF.evalDist_eq {α : Type u} (p : PMF α) : evalDist 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 α) : evalDist (liftM p) = evalDist 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) : Pr[e | liftM p] = Pr[e | p]

@[simp]

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

noncomputable instance Id.instHasEvalPMF : HasEvalPMF Id

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

Equations

• Id.instHasEvalPMF = { toSet := MonadHom.pure SetM, toSPMF := MonadHom.pure SPMF, support_eq := ⋯, toPMF := MonadHom.pure PMF, toSPMF_eq := @Id.instHasEvalPMF._proof_2 }

instance Id.instHasEvalFinset : HasEvalFinset Id

Equations

• Id.instHasEvalFinset = { finSupport := fun {α : Type ?u.8} [DecidableEq α] (x : Id α) => {x}, coe_finSupport := @Id.instHasEvalFinset._proof_1 }

@[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} [DecidableEq α] (x : Id α) (p : α → Prop) [DecidablePred p] : Pr[p | x] = if p x.run then 1 else 0

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