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.

@[simp]

theorem SetM.pure_def {α : Type u} (x : α) : pure x = {x}

@[simp]

theorem SetM.bind_def {α β : Type u} (mx : SetM α) (my : α → SetM β) : mx >>= my = ⋃ x ∈ mx.run, my x

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.

• toSet : m →ᵐ SetM

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.

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

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.

• finSupport {α : Type u} [DecidableEq α] (mx : m α) : Finset α
• coe_finSupport {α : Type u} [DecidableEq α] (mx : m α) : ↑(finSupport mx) = support mx

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

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

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

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

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

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

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

def allOutputsSatisfy {m : Type u → Type v} [Monad m] [HasEvalSet m] {α : Type u} (p : α → Prop) (mx : m α) : Prop

A predicate holds on every output reachable from a monadic computation mx, i.e. ∀ x ∈ support mx, p x. This is the "almost-sure" assertion at the qualitative denotational level provided by HasEvalSet.

For OracleComp, see also the structural-recursion variant OracleComp.allOutputsSatisfyWhen in VCVio/OracleComp/Traversal.lean, which is parameterized by a set of possible oracle outputs.

def someOutputSatisfies {m : Type u → Type v} [Monad m] [HasEvalSet m] {α : Type u} (p : α → Prop) (mx : m α) : Prop

A predicate holds on some output reachable from a monadic computation mx, i.e. ∃ x ∈ support mx, p x.

theorem allOutputsSatisfy_iff_forall_support {m : Type u → Type v} [Monad m] [HasEvalSet m] {α : Type u} (p : α → Prop) (mx : m α) : allOutputsSatisfy p mx ↔ ∀ x ∈ support mx, p x

theorem someOutputSatisfies_iff_exists_support {m : Type u → Type v} [Monad m] [HasEvalSet m] {α : Type u} (p : α → Prop) (mx : m α) : someOutputSatisfies p mx ↔ ∃ x ∈ support mx, p x

theorem allOutputsSatisfy_mono {m : Type u → Type v} [Monad m] [HasEvalSet m] {α : Type u} {p q : α → Prop} (hpq : ∀ (a : α), p a → q a) (mx : m α) : allOutputsSatisfy p mx → allOutputsSatisfy q mx

theorem someOutputSatisfies_mono {m : Type u → Type v} [Monad m] [HasEvalSet m] {α : Type u} {p q : α → Prop} (hpq : ∀ (a : α), p a → q a) (mx : m α) : someOutputSatisfies p mx → someOutputSatisfies q mx

@[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'

@[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'

theorem support_eqRec {m : Type u → Type v} [Monad m] {α β : Type u} [HasEvalSet m] (h : α = β) (mx : m α) : support (h ▸ mx) = h ▸ support mx

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

class HasEvalSet.Decidable (m : Type u → Type v) [Monad m] [HasEvalSet m] : Type (max (u + 1) v)

Membership in the support of computations in.

• mem_support_decidable {α : Type u} (mx : m α) : DecidablePred fun (x : α) => x ∈ support mx

@[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

@[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