Imports
import CLRSLean.ProofPatterns.Boundary
import CLRSLean.ProofPatterns.Exchange
import CLRSLean.ProofPatterns.Fiber
import CLRSLean.ProofPatterns.IntervalReusable CLRS proof patterns
This namespace contains small, proof-oriented abstractions that occur across several CLRS chapters. The modules are intentionally light: they name recurring proof geometry without forcing chapter-specific algorithms into one interface.
Current modules:
-
Boundary: one-step boundary-shift induction for prefix/suffix and scan invariants. -
Exchange: the certificate shape for greedy exchange arguments. -
Fiber: key-fiber decomposition for buckets, digit classes, and chains. -
Interval: strict before/nested interval relations for DFS and recursive decompositions.
Implementation details
The reusable proof-support pages remain available outside the main sidebar: