Exact Support: Instances and Lift Transport

The instance side of the exact-support layer: the MonadLiftT m SetM compatibility shim, transport of the judgments along a lawful monad lift, the MonadAttach / ExactMonadAttach instances for Except, SetM, and Mathlib's WriterT, the exactness instances for Id, Option, OptionT, and ExceptT, and the per-monad CanReturn unfoldings. The judgments and their structural laws live in PolyFun.Control.Monad.Support; the per-run support of StateT and ReaderT lives in PolyFun.Control.Monad.Support.Indexed.

Recovering the MonadLiftT presentation

MonadAttach is the canonical interface for reachability here: it is core's, it carries a lawfulness hierarchy, and core supplies instances for the transformers this library cares about. The MonadLiftT m SetM spelling below is a compatibility shim for a downstream still phrased that way, not the recommended API — register it locally when migrating, rather than building against it.

Two things this does not say. SetM remains perfectly good as a carrier: support : Set α is unchanged, and PFunctor.FreeM.support_eq_liftM_univ — which genuinely folds into SetM as a monad — stays. What is being demoted is the lift as an interface. And unlike the probability layer's PMF retirement, there is no upstream force here: SetM is not being deprecated by Mathlib. This is a project standardizing on core's vocabulary, nothing more.

One concrete argument for the direction, which is otherwise recorded nowhere: support_eq_liftM_univ is restricted to {γ : Type uB}, because FreeM.liftM pins the payload universe to the direction universe. MonadAttach.support on FreeM P carries no such restriction. The attach-based presentation is strictly more universe-polymorphic than the fold.

The two declarations are deliberately not instances, so that support reasoning does not perturb monad-lift instance search.

@[instance_reducible]

def MonadAttach.toMonadLiftT (m : Type u → Type v) [MonadAttach m] : MonadLiftT m SetM

The support map as a monad lift into SetM. Not an instance.

theorem MonadAttach.toLawfulMonadLiftT (m : Type u → Type v) [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] : LawfulMonadLiftT m SetM

The support lift is lawful. Not an instance.

Transport along a monad lift

Core proves the elimination half — lifting cannot create possible outputs — so a lift can only shrink the support, and a demonic obligation therefore transfers along it for free.

The introduction half is not available generically, and cannot be: nothing in MonadLiftT or its lawfulness class says the lift preserves reachability, and a lift into a monad whose CanReturn is uniformly False satisfies every law while losing every output. A caller that needs support (liftM x) = support x must supply that equation for its particular lift; FreeM's powerset fold (PFunctor.FreeM.support_eq_liftM_univ) is the worked instance.

theorem MonadAttach.support_liftM_subset {m : Type u → Type v} {n : Type u → Type w} {α : Type u} [Monad m] [LawfulMonad m] [MonadAttach m] [LawfulMonadAttach m] [Monad n] [LawfulMonad n] [MonadAttach n] [LawfulMonadAttach n] [MonadLiftT m n] [LawfulMonadLiftT m n] (x : m α) : support (liftM x) ⊆ support x

Lifting cannot create possible outputs. The set form of core's LawfulMonadAttach.canReturn_liftM_imp'.

theorem MonadAttach.allOutputs_liftM {m : Type u → Type v} {n : Type u → Type w} {α : Type u} [Monad m] [LawfulMonad m] [MonadAttach m] [LawfulMonadAttach m] [Monad n] [LawfulMonad n] [MonadAttach n] [LawfulMonadAttach n] [MonadLiftT m n] [LawfulMonadLiftT m n] {p : α → Prop} {x : m α} (h : AllOutputs p x) : AllOutputs p (liftM x)

A demonic guarantee survives lifting: the lifted computation has no outputs the original did not have, so a property of all of the original's outputs holds of all of the lift's.

theorem MonadAttach.someOutput_of_someOutput_liftM {m : Type u → Type v} {n : Type u → Type w} {α : Type u} [Monad m] [LawfulMonad m] [MonadAttach m] [LawfulMonadAttach m] [Monad n] [LawfulMonad n] [MonadAttach n] [LawfulMonadAttach n] [MonadLiftT m n] [LawfulMonadLiftT m n] {p : α → Prop} {x : m α} (h : SomeOutput p (liftM x)) : SomeOutput p x

Dually, an angelic fact about the lift transfers back to the original.

theorem MonadAttach.noOutput_liftM {m : Type u → Type v} {n : Type u → Type w} {α : Type u} [Monad m] [LawfulMonad m] [MonadAttach m] [LawfulMonadAttach m] [Monad n] [LawfulMonad n] [MonadAttach n] [LawfulMonadAttach n] [MonadLiftT m n] [LawfulMonadLiftT m n] {p : α → Prop} {x : m α} (h : NoOutput p x) : NoOutput p (liftM x)

And a "never" guarantee survives lifting.

Base instances

Core supplies MonadAttach and LawfulMonadAttach for Id, Option, OptionT, ExceptT, StateT, and ReaderT; only the exactness fields are needed here. Except and SetM have no core instance and are supplied below.

@[instance_reducible]

instance MonadAttach.instMonadAttachExcept {ε : Type u} : MonadAttach (Except ε)

Core provides no MonadAttach (Except ε) at this pin, only the transformer version; this mirrors core's Option instance. An identical declaration has landed upstream and ships in Lean v4.35, so delete this instance and the one below it at that toolchain bump.

