Monadic Support and Exact Composition

Lean core's MonadAttach already provides the notion this layer needs: a predicate MonadAttach.CanReturn x a, meaning a is a possible return value of x, together with attach, which decorates a computation's results with proofs of that predicate. LawfulMonadAttach further pins CanReturn down as the strongest postcondition. This file adds a Set-valued view and optional composition laws:

• ExactMonadAttach — additional introduction rules for CanReturn. Together with core's elimination rules they give exact support equations for pure and bind. These are properties of the monad, not a choice of a more precise return predicate. For example, the constant monad fun _ => PUnit forgets every result and has canonical empty support, even for pure; it is lawful but does not satisfy these extra laws.
• MonadAttach.support x : Set α — the Set-valued view of CanReturn, definitionally the predicate itself, so a ∈ support x ↔ CanReturn x a is Iff.rfl.
• The qualitative judgments AllOutputs ("always"), SomeOutput, and NoOutput ("never"), with scoped notation x ⊨ₐ p, x ⊨ₛ p, and x ⊭ p.

ExactMonadAttach is a proof-only extension of LawfulMonadAttach over the existing attachment data. Strong lawfulness already identifies the return predicate; weak lawfulness alone permits coarse predicates such as MonadAttach.trivial. Universal safety reasoning needs only the strong upstream laws. Exact composition is needed for the equations below and for introducing existential reachability through a bind.

With exact composition, AllOutputs induces the demonic ordered monad algebra MAlgOrdered m Prop, identifying "always" with the trivial-precondition Hoare triple (triple_top_iff_allOutputs); SomeOutput gives the angelic companion. Both algebras are named definitions rather than global instances: transformer algebras such as MAlgOrdered.instOptionT give failures a different meaning, so a generic global support instance would be incoherent with them.

Scope

Support is a value-level notion here: CanReturn does not retain the initial state or state changes. Concretely, StateT σ m and ReaderT ρ m do have MonadAttach instances — quantifying existentially over the initial state — and those supports are canonical, so the elimination theory applies. They do not admit a general ExactMonadAttach instance: flattened premises may choose unrelated indices on the sides of a bind. For StateT this can let the continuation observe a state the prefix did not produce; for ReaderT it can let the two premises use different environments. Reason about those per run instead, via mem_support_stateT_iff / mem_support_readerT_iff; PolyFunTest pins the failure with a counterexample. Oracle- and state-relative supports belong at the specification layer (PolyFun.PFunctor.Free.WP), which indexes the notion by a per-operation answer assignment.

A second limitation is inherited from MonadAttach: an instance must supply attach. Informative computable attachment is not generally available for continuation-passing encodings. Core therefore uses trivial, weakly lawful attachment for StateCpsT and ExceptCpsT; those instances do not supply the strong laws required here.

Companion modules

This file keys everything on pure and bind. The instances (Except, SetM, the transformers) and the lift transport are in Support/Instances.lean; the per-run support of StateT / ReaderT (mem_support_stateT_iff, mem_support_readerT_iff, supportFrom, supportAt) in Support/Indexed.lean; the remaining do-fragment constructs (<*, *>, if, match on Option / Sum) in Support/Structural.lean; loop rules in Support/Loops.lean; and the interpretations as core WPMonads in Support/WP.lean.

class ExactMonadAttach (m : Type u → Type v) [Monad m] [MonadAttach m] extends LawfulMonadAttach m : Prop

Exact pure and bind composition for the existing lawful attachment predicate.

The two introduction rules complement core's elimination rules to give support equations. This class carries proofs only: LawfulMonadAttach already fixes the return predicate, while these additional laws need not hold for every lawful monad.

• map_attach {α : Type u} {x : m α} : Subtype.val <$> MonadAttach.attach x = x
• canReturn_map_imp {α : Type u} {P : α → Prop} {x : m (Subtype P)} {a : α} : MonadAttach.CanReturn (Subtype.val <$> x) a → P a
• canReturn_pure {α : Type u} (a : α) : MonadAttach.CanReturn (pure a) a

  A pure computation can return its own value.

