Exact Support of the Free Monad

The free monad FreeM P carries a canonical MonadAttach instance: the possible outputs of a program are the leaf payloads reachable by choosing some direction at every operation node,

• supp (pure x) = {x},
• supp (liftBind a r) = ⋃ b, supp (r b),

and attach decorates each leaf with its reachability proof by structural recursion. Both are computable and axiom-free, so MonadAttach.pbind is available for well-founded recursion over free programs.

The instance is lawful, and structural induction also proves the pure and bind introduction rules of ExactMonadAttach. MonadAttach.support on FreeM P reduces definitionally — support (pure x) = {x} and support (liftBind a r) = ⋃ b, support (r b) are both rfl — and the judgments AllOutputs/SomeOutput/NoOutput recurse structurally over trees.

Two coherence results connect this to the rest of the library: support_eq_range_output identifies the support with the range of FreeM.output over the canonical FreeM.Path type, and support_eq_liftM_univ identifies it with the fold of the "every response possible" handler into the powerset monad.

def PFunctor.FreeM.supp {P : PFunctor.{uA, uB}} {α : Type v} : P.FreeM α → Set α

The structural support of a free tree: every direction of every operation node is possible.

theorem PFunctor.FreeM.mem_supp_liftBind_of_mem {P : PFunctor.{uA, uB}} {α : Type v} {op : P.A} {r : P.B op → P.FreeM α} {b : P.B op} {a : α} (h : a ∈ (r b).supp) : a ∈ (liftBind op r).supp

Reachability at a child is reachability at the node.

