Internal.Ensures and Internal.MayReturn

Internal.Ensures p x characterizes the postconditions of a monadic action x: it holds iff every value returned by x satisfies p. The witness is a Subtype-refined action y : m {a // p a} that is bind-faithful w.r.t. x.

Internal.MayReturn x a is the strongest postcondition of x evaluated at a: a is in every postcondition of x ↔ a is reachable as a value of x.

structure Std.Do.Internal.ErasesTo {α : Type u} {m : Type u → Type v} [Bind m] {P : α → Prop} (x : m { b : α // P b }) (y : m α) : Prop

{lean}ErasesTo x y says the property-tagged {name}x is bind-faithful to {name}y: binding {name}x and forgetting the property agrees with binding {name}y.

• bind_eq {β : Type u} (k : α → m β) : (do let a ← x k a.val) = y >>= k

  The bind-faithful equation: binding x and projecting agrees with binding y.

structure Std.Do.Internal.Ensures {m : Type u → Type v} [Bind m] {α : Type u} (P : α → Prop) (x : m α) : Prop

Ensures p x says every value returned by x satisfies p. The witness is a Subtype-refined monadic action that is bind-faithful w.r.t. x.

• exists_refinement : ∃ (y : m { a : α // P a }), ErasesTo y x

  A P-tagged refinement of x exists.

structure Std.Do.Internal.MayReturn {m : Type u → Type v} [Bind m] {α : Type u} (x : m α) (a : α) : Prop

MayReturn x a says a is in every postcondition of x, equivalently that a is a value returnable from x. (The strongest postcondition, evaluated at a.)

• imp {P : α → Prop} : Ensures P x → P a

  Apply a MayReturn witness to an Ensures proof to extract the postcondition at a.

structure Std.Do.Internal.IsAttach {m : Type u → Type v} [Bind m] (attach : ⦃α : Type u⦄ → (x : m α) → m { a : α // MayReturn x a }) : Prop

IsAttach attach says attach tags each value of x with its MayReturn proof in a bind-faithful way.

• erases {α : Type u} (x : m α) : ErasesTo (attach x) x

  For each x, the attached version is bind-faithful with x.