• canReturn_bind {α β : Type u} {x : m α} {f : α → m β} {a : α} {b : β} : MonadAttach.CanReturn x a → MonadAttach.CanReturn (f a) b → MonadAttach.CanReturn (x >>= f) b

  Possible outputs compose along bind.

def MonadAttach.support {m : Type u → Type v} {α : Type u} [MonadAttach m] (x : m α) : Set α

The set of possible outputs of a monadic computation: the Set-valued view of CanReturn. Available for any MonadAttach; the structural equations are gated behind ExactMonadAttach.

@[simp]

theorem MonadAttach.mem_support {m : Type u → Type v} {α : Type u} [MonadAttach m] {x : m α} {a : α} : a ∈ support x ↔ CanReturn x a

Membership in support is CanReturn, definitionally.

Stated as a simp lemma because Set.ofPred and Set.Mem are implicit_reducible: rfl and exact see through them, but simp's reducible-transparency discharge does not.

Automation contract

Two normal forms, one per layer, chosen so the two do not fight:

• Membership normalizes to CanReturn. mem_support is @[simp, grind =], so a ∈ support x becomes the atomic reachability predicate, and the per-monad canReturn_iff lemmas take it the rest of the way to a concrete equation. Those lemmas key on CanReturn, not on membership, precisely so that they extend the chain rather than race mem_support for the same left-hand side.
• Set-level laws produce support terms. support_pure, support_bind, support_map are @[simp], so a structural goal is first decomposed at the set level and only then unfolded pointwise.

grind tags go on the directed, single-variable bridges only: membership unfoldings and the closed-form supports of pure/none/error. The characterizations that quantify over the support — support_eq_empty_iff, support_nonempty_iff, and the AllOutputs/SomeOutput iffs — stay @[simp]-only. Those are saturation hazards: grind case-splits the iff, Skolemizes the support quantifier into a fresh witness, and the always-tagged bind expansions turn that witness back into more support terms with no finite grounding. A proof that needs one re-supplies it locally, as grind [allOutputs_iff_forall_support].

Emptiness and branching

These need no exactness: they are about the shape of the Set, not about how the monad's operations act on it.

theorem MonadAttach.support_eq_empty_iff {m : Type u → Type v} {α : Type u} [MonadAttach m] {x : m α} : support x = ∅ ↔ ∀ (a : α), ¬CanReturn x a

theorem MonadAttach.support_nonempty_iff {m : Type u → Type v} {α : Type u} [MonadAttach m] {x : m α} : (support x).Nonempty ↔ ∃ (a : α), CanReturn x a

theorem MonadAttach.not_mem_support_iff {m : Type u → Type v} {α : Type u} [MonadAttach m] {x : m α} {a : α} : a ∉ support x ↔ ¬CanReturn x a

theorem MonadAttach.bind_congr_of_canReturn {m : Type u → Type v} {α β : Type u} [Monad m] [LawfulMonad m] [MonadAttach m] [WeaklyLawfulMonadAttach m] (x : m α) {f g : α → m β} (h : ∀ (a : α), CanReturn x a → f a = g a) : x >>= f = x >>= g

Continuations agreeing on possible returns produce the same computation.

theorem MonadAttach.bind_congr_of_forall_mem_support {m : Type u → Type v} {α β : Type u} [Monad m] [LawfulMonad m] [MonadAttach m] [WeaklyLawfulMonadAttach m] (x : m α) {f g : α → m β} (h : ∀ a ∈ support x, f a = g a) : x >>= f = x >>= g

Continuations agreeing on the support produce the same computation.

@[simp]

theorem MonadAttach.support_ite {m : Type u → Type v} {α : Type u} [MonadAttach m] (c : Prop) [Decidable c] (x y : m α) : support (if c then x else y) = if c then support x else support y

@[simp]

theorem MonadAttach.support_dite {m : Type u → Type v} {α : Type u} [MonadAttach m] (c : Prop) [Decidable c] (x : c → m α) (y : ¬c → m α) : support (if h : c then x h else y h) = if h : c then support (x h) else support (y h)

