Writer Monad Transformer Utilities

This file extends WriterT with helper lemmas and the additive wrapper AddWriterT.

The first half of the file collects basic WriterT run, bind, and lifting lemmas, together with the LawfulAppend class used to build lawful WriterT instances over append-like logs.

The second half specializes WriterT to additive cost accumulation via Multiplicative, and introduces predicates and notation for reasoning about outputs and accumulated costs.

class LawfulAppend (α : Type u) [EmptyCollection α] [Append α] : Prop

Typeclass for instances where ∅ is an identity for ++.

• empty_append (x : α) : ∅ ++ x = x
• append_empty (x : α) : x ++ ∅ = x
• append_assoc (x y z : α) : x ++ (y ++ z) = x ++ y ++ z

instance LawfulAppend.instLawfulMonadWriterT {M : Type u → Type v} {ω : Type u} [Monad M] [EmptyCollection ω] [Append ω] [LawfulAppend ω] [LawfulMonad M] : LawfulMonad (WriterT ω M)

instance LawfulAppend.instList (α : Type u) : LawfulAppend (List α)

@[simp]

theorem WriterT.run_monadLift {m : Type u → Type v} [Monad m] {ω α : Type u} [Monoid ω] (x : m α) : (monadLift x).run = (fun (x : α) => (x, 1)) <$> x

theorem WriterT.liftM_def {m : Type u → Type v} [Monad m] {ω α : Type u} [Monoid ω] (x : m α) : liftM x = WriterT.mk ((fun (x : α) => (x, 1)) <$> x)

theorem WriterT.monadLift_def {m : Type u → Type v} [Monad m] {ω α : Type u} [Monoid ω] (x : m α) : MonadLift.monadLift x = WriterT.mk ((fun (x : α) => (x, 1)) <$> x)

theorem WriterT.bind_def {m : Type u → Type v} [Monad m] {ω α β : Type u} [Monoid ω] (x : WriterT ω m α) (f : α → WriterT ω m β) : x >>= f = WriterT.mk do let x ← x.run match x with | (a, w₁) => (Prod.map id fun (x : ω) => w₁ * x) <$> f a

@[simp]

theorem WriterT.run_seqLeft {m : Type u → Type v} [Monad m] {ω : Type u} [Monoid ω] {α β : Type u} (x : WriterT ω m α) (y : WriterT ω m β) : (x *> y).run = do let z ← x.run (Prod.map id fun (x : ω) => z.snd * x) <$> y.run

@[simp]

theorem WriterT.run_monadLift' {m : Type u → Type v} [Monad m] {ω α : Type u} [EmptyCollection ω] (x : m α) : (monadLift x).run = (fun (x : α) => (x, ∅)) <$> x

theorem WriterT.liftM_def' {m : Type u → Type v} [Monad m] {ω α : Type u} [EmptyCollection ω] (x : m α) : liftM x = WriterT.mk ((fun (x : α) => (x, ∅)) <$> x)

theorem WriterT.monadLift_def' {m : Type u → Type v} [Monad m] {ω α : Type u} [EmptyCollection ω] (x : m α) : MonadLift.monadLift x = WriterT.mk ((fun (x : α) => (x, ∅)) <$> x)

theorem WriterT.bind_def' {m : Type u → Type v} [Monad m] {ω α β : Type u} [EmptyCollection ω] [Append ω] (x : WriterT ω m α) (f : α → WriterT ω m β) : x >>= f = WriterT.mk do let x ← x.run match x with | (a, w₁) => (Prod.map id fun (x : ω) => w₁ ++ x) <$> f a

@[simp]

theorem WriterT.run_pure' {m : Type u → Type v} [Monad m] {ω α : Type u} [EmptyCollection ω] [Append ω] [LawfulMonad m] (x : α) : (pure x).run = pure (x, ∅)

@[simp]

theorem WriterT.run_bind' {m : Type u → Type v} [Monad m] {ω α β : Type u} [EmptyCollection ω] [Append ω] [LawfulMonad m] (x : WriterT ω m α) (f : α → WriterT ω m β) : (x >>= f).run = do let x ← x.run match x with | (a, w₁) => (Prod.map id fun (x : ω) => w₁ ++ x) <$> (f a).run

@[simp]

