Lean declarations

def ReverseSpace.naiveReverse EconCSLib @ cef01c7, EconCSLib.Examples.CostM.ReverseSpace

def naiveReverse {A : Type} : List A → CostM ℕ (List A)
  | []      => pure []
  | a :: as => do
    ✓[as.length + 1] do
      let rest ← naiveReverse as
      pure (rest ++ [a])

/-- Cumulative `++` allocation is quadratic in input length. -/

theorem ReverseSpace.naiveReverse_cost_le EconCSLib @ cef01c7, EconCSLib.Examples.CostM.ReverseSpace
Cumulative `++` allocation is quadratic in input length.
```
theorem naiveReverse_cost_le {A : Type} (l : List A) :
    (naiveReverse l).cost ≤ l.length * l.length
```

Modules: EconCSLib.Examples.CostM.ReverseSpace

Worked Example: Quadratic Naive List Reversal

The append-at-the-end naive list reversal, instrumented in CostM ℕ to exhibit a quadratic cost. Each of the length recursive steps performs an append whose cost is proportional to the accumulated length, giving $$ (\operatorname{naiveReverse}\,l).\mathrm{cost} \;\le\; |l|^2, $$ proved as naiveReverse_cost_le. This is the counterpoint to the linear and logarithmic CostM ℕ examples (Worked Example: Euclidean GCD Step Count): a worse algorithm shows up directly as a worse bound on .cost, with no change to the monad or to the correctness of the reversed result on .ret.