@[simp]

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

@[simp]

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

theorem MonadAttach.mem_support_pure {m : Type u → Type v} {α : Type u} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] {a b : α} : a ∈ support (pure b) ↔ a = b

The structural laws on CanReturn

The same three equations keyed on the reachability predicate rather than on set membership. support_pure/support_bind/support_map decompose a goal at the set level; these finish it pointwise, and they are what makes CanReturn a usable normal form rather than a dead end. Core supplies only the elimination halves (eq_of_canReturn_pure, canReturn_bind_imp', canReturn_map_imp'); the introduction halves are exactly ExactMonadAttach's two fields, so the equivalences need both classes.

Their orientation matches the corresponding mem_support_* lemmas, so the two routes through the simp set — unfold membership first, or rewrite the set first — converge on the same normal form instead of racing.

@[simp]

theorem MonadAttach.canReturn_pure_iff {m : Type u → Type v} {α : Type u} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] {a b : α} : CanReturn (pure b) a ↔ a = b

@[simp]

theorem MonadAttach.canReturn_bind_iff {m : Type u → Type v} {α β : Type u} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] {x : m α} {f : α → m β} {b : β} : CanReturn (x >>= f) b ↔ ∃ (a : α), CanReturn x a ∧ CanReturn (f a) b

@[simp]

theorem MonadAttach.canReturn_map_iff {m : Type u → Type v} {α β : Type u} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] {g : α → β} {x : m α} {b : β} : CanReturn (g <$> x) b ↔ ∃ (a : α), CanReturn x a ∧ g a = b

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

@[simp]

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

@[simp]

theorem MonadAttach.support_seq {m : Type u → Type v} {α β : Type u} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] (f : m (α → β)) (x : m α) : support (f <*> x) = ⋃ g ∈ support f, g '' support x

Always / some / never output judgments

def MonadAttach.AllOutputs {m : Type u → Type v} {α : Type u} [MonadAttach m] (p : α → Prop) (x : m α) : Prop

Every possible output of x satisfies p — the "always true" judgment.

Stated over CanReturn rather than as a bounded quantifier over support, because the modality does not need to expose a Set in its interface. This makes the same shape easy to index when a flattened set of values is too coarse, as for StateT; the indexed carrier there is still the honest set of value/final-state pairs. The two unindexed spellings are definitionally interchangeable — allOutputs_iff_forall_support and allOutputs_iff_forall_canReturn are both Iff.rfl — so nothing downstream has to choose.

def MonadAttach.SomeOutput {m : Type u → Type v} {α : Type u} [MonadAttach m] (p : α → Prop) (x : m α) : Prop

Some possible output of x satisfies p. The angelic half of the pair; see AllOutputs for why it is stated over CanReturn.

def MonadAttach.NoOutput {m : Type u → Type v} {α : Type u} [MonadAttach m] (p : α → Prop) (x : m α) : Prop

No possible output of x satisfies p — the "never true" judgment.

def MonadAttach.«term_⊨ₐ_» : Lean.TrailingParserDescr

Every possible output of x satisfies p — the "always true" judgment.

Stated over CanReturn rather than as a bounded quantifier over support, because the modality does not need to expose a Set in its interface. This makes the same shape easy to index when a flattened set of values is too coarse, as for StateT; the indexed carrier there is still the honest set of value/final-state pairs. The two unindexed spellings are definitionally interchangeable — allOutputs_iff_forall_support and allOutputs_iff_forall_canReturn are both Iff.rfl — so nothing downstream has to choose.

def MonadAttach.«term_⊨ₛ_» : Lean.TrailingParserDescr

Some possible output of x satisfies p. The angelic half of the pair; see AllOutputs for why it is stated over CanReturn.

def MonadAttach.«term_⊭_» : Lean.TrailingParserDescr

No possible output of x satisfies p — the "never true" judgment.

