Lean declarations

def LCS.lcs EconCSLib @ cef01c7, EconCSLib.Examples.CostM.LCS

def lcs : List A → List A → CostM (Visited (ℕ × ℕ)) ℕ
  | [],      ys      => do
    CostM.tick (Visited.singleton (0, ys.length))
    pure 0
  | x :: xs, []      => do
    CostM.tick (Visited.singleton (xs.length + 1, 0))
    pure 0
  | x :: xs, y :: ys =>
    if x = y then do
      CostM.tick (Visited.singleton (xs.length + 1, ys.length + 1))
      let r ← lcs xs ys
      pure (r + 1)
    else do
      CostM.tick (Visited.singleton (xs.length + 1, ys.length + 1))
      let r1 ← lcs xs (y :: ys)
      let r2 ← lcs (x :: xs) ys
      pure (max r1 r2)

/-- Monotonicity helper: enlarging both arguments of `Finset.range`
preserves the `×ˢ` containment. -/

theorem LCS.lcs_cost_subset EconCSLib @ cef01c7, EconCSLib.Examples.CostM.LCS

theorem lcs_cost_subset (xs : List A) : ∀ (ys : List A),
    (lcs xs ys).cost.toFinset ⊆
      Finset.range (xs.length + 1) ×ˢ Finset.range (ys.length + 1)

theorem LCS.lcs_cost_card_le EconCSLib @ cef01c7, EconCSLib.Examples.CostM.LCS

theorem lcs_cost_card_le (xs ys : List A) :
    (lcs xs ys).cost.toFinset.card ≤ (xs.length + 1) * (ys.length + 1)

Modules: EconCSLib.Examples.CostM.LCS

Worked Example: Longest Common Subsequence DP Grid

Longest common subsequence in CostM (Visited (ℕ × ℕ)): the cost footprint is now a set of 2-D grid cells (i, j), one per (prefix of xs, prefix of ys) subproblem. The memoization footprint is contained in the full DP grid, $$ (\operatorname{lcs}\,xs\,ys).\mathrm{cost} \;\subseteq\; \{0,\dots,|xs|\} \times \{0,\dots,|ys|\}, $$ which is lcs_cost_subset; taking cardinalities gives the polynomial-space bound $$ (\operatorname{lcs}\,xs\,ys).\mathrm{cost}.\mathrm{toFinset}.\mathrm{card} \;\le\; (|xs|+1)\,(|ys|+1), $$ i.e. lcs_cost_card_le. This is the canonical polynomial-space DP example — the 2-D analogue of Worked Example: Memoized Fibonacci Footprint.

lcs uses the bare CostM.tick form (rather than the ✓ macro) at its footprint-recording points, since each tick records a specific grid cell Visited.singleton (i, j) rather than a unit cost.