Documentation

VCVio.EvalDist.Instances.OptionT

Probability Distributions on Potentially Failing Computations #

This file gives an instance to extend a evalDist instance on a monad to one transformed by the OptionT monad transformer.

dt: should add more instances and connecting lemmas

source
noncomputable instance OptionT.instHasEvalSet (m : Type u → Type v) [Monad m] [HasEvalSet m] :
HasEvalSet (OptionT m)

TODO: fintype version of this lemma

Equations
    source
    @[simp]
    theorem OptionT.support_liftM {α : Type u} (m : Type u → Type v) [Monad m] [HasEvalSet m] (mx : m α) :
    support (liftM mx) = support mx
    source
    noncomputable instance OptionT.instHasEvalSPMF (m : Type u → Type v) [Monad m] [HasEvalSPMF m] :
    HasEvalSPMF (OptionT m)

    If we have a HasEvalPMF m instance, we can lift it to HasEvalSPMF (OptionT m).

    Equations
      source
      theorem OptionT.support_eq (m : Type u → Type v) [Monad m] [HasEvalSPMF m] {α : Type u} (mx : OptionT m α) :
      support mx = some ⁻¹' support mx.run
      source
      noncomputable instance OptionT.instHasEvalFinset (m : Type u → Type v) [Monad m] [HasEvalSPMF m] [HasEvalFinset m] :
      HasEvalFinset (OptionT m)

      Lift a finSupport instance to OptionT. by just taking preimage under some.

      Equations
        source
        theorem OptionT.finSupport_eq (m : Type u → Type v) [Monad m] [HasEvalSPMF m] {α : Type u} [HasEvalFinset m] [DecidableEq α] (mx : OptionT m α) :
        finSupport mx = (finSupport mx.run).preimage some ⋯
        source
        @[simp]
        theorem OptionT.mem_finSupport_iff (m : Type u → Type v) [Monad m] [HasEvalSPMF m] {α : Type u} [HasEvalFinset m] [DecidableEq α] (mx : OptionT m α) (x : α) :
        x ∈ finSupport mx ↔ ∃ y ∈ finSupport mx.run, some (some x) = some y
        source
        instance OptionT.instLawfulFailure (m : Type u → Type v) [Monad m] [HasEvalSPMF m] :
        HasEvalSet.LawfulFailure (OptionT m)
        source
        theorem OptionT.evalDist_eq (m : Type u → Type v) [Monad m] [HasEvalSPMF m] {α : Type u} (mx : OptionT m α) :
        evalDist mx = (fun {α : Type u} (x : OptionT m α) => (OptionT.mapM' HasEvalSPMF.toSPMF).toFun α x) mx
        source
        theorem OptionT.probOutput_eq (m : Type u → Type v) [Monad m] [HasEvalSPMF m] {α : Type u} (mx : OptionT m α) (x : α) :
        Pr[=x | mx] = Pr[=some x | mx.run]
        source
        theorem OptionT.probEvent_eq (m : Type u → Type v) [Monad m] [HasEvalSPMF m] {α : Type u} (mx : OptionT m α) (p : α → Prop) [DecidablePred p] :
        Pr[p | mx] = Pr[fun (x : Option α) => Option.all (fun (b : α) => decide (p b)) x = true | mx.run]
        source
        theorem OptionT.probFailure_eq (m : Type u → Type v) [Monad m] [HasEvalSPMF m] {α : Type u} (mx : OptionT m α) :
        Pr[⊥ | mx] = Pr[=none | mx.run]
        source
        @[simp]
        theorem OptionT.probOutput_lift (m : Type u → Type v) [Monad m] [HasEvalSPMF m] {α : Type u} [LawfulMonad m] (mx : m α) (x : α) :
        Pr[=x | OptionT.lift mx] = Pr[=x | mx]
        source
        @[simp]
        theorem OptionT.probEvent_lift (m : Type u → Type v) [Monad m] [HasEvalSPMF m] {α : Type u} [LawfulMonad m] (mx : m α) (p : α → Prop) :
        Pr[p | OptionT.lift mx] = Pr[p | mx]
        source
        @[simp]
        theorem OptionT.probOutput_liftM (m : Type u → Type v) [Monad m] [HasEvalSPMF m] {α : Type u} [LawfulMonad m] (mx : m α) (x : α) :
        Pr[=x | liftM mx] = Pr[=x | mx]
        source
        @[simp]
        theorem OptionT.probEvent_liftM (m : Type u → Type v) [Monad m] [HasEvalSPMF m] {α : Type u} [LawfulMonad m] (mx : m α) (p : α → Prop) :
        Pr[p | liftM mx] = Pr[p | mx]
        source
        @[simp]
        theorem OptionT.probFailure_liftM (m : Type u → Type v) [Monad m] [HasEvalSPMF m] {α : Type u} [LawfulMonad m] (mx : m α) :
        Pr[⊥ | liftM mx] = 0