EconCSLib.Foundation.CostM

CostM C A is the writer monad over an arbitrary additive monoid C: a value of type A together with an accumulated cost in C. Sequential composition (>>=) adds the cost components via the monoid operation.

Design

The cost type C is deliberately abstract. Picking C is what selects which resource is being measured; the monad itself is the same for all of them.

• C := ℕ — count comparisons, recursive calls, or any single additive resource. This is the conventional "time complexity" instance.
• C := A × B — track two costs at once. Prod.instAddMonoid makes this automatic; no extra wiring needed.
• C := Finset A with + := (· ∪ ·), 0 := ∅ — track the set of subproblems touched by a recursive algorithm. The monoid is idempotent (s + s = s); this is the algebraic shadow of memoization.
• C := { c : ℕ × ℤ // c.2 ≤ c.1 } (peak/delta) — a non-additive monoid for peak memory. This is the only resource shape that additive cost fundamentally cannot express.

The structure field is cost, not time: time is one cost among many and has no architectural privilege.

This is the standard writer-monad-over-a-monoid pattern; see Danielsson, Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures (POPL 2008).

Discipline

Cost annotations are trusted: the elaborator does not check that tick calls correspond to actual work. Each algorithm file must document its cost model — what counts as a unit, what is free, whether recursive calls are charged — and the author must tick accordingly.

Proofs separate cleanly:

• Functional correctness lives on m.ret (alias ⟪m⟫).
• Complexity bounds live on m.cost.

The two are independent: changing the cost model never disturbs correctness proofs, and refactoring the algorithm preserves cost annotations by construction.

Main definitions

• CostM C A — the monad.
• CostM.pure, CostM.bind, CostM.tick — primitives.
• Monad (CostM C) for [Zero C] [Add C].
• LawfulMonad (CostM C) for [AddMonoid C].
• CostM.par — independent (parallel) composition; cost combined via ⊔. Requires [SemilatticeSup C].
• CostM.Bounded / CostM.IsPolyBounded — bound predicates over [LE C] (and the C = ℕ polynomial specialization).

Notation

• tick c — charge cost c.
• ✓[c] body — sugar for do tick c; body inside a do-block.
• ✓ body — ✓[1] body; requires [OfNat C 1] at the use site.
• implicit coercion (m : A) — a Coe (CostM C A) A instance projects m.ret. Use the .cost field explicitly to get the cost.

Attribution

The monad core of this file is adapted from TimeM in the leanprover/cslib project, file Cslib/Algorithms/Lean/TimeM.lean (Apache License 2.0).

Original authors of TimeM: Sorrachai Yingchareonthawornhcai and Eric Wieser. Original copyright © 2025 Sorrachai Yingchareonthawornhcai.

What is adapted from upstream

• the structure CostM layout (ret, accumulated-cost field) ↔ TimeM (ret, time);
• protected def pure / protected def bind and the matching instance : Pure / Bind / Functor / Seq typeclass instances;
• instance : Monad and instance : LawfulMonad;
• the simp-lemma layout for ret_* / cost_* projections;
• def tick, the ✓[c] body and ✓ body doElem macros;
• the writer-over-additive-monoid design pattern and the Danielsson POPL 2008 reference.

What is added in this file (not upstream as of the pinned commit)

• Generalization of vocabulary from "time" to "cost"; the field is cost, the type parameter is C. This makes room for cost shapes that are not time — set-of-cells-touched (Visited, idempotent monoid), peak / delta memory (Cells, tropical monoid), product costs (work × depth), etc.
• def par (binary parallel composition) and def parList (n-ary parallel composition over List), with cost combined via the semilattice join ⊔; corresponding simp lemmas.
• The complexity-bound predicates Bounded and IsPolyBounded over [LE C] and C = ℕ respectively.
• instance instCoeHead : CoeHead (CostM C A) A projecting m.ret, giving (m : A) shorthand at use sites.
• Companion modules Foundation/CostM/Cells.lean (tropical / peak memory) and Foundation/CostM/Visited.lean (idempotent / footprint).

structure CostM (C : Type u_1) (A : Type u_2) : Type (max u_1 u_2)

Writer monad over an arbitrary additive monoid C.

A CostM C A is a return value of type A together with an accumulated cost in C. The cost field aggregates via + and 0 of C. See the file docstring for the design rationale and for the choices of C that recover specific complexity measures.

• ret : A

  The result of the computation.

• cost : C

  The accumulated cost in C.

theorem CostM.ext {C : Type u_1} {A : Type u_2} {x y : CostM C A} (ret : x.ret = y.ret) (cost : x.cost = y.cost) : x = y

theorem CostM.ext_iff {C : Type u_1} {A : Type u_2} {x y : CostM C A} : x = y ↔ x.ret = y.ret ∧ x.cost = y.cost

def CostM.pure {C : Type u_1} {A : Type u} [Zero C] (a : A) : CostM C A

Lift a pure value at zero cost.

Equations

• CostM.pure a = { ret := a, cost := 0 }

@[implicit_reducible]

instance CostM.instPure {C : Type u_1} [Zero C] : Pure (CostM C)

Equations

• CostM.instPure = { pure := fun {α : Type ?u.13} => CostM.pure }

def CostM.bind {C : Type u_1} {A B : Type u} [Add C] (m : CostM C A) (f : A → CostM C B) : CostM C B

Sequential composition. The cost of m >>= f is m.cost + (f m.ret).cost.

Equations

• m.bind f = { ret := (f m.ret).ret, cost := m.cost + (f m.ret).cost }

@[implicit_reducible]

instance CostM.instBind {C : Type u_1} [Add C] : Bind (CostM C)

Equations

• CostM.instBind = { bind := fun {α β : Type ?u.14} => CostM.bind }

@[implicit_reducible]

instance CostM.instFunctor {C : Type u_1} : Functor (CostM C)

Equations

• CostM.instFunctor = { map := fun {α β : Type ?u.17} (f : α → β) (x : CostM C α) => { ret := f x.ret, cost := x.cost } }

@[implicit_reducible]

instance CostM.instSeq {C : Type u_1} [Add C] : Seq (CostM C)

Equations

• CostM.instSeq = { seq := fun {α β : Type ?u.18} (f : CostM C (α → β)) (x : Unit → CostM C α) => { ret := f.ret (x ()).ret, cost := f.cost + (x ()).cost } }

@[implicit_reducible]

instance CostM.instSeqLeft {C : Type u_1} [Add C] : SeqLeft (CostM C)

Equations

• CostM.instSeqLeft = { seqLeft := fun {α β : Type ?u.17} (x : CostM C α) (y : Unit → CostM C β) => { ret := x.ret, cost := x.cost + (y ()).cost } }

@[implicit_reducible]

instance CostM.instSeqRight {C : Type u_1} [Add C] : SeqRight (CostM C)

Equations

• CostM.instSeqRight = { seqRight := fun {α β : Type ?u.17} (x : CostM C α) (y : Unit → CostM C β) => { ret := (y ()).ret, cost := x.cost + (y ()).cost } }

@[implicit_reducible]

instance CostM.instMonad {C : Type u_1} [Zero C] [Add C] : Monad (CostM C)

Equations

• One or more equations did not get rendered due to their size.

simp lemmas — return component

@[simp]

theorem CostM.ret_pure {C : Type u_1} {A : Type u} [Zero C] (a : A) : (pure a).ret = a

@[simp]

theorem CostM.ret_bind {C : Type u_1} {A B : Type u} [Add C] (m : CostM C A) (f : A → CostM C B) : (m >>= f).ret = (f m.ret).ret

@[simp]

theorem CostM.ret_map {C : Type u_1} {A B : Type u} (f : A → B) (x : CostM C A) : (f <$> x).ret = f x.ret

@[simp]

theorem CostM.ret_seqLeft {C : Type u_1} {A B : Type u} [Add C] (x : CostM C A) (y : Unit → CostM C B) : (x <* y ()).ret = x.ret

@[simp]

theorem CostM.ret_seqRight {C : Type u_1} {A B : Type u} [Add C] (x : CostM C A) (y : Unit → CostM C B) : (x *> y ()).ret = (y ()).ret

@[simp]

theorem CostM.ret_seq {C : Type u_1} {A B : Type u} [Add C] (f : CostM C (A → B)) (x : Unit → CostM C A) : (f <*> x ()).ret = f.ret (x ()).ret

simp lemmas — cost component

@[simp]

theorem CostM.cost_pure {C : Type u_1} {A : Type u} [Zero C] (a : A) : (pure a).cost = 0

@[simp]

theorem CostM.cost_bind {C : Type u_1} {A B : Type u} [Add C] (m : CostM C A) (f : A → CostM C B) : (m >>= f).cost = m.cost + (f m.ret).cost

@[simp]

theorem CostM.cost_map {C : Type u_1} {A B : Type u} (f : A → B) (x : CostM C A) : (f <$> x).cost = x.cost

@[simp]

theorem CostM.cost_seqLeft {C : Type u_1} {A B : Type u} [Add C] (x : CostM C A) (y : Unit → CostM C B) : (x <* y ()).cost = x.cost + (y ()).cost

@[simp]

theorem CostM.cost_seqRight {C : Type u_1} {A B : Type u} [Add C] (x : CostM C A) (y : Unit → CostM C B) : (x *> y ()).cost = x.cost + (y ()).cost

@[simp]

theorem CostM.cost_seq {C : Type u_1} {A B : Type u} [Add C] (f : CostM C (A → B)) (x : Unit → CostM C A) : (f <*> x ()).cost = f.cost + (x ()).cost

instance CostM.instLawfulMonad {C : Type u_1} [AddMonoid C] : LawfulMonad (CostM C)

CostM C is a lawful monad whenever C is an additive monoid.

tick and notation

def CostM.tick {C : Type u_1} (c : C) : CostM C PUnit

Charge a cost of c, returning unit. Use inside a do-block.

Equations

• CostM.tick c = { ret := PUnit.unit, cost := c }

@[simp]

theorem CostM.ret_tick {C : Type u_1} (c : C) : (tick c).ret = ()

@[simp]

theorem CostM.cost_tick {C : Type u_1} (c : C) : (tick c).cost = c

def CostM.«doElem✓[_]_» : Lean.ParserDescr

✓[c] body adds a cost of c and then runs body.

Equations

• One or more equations did not get rendered due to their size.

def CostM.«doElem✓_» : Lean.ParserDescr

✓ body is ✓[1] body. The use site must provide [OfNat C 1].

Equations

• CostM.«doElem✓_» = Lean.ParserDescr.node `CostM.«doElem✓_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "✓") (Lean.ParserDescr.cat `doElem 0))