instance MonadAttach.instLawfulMonadAttachExcept {ε : Type u} : LawfulMonadAttach (Except ε)

@[instance_reducible]

instance MonadAttach.instMonadAttachExceptT {ε : Type u} {m : Type u → Type v} [Monad m] [MonadAttach m] : MonadAttach (ExceptT ε m)

Core's MonadAttach (ExceptT ε m) is stated at max-joined universes, which blocks synthesis in a universe-polymorphic context; this alias instantiates it at a single universe. Delete once the upstream declaration is repaired.

@[instance_reducible]

instance MonadAttach.instMonadAttachSetM : MonadAttach SetM

The powerset monad is its own support.

instance MonadAttach.instLawfulMonadAttachSetM : LawfulMonadAttach SetM

instance MonadAttach.instExactMonadAttachId : ExactMonadAttach Id

instance MonadAttach.instExactMonadAttachOption : ExactMonadAttach Option

instance MonadAttach.instExactMonadAttachExcept {ε : Type u} : ExactMonadAttach (Except ε)

instance MonadAttach.instExactMonadAttachSetM : ExactMonadAttach SetM

instance MonadAttach.instExactMonadAttachOptionT {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] : ExactMonadAttach (OptionT m)

instance MonadAttach.instExactMonadAttachExceptT {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] {ε : Type u} : ExactMonadAttach (ExceptT ε m)

Per-monad unfoldings

Each base monad's CanReturn is a concrete predicate, so membership in its support has a concrete spelling. Every one of these is Iff.rfl; naming them keeps callers from reaching through support and CanReturn with change.

@[simp]

theorem MonadAttach.Id.canReturn_iff {α : Type u} {x : Id α} {a : α} : CanReturn x a ↔ x.run = a

@[simp]

theorem MonadAttach.Id.support_eq_singleton {α : Type u} (x : Id α) : support x = {x.run}

@[simp]

theorem MonadAttach.Option.canReturn_iff {α : Type u} {x : Option α} {a : α} : CanReturn x a ↔ x = some a

@[simp]

theorem MonadAttach.Option.support_some {α : Type u} (a : α) : support (some a) = {a}

@[simp]

theorem MonadAttach.Option.support_none {α : Type u} : support none = ∅

@[simp]

theorem MonadAttach.Except.canReturn_iff {α ε : Type u} {x : Except ε α} {a : α} : CanReturn x a ↔ x = Except.ok a

@[simp]

theorem MonadAttach.Except.support_ok {α ε : Type u} (a : α) : support (Except.ok a) = {a}

@[simp]

theorem MonadAttach.Except.support_error {α ε : Type u} (e : ε) : support (Except.error e) = ∅

@[simp]

theorem MonadAttach.SetM.canReturn_iff {α : Type u} {x : SetM α} {a : α} : CanReturn x a ↔ a ∈ x.run

@[simp]

theorem MonadAttach.SetM.support_eq_run {α : Type u} (x : SetM α) : support x = x.run

@[simp]

theorem MonadAttach.OptionT.canReturn_iff {α : Type u} {m : Type u → Type v} [Monad m] [MonadAttach m] {x : OptionT m α} {a : α} : CanReturn x a ↔ some a ∈ support x.run

@[simp]

theorem MonadAttach.ExceptT.canReturn_iff {α : Type u} {m : Type u → Type v} [Monad m] [MonadAttach m] {ε : Type u} {x : ExceptT ε m α} {a : α} : CanReturn x a ↔ Except.ok a ∈ support x.run

The writer transformer

WriterT ω m accumulates an output alongside the value, so the honest reading of its support is the one that keeps that output: a value is possible exactly when it is returned together with some accumulator. This is the same rule the measure semantics uses for the same transformer — a writer computation denotes the underlying m (α × ω) rather than discarding ω — and unlike StateT it costs nothing, because there is no input index to choose. Both introduction rules survive: pure writes the unit, and two composable outputs compose with their accumulators multiplied.

@[instance_reducible]

instance MonadAttach.instMonadAttachWriterT {m : Type u → Type v} [Monad m] [MonadAttach m] {ω : Type u} : MonadAttach (WriterT ω m)

theorem MonadAttach.mem_support_writerT_iff {α : Type u} {m : Type u → Type v} [Monad m] [MonadAttach m] {ω : Type u} {x : WriterT ω m α} {a : α} : a ∈ support x ↔ ∃ (w : ω), (a, w) ∈ support x.run

theorem MonadAttach.mem_support_of_run_writerT {α : Type u} {m : Type u → Type v} [Monad m] [MonadAttach m] {ω : Type u} {x : WriterT ω m α} {a : α} {w : ω} (h : (a, w) ∈ support x.run) : a ∈ support x

instance MonadAttach.instWeaklyLawfulMonadAttachWriterT {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] {ω : Type u} [Monoid ω] [WeaklyLawfulMonadAttach m] : WeaklyLawfulMonadAttach (WriterT ω m)

instance MonadAttach.instLawfulMonadAttachWriterT {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] {ω : Type u} [Monoid ω] [LawfulMonadAttach m] : LawfulMonadAttach (WriterT ω m)

instance MonadAttach.instExactMonadAttachWriterT {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] {ω : Type u} [Monoid ω] [ExactMonadAttach m] : ExactMonadAttach (WriterT ω m)

Both introduction rules hold: pure writes the unit accumulator, and composable outputs compose with their accumulators multiplied. This is what StateT cannot have — there is no input index to quantify over, so nothing is flattened away.