def PFunctor.FreeM.attachSupp {P : PFunctor.{uA, uB}} {α : Type v} (x : P.FreeM α) : P.FreeM { a : α // a ∈ x.supp }

Attach the structural-support proof to every leaf, by structural recursion.

@[instance_reducible]

instance PFunctor.FreeM.instMonadAttach {P : PFunctor.{uA, uB}} : MonadAttach P.FreeM

theorem PFunctor.FreeM.supp_map {P : PFunctor.{uA, uB}} {α : Type v} {Q : α → Prop} (x : P.FreeM { a : α // Q a }) {b : α} : b ∈ (Subtype.val <$> x).supp → Q b

The structural support is the strongest postcondition: anything reachable in a tree of refined values satisfies the refinement.

theorem PFunctor.FreeM.map_attachSupp {P : PFunctor.{uA, uB}} {α : Type v} (x : P.FreeM α) : Subtype.val <$> x.attachSupp = x

instance PFunctor.FreeM.instExactMonadAttach {P : PFunctor.{uA, uB}} : ExactMonadAttach P.FreeM

Structural equations

MonadAttach.support on FreeM P unfolds to supp, so the leaf and node equations hold by rfl.

theorem PFunctor.FreeM.support_eq_supp {P : PFunctor.{uA, uB}} {α : Type v} (x : P.FreeM α) : MonadAttach.support x = x.supp

@[simp]

theorem PFunctor.FreeM.support_pure' {P : PFunctor.{uA, uB}} {α : Type v} (a : α) : MonadAttach.support (pure a) = {a}

theorem PFunctor.FreeM.support_liftBind {P : PFunctor.{uA, uB}} {α : Type v} (a : P.A) (r : P.B a → P.FreeM α) : MonadAttach.support (liftBind a r) = ⋃ (b : P.B a), MonadAttach.support (r b)

@[simp]

theorem PFunctor.FreeM.support_lift {P : PFunctor.{uA, uB}} (a : P.A) : MonadAttach.support (lift a) = Set.univ

theorem PFunctor.FreeM.mem_support_liftBind {P : PFunctor.{uA, uB}} {α : Type v} {a : P.A} {r : P.B a → P.FreeM α} {c : α} : c ∈ MonadAttach.support (liftBind a r) ↔ ∃ (b : P.B a), c ∈ MonadAttach.support (r b)

@[simp]

theorem PFunctor.FreeM.support_lift_bind {P : PFunctor.{uA, uB}} {α : Type v} (a : P.A) (r : P.B a → P.FreeM α) : MonadAttach.support ((lift a).bind r) = ⋃ (b : P.B a), MonadAttach.support (r b)

A primitive operation followed by a continuation can return any child output.

@[simp]

theorem PFunctor.FreeM.support_map {P : PFunctor.{uA, uB}} {γ : Type v} {δ : Type w} (f : γ → δ) (program : P.FreeM γ) : MonadAttach.support (map f program) = f '' MonadAttach.support program

Mapping a free tree maps its reachable leaves, independently of result universes.

@[simp]

theorem PFunctor.FreeM.support_liftObj {P : PFunctor.{uA, uB}} {α : Type v} (object : ↑P α) : MonadAttach.support (liftObj object) = Set.range object.snd

An operation object can return exactly the outputs of its continuation.

theorem PFunctor.FreeM.support_nonempty {P : PFunctor.{uA, uB}} {α : Type v} [∀ (a : P.A), Nonempty (P.B a)] (program : P.FreeM α) : (MonadAttach.support program).Nonempty

A free program has a possible return when every operation has an answer.

@[simp]

theorem PFunctor.FreeM.support_finite {P : PFunctor.{uA, uB}} {α : Type v} [∀ (a : P.A), Finite (P.B a)] (program : P.FreeM α) : (MonadAttach.support program).Finite

A free program has finitely many possible returns when every answer type is finite.

Structural recursion for the satisfaction judgments

theorem PFunctor.FreeM.allOutputs_liftBind {P : PFunctor.{uA, uB}} {α : Type v} (p : α → Prop) (a : P.A) (r : P.B a → P.FreeM α) : MonadAttach.AllOutputs p (liftBind a r) ↔ ∀ (b : P.B a), MonadAttach.AllOutputs p (r b)

theorem PFunctor.FreeM.someOutput_liftBind {P : PFunctor.{uA, uB}} {α : Type v} (p : α → Prop) (a : P.A) (r : P.B a → P.FreeM α) : MonadAttach.SomeOutput p (liftBind a r) ↔ ∃ (b : P.B a), MonadAttach.SomeOutput p (r b)

@[simp]

theorem PFunctor.FreeM.allOutputs_lift {P : PFunctor.{uA, uB}} (a : P.A) (p : P.B a → Prop) : MonadAttach.AllOutputs p (lift a) ↔ ∀ (b : P.B a), p b

@[simp]

theorem PFunctor.FreeM.someOutput_lift {P : PFunctor.{uA, uB}} (a : P.A) (p : P.B a → Prop) : MonadAttach.SomeOutput p (lift a) ↔ ∃ (b : P.B a), p b

theorem PFunctor.FreeM.noOutput_liftBind {P : PFunctor.{uA, uB}} {α : Type v} (p : α → Prop) (a : P.A) (r : P.B a → P.FreeM α) : MonadAttach.NoOutput p (liftBind a r) ↔ ∀ (b : P.B a), MonadAttach.NoOutput p (r b)

Coherence with paths and with the powerset fold

theorem PFunctor.FreeM.support_eq_range_output {P : PFunctor.{uA, uB}} {α : Type v} (s : P.FreeM α) : MonadAttach.support s = Set.range s.output

The support is exactly the set of leaf payloads reachable along a canonical root-to-leaf path.

theorem PFunctor.FreeM.support_eq_liftM_univ {P : PFunctor.{uA, uB}} {γ : Type uB} (x : P.FreeM γ) : MonadAttach.support x = (FreeM.liftM (fun (x : P.A) => Set.univ) x).run

The support is the powerset-monad interpretation of the "every response possible" handler — the shape a support-as-fold presentation expects.

theorem PFunctor.FreeM.allOutputs_iff_forall_path {P : PFunctor.{uA, uB}} {α : Type v} (p : α → Prop) (s : P.FreeM α) : MonadAttach.AllOutputs p s ↔ ∀ (path : s.Path), p (s.output path)

Every possible output is witnessed by a path, and conversely.

theorem PFunctor.FreeM.someOutput_iff_exists_path {P : PFunctor.{uA, uB}} {α : Type v} (p : α → Prop) (s : P.FreeM α) : MonadAttach.SomeOutput p s ↔ ∃ (path : s.Path), p (s.output path)

Some possible output is witnessed by a path, and conversely.