Documentation

VCVio.EvalDist.Defs.Support

Typeclasses for Denotational Monad Support #

This file defines typeclasses HasEvalSet m and HasEvalFinset m for asigning a set of possible outputs to computations in a monad m.

source
@[simp]
theorem SetM.pure_def {α : Type u} (x : α) :
pure x = {x}
source
@[simp]
theorem SetM.bind_def {α β : Type u} (mx : SetM α) (my : α → SetM β) :
mx >>= my = ⋃ x ∈ mx.run, my x
source
class HasEvalSet (m : Type u → Type v) [Monad m] :
Type (max (u + 1) v)

The monad m can be evaluated to get a set of possible outputs. Note that we don't implement this for Set with the monad type-class strangeness. Should not be implemented manually if a HasEvalSPMF instance already exists.

Instances
    source
    def support {m : Type u → Type v} [Monad m] [HasEvalSet m] {α : Type u} (mx : m α) :
    Set α

    The set of possible outputs of running the monadic computation mx.

    Instances For
      source
      theorem support_def {m : Type u → Type v} [Monad m] [HasEvalSet m] {α : Type u} (mx : m α) :
      support mx = ((fun {α : Type u} (x : m α) => HasEvalSet.toSet.toFun α x) mx).run
      source
      class HasEvalFinset (m : Type u → Type v) [Monad m] [HasEvalSet m] :
      Type (max (u + 1) v)

      The monad m can be evaluated to get a finite set of possible outputs. We restrict to the case of decidable equality of the output type, so Finset.biUnion exists. Note: we can't use MonadHomClass since Finset has no Monad instance.

      Instances
        source
        theorem mem_finSupport_iff_mem_support {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSet m] [HasEvalFinset m] [DecidableEq α] (mx : m α) (x : α) :
        x ∈ finSupport mx ↔ x ∈ support mx
        source
        theorem finSupport_eq_iff_support_eq_coe {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSet m] [HasEvalFinset m] [DecidableEq α] (mx : m α) (s : Finset α) :
        finSupport mx = s ↔ support mx = ↑s
        source
        theorem finSupport_eq_of_support_eq_coe {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSet m] [HasEvalFinset m] [DecidableEq α] {mx : m α} {s : Finset α} (h : support mx = ↑s) :
        finSupport mx = s
        source
        theorem mem_finSupport_of_mem_support {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSet m] [HasEvalFinset m] [DecidableEq α] {mx : m α} {x : α} (h : x ∈ support mx) :
        x ∈ finSupport mx
        source
        theorem mem_support_of_mem_finSupport {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSet m] [HasEvalFinset m] [DecidableEq α] {mx : m α} {x : α} (h : x ∈ finSupport mx) :
        x ∈ support mx
        source
        theorem not_mem_finSupport_of_not_mem_support {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSet m] [HasEvalFinset m] [DecidableEq α] {mx : m α} {x : α} (h : x ∉ support mx) :
        x ∉ finSupport mx
        source
        theorem not_mem_support_of_not_mem_finSupport {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSet m] [HasEvalFinset m] [DecidableEq α] {mx : m α} {x : α} (h : x ∉ finSupport mx) :
        x ∉ support mx
        source
        @[simp]
        theorem support_ite {m : Type u → Type v} [Monad m] {α : Type u} (p : Prop) [Decidable p] [HasEvalSet m] (mx mx' : m α) :
        support (if p then mx else mx') = if p then support mx else support mx'
        source
        @[simp]
        theorem finSupport_ite {m : Type u → Type v} [Monad m] {α : Type u} (p : Prop) [Decidable p] [HasEvalSet m] [HasEvalFinset m] [DecidableEq α] (mx mx' : m α) :
        finSupport (if p then mx else mx') = if p then finSupport mx else finSupport mx'
        source
        theorem support_eqRec {m : Type u → Type v} [Monad m] {α β : Type u} [HasEvalSet m] (h : α = β) (mx : m α) :
        support (h ▸ mx) = h ▸ support mx
        source
        theorem finSupport_eqRec {α β : Type u} {m : Type u → Type u_1} [hm : Monad m] [hms : HasEvalSet m] [hmfs : HasEvalFinset m] [hα : DecidableEq α] (h : α = β) (mx : m α) :
        finSupport (h ▸ mx) = h ▸ finSupport mx
        source
        class HasEvalSet.Decidable (m : Type u → Type v) [Monad m] [HasEvalSet m] :
        Type (max (u + 1) v)

        Membership in the support of computations in.

        Instances
          source
          @[implicit_reducible]
          instance decidablePred_mem_support {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSet m] [HasEvalSet.Decidable m] (mx : m α) :
          DecidablePred fun (x : α) => x ∈ support mx
          source
          @[implicit_reducible]
          instance decidablePred_mem_finSupport {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSet m] [HasEvalSet.Decidable m] [HasEvalFinset m] [DecidableEq α] (mx : m α) :
          DecidablePred fun (x : α) => x ∈ finSupport mx