Leftist heaps and tail-recursive adjacent merging

28 fully proved

Leftist Heap datatype (concrete)

InductiveLeftist heap#✓fully proved

Leftist heap: Empty or Node rank value left right

inductive LHeap (α : Type u) : Type u where
| E : LHeap α
| N : Nat → α → LHeap α → LHeap α → LHeap α
deriving DecidableEq

Used by 26

Used byLower bound on all elements of a heap · Correctness and cost equivalence of tail-recursive heap construction · Min-heap property · List-to-heap construction gives a min-heap · Min-heap ordering of every heap in a list · Leftist heap from a list by tail-recursive merging · Leftist invariant with correct stored ranks · List-to-heap construction gives a leftist tree · Leftist invariant for every heap in a list · Node constructor restoring the leftist property · Merge of leftist heaps · Non-tail-recursive adjacent merging of heaps · Tail-recursive adjacent merging with an accumulator · Accumulator characterization of tail-recursive adjacent merging · Fuel-based merging of all heaps with tail-recursive passes · Fuel-based auxiliary merge of leftist heaps · List-to-heap construction preserves the multiset · Multiset of elements of a leftist heap · Rank of a leftist heap · Singleton leftist heap · Number of nodes of a leftist heap · Combined multiset of a list of heaps · Cost of merging leftist heaps · Cost of non-tail-recursive adjacent merging · Cost of tail-recursive adjacent merging · Fuel-based auxiliary cost of merging

DefinitionNumber of nodes of a leftist heap#✓fully proved

Size (number of nodes)

def size : LHeap α → Nat
| .E => 0
| .N _ _ l r => 1 + size l + size r

Uses 1 · Used by 3

Statement usesLeftist heap

Used byCorrectness and cost equivalence of tail-recursive heap construction · Merge of leftist heaps · Cost of merging leftist heaps

DefinitionRank of a leftist heap#✓fully proved

Rank (right spine length, or stored rank)

def rank : LHeap α → Nat
| .E => 0
| .N r _ _ _ => r

Uses 1 · Used by 3

Statement usesLeftist heap

Used byCorrectness and cost equivalence of tail-recursive heap construction · Leftist invariant with correct stored ranks · Node constructor restoring the leftist property

DefinitionMultiset of elements of a leftist heap#✓fully proved

Multiset of elements

def mset_tree : LHeap α → Multiset α
| .E => 0
| .N _ x l r => {x} + mset_tree l + mset_tree r

Uses 1 · Used by 6

Statement usesLeftist heap

Used byCorrectness and cost equivalence of tail-recursive heap construction · List-to-heap construction gives a min-heap · Per-input correctness of list-to-heap construction · List-to-heap construction gives a leftist tree · List-to-heap construction preserves the multiset · Combined multiset of a list of heaps

DefinitionLower bound on all elements of a heap#✓fully proved

All elements in heap are ≥ x (for heap ordering)

def all_le [LE α] (x : α) : LHeap α → Prop
| .E => True
| .N _ y l r => x ≤ y ∧ all_le x l ∧ all_le x r

Uses 1 · Used by 2

Statement usesLeftist heap

Used byCorrectness and cost equivalence of tail-recursive heap construction · Min-heap property

DefinitionMin-heap property#✓fully proved

Min-heap property: root ≤ all in subtrees

def heap [LE α] : LHeap α → Prop
| .E => True
| .N _ x l r => all_le x l ∧ all_le x r ∧ heap l ∧ heap r

Uses 2 · Used by 6

Statement usesLeftist heap · Lower bound on all elements of a heap

Used byCorrectness and cost equivalence of tail-recursive heap construction · List-to-heap construction gives a min-heap · Min-heap ordering of every heap in a list · Per-input correctness of list-to-heap construction · List-to-heap construction gives a leftist tree · List-to-heap construction preserves the multiset

DefinitionLeftist invariant with correct stored ranks#✓fully proved

Leftist invariant: stored rank is correct and left rank ≥ right rank For every node N storedRank x l r, require: - storedRank = rank r + 1; - rank l ≥ rank r; - ltree l; - ltree r.

def ltree : LHeap α → Prop
| .E => True
| .N rk _ l r => rk = r.rank + 1 ∧ l.rank ≥ r.rank ∧ l.ltree ∧ r.ltree

Uses 2 · Used by 6

Statement usesLeftist heap · Rank of a leftist heap

Used byCorrectness and cost equivalence of tail-recursive heap construction · List-to-heap construction gives a min-heap · Per-input correctness of list-to-heap construction · List-to-heap construction gives a leftist tree · Leftist invariant for every heap in a list · List-to-heap construction preserves the multiset

DefinitionNode constructor restoring the leftist property#✓fully proved

