TimeM: Time Complexity Monad

TimeM α represents a computation that produces a value of type α and tracks its time cost.

Design Principles

1. Pure inputs, timed outputs: Functions take plain values and return TimeM results
2. Time annotations are trusted: The time field is NOT verified against actual cost. You must manually ensure annotations match the algorithm's complexity in your cost model.
3. Separation of concerns: Prove correctness properties on .ret, prove complexity on .time

Cost Model

Document your cost model explicitly Decide and be consistent about:

• What costs 1 unit? (comparison, arithmetic operation, etc.)
• What is free? (variable lookup, pattern matching, etc.)
• Recursive calls: Do you charge for the call itself?

Notation

• ✓ : A tick of time, see tick.
• ⟪tm⟫ : Extract the pure value from a TimeM computation (notation for tm.ret)

References

See [Danielsson2008] for the discussion.

structure Cslib.Algorithms.Lean.TimeM (α : Type u_1) : Type u_1

A monad for tracking time complexity of computations. TimeM α represents a computation that returns a value of type α and accumulates a time cost (represented as a natural number).

• ret : α

  The return value of the computation

• time : ℕ

  The accumulated time cost of the computation

theorem Cslib.Algorithms.Lean.TimeM.ext {α : Type u_1} {x y : TimeM α} (ret : x.ret = y.ret) (time : x.time = y.time) : x = y

theorem Cslib.Algorithms.Lean.TimeM.ext_iff {α : Type u_1} {x y : TimeM α} : x = y ↔ x.ret = y.ret ∧ x.time = y.time

def Cslib.Algorithms.Lean.TimeM.pure {α : Type u_1} (a : α) : TimeM α

Lifts a pure value into a TimeM computation with zero time cost.

Prefer to use pure instead of TimeM.pure.

Equations

• Cslib.Algorithms.Lean.TimeM.pure a = { ret := a, time := 0 }

def Cslib.Algorithms.Lean.TimeM.bind {α : Type u_1} {β : Type u_2} (m : TimeM α) (f : α → TimeM β) : TimeM β

Sequentially composes two TimeM computations, summing their time costs.

Prefer to use the >>= notation.

Equations

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

instance Cslib.Algorithms.Lean.TimeM.instMonad : Monad TimeM

Equations

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

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.ret_pure {α : Type u_1} (a : α) : (pure a).ret = a

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.ret_bind {α β : Type u_1} (m : TimeM α) (f : α → TimeM β) : (m >>= f).ret = (f m.ret).ret

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.ret_map {α β : Type u_1} (f : α → β) (x : TimeM α) : (f <$> x).ret = f x.ret

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.ret_seqRight {α : Type u_1} (x y : TimeM α) : (x *> y).ret = y.ret

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.ret_seqLeft {α : Type u_1} (x y : TimeM α) : (x <* y).ret = x.ret

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.ret_seq {α β : Type u_1} (f : TimeM (α → β)) (x : TimeM α) : (f <*> x).ret = f.ret x.ret

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.time_bind {α β : Type u_1} (m : TimeM α) (f : α → TimeM β) : (m >>= f).time = m.time + (f m.ret).time

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.time_pure {α : Type u_1} (a : α) : (pure a).time = 0

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.time_map {α β : Type u_1} (f : α → β) (x : TimeM α) : (f <$> x).time = x.time

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.time_seqRight {α : Type u_1} (x y : TimeM α) : (x *> y).time = x.time + y.time

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.time_seqLeft {α : Type u_1} (x y : TimeM α) : (x <* y).time = x.time + y.time

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.time_seq {α β : Type u_1} (f : TimeM (α → β)) (x : TimeM α) : (f <*> x).time = f.time + x.time

instance Cslib.Algorithms.Lean.TimeM.instLawfulMonad : LawfulMonad TimeM

def Cslib.Algorithms.Lean.TimeM.tick (c : ℕ := 1) : TimeM PUnit.{u_1 + 1}

Creates a TimeM computation with a time cost. The time cost defaults to 1 if not provided.

Equations

• Cslib.Algorithms.Lean.TimeM.tick c = { ret := PUnit.unit, time := c }

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.ret_tick (c : ℕ) : (tick c).ret = ()

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.time_tick (c : ℕ) : (tick c).time = c

def Cslib.Algorithms.Lean.TimeM.«doElem✓[_]_» : Lean.ParserDescr

✓[c] x adds c ticks, then executes x.

Equations

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

def Cslib.Algorithms.Lean.TimeM.«doElem✓_» : Lean.ParserDescr

✓ x is a shorthand for ✓[1] x, which adds one tick and executes x.

Equations

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

def Cslib.Algorithms.Lean.TimeM.«term⟪_⟫» : Lean.ParserDescr

Notation for extracting the return value from a TimeM computation: ⟪tm⟫

Equations

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