theorem MonadAttach.allOutputs_iff_forall_support {m : Type u → Type v} {α : Type u} [MonadAttach m] (p : α → Prop) (x : m α) : AllOutputs p x ↔ ∀ a ∈ support x, p a

theorem MonadAttach.someOutput_iff_exists_support {m : Type u → Type v} {α : Type u} [MonadAttach m] (p : α → Prop) (x : m α) : SomeOutput p x ↔ ∃ a ∈ support x, p a

theorem MonadAttach.noOutput_iff_forall_support {m : Type u → Type v} {α : Type u} [MonadAttach m] (p : α → Prop) (x : m α) : NoOutput p x ↔ ∀ a ∈ support x, ¬p a

theorem MonadAttach.allOutputs_iff_forall_canReturn {m : Type u → Type v} {α : Type u} [MonadAttach m] (p : α → Prop) (x : m α) : AllOutputs p x ↔ ∀ (a : α), CanReturn x a → p a

theorem MonadAttach.support_eq_setOf_someOutput {m : Type u → Type v} {α : Type u} [MonadAttach m] (x : m α) : support x = {a : α | SomeOutput (fun (x : α) => x = a) x}

support is the equality instance of the angelic judgment: a value is a possible output exactly when "some output equals it" holds.

The two presentations of the layer meet here. support is the Set-valued carrier and AllOutputs/SomeOutput are the demonic and angelic modalities over it; this equation says nothing is lost by reading the carrier off the modality instead. The modality is the more flexible presentation: its shape can be indexed when a flattened set of values is too coarse, as in the StateT section below. It is also what the weakest-precondition bridge consumes: MonadAttach.toWP is built from AllOutputs, not from support.

theorem MonadAttach.someOutput_eq_iff_mem_support {m : Type u → Type v} {α : Type u} [MonadAttach m] (x : m α) (a : α) : SomeOutput (fun (x : α) => x = a) x ↔ a ∈ support x

The angelic judgment at an equality predicate is membership in the support. The pointwise form of support_eq_setOf_someOutput.

theorem MonadAttach.not_someOutput_iff_noOutput {m : Type u → Type v} {α : Type u} [MonadAttach m] (p : α → Prop) (x : m α) : ¬SomeOutput p x ↔ NoOutput p x

theorem MonadAttach.allOutputs_and {m : Type u → Type v} {α : Type u} [MonadAttach m] (p q : α → Prop) (x : m α) : AllOutputs (fun (a : α) => p a ∧ q a) x ↔ AllOutputs p x ∧ AllOutputs q x

theorem MonadAttach.allOutputs_mono {m : Type u → Type v} {α : Type u} [MonadAttach m] {p q : α → Prop} (h : ∀ (a : α), p a → q a) {x : m α} (hx : AllOutputs p x) : AllOutputs q x

theorem MonadAttach.someOutput_mono {m : Type u → Type v} {α : Type u} [MonadAttach m] {p q : α → Prop} (h : ∀ (a : α), p a → q a) {x : m α} (hx : SomeOutput p x) : SomeOutput q x

theorem MonadAttach.noOutput_mono {m : Type u → Type v} {α : Type u} [MonadAttach m] {p q : α → Prop} (h : ∀ (a : α), q a → p a) {x : m α} (hx : NoOutput p x) : NoOutput q x

Negation

Classically, the pair is dual: the demonic judgment is the negation of the angelic one at the negated predicate, and conversely. Only one direction was available before.

theorem MonadAttach.not_allOutputs_iff {m : Type u → Type v} {α : Type u} [MonadAttach m] (p : α → Prop) (x : m α) : ¬AllOutputs p x ↔ SomeOutput (fun (a : α) => ¬p a) x

theorem MonadAttach.not_noOutput_iff {m : Type u → Type v} {α : Type u} [MonadAttach m] (p : α → Prop) (x : m α) : ¬NoOutput p x ↔ SomeOutput p x

theorem MonadAttach.someOutput_iff_not_noOutput {m : Type u → Type v} {α : Type u} [MonadAttach m] (p : α → Prop) (x : m α) : SomeOutput p x ↔ ¬NoOutput p x

