CLRS-Lean
Chapters 1–35 · CLRS Fourth Edition
Chapter 10. Elementary Data Structures

Chapter 10 — Elementary Data Structures

CLRS, fourth edition · Lean 4 formalization

The proofs below use the models and assumptions described in the scope and implementation notes.

Imports

import Mathlib

10.1. Simple Array-Based Data Structures

This section models stacks and queues both as functional lists and, matching the fourth-edition §10.1 "simple array-based data structures" interface, as array-backed stacks and queues with a top/head/tail pointer, overflow and underflow handling, and circular wrap-around. The list model captures the textbook algebra; the array model captures the bounded-storage reading while still deferring a concrete RAM execution layer.

Main results:

Theorem pop_push: popping after pushing returns the pushed element and the old stack.
Theorem dequeue_enqueue_empty: enqueueing into an empty queue then dequeueing returns that element.
Theorem dequeue_enqueue_nonempty: enqueueing at the back of a nonempty queue does not change the next dequeued front element.
Theorem arrayPop_arrayPush: popping immediately after pushing an array-backed stack returns the pushed element and restores the top pointer.
Theorem arrayDequeue_arrayEnqueue_empty: enqueueing into an empty array-backed circular queue and then dequeueing returns the enqueued element.
Theorem arrayPush_overflow / arrayPop_empty / arrayEnqueue_overflow / arrayDequeue_empty: array overflow and underflow are reported as none.

Status: proved for functional-list LIFO/FIFO, valid array-pointer transitions, and the stated local array round trips. A general circular-array FIFO abstraction theorem is not claimed here.

Deferred refinements: RAM execution, pointer mutation, and memory costs.

namespace CLRSnamespace Chapter10

Stacks

A functional stack is a list whose head is the stack top.

abbrev Stack (α : Type u) := List α

The empty stack.

def emptyStack : Stack α :=
  []

Push an element onto the top of a stack.

def push (x : α) (s : Stack α) : Stack α :=
  x :: s

Pop the top element from a stack, returning none on underflow.

def pop : Stack α → Option (α × Stack α)
  | [] => none
  | x :: xs => some (x, xs)

Popping immediately after pushing recovers the pushed element and old stack.

theorem pop_push (x : α) (s : Stack α) :
    pop (push x s) = some (x, s) := by
  rfl

Popping the empty stack reports underflow.

theorem pop_empty : pop (emptyStack : Stack α) = none := by
  rfl

Pushing increases stack length by one.

theorem length_push (x : α) (s : Stack α) :
    (push x s).length = s.length + 1 := by
  simp [push]

Queues

A functional queue is a list whose head is the dequeue front.

abbrev Queue (α : Type u) := List α

The empty queue.

def emptyQueue : Queue α :=
  []

Enqueue an element at the back of the queue.

def enqueue (x : α) (q : Queue α) : Queue α :=
  q ++ [x]

Dequeue the front element, returning none on underflow.

def dequeue : Queue α → Option (α × Queue α)
  | [] => none
  | x :: xs => some (x, xs)

Dequeueing the empty queue reports underflow.

theorem dequeue_empty : dequeue (emptyQueue : Queue α) = none := by
  rfl

Enqueueing into an empty queue and then dequeueing returns that element.

theorem dequeue_enqueue_empty (x : α) :
    dequeue (enqueue x emptyQueue) = some (x, emptyQueue) := by
  rfl

If a queue is already nonempty, enqueueing at the back does not change the next front element to be dequeued.

theorem dequeue_enqueue_nonempty (front x : α) (rest : List α) :
    dequeue (enqueue x (front :: rest)) = some (front, rest ++ [x]) := by
  rfl

Enqueueing increases queue length by one.

theorem length_enqueue (x : α) (q : Queue α) :
    (enqueue x q).length = q.length + 1 := by
  simp [enqueue]

Array-backed stacks and queues