theorem WriterT.run_seqLeft' {m : Type u → Type v} [Monad m] {ω : Type u} [Monoid ω] {α β : Type u} (x : WriterT ω m α) (y : WriterT ω m β) : (x *> y).run = do let z ← x.run (Prod.map id fun (x : ω) => z.snd * x) <$> y.run

@[simp]

theorem WriterT.run_map' {m : Type u → Type v} [Monad m] {ω α β : Type u} [EmptyCollection ω] [Append ω] (x : WriterT ω m α) (f : α → β) : (f <$> x).run = Prod.map f id <$> x.run

@[inline]

def WriterT.orElse {m : Type u → Type v} [AlternativeMonad m] {ω α : Type u} (x₁ : WriterT ω m α) (x₂ : Unit → WriterT ω m α) : WriterT ω m α

@[inline]

def WriterT.failure {m : Type u → Type v} [AlternativeMonad m] {ω α : Type u} : WriterT ω m α

@[implicit_reducible]

instance WriterT.instAlternativeMonadOfMonoid_toMathlib {m : Type u → Type v} [AlternativeMonad m] {ω : Type u} [Monoid ω] : AlternativeMonad (WriterT ω m)

@[simp]

theorem WriterT.run_failure {m : Type u → Type v} [AlternativeMonad m] {ω : Type u} [Monoid ω] {α : Type u} : failure.run = failure

instance WriterT.instLawfulMonadLiftOfLawfulMonad_toMathlib {m : Type u → Type v} [AlternativeMonad m] {ω : Type u} [Monoid ω] [LawfulMonad m] : LawfulMonadLift m (WriterT ω m)

AddWriterT: Additive Writer Monad Transformer

@[reducible, inline]

abbrev AddWriterT (ω : Type u) (M : Type u → Type v) (α : Type u) : Type v

Writer monad transformer with additive cost accumulation. Defined as WriterT (Multiplicative ω) M, which uses Monoid (Multiplicative ω) (derived from AddMonoid ω) so that tell accumulates via + with identity 0.

The types Multiplicative ω and ω are definitionally equal (Multiplicative is a plain def, not a structure), so no runtime wrapping occurs.

def AddWriterT.outputs {ω : Type u} {M : Type u → Type v} [Monad M] {α : Type u} (oa : AddWriterT ω M α) : M α

Forget the additive cost log and keep only the outputs of an AddWriterT computation.

def AddWriterT.costs {ω : Type u} {M : Type u → Type v} [Monad M] {α : Type u} (oa : AddWriterT ω M α) : M ω

Observe only the accumulated additive cost of an AddWriterT computation.

def AddWriterT.addTell {ω : Type u} {M : Type u → Type v} [Monad M] [AddMonoid ω] (w : ω) : AddWriterT ω M PUnit

Record an additive cost w in the writer log.

@[simp]

theorem AddWriterT.outputs_def {ω : Type u} {M : Type u → Type v} [Monad M] {α : Type u} (oa : AddWriterT ω M α) : oa.outputs = Prod.fst <$> WriterT.run oa

@[simp]

theorem AddWriterT.costs_def {ω : Type u} {M : Type u → Type v} [Monad M] {α : Type u} (oa : AddWriterT ω M α) : oa.costs = (fun (z : α × Multiplicative ω) => Multiplicative.toAdd z.snd) <$> WriterT.run oa

@[simp]

theorem AddWriterT.run_addTell {ω : Type u} {M : Type u → Type v} [Monad M] [AddMonoid ω] (w : ω) : WriterT.run (addTell w) = pure (PUnit.unit, Multiplicative.ofAdd w)

@[simp]

theorem AddWriterT.outputs_addTell {ω : Type u} {M : Type u → Type v} [Monad M] [AddMonoid ω] [LawfulMonad M] (w : ω) : (addTell w).outputs = pure PUnit.unit

@[simp]

theorem AddWriterT.costs_addTell {ω : Type u} {M : Type u → Type v} [Monad M] [AddMonoid ω] [LawfulMonad M] (w : ω) : (addTell w).costs = pure w

def AddWriterT.CostsAs {ω : Type u} {M : Type u → Type v} [Monad M] {α : Type u} (oa : AddWriterT ω M α) (f : α → ω) : Prop

CostsAs oa f means that the accumulated cost of oa is determined by its output via the function f.

