EconCSLib.Foundation.CostM.Visited

The "memoization-shaped" cost monoid for CostM: an AddMonoid whose elements are finite sets of sub-problem indices, with + := (· ∪ ·) and 0 := ∅.

The defining feature is idempotence (s + s = s): repeated visits to the same sub-problem do not enlarge the recorded cost. This is the algebraic shadow of memoization — when the cost type is Visited A, the recorded cost is the distinct set of sub-problems touched, regardless of whether the algorithm actually memoizes.

Type synonym, not direct instance

Visited A is a type synonym for Finset A. We do not give the union-monoid as a direct instance on Finset A because Mathlib's Mathlib.Algebra.Group.Pointwise.Finset.Basic already provides a scoped Zero (Finset A) := ⟨{0}⟩ (the singleton of the underlying zero, not ∅). The two interpretations are incompatible, so we firewall instance resolution behind a fresh type name. Cf. Mathlib's Additive / Multiplicative / OrderDual.

Use site

import EconCSLib.Foundation.CostM
import EconCSLib.Foundation.CostM.Visited

def alg : ℕ → CostM (Visited ℕ) Result := …

Tick Visited.singleton i whenever sub-problem i is touched; the recorded cost will be exactly the set of indices reached. See Examples/CostM/MemoFib.lean for a worked example.

def Visited (A : Type u_1) : Type u_1

Cost type tracking the set of sub-problem indices an algorithm touches, with (∪, ∅) as its (+, 0) monoid.

Type synonym for Finset A; the type synonym blocks Mathlib's scoped pointwise instances on Finset A from leaking into CostM cost arithmetic.

Equations

• Visited A = Finset A

def Visited.toFinset {A : Type u_1} (v : Visited A) : Finset A

View a Visited A as the underlying Finset A.

Equations

• v.toFinset = v

def Visited.ofFinset {A : Type u_1} (s : Finset A) : Visited A

View a Finset A as a Visited A.

Equations

• Visited.ofFinset s = s

theorem Visited.ext {A : Type u_1} {a b : Visited A} (h : a.toFinset = b.toFinset) : a = b

theorem Visited.ext_iff {A : Type u_1} {a b : Visited A} : a = b ↔ a.toFinset = b.toFinset

@[simp]

theorem Visited.toFinset_ofFinset {A : Type u_1} (s : Finset A) : (ofFinset s).toFinset = s

@[implicit_reducible]

instance Visited.instZero {A : Type u_1} : Zero (Visited A)

Equations

• Visited.instZero = { zero := ∅ }

@[simp]

theorem Visited.toFinset_zero {A : Type u_1} : toFinset 0 = ∅

def Visited.singleton {A : Type u_1} (a : A) : Visited A

Mark a single sub-problem a as visited.

Equations

• Visited.singleton a = {a}

@[simp]

theorem Visited.toFinset_singleton {A : Type u_1} (a : A) : (singleton a).toFinset = {a}

@[implicit_reducible]

instance Visited.instAdd {A : Type u_1} [DecidableEq A] : Add (Visited A)

Equations

• Visited.instAdd = { add := fun (a b : Visited A) => Visited.ofFinset (a.toFinset ∪ b.toFinset) }

@[simp]

theorem Visited.toFinset_add {A : Type u_1} [DecidableEq A] (a b : Visited A) : (a + b).toFinset = a.toFinset ∪ b.toFinset

@[implicit_reducible]

instance Visited.instAddMonoid {A : Type u_1} [DecidableEq A] : AddMonoid (Visited A)

Equations

• Visited.instAddMonoid = { toAdd := Visited.instAdd, add_assoc := ⋯, toZero := Visited.instZero, zero_add := ⋯, add_zero := ⋯, nsmul := nsmulRec, nsmul_zero := ⋯, nsmul_succ := ⋯ }