A bounded array is modeled as a total indexed function; unwritten slots take a junk value. This is the functional interface of the fourth-edition §10.1 array, deferring RAM storage to a later execution model.

abbrev ArrayStore (α : Type u) := Nat → α

Read the element stored at index i of an array.

def arrayRead (A : ArrayStore α) (i : Nat) : α := A i

Write x at index i, leaving every other index unchanged.

def arrayWrite (i : Nat) (x : α) (A : ArrayStore α) : ArrayStore α :=
  Function.update A i x

Reading immediately after writing returns the written value.

theorem arrayRead_arrayWrite_same (i : Nat) (x : α) (A : ArrayStore α) :
    arrayRead (arrayWrite i x A) i = x := by
  simp [arrayRead, arrayWrite]

Writing at one index leaves every other index unchanged.

theorem arrayRead_arrayWrite_other {i j : Nat} (h : j ≠ i) (x : α) (A : ArrayStore α) :
    arrayRead (arrayWrite i x A) j = arrayRead A j := by
  simp [arrayRead, arrayWrite, h]

An array-backed stack of capacity n: a store together with a top pointer and its capacity bound. Elements occupy slots 0..top-1 with the stack top at index top-1 (CLRS §10.1).

structure ArrayStack (α : Type u) where
  store : ArrayStore α
  top : Nat
  capacity : Nat

Legal raw stack state: occupied slots fit within the capacity. Zero-capacity stacks are valid exactly when empty.

def ArrayStack.Valid (s : ArrayStack α) : Prop := s.top ≤ s.capacity

Construct an empty stack over any supplied backing store.

def ArrayStack.empty (capacity : Nat) (store : ArrayStore α) : ArrayStack α :=
  ⟨store, 0, capacity⟩

Every empty stack satisfies its pointer bound, including capacity zero.

theorem ArrayStack.empty_valid (capacity : Nat) (store : ArrayStore α) :
    (ArrayStack.empty capacity store).Valid := Nat.zero_le _

PUSH onto an array-backed stack: write at the current top and advance the top pointer; returns none on overflow when the stack is already full.

def arrayPush (x : α) (s : ArrayStack α) : Option (ArrayStack α) :=
  if s.top < s.capacity then
    some { store := arrayWrite s.top x s.store, top := s.top + 1, capacity := s.capacity }
  else
    none

POP from an array-backed stack: return the top element and the stack with the top pointer lowered; returns none on underflow when the stack is empty.

def arrayPop (s : ArrayStack α) : Option (α × ArrayStack α) :=
  if s.top = 0 then
    none
  else
    let t := s.top - 1
    some (arrayRead s.store t, { store := s.store, top := t, capacity := s.capacity })

Popping immediately after pushing (on a non-full stack) returns the pushed element and restores the top pointer; the freed slot keeps its value.

theorem arrayPop_arrayPush (x : α) (s : ArrayStack α) (h : s.top < s.capacity) :
    (arrayPush x s).bind (fun s' => arrayPop s') =
      some (x, { store := arrayWrite s.top x s.store, top := s.top, capacity := s.capacity }) := by
  unfold arrayPush arrayPop
  simp [h, arrayRead, arrayWrite]

Popping an empty array-backed stack reports underflow.

theorem arrayPop_empty (f : Nat → α) (n : Nat) :
    arrayPop ({ store := f, top := 0, capacity := n } : ArrayStack α) = none := by
  simp [arrayPop]

Pushing onto a full array-backed stack reports overflow.

theorem arrayPush_overflow (x : α) (s : ArrayStack α) (h : s.top = s.capacity) :
    arrayPush x s = none := by
  simp [arrayPush, h]

An array-backed circular queue of capacity n: a store with head and tail pointers (CLRS §10.1). Following the textbook, the array holds at most n-1 elements: the queue is empty when head = tail and full when head = (tail + 1) mod n, with indices wrapping around.

structure ArrayQueue (α : Type u) where
  store : ArrayStore α
  head : Nat
  tail : Nat
  capacity : Nat