Helper to restore leftist property. Constructs a node whose stored rank is exactly one plus the rank of its resulting right subtree (b.rank + 1 or a.rank + 1 after swap).

def make (x : α) (a b : LHeap α) : LHeap α :=
  if a.rank ≥ b.rank then
    .N (b.rank + 1) x a b
  else
    .N (a.rank + 1) x b a

Uses 2 · Used by 2

Statement usesLeftist heap · Rank of a leftist heap

Used byCorrectness and cost equivalence of tail-recursive heap construction · Fuel-based auxiliary merge of leftist heaps

DefinitionFuel-based auxiliary merge of leftist heaps#✓fully proved

Auxiliary fuel-based merge to avoid termination proof complexity. When reconstructing an existing node during recursion, preserves its original stored rank (does not replace it with 0).

def mergeAux [LinearOrder α] : Nat → LHeap α → LHeap α → LHeap α
| _, .E, h => h
| _, h, .E => h
| 0, _, _ => .E
| fuel + 1, .N rx x la ra, .N ry y lb rb =>
  if x ≤ y then
    make x la (mergeAux fuel ra (LHeap.N ry y lb rb))
  else
    make y lb (mergeAux fuel (LHeap.N rx x la ra) rb)

Uses 2 · Used by 2

Statement usesLeftist heap · Node constructor restoring the leftist property

Used byCorrectness and cost equivalence of tail-recursive heap construction · Merge of leftist heaps

DefinitionMerge of leftist heaps#✓fully proved

Leftist merge (public API)

def merge [LinearOrder α] (h1 h2 : LHeap α) : LHeap α :=
  mergeAux (h1.size + h2.size) h1 h2

Uses 3 · Used by 5

Statement usesLeftist heap · Fuel-based auxiliary merge of leftist heaps · Number of nodes of a leftist heap

Used byCorrectness and cost equivalence of tail-recursive heap construction · Non-tail-recursive adjacent merging of heaps · Tail-recursive adjacent merging with an accumulator · Accumulator characterization of tail-recursive adjacent merging · Cost of tail-recursive adjacent merging

DefinitionFuel-based auxiliary cost of merging#✓fully proved

Auxiliary fuel-based cost of merge. Complexity model faithful to textbook convention: only calls/steps of merge are counted. Reversal of accumulator in merge_adj2 and other auxiliary operations are not counted.

def T_mergeAux [LinearOrder α] : Nat → LHeap α → LHeap α → Nat
| _, .E, _ => 0
| _, _, .E => 0
| 0, _, _ => 0
| fuel + 1, .N rx x _ ra, .N ry y _ rb =>
  if x ≤ y then
    1 + T_mergeAux fuel ra (LHeap.N ry y (LHeap.E : LHeap α) rb)
  else
    1 + T_mergeAux fuel (LHeap.N rx x (LHeap.E : LHeap α) ra) rb

Uses 1 · Used by 1

Statement usesLeftist heap

Used byCost of merging leftist heaps

DefinitionCost of merging leftist heaps#✓fully proved

Cost of merge: number of merge steps (only merge calls counted)

def T_merge [LinearOrder α] (h1 h2 : LHeap α) : Nat :=
  T_mergeAux (h1.size + h2.size) h1 h2

Uses 3 · Used by 3

Statement usesLeftist heap · Fuel-based auxiliary cost of merging · Number of nodes of a leftist heap

Used byCorrectness and cost equivalence of tail-recursive heap construction · Cost of non-tail-recursive adjacent merging · Cost of tail-recursive adjacent merging

DefinitionNon-tail-recursive adjacent merging of heaps#✓fully proved

Non-tail-recursive merge_adj

def merge_adj [LinearOrder α] : List (LHeap α) → List (LHeap α)
| [] => []
| [t] => [t]
| t1 :: t2 :: ts => (t1.merge t2) :: merge_adj ts

Uses 2 · Used by 1

Statement usesLeftist heap · Merge of leftist heaps

Used byAccumulator characterization of tail-recursive adjacent merging

DefinitionTail-recursive adjacent merging with an accumulator#✓fully proved

Tail-recursive merge_adj2 with accumulator, no use of List.append. Genuinely tail-recursive: uses an accumulator and reverse at base case. Does not use List.append (avoids append operator). Complexity model: only merge steps counted, so T_merge_adj2 acc ts = T_merge_adj ts should hold; accumulator reversal overhead is intentionally excluded per textbook convention that only merge calls are counted.

def merge_adj2 [LinearOrder α] (acc : List (LHeap α)) (ts : List (LHeap α)) : List (LHeap α) :=
  match ts with
  | [] => acc.reverse
  | [t] => (t :: acc).reverse
  | t1 :: t2 :: ts' => merge_adj2 (t1.merge t2 :: acc) ts'
termination_by ts.length

Uses 2 · Used by 3

Statement usesLeftist heap · Merge of leftist heaps

Used byCorrectness and cost equivalence of tail-recursive heap construction · Accumulator characterization of tail-recursive adjacent merging · Fuel-based merging of all heaps with tail-recursive passes

DefinitionCost of non-tail-recursive adjacent merging#✓fully proved

Cost of merge_adj: only merge steps counted per textbook

def T_merge_adj [LinearOrder α] : List (LHeap α) → Nat
| [] => 0
| [_] => 0
| t1 :: t2 :: ts => (T_merge t1 t2) + T_merge_adj ts

Uses 2 · Used by 4

Statement usesLeftist heap · Cost of merging leftist heaps

Used byCorrectness and cost equivalence of tail-recursive heap construction · List-to-heap construction gives a min-heap · List-to-heap construction gives a leftist tree · List-to-heap construction preserves the multiset

DefinitionCost of tail-recursive adjacent merging#✓fully proved

Cost of merge_adj2 (accumulator version): only merge steps counted. Follows textbook convention that only calls/steps of merge are counted, so accumulator handling does not contribute to cost. Hence the required comparison T_merge_adj2 acc ts = T_merge_adj ts remains valid.

def T_merge_adj2 [LinearOrder α] : List (LHeap α) → List (LHeap α) → Nat
| _, [] => 0
| _, [_] => 0
| acc, t1 :: t2 :: ts => (T_merge t1 t2) + T_merge_adj2 (t1.merge t2 :: acc) ts
termination_by _ ts => ts.length

Uses 3 · Used by 4

Statement usesLeftist heap · Cost of merging leftist heaps · Merge of leftist heaps

Used byCorrectness and cost equivalence of tail-recursive heap construction · List-to-heap construction gives a min-heap · List-to-heap construction gives a leftist tree · List-to-heap construction preserves the multiset

Merging all heaps

DefinitionFuel-based merging of all heaps with tail-recursive passes#✓fully proved

merge_all2 uses merge_adj2 (tail-recursive variant)

def merge_all2Aux [LinearOrder α] : Nat → List (LHeap α) → LHeap α
| _, [] => .E
| _, [t] => t
| 0, _ => .E
| fuel + 1, ts => merge_all2Aux fuel (merge_adj2 [] ts)

Uses 2 · Used by 2

Statement usesLeftist heap · Tail-recursive adjacent merging with an accumulator

Used byCorrectness and cost equivalence of tail-recursive heap construction · Leftist heap from a list by tail-recursive merging

DefinitionSingleton leftist heap#✓fully proved

Singleton heap: stored rank 1 = rank E + 1, leftist

def singleton (x : α) : LHeap α :=
  .N 1 x .E .E

Uses 1 · Used by 2

Statement usesLeftist heap

Used byCorrectness and cost equivalence of tail-recursive heap construction · Leftist heap from a list by tail-recursive merging

DefinitionLeftist heap from a list by tail-recursive merging#✓fully proved

lheap_list2: convert list to leftist heap via merge_all2 (tail-recursive adj). Uses merge_all2 which itself uses merge_adj2.

def lheap_list2 [LinearOrder α] (xs : List α) : LHeap α :=
  merge_all2 (xs.map singleton)

Uses 3 · Used by 5

Statement usesLeftist heap · Fuel-based merging of all heaps with tail-recursive passes · Singleton leftist heap

Used byCorrectness and cost equivalence of tail-recursive heap construction · List-to-heap construction gives a min-heap · Per-input correctness of list-to-heap construction · List-to-heap construction gives a leftist tree · List-to-heap construction preserves the multiset

Node construction and merge correctness

DefinitionCombined multiset of a list of heaps#✓fully proved

Combined multiset of every heap in a list, including duplicates.

def sumMSet : List (LHeap α) → Multiset α
| [] => 0
| t :: ts => mset_tree t + sumMSet ts

Uses 2 · Used by 1

Statement usesLeftist heap · Multiset of elements of a leftist heap

Used byCorrectness and cost equivalence of tail-recursive heap construction

DefinitionMin-heap ordering of every heap in a list#✓fully proved

Every heap in the list satisfies the min-heap ordering predicate.

def HeapList [LE α] (ts : List (LHeap α)) : Prop := ∀ t ∈ ts, heap t

Uses 2 · Used by 1

Statement usesLeftist heap · Min-heap property

Used byCorrectness and cost equivalence of tail-recursive heap construction

DefinitionLeftist invariant for every heap in a list#✓fully proved

Every heap in the list has correct stored ranks and is leftist.

def LTreeList (ts : List (LHeap α)) : Prop := ∀ t ∈ ts, ltree t

Uses 2 · Used by 1

Statement usesLeftist heap · Leftist invariant with correct stored ranks

Used byCorrectness and cost equivalence of tail-recursive heap construction