@[implicit_reducible]

instance CostM.instCoeHead {C : Type u_1} {A : Type u} : CoeHead (CostM C A) A

Coerce a CostM C A to its return value, dropping the cost. Use this in contexts where the expected type is A; pair with .cost for complexity proofs. The pattern mirrors Subtype.val-style projection.

Equations

• CostM.instCoeHead = { coe := CostM.ret }

Parallel composition

par m₁ m₂ runs two independent CostM computations side by side; the cost is combined via ⊔ (sup). This is not a monadic operation — neither operand's value feeds into the other. Use this only when the two sides are data-independent.

The choice of ⊔ for the cost models the "depth" / branch-worst-case view: both branches run concurrently, so the joint cost is the worse of the two. For combined work-and-depth tracking (cost type ℕ × ℕ with + on work and ⊔ on depth), a custom combining function per cost type is required; this file does not provide it.

def CostM.par {C : Type u_1} {A B : Type u} [SemilatticeSup C] (m₁ : CostM C A) (m₂ : CostM C B) : CostM C (A × B)

Independent (parallel) composition of two CostM computations. The return is the pair of return values; the cost is the sup of the two costs.

Equations

• m₁.par m₂ = { ret := (m₁.ret, m₂.ret), cost := m₁.cost ⊔ m₂.cost }