Legal circular-queue state. One slot is reserved to distinguish full from empty, so a valid capacity-one queue has no usable storage slots.

def ArrayQueue.Valid (q : ArrayQueue α) : Prop :=
  0 < q.capacity ∧ q.head < q.capacity ∧ q.tail < q.capacity

instance (q : ArrayQueue α) : Decidable q.Valid :=
  inferInstanceAs (Decidable (0 < q.capacity ∧ q.head < q.capacity ∧ q.tail < q.capacity))

Construct an empty raw queue; positive capacity makes it valid.

def ArrayQueue.empty (capacity : Nat) (store : ArrayStore α) : ArrayQueue α :=
  ⟨store, 0, 0, capacity⟩

Empty circular queues are valid precisely for positive capacity.

theorem ArrayQueue.empty_valid (capacity : Nat) (store : ArrayStore α)
    (hcapacity : 0 < capacity) : (ArrayQueue.empty capacity store).Valid :=
  ⟨hcapacity, hcapacity, hcapacity⟩

ENQUEUE: write at the tail and advance the tail (wrapping around); returns none on overflow or an invalid raw state, including zero capacity.

def arrayEnqueue (x : α) (q : ArrayQueue α) : Option (ArrayQueue α) :=
  if q.Valid then
    if q.head = (q.tail + 1) % q.capacity then
      none
    else
      some { store := arrayWrite q.tail x q.store, head := q.head,
             tail := (q.tail + 1) % q.capacity, capacity := q.capacity }
  else none

DEQUEUE: read at the head and advance the head (wrapping around); returns none on underflow or an invalid raw state.

def arrayDequeue (q : ArrayQueue α) : Option (α × ArrayQueue α) :=
  if q.Valid then
    if q.head = q.tail then
      none
    else
      some (arrayRead q.store q.head,
            { store := q.store, head := (q.head + 1) % q.capacity,
              tail := q.tail, capacity := q.capacity })
  else none

Enqueueing into an empty array-backed queue and then dequeueing returns the enqueued element; the resulting head and tail are equal again after the dequeue.

theorem arrayDequeue_arrayEnqueue_empty (x : α) (n : Nat) (f : Nat → α) (hn : 1 < n) :
    (arrayEnqueue x { store := f, head := 0, tail := 0, capacity := n }).bind
        (fun q' => arrayDequeue q') =
      some (x, { store := arrayWrite 0 x f, head := 1 % n, tail := 1 % n, capacity := n }) := by
  unfold arrayEnqueue arrayDequeue
  simp [ArrayQueue.Valid, hn, show 0 < n by omega, Nat.mod_eq_of_lt, arrayRead, arrayWrite]

Dequeueing an empty array-backed queue reports underflow.

theorem arrayDequeue_empty (f : Nat → α) (n : Nat) :
    arrayDequeue ({ store := f, head := 0, tail := 0, capacity := n } : ArrayQueue α) = none := by
  simp [arrayDequeue]

Enqueueing into a full array-backed queue reports overflow.

theorem arrayEnqueue_overflow (x : α) (q : ArrayQueue α)
    (h : q.head = (q.tail + 1) % q.capacity) :
    arrayEnqueue x q = none := by
  simp [arrayEnqueue, h]

Enqueueing advances the tail pointer, wrapping modulo the capacity.

theorem arrayEnqueue_tail_wraps (x : α) (q : ArrayQueue α)
    (hq : q.Valid) (h : q.head ≠ (q.tail + 1) % q.capacity) :
    (arrayEnqueue x q).map (fun q' => q'.tail) = some ((q.tail + 1) % q.capacity) := by
  simp [arrayEnqueue, hq, h]

Validity and safe raw-state handling

A successful push stays within capacity and preserves that capacity.

theorem arrayPush_preserves_valid {x : α} {s s' : ArrayStack α}
    (h : arrayPush x s = some s') : s'.Valid ∧ s'.capacity = s.capacity := by
  unfold arrayPush at h
  split at h
  · simp only [Option.some.injEq] at h
    subst s'
    constructor
    · dsimp [ArrayStack.Valid]
      omega
    · rfl
  · simp at h

Popping a valid stack preserves validity and capacity.

theorem arrayPop_preserves_valid {s s' : ArrayStack α} {x : α}
    (hs : s.Valid) (h : arrayPop s = some (x, s')) :
    s'.Valid ∧ s'.capacity = s.capacity := by
  unfold arrayPop at h
  split at h
  · simp at h
  · simp only [Option.some.injEq, Prod.mk.injEq] at h
    rcases h with ⟨_, rfl⟩
    dsimp [ArrayStack.Valid] at hs ⊢
    omega

Invalid raw queues cannot accept an element.

theorem arrayEnqueue_invalid (x : α) (q : ArrayQueue α) (hq : ¬ q.Valid) :
    arrayEnqueue x q = none := by simp [arrayEnqueue, hq]

Invalid raw queues cannot produce an element.

theorem arrayDequeue_invalid (q : ArrayQueue α) (hq : ¬ q.Valid) :
    arrayDequeue q = none := by simp [arrayDequeue, hq]

Zero-capacity queues reject every enqueue, independently of pointer values.

theorem arrayEnqueue_zero_capacity (x : α) (q : ArrayQueue α) (h : q.capacity = 0) :
    arrayEnqueue x q = none :=
  arrayEnqueue_invalid x q (by simp [ArrayQueue.Valid, h])

Zero-capacity queues reject every dequeue, independently of pointer values.

theorem arrayDequeue_zero_capacity (q : ArrayQueue α) (h : q.capacity = 0) :
    arrayDequeue q = none :=
  arrayDequeue_invalid q (by simp [ArrayQueue.Valid, h])

Successful enqueue preserves legal pointers and the capacity. The validity check also guarantees that its write occurs at an in-range tail index.

theorem arrayEnqueue_preserves_valid {x : α} {q q' : ArrayQueue α}
    (h : arrayEnqueue x q = some q') : q'.Valid ∧ q'.capacity = q.capacity := by
  unfold arrayEnqueue at h
  split at h
  next hq =>
    split at h
    · simp at h
    · simp only [Option.some.injEq] at h
      subst q'
      exact ⟨⟨hq.1, hq.2.1, Nat.mod_lt _ hq.1⟩, rfl⟩
  · simp at h

Successful dequeue preserves legal pointers and the capacity.

theorem arrayDequeue_preserves_valid {q q' : ArrayQueue α} {x : α}
    (h : arrayDequeue q = some (x, q')) : q'.Valid ∧ q'.capacity = q.capacity := by
  unfold arrayDequeue at h
  split at h
  next hq =>
    split at h
    · simp at h
    · simp only [Option.some.injEq, Prod.mk.injEq] at h
      rcases h with ⟨_, rfl⟩
      exact ⟨⟨hq.1, Nat.mod_lt _ hq.1, hq.2.2⟩, rfl⟩
  · simp at h

Every successful enqueue uses a valid input state and an in-range write.

theorem arrayEnqueue_valid_input {x : α} {q q' : ArrayQueue α}
    (h : arrayEnqueue x q = some q') : q.Valid := by
  by_contra hq
  simp [arrayEnqueue, hq] at h

Every successful dequeue reads a valid input state.

theorem arrayDequeue_valid_input {q q' : ArrayQueue α} {x : α}
    (h : arrayDequeue q = some (x, q')) : q.Valid := by
  by_contra hq
  simp [arrayDequeue, hq] at h

end Chapter10end CLRS

Imports

import Mathlib

10.2. Linked Lists

This section uses ordinary Lean lists as the mathematical model of a linked list. It captures the lookup, front insertion, and deletion-by-key behavior that CLRS proves informally before one adds pointer fields and memory allocation.

Main results:

Theorem listSearch_sound: a successful search returns an element from the input list satisfying the predicate.
Theorem listSearch_eq_none_iff: failure is equivalent to no match.
Theorems listSearch_eq_some_iff_prefix and listSearch_eq_some_iff_firstIndex: success identifies the first match.
Theorem mem_listInsert_self: inserting at the front makes the inserted element a member.
Theorem mem_listDeleteAll_iff: deleting all nodes with a key gives the expected membership characterization.

Status: proved for the functional-list model.

Deletion in this model removes every equal value, including duplicates; it does not represent deletion of one node by pointer identity.

Deferred refinements: pointer updates, identity-based deletion, and free-list allocation.

namespace CLRSnamespace Chapter10

Functional linked-list operations

Search a list for the first element satisfying a Boolean predicate.

def listSearch (p : α → Bool) : List α → Option α
  | [] => none
  | x :: xs => if p x then some x else listSearch p xs

Insert an element at the head of a linked list.

def listInsert (x : α) (xs : List α) : List α :=
  x :: xs

Delete every node whose key equals x.

def listDeleteAll [DecidableEq α] (x : α) (xs : List α) : List α :=
  xs.filter fun y => y != x

Search correctness

A successful search returns a member of the input list satisfying the predicate.


theorem listSearch_sound {p : α → Bool} {xs : List α} {x : α}
    (h : listSearch p xs = some x) :
    x ∈ xs ∧ p x = true := by
  induction xs with
  | nil =>
      simp [listSearch] at h
  | cons y ys ih =>
      by_cases hy : p y = true
      · simp [listSearch, hy] at h
        subst x
        exact ⟨by simp, hy⟩
      · have hyfalse : p y = false := by
          cases hpy : p y <;> simp [hpy] at hy ⊢
        simp [listSearch, hyfalse] at h
        rcases ih h with ⟨hmem, hp⟩
        exact ⟨by simp [hmem], hp⟩

The local executable search is the standard first-match list search.

theorem listSearch_eq_find? (p : α → Bool) (xs : List α) :
    listSearch p xs = xs.find? p := by
  induction xs with
  | nil => rfl
  | cons x xs ih =>
      cases hp : p x <;> simp [listSearch, ih, hp]

Search fails exactly when every input element fails the predicate.


theorem listSearch_eq_none_iff (p : α → Bool) (xs : List α) :
    listSearch p xs = none ↔ ∀ x ∈ xs, p x = false := by
  rw [listSearch_eq_find?, List.find?_eq_none]
  simp

A successful search splits the input at a matching value, with no match in the preceding prefix. This characterizes the first match even with duplicates.


theorem listSearch_eq_some_iff_prefix (p : α → Bool) (xs : List α) (x : α) :
    listSearch p xs = some x ↔ p x = true ∧
      ∃ before after, xs = before ++ x :: after ∧ ∀ y ∈ before, p y = false := by
  rw [listSearch_eq_find?]
  simpa using (List.find?_eq_some_iff_append (xs := xs) (p := p) (b := x))

Search succeeds precisely at a matching index whose earlier positions all fail the predicate. The index is in range and identifies the returned payload.


theorem listSearch_eq_some_iff_firstIndex (p : α → Bool) (xs : List α) (x : α) :
    listSearch p xs = some x ↔ p x = true ∧
      ∃ (i : Nat) (hi : i < xs.length), xs[i] = x ∧
        ∀ j (hj : j < i), p (xs[j]'(Nat.lt_trans hj hi)) = false := by
  rw [listSearch_eq_find?]
  simpa using (List.find?_eq_some_iff_getElem (xs := xs) (p := p) (b := x))

Insert and delete correctness

The inserted element is a member of the resulting list.

theorem mem_listInsert_self (x : α) (xs : List α) :
    x ∈ listInsert x xs := by
  simp [listInsert]

Existing members remain members after front insertion.

theorem mem_listInsert_of_mem {x y : α} {xs : List α}
    (h : y ∈ xs) : y ∈ listInsert x xs := by
  simp [listInsert, h]

Delete-all has the expected membership characterization.

theorem mem_listDeleteAll_iff [DecidableEq α] {x y : α} {xs : List α} :
    y ∈ listDeleteAll x xs ↔ y ∈ xs ∧ y ≠ x := by
  simp [listDeleteAll]

Deleting all copies of x removes x.

theorem not_mem_listDeleteAll_self [DecidableEq α] (x : α) (xs : List α) :
    x ∉ listDeleteAll x xs := by
  simp [listDeleteAll]

end Chapter10end CLRS

Imports

import Mathlib

10.3. Representing Rooted Trees

CLRS §10.3 shows how to store a rooted tree with an unbounded branching factor using only two pointers per node -- the left-child, right-sibling (LCRS) representation -- instead of a per-node child array. In the textbook, x.left-child points to the leftmost child of x and x.right-sibling points to the next sibling of x to its right.

This section formalizes the LCRS scheme as a purely functional, information-preserving encoding between two data models:

RoseTree: a multiway rooted tree -- a label together with a List (RoseTree α) of children (arbitrary branching factor).
LCRSTree: a binary tree whose left subtree means "leftmost child" and whose right subtree means "next sibling".

The clean correctness statement is a round-trip isomorphism between a rooted forest (an ordered list of sibling trees) and its LCRS binary encoding.

Main results:

toLCRSForest / ofLCRSForest: total encode/decode between a forest (List (RoseTree α)) and an LCRSTree α.
Theorem ofLCRSForest_toLCRSForest and toLCRSForest_ofLCRSForest: the two maps are mutually inverse, so the LCRS binary encoding is a faithful, information-preserving representation of a rooted forest.
lcrsEquiv: the round trip packaged as an Equiv (bijection) between List (RoseTree α) and LCRSTree α.
Theorem ofLCRS_toLCRS: the single-tree round trip ofLCRS (toLCRS t) = t.
Theorem toLCRSForest_preorder: the encoding preserves the preorder label sequence, and toLCRSForest_numNodes: it preserves the node count.

Status: proved. This is the functional/representational core of §10.3; the pointer/free-list RAM layer for Chapter 10 stays under the imperative-memory epic and is out of scope here.

Notation conventions used in this section:

α : the node-label type
a forest is a List (RoseTree α) -- an ordered list of sibling subtrees

              namespace CLRSnamespace Chapter10universe u

Models

A RoseTree α is a multiway rooted tree: a label of type α together with an ordered list of child subtrees (arbitrary branching factor). This is the "logical" rooted tree of CLRS §10.3, before any pointer representation is chosen.

inductive RoseTree (α : Type u) where
  | node : α → List (RoseTree α) → RoseTree α

An LCRSTree α is the binary tree used for the left-child / right-sibling representation of CLRS §10.3. node a l r stores label a; its left subtree l encodes a's children (its leftmost child together with that child's sibling chain) and its right subtree r encodes a's own right siblings. nil is the null pointer.

inductive LCRSTree (α : Type u) where
  | nil : LCRSTree α
  | node : α → LCRSTree α → LCRSTree α → LCRSTree α

Encoding and decoding

Encode a forest (an ordered list of sibling rose trees) into a single LCRSTree. The head tree node a cs becomes an LCRS node whose left subtree encodes its children cs and whose right subtree encodes the remaining siblings ts. This is the recursive heart of the LCRS representation (CLRS §10.3).

def toLCRSForest : List (RoseTree α) → LCRSTree α
  | [] => .nil
  | RoseTree.node a cs :: ts => .node a (toLCRSForest cs) (toLCRSForest ts)
termination_by l => sizeOf l
decreasing_by all_goals (simp_wf <;> omega)

Encode a single rooted tree: toLCRS t is the forest encoding of the one-tree forest [t], i.e. an LCRS node whose right-sibling pointer is null.

def toLCRS (t : RoseTree α) : LCRSTree α :=
  toLCRSForest [t]

Decode an LCRSTree back into a forest. An LCRS node node a l r yields the rose tree node a (ofLCRSForest l) followed by the decoded sibling chain ofLCRSForest r. This is structurally recursive on the binary tree.

def ofLCRSForest : LCRSTree α → List (RoseTree α)
  | .nil => []
  | .node a l r => RoseTree.node a (ofLCRSForest l) :: ofLCRSForest r

Decode an LCRSTree into a single rooted tree, dropping any right-sibling chain of the root. The null tree maps to the junk value node default [] (hence the [Inhabited α] assumption), which makes the function total; on genuine single-tree encodings (whose root has a null right sibling) it is the exact inverse of toLCRS.

def ofLCRS [Inhabited α] : LCRSTree α → RoseTree α
  | .nil => RoseTree.node default []
  | .node a l _ => RoseTree.node a (ofLCRSForest l)

Round-trip isomorphism (headline)

Decode ∘ encode = id on forests. Encoding a forest to its LCRS binary tree and decoding it back returns the original forest: the LCRS representation loses no information (CLRS §10.3).

theorem ofLCRSForest_toLCRSForest (f : List (RoseTree α)) :
    ofLCRSForest (toLCRSForest f) = f := by
  induction f using toLCRSForest.induct with
  | case1 => simp [toLCRSForest, ofLCRSForest]
  | case2 a cs ts ihcs ihts =>
      simp [toLCRSForest, ofLCRSForest, ihcs, ihts]

Encode ∘ decode = id on LCRS trees. Decoding an LCRSTree to a forest and re-encoding it returns the original binary tree: the decode map hits every LCRS tree, so the encoding is onto.

theorem toLCRSForest_ofLCRSForest (b : LCRSTree α) :
    toLCRSForest (ofLCRSForest b) = b := by
  induction b with
  | nil => simp [ofLCRSForest, toLCRSForest]
  | node a l r ihl ihr =>
      simp [ofLCRSForest, toLCRSForest, ihl, ihr]

The LCRS round trip packaged as an Equiv: the forest encoding toLCRSForest is a bijection from rooted forests (List (RoseTree α)) to LCRS binary trees (LCRSTree α), with inverse ofLCRSForest. This is the precise sense in which the left-child / right-sibling scheme of CLRS §10.3 is a faithful representation.

def lcrsEquiv : List (RoseTree α) ≃ LCRSTree α where
  toFun := toLCRSForest
  invFun := ofLCRSForest
  left_inv := ofLCRSForest_toLCRSForest
  right_inv := toLCRSForest_ofLCRSForest

Single-tree round trip. Decoding the LCRS encoding of one rooted tree returns that tree exactly: ofLCRS (toLCRS t) = t. A corollary of the forest-level round trip ofLCRSForest_toLCRSForest.

theorem ofLCRS_toLCRS [Inhabited α] (t : RoseTree α) :
    ofLCRS (toLCRS t) = t := by
  cases t with
  | node a cs =>
      simp [toLCRS, toLCRSForest, ofLCRS, ofLCRSForest_toLCRSForest]

Structure preservation

Preorder label sequence of an LCRSTree: visit the node, then its left subtree (children), then its right subtree (siblings). This is the order in which an LCRS traversal reads the labels.

def LCRSTree.preorder : LCRSTree α → List α
  | .nil => []
  | .node a l r => a :: (LCRSTree.preorder l ++ LCRSTree.preorder r)

Preorder label sequence of a rooted forest: for each tree in order emit its root label, then recurse into its children, then continue with the following siblings. This is the canonical reading order of the multiway forest.

def forestPreorder : List (RoseTree α) → List α
  | [] => []
  | RoseTree.node a cs :: ts => a :: (forestPreorder cs ++ forestPreorder ts)
termination_by l => sizeOf l
decreasing_by all_goals (simp_wf <;> omega)

Preorder preservation (structure preservation). The LCRS encoding preserves the preorder label sequence of the forest: reading the binary encoding in node/left/right order reproduces the forest's canonical reading order. In particular the encoding reorders no labels and drops none.

theorem toLCRSForest_preorder (f : List (RoseTree α)) :
    (toLCRSForest f).preorder = forestPreorder f := by
  induction f using toLCRSForest.induct with
  | case1 => simp [toLCRSForest, LCRSTree.preorder, forestPreorder]
  | case2 a cs ts ihcs ihts =>
      simp [toLCRSForest, LCRSTree.preorder, forestPreorder, ihcs, ihts]

Number of internal nodes in an LCRSTree.

def LCRSTree.numNodes : LCRSTree α → Nat
  | .nil => 0
  | .node _ l r => LCRSTree.numNodes l + LCRSTree.numNodes r + 1

The node count of an LCRSTree equals the length of its preorder sequence.

theorem LCRSTree.numNodes_eq_length_preorder (b : LCRSTree α) :
    b.numNodes = b.preorder.length := by
  induction b with
  | nil => simp [LCRSTree.numNodes, LCRSTree.preorder]
  | node a l r ihl ihr =>
      simp only [LCRSTree.numNodes, LCRSTree.preorder, List.length_cons,
        List.length_append, ihl, ihr]

Node-count preservation. The LCRS binary encoding of a forest has exactly one binary node per rose-tree node, i.e. the encoding introduces no extra nodes and loses none.


theorem toLCRSForest_numNodes (f : List (RoseTree α)) :
    (toLCRSForest f).numNodes = (forestPreorder f).length := by
  rw [LCRSTree.numNodes_eq_length_preorder, toLCRSForest_preorder]

Single-tree preorder preservation: the LCRS encoding of one rooted tree reads back the forest preorder of the one-tree forest [t].

theorem toLCRS_preorder (t : RoseTree α) :
    (toLCRS t).preorder = forestPreorder [t] := by
  simp only [toLCRS, toLCRSForest_preorder]

end Chapter10end CLRS

Scope and implementation notes

Imports

import CLRSLean.FourthEdition.Chapter_10.Section_10_1_Simple_Array_Based_Data_Structures
import CLRSLean.FourthEdition.Chapter_10.Section_10_2_Linked_Lists
import CLRSLean.FourthEdition.Chapter_10.Section_10_3_Representing_Rooted_Trees

Current source

Sections 10.1--10.3 are native fourth-edition sections (simple array-based data structures, linked lists, and representing rooted trees), imported directly from Section 10.1, Section 10.2, and Section 10.3. Section 10.3 re-homes the legacy third-edition §10.4 rooted-tree source. Declarations retain the CLRS.Chapter10 namespace during the compatibility period; the third-edition-numbered imports CLRSLean.Chapter_10 and CLRSLean.Chapter_10.Section_10_* forward to these sources.

Coverage boundary

The legacy stack, queue, list, and rooted-tree developments are reused, together with the fourth-edition §10.1 array-backed stack and queue interface (top/head/tail pointers with overflow, underflow, and circular wrap-around). ArrayStack.Valid bounds the top by capacity; ArrayQueue.Valid requires positive capacity and in-range head/tail. Empty constructors and successful-operation preservation are proved. Queue operations reject invalid raw states, including zero capacity. General FIFO is proved for functional queues; the circular-array layer provides valid transitions and local round trips.

Linked search has failure-completeness and first-match/minimal-index contracts. listDeleteAll removes every equal value, not one identity-bearing node. Concrete RAM execution and pointer memory remain outside these models.

See docs/clrs-fourth-edition-map.csv for the section-level mapping and docs/migrations/clrs4.md for compatibility and deprecation policy.

CLRS, fourth edition · Chapter 10 of 35