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.

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 = HasEvalSet.toSet.toFun α mx

instance instHasEvalSetSetM : HasEvalSet SetM

The support of a SetM computation is the resulting set.

@[simp]

theorem SetM.support_eq {α : Type u} (x : SetM α) : support x = x.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

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

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

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