theorem MonadAttach.noOutput_iff_allOutputs_not {m : Type u → Type v} {α : Type u} [MonadAttach m] (p : α → Prop) (x : m α) : NoOutput p x ↔ AllOutputs (fun (a : α) => ¬p a) x

Disjunction, conjunction, and monotonicity in the computation

allOutputs_and was already available; these complete the square. Note the directions: the demonic judgment distributes over ∧ and only absorbs ∨, and the angelic one is the mirror image.

theorem MonadAttach.someOutput_or {m : Type u → Type v} {α : Type u} [MonadAttach m] (p q : α → Prop) (x : m α) : SomeOutput (fun (a : α) => p a ∨ q a) x ↔ SomeOutput p x ∨ SomeOutput q x

theorem MonadAttach.allOutputs_or_of_left {m : Type u → Type v} {α : Type u} [MonadAttach m] {p q : α → Prop} {x : m α} (h : AllOutputs p x) : AllOutputs (fun (a : α) => p a ∨ q a) x

theorem MonadAttach.someOutput_and_left {m : Type u → Type v} {α : Type u} [MonadAttach m] {p q : α → Prop} {x : m α} (h : SomeOutput (fun (a : α) => p a ∧ q a) x) : SomeOutput p x

theorem MonadAttach.allOutputs_of_support_subset {m : Type u → Type v} {α : Type u} [MonadAttach m] {p : α → Prop} {x y : m α} (hsub : support x ⊆ support y) (h : AllOutputs p y) : AllOutputs p x

Monotonicity in the computation, not the predicate: a demonic obligation transfers to anything with a smaller support. allOutputs_mono varies only the predicate.

theorem MonadAttach.someOutput_of_support_subset {m : Type u → Type v} {α : Type u} [MonadAttach m] {p : α → Prop} {x y : m α} (hsub : support x ⊆ support y) (h : SomeOutput p x) : SomeOutput p y

@[simp]

theorem MonadAttach.allOutputs_true {m : Type u → Type v} {α : Type u} [MonadAttach m] (x : m α) : AllOutputs (fun (x : α) => True) x

@[simp]

theorem MonadAttach.someOutput_false_iff {m : Type u → Type v} {α : Type u} [MonadAttach m] (x : m α) : SomeOutput (fun (x : α) => False) x ↔ False

theorem MonadAttach.allOutputs_congr {m : Type u → Type v} {α : Type u} [MonadAttach m] {p q : α → Prop} (h : ∀ (a : α), p a ↔ q a) (x : m α) : AllOutputs p x ↔ AllOutputs q x

theorem MonadAttach.someOutput_congr {m : Type u → Type v} {α : Type u} [MonadAttach m] {p q : α → Prop} (h : ∀ (a : α), p a ↔ q a) (x : m α) : SomeOutput p x ↔ SomeOutput q x

@[simp]

theorem MonadAttach.allOutputs_pure {m : Type u → Type v} {α : Type u} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] (p : α → Prop) (a : α) : AllOutputs p (pure a) ↔ p a

@[simp]

theorem MonadAttach.allOutputs_bind {m : Type u → Type v} {α β : Type u} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] (p : β → Prop) (x : m α) (f : α → m β) : AllOutputs p (x >>= f) ↔ ∀ a ∈ support x, AllOutputs p (f a)

@[simp]

theorem MonadAttach.allOutputs_map {m : Type u → Type v} {α β : Type u} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] (p : β → Prop) (f : α → β) (x : m α) : AllOutputs p (f <$> x) ↔ AllOutputs (p ∘ f) x

Mapping the returned value pulls an output assertion back along that map.

@[simp]

theorem MonadAttach.someOutput_pure {m : Type u → Type v} {α : Type u} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] (p : α → Prop) (a : α) : SomeOutput p (pure a) ↔ p a

@[simp]

theorem MonadAttach.someOutput_bind {m : Type u → Type v} {α β : Type u} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] (p : β → Prop) (x : m α) (f : α → m β) : SomeOutput p (x >>= f) ↔ ∃ a ∈ support x, SomeOutput p (f a)