TheoremCorrectness and cost equivalence of tail-recursive heap construction#✓fully proved

Graded theorem: correctness of lheap_list2 and complexity equivalence. Complexity model faithful to textbook: only merge calls counted.

theorem fdsa_chap15_ex04 {α : Type u} [LinearOrder α] :
    (∀ xs : List α, (lheap_list2 xs).mset_tree = (xs : Multiset α)) ∧
    (∀ xs : List α, (lheap_list2 xs).heap) ∧
    (∀ xs : List α, (lheap_list2 xs).ltree) ∧
    (∀ (acc : List (LHeap α)) (ts : List (LHeap α)),
        T_merge_adj2 acc ts = T_merge_adj ts)

Uses 20 · Used by 3

Statement usesLeftist heap · Cost of non-tail-recursive adjacent merging · Cost of tail-recursive adjacent merging · Min-heap property · Leftist heap from a list by tail-recursive merging · Leftist invariant with correct stored ranks · Multiset of elements of a leftist heap

Proof usesMin-heap ordering of every heap in a list · Leftist invariant for every heap in a list · Cost of merging leftist heaps · Lower bound on all elements of a heap · Node constructor restoring the leftist property · Merge of leftist heaps · Fuel-based auxiliary merge of leftist heaps · Tail-recursive adjacent merging with an accumulator · Fuel-based merging of all heaps with tail-recursive passes · Rank of a leftist heap · Singleton leftist heap · Number of nodes of a leftist heap · Combined multiset of a list of heaps

Used byList-to-heap construction gives a min-heap · List-to-heap construction gives a leftist tree · List-to-heap construction preserves the multiset

TheoremList-to-heap construction preserves the multiset#✓fully proved

List construction preserves the entire input multiset, including duplicates.

theorem mset_lheap_list2 (xs : List α) :
    (lheap_list2 xs).mset_tree = (xs : Multiset α)

Uses 8 · Used by 1

Statement usesLeftist heap from a list by tail-recursive merging · Multiset of elements of a leftist heap

Proof usesLeftist heap · Cost of non-tail-recursive adjacent merging · Cost of tail-recursive adjacent merging · Min-heap property · Leftist invariant with correct stored ranks · Correctness and cost equivalence of tail-recursive heap construction

Used byPer-input correctness of list-to-heap construction

TheoremList-to-heap construction gives a min-heap#✓fully proved

List construction satisfies min-heap ordering.

theorem heap_lheap_list2 (xs : List α) : (lheap_list2 xs).heap

Uses 8 · Used by 1

Statement usesMin-heap property · Leftist heap from a list by tail-recursive merging

Proof usesLeftist heap · Cost of non-tail-recursive adjacent merging · Cost of tail-recursive adjacent merging · Leftist invariant with correct stored ranks · Multiset of elements of a leftist heap · Correctness and cost equivalence of tail-recursive heap construction

Used byPer-input correctness of list-to-heap construction

TheoremList-to-heap construction gives a leftist tree#✓fully proved

List construction satisfies both stored-rank correctness and leftist balance.

theorem ltree_lheap_list2 (xs : List α) : (lheap_list2 xs).ltree

Uses 8 · Used by 1

Statement usesLeftist heap from a list by tail-recursive merging · Leftist invariant with correct stored ranks

Proof usesLeftist heap · Cost of non-tail-recursive adjacent merging · Cost of tail-recursive adjacent merging · Min-heap property · Multiset of elements of a leftist heap · Correctness and cost equivalence of tail-recursive heap construction

Used byPer-input correctness of list-to-heap construction

TheoremPer-input correctness of list-to-heap construction#✓fully proved

A reusable per-input form of the three construction-correctness conjuncts.

theorem lheap_list2_correct (xs : List α) :
    (lheap_list2 xs).mset_tree = (xs : Multiset α) ∧
    (lheap_list2 xs).heap ∧ (lheap_list2 xs).ltree

Uses 7

Statement usesMin-heap property · Leftist heap from a list by tail-recursive merging · Leftist invariant with correct stored ranks · Multiset of elements of a leftist heap

Proof usesList-to-heap construction gives a min-heap · List-to-heap construction gives a leftist tree · List-to-heap construction preserves the multiset

TheoremAccumulator characterization of tail-recursive adjacent merging#✓fully proved

The accumulator is a reversed prefix; newly merged pairs follow it in input order. This additional output characterization is not required by the original exercise. Append appears only in the specification, not the algorithm.

theorem merge_adj2_eq_reverse_append (acc ts : List (LHeap α)) :
    merge_adj2 acc ts = acc.reverse ++ merge_adj ts

Uses 4

Statement usesLeftist heap · Non-tail-recursive adjacent merging of heaps · Tail-recursive adjacent merging with an accumulator

Proof usesMerge of leftist heaps

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.