Concretely, whenever oa produces output a, the recorded cost is exactly f a. This is a strong structural property: it can fail when the same output can be reached by different execution paths carrying different costs.

def AddWriterT.HasCost {ω : Type u} {M : Type u → Type v} [Monad M] {α : Type u} (oa : AddWriterT ω M α) (w : ω) : Prop

HasCost oa w means that every execution path of oa incurs the constant cost w.

def AddWriterT.OutputCostAtMost {ω : Type u} {M : Type u → Type v} [Monad M] {α : Type u} [Preorder ω] (oa : AddWriterT ω M α) (w : ω) : Prop

OutputCostAtMost oa w means that oa admits an output-indexed cost description bounded above by the constant w.

Concretely, there is some function f : α → ω such that every execution producing output a accumulates cost f a, and each such f a is at most w. This is stronger than a merely pathwise upper bound when the same output can be reached with different costs.

def AddWriterT.OutputCostAtLeast {ω : Type u} {M : Type u → Type v} [Monad M] {α : Type u} [Preorder ω] (oa : AddWriterT ω M α) (w : ω) : Prop

OutputCostAtLeast oa w means that oa admits an output-indexed cost description bounded below by the constant w.

As with [AddWriterT.OutputCostAtMost], this packages a cost function determined by the final output, not just an arbitrary pathwise lower bound.

def AddWriterT.«termCost[_]=_» : Lean.ParserDescr

Cost[ oa ] = w means that the AddWriterT computation oa incurs the same additive cost w on every execution path.

This is notation for [AddWriterT.HasCost]. It is intended for theorem statements where the constant-cost reading is more natural than the underlying output-indexed formulation [AddWriterT.CostsAs].

def AddWriterT.«termOutputCost[_]≤_» : Lean.ParserDescr

OutputCost[ oa ] ≤ w means that oa admits an output-indexed additive-cost bound by w.

This is notation for [AddWriterT.OutputCostAtMost]. It is best used when cost is already known to be determined by the final output, or when that stronger formulation is useful in a proof.

def AddWriterT.«termOutputCost[_]≥_» : Lean.ParserDescr

OutputCost[ oa ] ≥ w means that oa admits an output-indexed additive-cost lower bound by w.

This is notation for [AddWriterT.OutputCostAtLeast]. As with [OutputCost[ oa ] ≤ w], it is formulated in terms of an output-indexed cost witness rather than arbitrary execution paths.

@[simp]

theorem AddWriterT.costsAs_iff {ω : Type u} {M : Type u → Type v} [Monad M] {α : Type u} (oa : AddWriterT ω M α) (f : α → ω) : oa.CostsAs f ↔ oa.costs = f <$> oa.outputs

@[simp]

theorem AddWriterT.hasCost_iff {ω : Type u} {M : Type u → Type v} [Monad M] {α : Type u} (oa : AddWriterT ω M α) (w : ω) : oa.HasCost w ↔ oa.costs = (fun (x : α) => w) <$> oa.outputs

@[simp]

theorem AddWriterT.outputCostAtMost_iff {ω : Type u} {M : Type u → Type v} [Monad M] {α : Type u} [Preorder ω] (oa : AddWriterT ω M α) (w : ω) : oa.OutputCostAtMost w ↔ ∃ (f : α → ω), oa.CostsAs f ∧ ∀ (a : α), f a ≤ w

@[simp]

theorem AddWriterT.outputCostAtLeast_iff {ω : Type u} {M : Type u → Type v} [Monad M] {α : Type u} [Preorder ω] (oa : AddWriterT ω M α) (w : ω) : oa.OutputCostAtLeast w ↔ ∃ (f : α → ω), oa.CostsAs f ∧ ∀ (a : α), w ≤ f a

theorem AddWriterT.outputCostAtMost_of_hasCost {ω : Type u} {M : Type u → Type v} [Monad M] {α : Type u} [Preorder ω] {oa : AddWriterT ω M α} {w b : ω} (h : oa.HasCost w) (hwb : w ≤ b) : oa.OutputCostAtMost b

theorem AddWriterT.outputCostAtLeast_of_hasCost {ω : Type u} {M : Type u → Type v} [Monad M] {α : Type u} [Preorder ω] {oa : AddWriterT ω M α} {w b : ω} (h : oa.HasCost w) (hbw : b ≤ w) : oa.OutputCostAtLeast b