@[simp]

theorem MonadAttach.noOutput_pure {m : Type u → Type v} {α : Type u} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] (p : α → Prop) (a : α) : NoOutput p (pure a) ↔ ¬p a

@[simp]

theorem MonadAttach.noOutput_bind {m : Type u → Type v} {α β : Type u} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] (p : β → Prop) (x : m α) (f : α → m β) : NoOutput p (x >>= f) ↔ ∀ a ∈ support x, NoOutput p (f a)

Induced ordered monad algebras on Prop

AllOutputs is the demonic Prop-carrier ordered monad algebra: its induced MAlgOrdered.wp is the support-based weakest precondition, and the trivial-precondition triple is exactly the "always" judgment. The angelic companion built from SomeOutput is provided as a plain definition rather than an instance, since the two share an instance head.

@[instance_reducible]

def MonadAttach.mAlgOrderedPropDemonic {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] : MAlgOrdered m Prop

The demonic Prop-carrier ordered monad algebra of a monad with exact support: μ asserts that every possible output is a true proposition. This is deliberately not a global instance: for example, the existing OptionT algebra interprets none as ⊥, whereas exact-support partial correctness interprets its empty support vacuously. Install this definition locally when support semantics is intended.

theorem MonadAttach.wp_iff_forall_support {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] {α : Type} (x : m α) (post : α → Prop) : MAlgOrdered.wp x post ↔ ∀ a ∈ support x, post a

Support-based characterization of the demonic Prop-valued weakest precondition.

theorem MonadAttach.wp_iff_allOutputs {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] {α : Type} (x : m α) (post : α → Prop) : MAlgOrdered.wp x post ↔ AllOutputs post x

The demonic Prop-valued weakest precondition is the "always" judgment.

theorem MonadAttach.triple_top_iff_allOutputs {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] {α : Type} (x : m α) (post : α → Prop) : MAlgOrdered.Triple ⊤ x post ↔ AllOutputs post x

The trivial-precondition Prop-valued triple is exactly the "always" judgment: ⊤-precondition triples assert that every possible output satisfies post.

theorem MonadAttach.triple_top_not_iff_noOutput {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] {α : Type} (x : m α) (post : α → Prop) : (MAlgOrdered.Triple ⊤ x fun (a : α) => ¬post a) ↔ NoOutput post x

The trivial-precondition Prop-valued triple against a negated postcondition is exactly the "never" judgment.

@[instance_reducible]

def MonadAttach.mAlgOrderedPropAngelic {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] : MAlgOrdered m Prop

The angelic Prop-carrier ordered monad algebra: μ asserts that some possible output is a true proposition. Not an instance — it shares an instance head with the demonic mAlgOrderedPropDemonic.

theorem MonadAttach.wp_angelic_iff_exists_support {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] {α : Type} (x : m α) (post : α → Prop) : MAlgOrdered.wp x post ↔ ∃ a ∈ support x, post a

Support-based characterization of the angelic Prop-valued weakest precondition — the mirror of wp_iff_forall_support.

theorem MonadAttach.wp_angelic_iff_someOutput {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] {α : Type} (x : m α) (post : α → Prop) : MAlgOrdered.wp x post ↔ SomeOutput post x

The angelic Prop-valued weakest precondition is the "sometimes" judgment.

theorem MonadAttach.triple_top_iff_someOutput {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] {α : Type} (x : m α) (post : α → Prop) : MAlgOrdered.Triple ⊤ x post ↔ SomeOutput post x

The trivial-precondition angelic triple is exactly the "sometimes" judgment — the mirror of triple_top_iff_allOutputs.

theorem MonadAttach.triple_top_not_iff_not_allOutputs {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] {α : Type} (x : m α) (post : α → Prop) : (MAlgOrdered.Triple ⊤ x fun (a : α) => ¬post a) ↔ ¬AllOutputs post x

Against a negated postcondition the angelic triple says that the demonic guarantee does not hold.