Lean declarations

def GCD.gcd EconCSLib @ cef01c7, EconCSLib.Examples.CostM.GCD

Euclidean GCD, instrumented with `CostM ℕ` to count `mod` calls.

def gcd : ℕ → ℕ → CostM ℕ ℕ
  | a, 0     => pure a
  | a, b + 1 => do
    ✓ gcd (b + 1) (a % (b + 1))
termination_by _ b => b
decreasing_by exact Nat.mod_lt _ (Nat.succ_pos _)

/-- Linear cost bound: `gcd a b` performs at most `b` `mod` operations. -/

theorem GCD.gcd_cost_le EconCSLib @ cef01c7, EconCSLib.Examples.CostM.GCD
Linear cost bound: `gcd a b` performs at most `b` `mod` operations.
```
theorem gcd_cost_le (a b : ℕ) : (gcd a b).cost ≤ b
```

theorem GCD.gcd_cost_log_le EconCSLib @ cef01c7, EconCSLib.Examples.CostM.GCD

theorem gcd_cost_log_le (a b : ℕ) :
    (gcd a b).cost ≤ 2 * Nat.log 2 b + 1

Modules: EconCSLib.Examples.CostM.GCD

Worked Example: Euclidean GCD Step Count

The simplest CostM instance: gcd in CostM ℕ, charging one unit per modulus operation. Two bounds are proved:

gcd_cost_le — (gcd a b).cost ≤ b (a trivial linear bound), and
gcd_cost_log_le — (gcd a b).cost ≤ 2 · \log_2 b + 1, the textbook logarithmic bound following from the fact that two consecutive remainders at least halve the modulus.

This is the canonical "C = ℕ, additive, counts one resource" use of the monad (The CostM Complexity Monad): the cost field accumulates the number of mod steps, and the bound lives purely on .cost while the returned gcd value lives on .ret.