Support of a Monadic Computation

This file defines support mx — the set of possible outputs of a monadic computation mx — as well as HasEvalFinset, a typeclass for assigning a finite version of the support.

The support is the Set-valued view of MonadAttach.CanReturn provided by PolyFun. Finite support and decidable membership are optional refinements of that view.

class HasEvalFinset (m : Type u → Type v) [MonadAttach 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} {α : Type u} [MonadAttach 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} {α : Type u} [MonadAttach 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} {α : Type u} [MonadAttach 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} {α : Type u} [MonadAttach 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} {α : Type u} [MonadAttach 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} {α : Type u} [MonadAttach 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} {α : Type u} [MonadAttach m] [HasEvalFinset m] [DecidableEq α] {mx : m α} {x : α} (h : x ∉ finSupport mx) : x ∉ support mx

def allOutputsSatisfy {m : Type u → Type v} [MonadAttach 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 a qualitative assertion about the possible outputs provided by MonadAttach m.

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} [MonadAttach 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} [MonadAttach 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} [MonadAttach m] {α : Type u} (p : α → Prop) (mx : m α) : someOutputSatisfies p mx ↔ ∃ x ∈ support mx, p x

theorem allOutputsSatisfy_mono {m : Type u → Type v} [MonadAttach 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} [MonadAttach m] {α : Type u} {p q : α → Prop} (hpq : ∀ (a : α), p a → q a) (mx : m α) : someOutputSatisfies p mx → someOutputSatisfies q mx

theorem support_ite {m : Type u → Type v} {α : Type u} (p : Prop) [Decidable p] [MonadAttach 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} {α : Type u} (p : Prop) [Decidable p] [MonadAttach 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} {α β : Type u} [MonadAttach m] (h : α = β) (mx : m α) : support (h ▸ mx) = h ▸ support mx

theorem finSupport_eqRec {α β : Type u} {m : Type u → Type u_1} [hms : MonadAttach m] [hmfs : HasEvalFinset m] [hα : DecidableEq α] (h : α = β) (mx : m α) : finSupport (h ▸ mx) = h ▸ finSupport mx

class HasEvalSet.Decidable (m : Type u → Type v) [MonadAttach 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

@[instance_reducible]

instance decidablePred_mem_support {m : Type u → Type v} {α : Type u} [MonadAttach m] [HasEvalSet.Decidable m] (mx : m α) : DecidablePred fun (x : α) => x ∈ support mx

@[instance_reducible]

instance decidablePred_mem_finSupport {m : Type u → Type v} {α : Type u} [MonadAttach m] [HasEvalSet.Decidable m] [HasEvalFinset m] [DecidableEq α] (mx : m α) : DecidablePred fun (x : α) => x ∈ finSupport mx