Lean declarations

def MemoFib.fibAux EconCSLib @ cef01c7, EconCSLib.Examples.CostM.MemoFib

def fibAux : ℕ → CostM (Visited ℕ) (ℕ × ℕ)
  | 0     => do ✓[singleton 0] pure (0, 1)
  | k + 1 => do
    let p ← fibAux k
    ✓[singleton (k + 1)] pure (p.2, p.1 + p.2)

/-- Bottom-up Fibonacci. Visits each sub-problem in `{0, …, n}` exactly
once. -/

def MemoFib.fib EconCSLib @ cef01c7, EconCSLib.Examples.CostM.MemoFib

def fib (n : ℕ) : CostM (Visited ℕ) ℕ := do
  let p ← fibAux n
  pure p.1

theorem MemoFib.fibAux_ret EconCSLib @ cef01c7, EconCSLib.Examples.CostM.MemoFib

theorem fibAux_ret (n : ℕ) :
    (fibAux n).ret = (Nat.fib n, Nat.fib (n + 1))

theorem MemoFib.fib_value EconCSLib @ cef01c7, EconCSLib.Examples.CostM.MemoFib
The value computed by `fib n` is the `n`-th Fibonacci number.
```
theorem fib_value (n : ℕ) : (fib n).ret = Nat.fib n
```

theorem MemoFib.fibAux_cost EconCSLib @ cef01c7, EconCSLib.Examples.CostM.MemoFib

theorem fibAux_cost (n : ℕ) :
    (fibAux n).cost.toFinset = Finset.range (n + 1)

theorem MemoFib.fib_cost EconCSLib @ cef01c7, EconCSLib.Examples.CostM.MemoFib
The set of sub-problems touched by `fib n` is exactly `{0, …, n}`.
```
theorem fib_cost (n : ℕ) :
    (fib n).cost.toFinset = Finset.range (n + 1)
```
theorem MemoFib.fib_cost_card EconCSLib @ cef01c7, EconCSLib.Examples.CostM.MemoFib
Exactly `n + 1` distinct sub-problems are touched by `fib n`.
```
theorem fib_cost_card (n : ℕ) : (fib n).cost.toFinset.card = n + 1
```

Modules: EconCSLib.Examples.CostM.MemoFib

Worked Example: Memoized Fibonacci Footprint

Fibonacci instrumented in CostM (Visited ℕ) (Memoization Footprint via the Visited Monoid), so the cost field records the set of indices the recursion touches rather than a call count. Because the Visited monoid is idempotent, the footprint collapses to the distinct subproblems: $$ (\operatorname{fib} n).\mathrm{cost}.\mathrm{toFinset} \;=\; \{0, 1, \dots, n\} \;=\; \operatorname{range}(n+1), $$ hence fib_cost_card : (fib n).cost.toFinset.card = n + 1 — exactly n+1 distinct subproblems, the hallmark of an O(n) memoized DP.

Correctness and cost are proved independently: fib_value : (fib n).ret = Nat.fib n lives on .ret, while fib_cost lives on .cost. This is the intended CostM separation (The CostM Complexity Monad).