Documentation

VCVio.EvalDist.Defs.Instances

Monad Evaluation Semantics Instances #

This file defines various instances of evaluation semantics for different monads

source
instance SetM.instHasEvalSet :
HasEvalSet SetM

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

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

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

    Equations
      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
      noncomputable instance PMF.instHasEvalPMF :
      HasEvalPMF PMF

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

      Equations
        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) :
        Pr[e | liftM p] = Pr[e | p]
        source
        @[simp]
        theorem SPMF.probFailure_liftM {α : Type u} (p : PMF α) :
        Pr[⊥ | liftM p] = Pr[⊥ | p]
        source
        noncomputable instance Id.instHasEvalPMF :
        HasEvalPMF Id

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

        Equations
          source
          instance Id.instHasEvalFinset :
          HasEvalFinset Id
          Equations
            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} [DecidableEq α] (x : Id α) (p : α → Prop) [DecidablePred p] :
            Pr[p | x] = if p x.run then 1 else 0
            source
            theorem Id.probFailure_eq_zero {α : Type u} (x : Id α) :
            Pr[⊥ | x] = 0