Structural support under monadic operations

Pure, bind, and map preserve operational reachability through ExactMonadAttach. Finite-support equations add enumeration assumptions without choosing probabilities.

theorem support_pure {α : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] (x : α) : support (pure x) = {x}

theorem mem_support_pure_iff {α : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] (x y : α) : x ∈ support (pure y) ↔ x = y

theorem mem_support_pure_iff' {α : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] (x y : α) : x ∈ support (pure y) ↔ y = x

theorem eq_of_mem_support_pure {α : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] {x y : α} (h : y ∈ support (pure x)) : y = x

obtain-friendly forward direction of mem_support_pure_iff: membership in the support of a pure forces equality with the pure value.

@[simp]

theorem finSupport_pure {α : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] [HasEvalFinset m] [DecidableEq α] (x : α) : finSupport (pure x) = {x}

theorem mem_finSupport_pure_iff {α : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] [HasEvalFinset m] [DecidableEq α] (x y : α) : x ∈ finSupport (pure y) ↔ x = y

theorem mem_finSupport_pure_iff' {α : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] [HasEvalFinset m] [DecidableEq α] (x y : α) : x ∈ finSupport (pure y) ↔ y = x

theorem support_bind {α β : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] (mx : m α) (my : α → m β) : support (mx >>= my) = ⋃ x ∈ support mx, support (my x)

theorem mem_support_bind_iff {α β : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] (mx : m α) (my : α → m β) (y : β) : y ∈ support (mx >>= my) ↔ ∃ x ∈ support mx, y ∈ support (my x)

theorem support_bind_exists {α β : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] {x : m α} {f : α → m β} {y : β} (hy : y ∈ support (x >>= f)) : ∃ a ∈ support x, y ∈ support (f a)

obtain-friendly forward direction of mem_support_bind_iff: peel an element of the support of a bind into a witness for the first computation and membership for the second.

@[simp]

theorem finSupport_bind {α β : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] [HasEvalFinset m] [DecidableEq α] [DecidableEq β] (mx : m α) (my : α → m β) : finSupport (mx >>= my) = (finSupport mx).biUnion fun (x : α) => finSupport (my x)

theorem mem_finSupport_bind_iff {α β : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] [HasEvalFinset m] [DecidableEq α] [DecidableEq β] (mx : m α) (my : α → m β) (y : β) : y ∈ finSupport (mx >>= my) ↔ ∃ x ∈ finSupport mx, y ∈ finSupport (my x)

theorem support_map {α β : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] (f : α → β) (mx : m α) : support (f <$> mx) = f '' support mx

@[simp]

theorem finSupport_map {α β : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] [HasEvalFinset m] [DecidableEq α] [DecidableEq β] (f : α → β) (mx : m α) : finSupport (f <$> mx) = Finset.image f (finSupport mx)

@[simp]

theorem allOutputsSatisfy_pure {α : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] (p : α → Prop) (x : α) : allOutputsSatisfy p (pure x) ↔ p x

@[simp]

theorem someOutputSatisfies_pure {α : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] (p : α → Prop) (x : α) : someOutputSatisfies p (pure x) ↔ p x

@[simp]

theorem allOutputsSatisfy_bind {α β : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] (mx : m α) (my : α → m β) (p : β → Prop) : allOutputsSatisfy p (mx >>= my) ↔ allOutputsSatisfy (fun (a : α) => allOutputsSatisfy p (my a)) mx

@[simp]

theorem someOutputSatisfies_bind {α β : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] (mx : m α) (my : α → m β) (p : β → Prop) : someOutputSatisfies p (mx >>= my) ↔ someOutputSatisfies (fun (a : α) => someOutputSatisfies p (my a)) mx