CLRS-Lean
Chapter 10. Elementary Data Structures

Imports

import CLRSLean.Chapter_10.Section_10_1_Stacks_And_Queues
import CLRSLean.Chapter_10.Section_10_2_Linked_Lists
import CLRSLean.Chapter_10.Section_10_4_Rooted_Trees

Chapter 10 - Elementary Data Structures

Chapter 10 introduces stacks, queues, linked lists, and rooted-tree representations. The current CLRS-Lean pass uses functional lists as the mathematical model for the first three structures, and a purely functional tree/forest model for the §10.4 rooted-tree encoding. This intentionally avoids pointer mutation while preserving the algebraic claims that the textbook uses when reasoning about the operations.

Sections

10.1 Stacks and queues: proved for the functional-list and array-backed models. Main results: CLRS.Chapter10.pop_push, CLRS.Chapter10.dequeue_enqueue_empty, CLRS.Chapter10.dequeue_enqueue_nonempty, and the array-backed round-trip and overflow/underflow theorems CLRS.Chapter10.arrayPop_arrayPush, CLRS.Chapter10.arrayDequeue_arrayEnqueue_empty.
10.2 Linked lists: proved for the functional-list model. Main results: CLRS.Chapter10.listSearch_sound, CLRS.Chapter10.mem_listDeleteAll_iff.
10.4 Representing rooted trees: proved for the functional rose-tree / left-child-right-sibling model. Main results: the round-trip isomorphism CLRS.Chapter10.ofLCRSForest_toLCRSForest and CLRS.Chapter10.toLCRSForest_ofLCRSForest (packaged as the bijection CLRS.Chapter10.lcrsEquiv), the single-tree round trip CLRS.Chapter10.ofLCRS_toLCRS, and structure preservation CLRS.Chapter10.toLCRSForest_preorder.

Current Gaps

The chapter does not yet formalize pointer-level linked lists or free-list allocation, and the array-backed stack/queue interface defers a concrete RAM execution layer (real memory bounds and operation costs). Section 10.3 ("Implementing pointers and objects") is tracked separately as pure imperative-memory / allocator work.

              namespace CLRSnamespace Chapter10end Chapter10end CLRS