@[simp]

theorem CostM.ret_par {C : Type u_1} {A B : Type u} [SemilatticeSup C] (m₁ : CostM C A) (m₂ : CostM C B) : (m₁.par m₂).ret = (m₁.ret, m₂.ret)

@[simp]

theorem CostM.cost_par {C : Type u_1} {A B : Type u} [SemilatticeSup C] (m₁ : CostM C A) (m₂ : CostM C B) : (m₁.par m₂).cost = m₁.cost ⊔ m₂.cost

N-ary parallel composition

parList ms extends par from a binary combinator to an arbitrary List of operands. All operands run independently (no data dependency between them); returns are collected into a List; costs are combined by the sup-semilattice join (⊔). The empty list has cost ⊥ (= 0 for C = ℕ).

parList requires [OrderBot C] in addition to [SemilatticeSup C] because the empty list needs an identity element for ⊔.

For n independent operations each charging c_i, the joint parallel cost is c_1 ⊔ c_2 ⊔ ⋯ ⊔ c_n (the max for C = ℕ). This corresponds to a flat "fan-out / fan-in" depth-1 schedule with n workers.

def CostM.parList {C : Type u_1} {A : Type u} [SemilatticeSup C] [OrderBot C] (ms : List (CostM C A)) : CostM C (List A)

N-ary parallel composition over a List of independent CostM operands. Returns are paired into a list in the original order; the cost is the sup of all operand costs (or ⊥ for the empty list).

Equations

• CostM.parList ms = { ret := List.map (fun (x : CostM C A) => x.ret) ms, cost := List.foldr (fun (m : CostM C A) (acc : C) => m.cost ⊔ acc) ⊥ ms }

@[simp]

theorem CostM.ret_parList {C : Type u_1} {A : Type u} [SemilatticeSup C] [OrderBot C] (ms : List (CostM C A)) : (parList ms).ret = List.map (fun (x : CostM C A) => x.ret) ms

@[simp]

theorem CostM.cost_parList {C : Type u_1} {A : Type u} [SemilatticeSup C] [OrderBot C] (ms : List (CostM C A)) : (parList ms).cost = List.foldr (fun (m : CostM C A) (acc : C) => m.cost ⊔ acc) ⊥ ms

@[simp]

theorem CostM.parList_nil {C : Type u_1} {A : Type u} [SemilatticeSup C] [OrderBot C] : parList [] = { ret := [], cost := ⊥ }

@[simp]

theorem CostM.cost_parList_cons {C : Type u_1} {A : Type u} [SemilatticeSup C] [OrderBot C] (m : CostM C A) (ms : List (CostM C A)) : (parList (m :: ms)).cost = m.cost ⊔ (parList ms).cost

Complexity bound predicates

Bounded alg size bound says "for every input i, the cost of alg i is at most bound (size i)". The size function reduces the input to a natural number (the conventional complexity-theoretic notion of "input size"). The bound function maps that size to an expected cost in C.

IsPolyBounded specializes to C = ℕ and existentially quantifies over the polynomial coefficient and degree: ∃ c k, cost ≤ c * size^k.

def CostM.Bounded {C : Type u_1} {Input : Type u_2} {Output : Type u_3} [LE C] (alg : Input → CostM C Output) (size : Input → ℕ) (bound : ℕ → C) : Prop

The cost of alg i is bounded by bound (size i) for every input i.

Equations

• CostM.Bounded alg size bound = ∀ (i : Input), (alg i).cost ≤ bound (size i)

def CostM.IsPolyBounded {Input : Type u_2} {Output : Type u_3} (alg : Input → CostM ℕ Output) (size : Input → ℕ) : Prop

Specialization of Bounded for C = ℕ: cost is polynomial in input size.

Equations

• CostM.IsPolyBounded alg size = ∃ (c : ℕ), ∃ (k : ℕ), CostM.Bounded alg size fun (n : ℕ) => c * n ^ k