Huffman coding

InductiveHuffman tree#✓fully proved

A Huffman tree over an alphabet \(\alpha\) is either a leaf, which carries a symbol \(a \in \alpha\) and a natural-number weight \(w\), or a fork, which joins a left and a right Huffman tree over \(\alpha\).

inductive HuffmanTree (α : Type u) where
  | leaf (symbol : α) (weight : Nat)
  | fork (left right : HuffmanTree α)
deriving DecidableEq, Repr
Used by 55
Used byAdmissible Huffman trees · Codeword lookup in a Huffman tree · Codeword lookup agrees with the leaf code · Every leaf symbol has a codeword · Codeword of a leaf symbol · Decoding a bit string · Decoding inverts the leaf code · Decoding inverts encoding · Decoding one codeword · Following a path in a Huffman tree · Huffman encoding of a message · Encoding concatenates leaf codewords · Encoded length of a coding tree · Encoded length is the total weighted codeword length · Encoded length of a fork · Erasing symbols from a Huffman tree · Erasing symbols preserves weighted path length · Erasing symbols preserves total weight · Erasing symbols preserves leaf weights · Huffman's algorithm · Huffman's algorithm minimizes the encoded length · Huffman's construction fails exactly on empty or repeated-symbol inputs · Cost of a Huffman work forest · Weighted leaves of a Huffman work forest · Weights of a Huffman work forest · Huffman's construction succeeds on nonempty inputs with distinct symbols · Bounded Huffman merge loop · Huffman loop invariant · Indexed reads of a successful Huffman loop · Huffman loop with lookup count · Huffman loop with an accumulated lookup count · Lookup count of the instrumented Huffman loop · Discarding the lookup count recovers the Huffman loop · Huffman's construction follows a two-minimum merge trace · Optimality of Huffman coding · A two-minimum merge trace gives a minimum weighted path length · Huffman codes are prefix-free · Huffman's construction keeps the weighted leaves · Huffman work item · Numbered leaf work items · Type of leaf symbols of a Huffman tree · Root-to-leaf path code · A symbol has a path code exactly when it labels a leaf · Huffman tree codes are prefix-free · List of leaf symbols of a Huffman tree · Removing a work item by serial · Removing a serial leaves the other table entries unchanged · A stored work item can be removed by its serial · Removing a serial removes one work item from the forest · Removing a serial preserves the table size · Total weight of a Huffman tree · Weighted leaves of a Huffman tree · Weighted path length · Weighted path length as a sum over leaves · Weighted path length of a merged tree

DefinitionWeighted leaves of a Huffman tree#✓fully proved

The list of pairs \((s, w)\), one for each leaf of a Huffman tree, where \(s\) is the symbol and \(w\) the weight at that leaf, read from left to right.

def HuffmanTree.weightedLeaves {α : Type u} : HuffmanTree α → List (α × Nat)
  | .leaf symbol weight => [(symbol, weight)]
  | .fork left right => left.weightedLeaves ++ right.weightedLeaves
Uses 1 · Used by 11
Statement usesHuffman tree
Used byAdmissible Huffman trees · Every leaf symbol has a codeword · Encoded length is the total weighted codeword length · Erasing symbols preserves leaf weights · Huffman's algorithm minimizes the encoded length · Weighted leaves of a Huffman work forest · A two-minimum merge trace gives a minimum weighted path length · Huffman's construction keeps the weighted leaves · A symbol has a path code exactly when it labels a leaf · List of leaf symbols of a Huffman tree · Weighted path length as a sum over leaves

DefinitionList of leaf symbols of a Huffman tree#✓fully proved

The list of the symbols at the leaves of a Huffman tree, read from left to right, with one entry per leaf.

def HuffmanTree.symbols {α : Type u} (tree : HuffmanTree α) : List α :=
  tree.weightedLeaves.map Prod.fst
Uses 2 · Used by 11
Statement usesHuffman tree · Weighted leaves of a Huffman tree
Used byCodeword lookup agrees with the leaf code · Every leaf symbol has a codeword · Codeword of a leaf symbol · Decoding inverts the leaf code · Decoding inverts encoding · Encoding concatenates leaf codewords · Encoded length is the total weighted codeword length · Type of leaf symbols of a Huffman tree · A symbol has a path code exactly when it labels a leaf · Huffman tree codes are prefix-free · Weighted path length as a sum over leaves

DefinitionTotal weight of a Huffman tree#✓fully proved

The sum of the weights at all leaves of a Huffman tree, counted once per leaf.

def HuffmanTree.totalWeight {α : Type u} : HuffmanTree α → Nat
  | .leaf _ weight => weight
  | .fork left right => left.totalWeight + right.totalWeight
Uses 1 · Used by 11
Statement usesHuffman tree
Used byEncoded length of a coding tree · Encoded length is the total weighted codeword length · Erasing symbols preserves weighted path length · Erasing symbols preserves total weight · Weights of a Huffman work forest · Huffman's construction succeeds on nonempty inputs with distinct symbols · Huffman loop invariant · Huffman's construction follows a two-minimum merge trace · Weighted path length · Weighted path length as a sum over leaves · Weighted path length of a merged tree

DefinitionWeighted path length#✓fully proved

The weighted path length of a Huffman tree is defined recursively: a single leaf has weighted path length \(0\), and the tree with left subtree \(L\) and right subtree \(R\) has weighted path length equal to the weighted path length of \(L\) plus that of \(R\) plus the total weight of \(L\) plus the total weight of \(R\).

Equivalently, it is the sum over the leaves of each leaf's weight times its depth, with the root at depth zero (the standard weighted external path length).

def HuffmanTree.weightedPathLength {α : Type u} : HuffmanTree α → Nat
  | .leaf _ _ => 0
  | .fork left right =>
      left.weightedPathLength + right.weightedPathLength +
        left.totalWeight + right.totalWeight
Uses 2 · Used by 11
Statement usesHuffman tree · Total weight of a Huffman tree
Used byEncoded length of a coding tree · Encoded length is the total weighted codeword length · Encoded length of a fork · Erasing symbols preserves weighted path length · Huffman's algorithm minimizes the encoded length · Cost of a Huffman work forest · Huffman's construction follows a two-minimum merge trace · Optimality of Huffman coding · A two-minimum merge trace gives a minimum weighted path length · Weighted path length as a sum over leaves · Weighted path length of a merged tree

TheoremWeighted path length of a merged tree#✓fully proved

For Huffman trees \(L\) and \(R\), the weighted path length of the tree with left subtree \(L\) and right subtree \(R\) equals the weighted path length of \(L\) plus the weighted path length of \(R\) plus the total weight of \(L\) plus the total weight of \(R\).

theorem HuffmanTree.weightedPathLength_fork {α : Type u} (left right : HuffmanTree α) :
    (HuffmanTree.fork left right).weightedPathLength =
      left.weightedPathLength + right.weightedPathLength +
        left.totalWeight + right.totalWeight
Uses 3
Statement usesHuffman tree · Total weight of a Huffman tree · Weighted path length

DefinitionEncoded length of a coding tree#✓fully proved

The encoded length of a leaf of weight \(w\) is \(w\) (its lone symbol receives a one-bit codeword). The encoded length of the tree with left subtree \(L\) and right subtree \(R\) is \(P(L) + P(R) + W(L) + W(R)\), where \(P\) is the weighted path length and \(W\) the total weight; this is the weighted path length of that tree.

When the leaf symbols are distinct, the encoded length equals the encoder's emitted cost, the sum over the weighted leaves of weight times codeword length. When symbols repeat, the encoder resolves each symbol to its first leaf, so on such trees the encoded length is the structural path cost rather than the emitted cost.

def HuffmanTree.encodedLength {α : Type u} : HuffmanTree α → Nat
  | .leaf _ weight => weight
  | .fork left right =>
      left.weightedPathLength + right.weightedPathLength +
        left.totalWeight + right.totalWeight
Uses 3 · Used by 3
Statement usesHuffman tree · Total weight of a Huffman tree · Weighted path length
Used byEncoded length is the total weighted codeword length · Encoded length of a fork · Huffman's algorithm minimizes the encoded length

TheoremEncoded length of a fork#✓fully proved

For any two coding trees \(L\) and \(R\), the encoded length of the tree with left subtree \(L\) and right subtree \(R\) equals its weighted path length.

theorem HuffmanTree.encodedLength_fork {α : Type u} (left right : HuffmanTree α) :
    (HuffmanTree.fork left right).encodedLength =
      (HuffmanTree.fork left right).weightedPathLength
Uses 3 · Used by 1
Statement usesHuffman tree · Encoded length of a coding tree · Weighted path length
Used byHuffman's algorithm minimizes the encoded length

DefinitionRoot-to-leaf path code#✓fully proved

For a Huffman tree \(T\) and a symbol \(s\), the path code of \(s\) in \(T\) records the edges on the path from the root of \(T\) to the leftmost leaf labelled \(s\), writing false for a left edge and true for a right edge. If \(T\) is a single leaf labelled \(s\), the path code is empty; if no leaf of \(T\) is labelled \(s\), there is no path code.

def HuffmanTree.pathCode? {α : Type u} [DecidableEq α] :
    HuffmanTree α → α → Option (List Bool)
  | .leaf symbol _, target => if target = symbol then some [] else none
  | .fork left right, target =>
      match HuffmanTree.pathCode? left target with
      | some bits => some (false :: bits)
      | none => (HuffmanTree.pathCode? right target).map (true :: ·)
Uses 1 · Used by 7
Statement usesHuffman tree
Used byCodeword lookup in a Huffman tree · Every leaf symbol has a codeword · Decoding inverts the leaf code · Encoded length is the total weighted codeword length · A symbol has a path code exactly when it labels a leaf · Huffman tree codes are prefix-free · Weighted path length as a sum over leaves

DefinitionCodeword lookup in a Huffman tree#✓fully proved

Let \(T\) be a Huffman tree and \(a\) a symbol, and write \(0\) for the bit false and \(1\) for the bit true. If \(T\) is a single leaf labelled \(s\), the codeword of \(a\) is the one-bit word \(0\) when \(a = s\) and is undefined otherwise. Otherwise the codeword of \(a\) records the edges from the root of \(T\) to the leftmost leaf labelled \(a\), with \(0\) for a left edge and \(1\) for a right edge; it is undefined when no leaf of \(T\) is labelled \(a\).

def HuffmanTree.code? {α : Type u} [DecidableEq α] :
    HuffmanTree α → α → Option (List Bool)
  | .leaf symbol _, target => if target = symbol then some [false] else none
  | .fork left right, target =>
      match left.pathCode? target with
      | some bits => some (false :: bits)
      | none => (right.pathCode? target).map (true :: ·)
Uses 2 · Used by 8
Statement usesHuffman tree · Root-to-leaf path code
Used byCodeword lookup agrees with the leaf code · Every leaf symbol has a codeword · Codeword of a leaf symbol · Decoding inverts the leaf code · Huffman encoding of a message · Encoding concatenates leaf codewords · Encoded length is the total weighted codeword length · Huffman tree codes are prefix-free

DefinitionFollowing a path in a Huffman tree#✓fully proved

Let \(T\) be a Huffman tree and \(w\) a bit string, and write \(0\) for the bit false and \(1\) for the bit true. Following \(w\) in \(T\) starts at the root and reads the bits of \(w\) one at a time, moving to the left subtree on \(0\) and to the right subtree on \(1\), until it reaches a leaf; it then returns the label of that leaf together with the unread bits of \(w\). It fails if \(w\) runs out before a leaf is reached. In particular, if \(T\) is a single leaf, it returns its label and all of \(w\).

def HuffmanTree.decodePath? {α : Type u} :
    HuffmanTree α → List Bool → Option (α × List Bool)
  | .leaf symbol _, bits => some (symbol, bits)
  | .fork _ _, [] => none
  | .fork left right, bit :: bits =>
      if bit then right.decodePath? bits else left.decodePath? bits
Uses 1 · Used by 4
Statement usesHuffman tree
Used byDecoding a bit string · Decoding inverts the leaf code · Decoding one codeword · Huffman tree codes are prefix-free

DefinitionDecoding one codeword#✓fully proved

Let \(T\) be a Huffman tree and \(w\) a bit string, and write \(0\) for the bit false and \(1\) for the bit true. If \(T\) is a single leaf labelled \(s\), decoding one codeword from \(w\) returns \(s\) together with the rest of \(w\) when \(w\) starts with \(0\), and fails otherwise. If \(T\) is a fork with left subtree \(L\) and right subtree \(R\), it fails when \(w\) is empty; when \(w\) is a bit \(b\) followed by \(w'\), it follows \(w'\) from the root of \(R\) if \(b = 1\) and from the root of \(L\) if \(b = 0\), reading one bit at a time, moving to the left subtree on \(0\) and to the right subtree on \(1\), until it reaches a leaf. It then returns the label of that leaf together with the unread bits, and fails if \(w'\) runs out before a leaf is reached.

def HuffmanTree.decodeOne? {α : Type u} :
    HuffmanTree α → List Bool → Option (α × List Bool)
  | .leaf symbol _, false :: bits => some (symbol, bits)
  | .leaf _ _, _ => none
  | .fork _ _, [] => none
  | .fork left right, bit :: bits =>
      if bit then right.decodePath? bits else left.decodePath? bits
Uses 2 · Used by 3
Statement usesHuffman tree · Following a path in a Huffman tree
Used byDecoding a bit string · Decoding inverts the leaf code · Huffman tree codes are prefix-free

DefinitionDecoding a bit string#✓fully proved

Let \(T\) be a Huffman tree. Decoding the empty bit string with \(T\) returns the empty sequence of symbols. To decode a nonempty bit string \(w\), decode one codeword from \(w\) with \(T\), obtaining a symbol \(s\) and the unread bits \(w'\), and return \(s\) followed by the decoding of \(w'\); decoding fails if decoding one codeword from \(w\) fails or if decoding \(w'\) fails.

def HuffmanTree.decode? {α : Type u} (tree : HuffmanTree α) :
    List Bool → Option (List α)
  | [] => some []
  | bit :: bits =>
      match _h : tree.decodeOne? (bit :: bits) with
      | none => none
      | some (symbol, rest) => (tree.decode? rest).map (symbol :: ·)
termination_by bits => bits.length
decreasing_by
  exact tree.decodeOne?_rest_lt _h
Uses 3 · Used by 2
Statement usesHuffman tree · Decoding one codeword · Following a path in a Huffman tree
Used byDecoding inverts the leaf code · Decoding inverts encoding

DefinitionHuffman encoding of a message#✓fully proved

Given a coding tree \(T\), the empty message encodes to the empty bit string, and a message \(s_1 s_2 \cdots s_n\) encodes to the concatenation, in order, of the codewords of \(s_1, \dots, s_n\) in \(T\). If some \(s_i\) has no codeword in \(T\), the message has no encoding.

def HuffmanTree.encode? {α : Type u} [DecidableEq α] (tree : HuffmanTree α) :
    List α → Option (List Bool)
  | [] => some []
  | symbol :: message => do
      let code ← tree.code? symbol
      let suffix ← tree.encode? message
      pure (code ++ suffix)
Uses 2 · Used by 2
Statement usesHuffman tree · Codeword lookup in a Huffman tree
Used byDecoding inverts encoding · Encoding concatenates leaf codewords

AbbreviationType of leaf symbols of a Huffman tree#✓fully proved

For a Huffman tree \(T\) over an alphabet \(\alpha\), the type of leaf symbols of \(T\) is the subtype of those \(a \in \alpha\) that occur in the list of leaf symbols of \(T\).

abbrev HuffmanTree.LeafSymbol {α : Type u} (tree : HuffmanTree α) :=
  {symbol : α // symbol ∈ tree.symbols}
Uses 2 · Used by 7
Statement usesHuffman tree · List of leaf symbols of a Huffman tree
Used byCodeword lookup agrees with the leaf code · Codeword of a leaf symbol · Decoding inverts the leaf code · Decoding inverts encoding · Encoding concatenates leaf codewords · Huffman codes are prefix-free · Huffman tree codes are prefix-free

DefinitionCodeword of a leaf symbol#✓fully proved

For a Huffman tree \(T\) and a symbol \(s\) occurring at a leaf of \(T\), the codeword of \(s\) is the word that the codeword lookup of \(T\) returns for \(s\), or the empty word if the lookup fails.

The lookup never fails on a leaf symbol, so the empty-word default is never used.

def HuffmanTree.codeOfLeaf {α : Type u} [DecidableEq α]
    (tree : HuffmanTree α) (symbol : tree.LeafSymbol) : List Bool :=
  (tree.code? symbol.1).getD []
Uses 4 · Used by 6
Statement usesHuffman tree · Type of leaf symbols of a Huffman tree · Codeword lookup in a Huffman tree · List of leaf symbols of a Huffman tree
Used byCodeword lookup agrees with the leaf code · Decoding inverts the leaf code · Decoding inverts encoding · Encoding concatenates leaf codewords · Huffman codes are prefix-free · Huffman tree codes are prefix-free

TheoremEvery leaf symbol has a codeword#✓fully proved

Let \(T\) be a Huffman tree and \(s\) a symbol occurring at a leaf of \(T\). Then the codeword lookup of \(s\) in \(T\) succeeds.

theorem HuffmanTree.code?_isSome_of_mem_symbols {α : Type u} [DecidableEq α]
    {tree : HuffmanTree α} {symbol : α} (h : symbol ∈ tree.symbols) :
    (tree.code? symbol).isSome
Uses 5 · Used by 1
Statement usesHuffman tree · Codeword lookup in a Huffman tree · List of leaf symbols of a Huffman tree
Proof usesRoot-to-leaf path code · Weighted leaves of a Huffman tree
Used byCodeword lookup agrees with the leaf code

TheoremCodeword lookup agrees with the leaf code#✓fully proved

Let \(T\) be a Huffman tree and \(s\) a symbol occurring at a leaf of \(T\). Then the codeword lookup of \(s\) in \(T\) succeeds and returns the codeword of \(s\) as a leaf symbol of \(T\).

theorem HuffmanTree.code?_codeOfLeaf {α : Type u} [DecidableEq α]
    (tree : HuffmanTree α) (symbol : tree.LeafSymbol) :
    tree.code? symbol.1 = some (tree.codeOfLeaf symbol)
Uses 6 · Used by 3
Statement usesHuffman tree · Type of leaf symbols of a Huffman tree · Codeword lookup in a Huffman tree · Codeword of a leaf symbol · List of leaf symbols of a Huffman tree
Proof usesEvery leaf symbol has a codeword
Used byDecoding inverts the leaf code · Encoding concatenates leaf codewords · Huffman tree codes are prefix-free

TheoremHuffman tree codes are prefix-free#✓fully proved

For every Huffman tree \(T\), the codeword map on the symbols occurring as leaves of \(T\) is prefix-free: if \(a\) and \(b\) are distinct leaf symbols of \(T\), then the codeword of \(a\) is not a prefix of the codeword of \(b\).

theorem HuffmanTree.prefixFree {α : Type u} [DecidableEq α] (tree : HuffmanTree α) :
    MathlibExt.InformationTheory.IsPrefixFree tree.codeOfLeaf
Uses 10 · Used by 1
Statement usesHuffman tree · Type of leaf symbols of a Huffman tree · Codeword of a leaf symbol · Prefix-free code
Proof usesCodeword lookup in a Huffman tree · Codeword lookup agrees with the leaf code · Decoding one codeword · Following a path in a Huffman tree · Root-to-leaf path code · List of leaf symbols of a Huffman tree
Used byHuffman codes are prefix-free

TheoremDecoding inverts the leaf code#✓fully proved

Let \(T\) be a Huffman tree and let \(s_1, \dots, s_n\) (\(n \ge 0\)) be symbols occurring at leaves of \(T\), with codewords \(c(s_1), \dots, c(s_n)\) as leaf symbols of \(T\). Decoding the concatenation \(c(s_1) c(s_2) \cdots c(s_n)\) with \(T\) succeeds and returns the sequence \(s_1, \dots, s_n\).

theorem HuffmanTree.decode_codeOfLeaf {α : Type u} [DecidableEq α]
    (tree : HuffmanTree α) (message : List tree.LeafSymbol) :
    tree.decode? (message.flatMap tree.codeOfLeaf) = some (message.map Subtype.val)
Uses 10 · Used by 1
Statement usesHuffman tree · Type of leaf symbols of a Huffman tree · Codeword of a leaf symbol · Decoding a bit string · List of leaf symbols of a Huffman tree
Proof usesCodeword lookup in a Huffman tree · Codeword lookup agrees with the leaf code · Decoding one codeword · Following a path in a Huffman tree · Root-to-leaf path code
Used byDecoding inverts encoding

TheoremEncoding concatenates leaf codewords#✓fully proved

Let \(T\) be a Huffman tree and let \(s_1, \dots, s_n\) (\(n \ge 0\)) be symbols occurring at leaves of \(T\), with codewords \(c(s_1), \dots, c(s_n)\) as leaf symbols of \(T\). Encoding \(s_1, \dots, s_n\) with \(T\) succeeds and returns the concatenation \(c(s_1) c(s_2) \cdots c(s_n)\).

theorem HuffmanTree.encode_codeOfLeaf {α : Type u} [DecidableEq α]
    (tree : HuffmanTree α) (message : List tree.LeafSymbol) :
    tree.encode? (message.map Subtype.val) =
      some (message.flatMap tree.codeOfLeaf)
Uses 7 · Used by 1
Statement usesHuffman tree · Type of leaf symbols of a Huffman tree · Codeword of a leaf symbol · Huffman encoding of a message · List of leaf symbols of a Huffman tree
Proof usesCodeword lookup in a Huffman tree · Codeword lookup agrees with the leaf code
Used byDecoding inverts encoding

TheoremDecoding inverts encoding#✓fully proved

Let \(T\) be a Huffman tree and let \(s_1, \dots, s_n\) (\(n \ge 0\)) be symbols occurring at leaves of \(T\). Encoding \(s_1, \dots, s_n\) with \(T\) and then decoding the resulting bit string with \(T\), failing if the encoding fails, returns \(s_1, \dots, s_n\). In particular, the encoding succeeds.

theorem HuffmanTree.decode_encode_leafSymbols {α : Type u} [DecidableEq α]
    (tree : HuffmanTree α) (message : List tree.LeafSymbol) :
    (match tree.encode? (message.map Subtype.val) with
      | none => none
      | some bits => tree.decode? bits) =
      some (message.map Subtype.val)
Uses 8
Statement usesHuffman tree · Type of leaf symbols of a Huffman tree · Decoding a bit string · Huffman encoding of a message · List of leaf symbols of a Huffman tree
Proof usesCodeword of a leaf symbol · Decoding inverts the leaf code · Encoding concatenates leaf codewords

TheoremA symbol has a path code exactly when it labels a leaf#✓fully proved

For a Huffman tree \(T\) over an alphabet \(\alpha\) with decidable equality and a symbol \(a \in \alpha\), the root-to-leaf path code of \(a\) in \(T\) is undefined exactly when \(a\) is not among the leaf symbols of \(T\).

theorem HuffmanTree.pathCode?_eq_none_iff {α : Type u} [DecidableEq α]
    {tree : HuffmanTree α} {symbol : α} :
    tree.pathCode? symbol = none ↔ symbol ∉ tree.symbols
Uses 4 · Used by 2
Statement usesHuffman tree · Root-to-leaf path code · List of leaf symbols of a Huffman tree
Proof usesWeighted leaves of a Huffman tree
Used byEncoded length is the total weighted codeword length · Weighted path length as a sum over leaves

TheoremWeighted path length as a sum over leaves#✓fully proved

Let \(T\) be a Huffman tree whose leaf symbols are pairwise distinct. Then the weighted path length of \(T\) equals the sum, over the leaves of \(T\) with symbol \(s\) and weight \(w\), of \(w\) times the length of the root-to-leaf path of \(s\) in \(T\) (the depth of that leaf, with the root at depth zero).

theorem HuffmanTree.weightedPathLength_eq_sum_pathLengths {α : Type u}
    [DecidableEq α] {tree : HuffmanTree α} (hnd : tree.symbols.Nodup) :
    (tree.weightedLeaves.map
        (fun x => x.2 * ((tree.pathCode? x.1).map List.length).getD 0)).sum =
      tree.weightedPathLength
Uses 7 · Used by 1
Statement usesHuffman tree · Root-to-leaf path code · List of leaf symbols of a Huffman tree · Weighted leaves of a Huffman tree · Weighted path length
Proof usesA symbol has a path code exactly when it labels a leaf · Total weight of a Huffman tree
Used byEncoded length is the total weighted codeword length

TheoremEncoded length is the total weighted codeword length#✓fully proved

Let \(T\) be a coding tree whose leaf symbols are pairwise distinct. For a symbol \(s\), let \(\ell(s)\) be the length of the codeword of \(s\) in \(T\), or \(0\) if \(s\) has no codeword. Then the encoded length of \(T\) equals \(\sum_{(s, w)} w \cdot \ell(s)\), the sum over the weighted leaves \((s, w)\) of \(T\).

Without distinct symbols, the encoder resolves a repeated symbol to its first leaf, and the encoded length remains the structural weighted path cost.

theorem HuffmanTree.encodedLength_eq_sum_codeLengths {α : Type u}
    [DecidableEq α] {tree : HuffmanTree α} (hnd : tree.symbols.Nodup) :
    (tree.weightedLeaves.map
        (fun x => x.2 * ((tree.code? x.1).map List.length).getD 0)).sum =
      tree.encodedLength
Uses 10
Statement usesHuffman tree · Codeword lookup in a Huffman tree · Encoded length of a coding tree · List of leaf symbols of a Huffman tree · Weighted leaves of a Huffman tree
Proof usesRoot-to-leaf path code · A symbol has a path code exactly when it labels a leaf · Total weight of a Huffman tree · Weighted path length · Weighted path length as a sum over leaves

StructureHuffman priority#✓fully proved

A Huffman priority is a pair \((w, s)\) of natural numbers: a weight \(w\) and a serial number \(s\).

Priorities are ordered lexicographically, first by weight and then by serial number, so serial numbers break ties between equal weights deterministically.

structure HuffmanPriority where
  /-- The weight, compared first in the queue order. -/
  weight : Nat
  /-- The serial number: it breaks weight ties and indexes the work table. -/
  serial : Nat
deriving DecidableEq, Repr
Used by 23
Used byExtracting two minima from a Huffman heap · Extracting two minima preserves the heap's elements · Two-minimum extraction is greedy · Priorities of a Huffman work forest · Heap of a Huffman work forest · Huffman's construction succeeds on nonempty inputs with distinct symbols · Bounded Huffman merge loop · Huffman loop invariant · Indexed reads of a successful Huffman loop · Huffman loop with lookup count · Huffman loop with an accumulated lookup count · Lookup count of the instrumented Huffman loop · Discarding the lookup count recovers the Huffman loop · Huffman's construction follows a two-minimum merge trace · Result of a two-minimum extraction · Huffman's construction keeps the weighted leaves · Huffman work item · Numbered leaf work items · Removing a work item by serial · Removing a serial leaves the other table entries unchanged · A stored work item can be removed by its serial · Removing a serial removes one work item from the forest · Removing a serial preserves the table size

StructureHuffman work item#✓fully proved

A work item over an alphabet \(\alpha\) pairs a Huffman priority, that is, a natural-number weight and a natural-number serial, with a Huffman tree over \(\alpha\).

The serial is used to find the tree again after its priority is extracted from the heap.

structure HuffmanWorkItem (α : Type u) where
  /-- The queue priority; its serial locates this item after heap extraction. -/
  priority : HuffmanPriority
  /-- The coding tree carried by this item. -/
  tree : HuffmanTree α
deriving DecidableEq, Repr
Uses 2 · Used by 28
Statement usesHuffman priority · Huffman tree
Used byHuffman's algorithm · Huffman's construction fails exactly on empty or repeated-symbol inputs · Cost of a Huffman work forest · Weighted leaves of a Huffman work forest · Priorities of a Huffman work forest · Weights of a Huffman work forest · Heap of a Huffman work forest · Huffman's construction succeeds on nonempty inputs with distinct symbols · Bounded Huffman merge loop · Huffman loop invariant · Indexed reads of a successful Huffman loop · Huffman loop with lookup count · Huffman loop with an accumulated lookup count · Lookup count of the instrumented Huffman loop · Discarding the lookup count recovers the Huffman loop · Huffman's construction follows a two-minimum merge trace · Work forest of a table · The initial table holds the initial forest · Appending to the table appends to the forest · Huffman's construction keeps the weighted leaves · Initial Huffman forest · Numbered leaf work items · Initial Huffman table · Removing a work item by serial · Removing a serial leaves the other table entries unchanged · A stored work item can be removed by its serial · Removing a serial removes one work item from the forest · Removing a serial preserves the table size

StructureResult of a two-minimum extraction#✓fully proved

A record consisting of two Huffman priorities, the first and the second, together with a binary min-heap of Huffman priorities, the rest.

The two-minimum extraction fills it with the two successive minima of a heap and the heap left after removing them.

structure HuffmanTwoMin where
  /-- The first extracted priority, minimal in the original heap. -/
  first : HuffmanPriority
  /-- The second extracted priority, minimal in the heap left after the first. -/
  second : HuffmanPriority
  /-- The heap left after both extractions. -/
  rest : MinHeap HuffmanPriority
Uses 2 · Used by 9
Statement usesHuffman priority · Binary min-heap
Used byExtracting two minima from a Huffman heap · Extracting two minima preserves the heap's elements · Two-minimum extraction is greedy · Huffman's construction succeeds on nonempty inputs with distinct symbols · Bounded Huffman merge loop · Huffman loop with an accumulated lookup count · Lookup count of the instrumented Huffman loop · Huffman's construction follows a two-minimum merge trace · Huffman's construction keeps the weighted leaves

DefinitionExtracting two minima from a Huffman heap#✓fully proved

Given a binary min-heap \(h\) of Huffman priorities, extract the minimum of \(h\), obtaining a priority \(p_1\) and a heap \(h_1\), then extract the minimum of \(h_1\), obtaining a priority \(p_2\) and a heap \(h_2\). The result is the triple \((p_1, p_2, h_2)\); if either extraction meets an empty heap, there is no result.

def extractTwoMin? (heap : MinHeap HuffmanPriority) : Option HuffmanTwoMin :=
  match heap.extractMin with
  | none => none
  | some (first, afterFirst) =>
      match afterFirst.extractMin with
      | none => none
      | some (second, rest) => some ⟨first, second, rest⟩
Uses 4 · Used by 8
Statement usesHuffman priority · Result of a two-minimum extraction · Binary min-heap · Extracting the minimum of a binary min-heap
Used byExtracting two minima preserves the heap's elements · Two-minimum extraction is greedy · Huffman's construction succeeds on nonempty inputs with distinct symbols · Bounded Huffman merge loop · Huffman loop with an accumulated lookup count · Lookup count of the instrumented Huffman loop · Huffman's construction follows a two-minimum merge trace · Huffman's construction keeps the weighted leaves

TheoremExtracting two minima preserves the heap's elements#✓fully proved

If extracting two minima from a binary min-heap \(h\) of Huffman priorities succeeds with first priority \(p_1\), second priority \(p_2\) and remaining heap \(h'\), then the multiset of elements of \(h\) equals the multiset of elements of \(h'\) with \(p_1\) and \(p_2\) added, counted with multiplicity.

theorem extractTwoMin_cons_elements {heap : MinHeap HuffmanPriority}
    {choice : HuffmanTwoMin} (h : extractTwoMin? heap = some choice) :
    choice.first ::ₘ choice.second ::ₘ choice.rest.elements = heap.elements
Uses 7 · Used by 2
Statement usesHuffman priority · Result of a two-minimum extraction · Binary min-heap · Elements of a binary min-heap · Extracting two minima from a Huffman heap
Proof usesExtracting the minimum of a binary min-heap · Binary heap extraction splits off the minimum
Used byHuffman's construction succeeds on nonempty inputs with distinct symbols · Huffman's construction follows a two-minimum merge trace

TheoremTwo-minimum extraction is greedy#✓fully proved

Order Huffman priorities lexicographically by weight and then serial number. If extracting two minima from a binary min-heap \(h\) of Huffman priorities succeeds with first priority \(p_1\), second priority \(p_2\) and remaining heap \(h'\), then \(p_1 \le q\) for every element \(q\) of \(h\), and \(p_2 \le q\) for every \(q\) that is \(p_2\) or an element of \(h'\).

theorem extractTwoMin_greedy {heap : MinHeap HuffmanPriority}
    {choice : HuffmanTwoMin} (h : extractTwoMin? heap = some choice) :
    (∀ item ∈ heap.elements, choice.first ≤ item) ∧
      (∀ item ∈ choice.second ::ₘ choice.rest.elements, choice.second ≤ item)
Uses 8 · Used by 1
Statement usesHuffman priority · Result of a two-minimum extraction · Binary min-heap · Elements of a binary min-heap · Extracting two minima from a Huffman heap
Proof usesExtracting the minimum of a binary min-heap · Binary heap extraction splits off the minimum · The value extracted from a binary min-heap is minimal
Used byHuffman's construction follows a two-minimum merge trace

DefinitionWork forest of a table#✓fully proved

For a table \(T\) whose cells each hold at most one work item, the work forest of \(T\) is the list of the work items held in the cells of \(T\), in increasing cell order; empty cells are skipped.

In the Huffman loop these are the work items still available to merge.

def huffmanTableForest {α : Type u} (table : Array (Option (HuffmanWorkItem α))) :
    List (HuffmanWorkItem α) :=
  table.toList.filterMap id
Uses 1 · Used by 10
Statement usesHuffman work item
Used byHuffman's construction succeeds on nonempty inputs with distinct symbols · Bounded Huffman merge loop · Huffman loop invariant · Huffman loop with an accumulated lookup count · Lookup count of the instrumented Huffman loop · Huffman's construction follows a two-minimum merge trace · The initial table holds the initial forest · Appending to the table appends to the forest · Huffman's construction keeps the weighted leaves · Removing a serial removes one work item from the forest

DefinitionRemoving a work item by serial#✓fully proved

Given a serial number \(s\) and a table \(t\) of optional Huffman work items, look up the entry of \(t\) at index \(s\). If that entry is a work item whose serial number is \(s\), the result is its tree together with the table obtained from \(t\) by emptying the entry at \(s\); otherwise (the index is out of bounds, the entry is empty, or it holds an item with a different serial number) the removal fails.

The table is indexed directly by serial, so this is one indexed lookup and one indexed update rather than a scan of the work forest.

def takeSerial? {α : Type u} (serial : Nat)
    (table : Array (Option (HuffmanWorkItem α))) :
    Option (HuffmanTree α × Array (Option (HuffmanWorkItem α))) :=
  (table[serial]?).bind fun
    | some item =>
        if item.priority.serial = serial then
          some (item.tree, table.setIfInBounds serial none)
        else
          none
    | none => none
Uses 3 · Used by 10
Statement usesHuffman priority · Huffman tree · Huffman work item
Used byHuffman's construction succeeds on nonempty inputs with distinct symbols · Bounded Huffman merge loop · Huffman loop with an accumulated lookup count · Lookup count of the instrumented Huffman loop · Huffman's construction follows a two-minimum merge trace · Huffman's construction keeps the weighted leaves · Removing a serial leaves the other table entries unchanged · A stored work item can be removed by its serial · Removing a serial removes one work item from the forest · Removing a serial preserves the table size

DefinitionWeighted leaves of a Huffman work forest#✓fully proved

The weighted leaves of a list of Huffman work items are the concatenation, in list order, of the weighted leaves of the items' trees.

def huffmanForestLeaves {α : Type u} (forest : List (HuffmanWorkItem α)) :
    List (α × Nat) :=
  forest.flatMap (fun item => item.tree.weightedLeaves)
Uses 3 · Used by 1
Statement usesHuffman tree · Weighted leaves of a Huffman tree · Huffman work item
Used byHuffman's construction keeps the weighted leaves

TheoremRemoving a serial removes one work item from the forest#✓fully proved

Let \(t\) be a table of optional Huffman work items, and call the list of work items present in a table its work forest. If removing serial number \(s\) from \(t\) succeeds and returns a tree \(T\) and an updated table \(t'\), then there is a work item \(w\) with tree \(T\) and serial number \(s\) such that \(w\) followed by the work forest of \(t'\) is a permutation of the work forest of \(t\).

theorem takeSerial?_item {α : Type u} {serial : Nat}
    {table remaining : Array (Option (HuffmanWorkItem α))} {tree : HuffmanTree α}
    (h : takeSerial? serial table = some (tree, remaining)) :
    ∃ item : HuffmanWorkItem α, item.tree = tree ∧ item.priority.serial = serial ∧
      (item :: huffmanTableForest remaining).Perm (huffmanTableForest table)
Uses 5 · Used by 3
Statement usesHuffman priority · Huffman tree · Huffman work item · Work forest of a table · Removing a work item by serial
Used byHuffman's construction succeeds on nonempty inputs with distinct symbols · Huffman's construction follows a two-minimum merge trace · Huffman's construction keeps the weighted leaves

TheoremRemoving a serial preserves the table size#✓fully proved

Let \(t\) be a table of optional Huffman work items. If removing serial number \(s\) from \(t\) succeeds and returns a tree together with an updated table \(t'\), then \(t'\) has the same size as \(t\).

theorem takeSerial?_size {α : Type u} {serial : Nat}
    {table remaining : Array (Option (HuffmanWorkItem α))} {tree : HuffmanTree α}
    (h : takeSerial? serial table = some (tree, remaining)) :
    remaining.size = table.size
Uses 4 · Used by 2
Statement usesHuffman tree · Huffman work item · Removing a work item by serial
Proof usesHuffman priority
Used byHuffman's construction succeeds on nonempty inputs with distinct symbols · Huffman's construction follows a two-minimum merge trace

TheoremRemoving a serial leaves the other table entries unchanged#✓fully proved

Let \(t\) be a table of optional Huffman work items. If removing serial number \(s\) from \(t\) succeeds and returns a tree together with an updated table \(t'\), then for every index \(j \ne s\) the entry of \(t'\) at \(j\) equals the entry of \(t\) at \(j\) (both are absent when \(j\) is out of bounds).

theorem takeSerial?_getElem?_of_ne {α : Type u} {serial : Nat}
    {table remaining : Array (Option (HuffmanWorkItem α))} {tree : HuffmanTree α}
    (h : takeSerial? serial table = some (tree, remaining)) {j : Nat}
    (hj : j ≠ serial) :
    remaining[j]? = table[j]?
Uses 4 · Used by 2
Statement usesHuffman tree · Huffman work item · Removing a work item by serial
Proof usesHuffman priority
Used byHuffman's construction succeeds on nonempty inputs with distinct symbols · Huffman's construction follows a two-minimum merge trace

TheoremA stored work item can be removed by its serial#✓fully proved

Let \(t\) be a table of optional Huffman work items and let \(w\) be a work item with serial number \(s\). If the entry of \(t\) at index \(s\) is \(w\), then removing serial \(s\) from \(t\) succeeds and returns the tree of \(w\) together with an updated table.

theorem takeSerial?_isSome_of_stored {α : Type u}
    {table : Array (Option (HuffmanWorkItem α))} {item : HuffmanWorkItem α}
    (h : table[item.priority.serial]? = some (some item)) :
    ∃ remaining : Array (Option (HuffmanWorkItem α)),
      takeSerial? item.priority.serial table = some (item.tree, remaining)
Uses 4 · Used by 1
Statement usesHuffman priority · Huffman tree · Huffman work item · Removing a work item by serial
Used byHuffman's construction succeeds on nonempty inputs with distinct symbols

DefinitionNumbered leaf work items#✓fully proved

Given a starting serial number \(s\) and a list of pairs \((a_0, w_0), \dots, (a_{k-1}, w_{k-1})\) of symbols and natural-number weights, this is the list of \(k\) Huffman work items whose \(i\)-th entry has priority (weight \(w_i\), serial \(s + i\)) and whose tree is the leaf with symbol \(a_i\) and weight \(w_i\).

def initialHuffmanForestFrom {α : Type u} :
    Nat → List (α × Nat) → List (HuffmanWorkItem α)
  | _, [] => []
  | serial, (symbol, weight) :: input =>
      ⟨⟨weight, serial⟩, .leaf symbol weight⟩ ::
        initialHuffmanForestFrom (serial + 1) input
Uses 3 · Used by 4
Statement usesHuffman priority · Huffman tree · Huffman work item
Used byHuffman's construction succeeds on nonempty inputs with distinct symbols · Huffman's construction follows a two-minimum merge trace · Huffman's construction keeps the weighted leaves · Initial Huffman forest

DefinitionInitial Huffman forest#✓fully proved

For a list of pairs \((a_0, w_0), \dots, (a_{k-1}, w_{k-1})\) of symbols and natural-number weights, the initial forest is the list of \(k\) Huffman work items whose \(i\)-th entry has priority (weight \(w_i\), serial \(i\)) and whose tree is the leaf with symbol \(a_i\) and weight \(w_i\).

def initialHuffmanForest {α : Type u} (input : List (α × Nat)) :
    List (HuffmanWorkItem α) :=
  initialHuffmanForestFrom 0 input
Uses 2 · Used by 7
Statement usesHuffman work item · Numbered leaf work items
Used byHuffman's algorithm · Huffman's construction fails exactly on empty or repeated-symbol inputs · Huffman's construction succeeds on nonempty inputs with distinct symbols · Huffman's construction follows a two-minimum merge trace · The initial table holds the initial forest · Huffman's construction keeps the weighted leaves · Initial Huffman table

DefinitionInitial Huffman table#✓fully proved

For a list of \(k\) pairs \((a_0, w_0), \dots, (a_{k-1}, w_{k-1})\) of symbols and natural-number weights, the initial table is the array of length \(k\) of optional Huffman work items whose cell \(i\) is present and holds the work item with priority (weight \(w_i\), serial \(i\)) and tree the leaf with symbol \(a_i\) and weight \(w_i\); that is, it is the initial Huffman forest with every entry marked present.

def initialHuffmanTable {α : Type u} (input : List (α × Nat)) :
    Array (Option (HuffmanWorkItem α)) :=
  ((initialHuffmanForest input).map some).toArray
Uses 2 · Used by 6
Statement usesHuffman work item · Initial Huffman forest
Used byHuffman's algorithm · Huffman's construction fails exactly on empty or repeated-symbol inputs · Huffman's construction succeeds on nonempty inputs with distinct symbols · Huffman's construction follows a two-minimum merge trace · The initial table holds the initial forest · Huffman's construction keeps the weighted leaves

TheoremThe initial table holds the initial forest#✓fully proved

For every list of weighted symbols, the work forest read off the initial serial-indexed table of the list is exactly the initial leaf forest of the list, in the same order.

theorem huffmanTableForest_initial {α : Type u} (input : List (α × Nat)) :
    huffmanTableForest (initialHuffmanTable input) = initialHuffmanForest input
Uses 4 · Used by 3
Statement usesHuffman work item · Work forest of a table · Initial Huffman forest · Initial Huffman table
Used byHuffman's construction succeeds on nonempty inputs with distinct symbols · Huffman's construction follows a two-minimum merge trace · Huffman's construction keeps the weighted leaves

TheoremAppending to the table appends to the forest#✓fully proved

For every table \(T\) whose cells each hold at most one work item and every work item \(x\), the work forest of the table obtained from \(T\) by appending a new last cell holding \(x\) is the work forest of \(T\) followed by \(x\).

theorem huffmanTableForest_push_some {α : Type u}
    (table : Array (Option (HuffmanWorkItem α))) (item : HuffmanWorkItem α) :
    huffmanTableForest (table.push (some item)) =
      huffmanTableForest table ++ [item]
Uses 2 · Used by 3
Statement usesHuffman work item · Work forest of a table
Used byHuffman's construction succeeds on nonempty inputs with distinct symbols · Huffman's construction follows a two-minimum merge trace · Huffman's construction keeps the weighted leaves

DefinitionHeap of a Huffman work forest#✓fully proved

The heap of a list of Huffman work items is obtained from the empty binary min-heap by inserting the priorities of the items one at a time, in list order.

def huffmanHeapOfForest {α : Type u} (forest : List (HuffmanWorkItem α)) :
    MinHeap HuffmanPriority :=
  forest.foldl (fun heap item => heap.push item.priority) MinHeap.empty
Uses 5 · Used by 5
Statement usesHuffman priority · Huffman work item · Binary min-heap · Empty binary min-heap · Insertion into a binary min-heap
Used byHuffman's algorithm · Huffman's construction fails exactly on empty or repeated-symbol inputs · Huffman's construction succeeds on nonempty inputs with distinct symbols · Huffman's construction follows a two-minimum merge trace · Huffman's construction keeps the weighted leaves

DefinitionBounded Huffman merge loop#✓fully proved

The loop takes a fuel \(n\), a next serial number \(s\), a binary min-heap \(H\) of Huffman priorities, ordered lexicographically by weight and then serial number, and a table \(T\) whose cells each hold at most one work item. Taking serial \(i\) from a table succeeds when cell \(i\) holds a work item whose priority has serial number \(i\), and returns that item's tree together with the table with cell \(i\) emptied. With fuel \(0\), the loop extracts the minimum \(p\) of \(H\), leaving a heap \(H'\), and takes the serial number of \(p\) from \(T\), obtaining a tree \(t\) and a table \(T'\); it returns \(t\) if \(H'\) is empty and no cell of \(T'\) holds a work item, and fails otherwise. With fuel \(n + 1\), it extracts the minimum \(p_1 = (w_1, s_1)\) of \(H\) and then the minimum \(p_2 = (w_2, s_2)\) of the remaining heap, leaving a heap \(H'\); it takes \(s_1\) from \(T\) and then \(s_2\) from the resulting table, obtaining trees \(t_1\), \(t_2\) and a table \(T'\). It then runs with fuel \(n\), next serial number \(s + 1\), the heap \(H'\) with the priority \(p = (w_1 + w_2, s)\) inserted, and the table \(T'\) with a new last cell holding the work item of priority \(p\) whose tree has left subtree \(t_1\) and right subtree \(t_2\). If any extraction or take fails, the loop fails.

Cslib.Algorithms.Lean.huffmanLoop · 28 lines 
def huffmanLoop {α : Type u} :
    Nat → Nat → MinHeap HuffmanPriority → Array (Option (HuffmanWorkItem α)) →
      Option (HuffmanTree α)
  | 0, _, heap, table =>
      match heap.extractMin with
      | none => none
      | some (priority, restHeap) =>
          match takeSerial? priority.serial table with
          | some (tree, remaining) =>
              if restHeap.data.isEmpty && (huffmanTableForest remaining).isEmpty then
                some tree
              else
                none
          | _ => none
  | fuel + 1, nextSerial, heap, table =>
      match extractTwoMin? heap with
      | none => none
      | some choice =>
          match takeSerial? choice.first.serial table with
          | none => none
          | some (firstTree, afterFirst) =>
              match takeSerial? choice.second.serial afterFirst with
              | none => none
              | some (secondTree, remaining) =>
                  let priority := ⟨choice.first.weight + choice.second.weight, nextSerial⟩
                  let tree := HuffmanTree.fork firstTree secondTree
                  huffmanLoop fuel (nextSerial + 1) (choice.rest.push priority)
                    (remaining.push (some ⟨priority, tree⟩))
Uses 10 · Used by 8
Statement usesHuffman priority · Huffman tree · Result of a two-minimum extraction · Huffman work item · Binary min-heap · Extracting the minimum of a binary min-heap · Insertion into a binary min-heap · Extracting two minima from a Huffman heap · Work forest of a table · Removing a work item by serial
Used byHuffman's algorithm · Huffman's construction fails exactly on empty or repeated-symbol inputs · Huffman's construction succeeds on nonempty inputs with distinct symbols · Indexed reads of a successful Huffman loop · Lookup count of the instrumented Huffman loop · Discarding the lookup count recovers the Huffman loop · Huffman's construction follows a two-minimum merge trace · Huffman's construction keeps the weighted leaves

DefinitionHuffman loop with an accumulated lookup count#✓fully proved

The loop takes a fuel \(n\), a next serial number \(s\), a binary min-heap \(H\) of Huffman priorities, ordered lexicographically by weight and then serial number, a table \(T\) whose cells each hold at most one work item, and a counter \(c\). Taking serial \(i\) from a table succeeds when cell \(i\) holds a work item whose priority has serial number \(i\), and returns that item's tree together with the table with cell \(i\) emptied. With fuel \(0\), the loop extracts the minimum \(p\) of \(H\), leaving a heap \(H'\), and takes the serial number of \(p\) from \(T\), obtaining a tree \(t\) and a table \(T'\); it returns \((t, c + 1)\) if \(H'\) is empty and no cell of \(T'\) holds a work item, and fails otherwise. With fuel \(n + 1\), it extracts the minimum \(p_1 = (w_1, s_1)\) of \(H\) and then the minimum \(p_2 = (w_2, s_2)\) of the remaining heap, leaving a heap \(H'\); it takes \(s_1\) from \(T\) and then \(s_2\) from the resulting table, obtaining trees \(t_1\), \(t_2\) and a table \(T'\). It then runs with fuel \(n\), next serial number \(s + 1\), the heap \(H'\) with the priority \(p = (w_1 + w_2, s)\) inserted, the table \(T'\) with a new last cell holding the work item of priority \(p\) whose tree has left subtree \(t_1\) and right subtree \(t_2\), and counter \(c + 2\). If any extraction or take fails, the loop fails.

The counter thus grows by one for each work item taken from the table. The Huffman loop with lookup count is the case \(c = 0\).

Cslib.Algorithms.Lean.huffmanLoopWithLookupCountAux · 29 lines 
def huffmanLoopWithLookupCountAux {α : Type u} :
    Nat → Nat → MinHeap HuffmanPriority → Array (Option (HuffmanWorkItem α)) →
      Nat → Option (HuffmanTree α × Nat)
  | 0, _, heap, table, count =>
      match heap.extractMin with
      | none => none
      | some (priority, restHeap) =>
          match takeSerial? priority.serial table with
          | some (tree, remaining) =>
              if restHeap.data.isEmpty && (huffmanTableForest remaining).isEmpty then
                some (tree, count + 1)
              else
                none
          | _ => none
  | fuel + 1, nextSerial, heap, table, count =>
      match extractTwoMin? heap with
      | none => none
      | some choice =>
          match takeSerial? choice.first.serial table with
          | none => none
          | some (firstTree, afterFirst) =>
              match takeSerial? choice.second.serial afterFirst with
              | none => none
              | some (secondTree, remaining) =>
                  let priority := ⟨choice.first.weight + choice.second.weight, nextSerial⟩
                  let tree := HuffmanTree.fork firstTree secondTree
                  huffmanLoopWithLookupCountAux fuel (nextSerial + 1)
                    (choice.rest.push priority)
                    (remaining.push (some ⟨priority, tree⟩)) (count + 2)
Uses 10 · Used by 2
Statement usesHuffman priority · Huffman tree · Result of a two-minimum extraction · Huffman work item · Binary min-heap · Extracting the minimum of a binary min-heap · Insertion into a binary min-heap · Extracting two minima from a Huffman heap · Work forest of a table · Removing a work item by serial
Used byHuffman loop with lookup count · Lookup count of the instrumented Huffman loop

DefinitionHuffman loop with lookup count#✓fully proved

For a fuel \(n\), a next serial number \(s\), a binary min-heap \(H\) of Huffman priorities and a table \(T\) whose cells each hold at most one work item, the Huffman loop with lookup count on \((n, s, H, T)\) is the Huffman loop with an accumulated lookup count on \((n, s, H, T)\) started with counter \(0\). It runs the bounded sequence of Huffman merges and counts indexed table lookups, one for each work item taken from the table: two per merge and one at the final step. On success it returns the resulting tree together with the count; otherwise it fails.

The count excludes heap operations, table writes (emptying cells and appending merged work items) and the final check that the table holds no work item.

def huffmanLoopWithLookupCount {α : Type u} :
    Nat → Nat → MinHeap HuffmanPriority → Array (Option (HuffmanWorkItem α)) →
      Option (HuffmanTree α × Nat) :=
  fun fuel nextSerial heap table =>
    huffmanLoopWithLookupCountAux fuel nextSerial heap table 0
Uses 5 · Used by 3
Statement usesHuffman priority · Huffman tree · Huffman work item · Binary min-heap · Huffman loop with an accumulated lookup count
Used byIndexed reads of a successful Huffman loop · Lookup count of the instrumented Huffman loop · Discarding the lookup count recovers the Huffman loop

TheoremLookup count of the instrumented Huffman loop#✓fully proved

For every fuel \(n\), next serial number \(s\), binary min-heap \(H\) of Huffman priorities and table \(T\) whose cells each hold at most one work item, the Huffman loop with lookup count on \((n, s, H, T)\) fails exactly when the bounded Huffman merge loop on \((n, s, H, T)\) fails, and returns \((t, 2n + 1)\) when the merge loop returns the tree \(t\): two indexed table reads for each of the \(n\) merges and one for the final step.

theorem huffmanLoopWithLookupCount_eq {α : Type u} (fuel nextSerial : Nat)
    (heap : MinHeap HuffmanPriority) (table : Array (Option (HuffmanWorkItem α))) :
    huffmanLoopWithLookupCount fuel nextSerial heap table =
      (huffmanLoop fuel nextSerial heap table).map fun tree => (tree, 2 * fuel + 1)
Uses 13 · Used by 2
Statement usesHuffman priority · Huffman tree · Huffman work item · Binary min-heap · Bounded Huffman merge loop · Huffman loop with lookup count
Proof usesResult of a two-minimum extraction · Extracting the minimum of a binary min-heap · Insertion into a binary min-heap · Extracting two minima from a Huffman heap · Huffman loop with an accumulated lookup count · Work forest of a table · Removing a work item by serial
Used byIndexed reads of a successful Huffman loop · Discarding the lookup count recovers the Huffman loop

TheoremDiscarding the lookup count recovers the Huffman loop#✓fully proved

For every fuel \(n\), next serial number \(s\), binary min-heap \(H\) of Huffman priorities and table \(T\) whose cells each hold at most one work item, discarding the count from the result of the Huffman loop with lookup count on \((n, s, H, T)\) gives the result of the bounded Huffman merge loop on \((n, s, H, T)\): the two fail together, and otherwise they return the same tree.

theorem huffmanLoopWithLookupCount_map_fst {α : Type u} (fuel nextSerial : Nat)
    (heap : MinHeap HuffmanPriority) (table : Array (Option (HuffmanWorkItem α))) :
    (huffmanLoopWithLookupCount fuel nextSerial heap table).map Prod.fst =
      huffmanLoop fuel nextSerial heap table
Uses 7
Statement usesHuffman priority · Huffman tree · Huffman work item · Binary min-heap · Bounded Huffman merge loop · Huffman loop with lookup count
Proof usesLookup count of the instrumented Huffman loop

TheoremIndexed reads of a successful Huffman loop#✓fully proved

Let \(k\) be a merge budget, \(n\) a next serial number, \(h\) a binary min-heap of Huffman priorities and \(t\) a serial-indexed table of optional Huffman work items. If the Huffman loop with budget \(k\) on \(n\), \(h\) and \(t\) returns a tree \(T\), then the Huffman loop with lookup counting on the same arguments returns \(T\) together with the count \(2k + 1\) of indexed payload-table reads.

theorem huffmanLoop_lookupCount {α : Type u} {fuel nextSerial : Nat}
    {heap : MinHeap HuffmanPriority} {table : Array (Option (HuffmanWorkItem α))}
    {tree : HuffmanTree α} (hresult : huffmanLoop fuel nextSerial heap table = some tree) :
    huffmanLoopWithLookupCount fuel nextSerial heap table =
      some (tree, 2 * fuel + 1)
Uses 7
Statement usesHuffman priority · Huffman tree · Huffman work item · Binary min-heap · Bounded Huffman merge loop · Huffman loop with lookup count
Proof usesLookup count of the instrumented Huffman loop

DefinitionHuffman's algorithm#✓fully proved

Let \(L\) be a list of \(n\) pairs \((a_0, w_0), \dots, (a_{n-1}, w_{n-1})\) of symbols and natural-number weights, with decidable equality on symbols. The construction fails when \(L\) is empty or two pairs share a symbol. Otherwise it starts from \(n\) leaves, the leaf for \((a_i, w_i)\) having priority (weight \(w_i\), serial \(i\)), and performs \(n - 1\) merges: each merge removes the two trees whose priorities are least in the lexicographic order on (weight, serial), and adds the fork with the first removed tree on the left, with priority the sum of the two weights and the next unused serial \(n, n + 1, \dots\). If exactly one tree then remains, it is returned; otherwise the construction fails.

Ties between equal weights are broken by serial: leaves come before merged trees, leaves in input order and merged trees in creation order.

def huffman {α : Type u} [DecidableEq α]
    (input : List (α × Nat)) : Option (HuffmanTree α) :=
  if input.isEmpty || !(input.map Prod.fst).Nodup then
    none
  else
    let forest := initialHuffmanForest input
    huffmanLoop (input.length - 1) input.length (huffmanHeapOfForest forest)
      (initialHuffmanTable input)
Uses 6 · Used by 7
Statement usesHuffman tree · Huffman work item · Heap of a Huffman work forest · Bounded Huffman merge loop · Initial Huffman forest · Initial Huffman table
Used byHuffman's algorithm minimizes the encoded length · Huffman's construction fails exactly on empty or repeated-symbol inputs · Huffman's construction succeeds on nonempty inputs with distinct symbols · Huffman's construction follows a two-minimum merge trace · Optimality of Huffman coding · Huffman codes are prefix-free · Huffman's construction keeps the weighted leaves

TheoremHuffman's construction keeps the weighted leaves#✓fully proved

Let \(L\) be a list of pairs \((a, w)\) of a symbol \(a\) and a natural-number weight \(w\), with decidable equality on symbols. If the Huffman construction on \(L\) succeeds with a tree \(T\), then the list of weighted leaves of \(T\), read left to right, is a permutation of \(L\).

theorem huffman_weightedLeaves_perm {α : Type u} [DecidableEq α]
    {input : List (α × Nat)} {tree : HuffmanTree α}
    (h : huffman input = some tree) : tree.weightedLeaves.Perm input
Uses 21 · Used by 1
Statement usesHuffman tree · Weighted leaves of a Huffman tree · Huffman's algorithm
Proof usesHuffman priority · Result of a two-minimum extraction · Huffman work item · Binary min-heap · Extracting the minimum of a binary min-heap · Insertion into a binary min-heap · Extracting two minima from a Huffman heap · Weighted leaves of a Huffman work forest · Heap of a Huffman work forest · Bounded Huffman merge loop · Work forest of a table · The initial table holds the initial forest · Appending to the table appends to the forest · Initial Huffman forest · Numbered leaf work items · Initial Huffman table · Removing a work item by serial · Removing a serial removes one work item from the forest
Used byHuffman's algorithm minimizes the encoded length

TheoremHuffman codes are prefix-free#✓fully proved

If the Huffman construction succeeds on a list of weighted symbols and returns a tree \(T\), then the code of \(T\) on its leaf symbols is prefix-free: for any two distinct leaf symbols of \(T\), neither codeword is a prefix of the other.

theorem huffman_prefixFree {α : Type u} [DecidableEq α]
    {input : List (α × Nat)} {tree : HuffmanTree α}
    (_h : huffman input = some tree) :
    MathlibExt.InformationTheory.IsPrefixFree tree.codeOfLeaf
Uses 6
Statement usesHuffman tree · Type of leaf symbols of a Huffman tree · Codeword of a leaf symbol · Huffman's algorithm · Prefix-free code
Proof usesHuffman tree codes are prefix-free

InductiveHuffman weight tree#✓fully proved

A Huffman weight tree is a full binary tree whose leaves carry only real weights: it is either a leaf with a weight \(w \in \mathbb{R}\), or a fork joining a left and a right Huffman weight tree.

inductive HuffmanWeightTree where
  | leaf (weight : Real)
  | fork (left right : HuffmanWeightTree)
deriving Inhabited
Used by 12
Used byWeight at a given depth · Contracting the two least weights · Erasing symbols from a Huffman tree · Contracting a deepest sibling pair · Height of a weight tree · Two-minimum merge costs lower-bound weighted path length · Weighted external path length of a Huffman weight tree · Raising one leaf weight in a bounded-height tree · Raising two leaf weights in a bounded-height tree · Reweighting one leaf occurrence · Total leaf weight of a Huffman weight tree · Multiset of leaf weights

DefinitionMultiset of leaf weights#✓fully proved

The leaf weights of a Huffman weight tree form a multiset of reals that forgets where the leaves sit: a leaf of weight \(w\) gives \(\{w\}\), and a tree with subtrees \(L\) and \(R\) gives the multiset sum of the leaf weights of \(L\) and those of \(R\).

def weights : HuffmanWeightTree → Multiset Real
  | .leaf weight => {weight}
  | .fork left right => left.weights + right.weights
Uses 1 · Used by 8
Statement usesHuffman weight tree
Used byContracting the two least weights · Erasing symbols preserves leaf weights · Contracting a deepest sibling pair · A two-minimum merge trace gives a minimum weighted path length · Two-minimum merge costs lower-bound weighted path length · Raising one leaf weight in a bounded-height tree · Raising two leaf weights in a bounded-height tree · Reweighting one leaf occurrence

DefinitionTotal leaf weight of a Huffman weight tree#✓fully proved

The total weight of a Huffman weight tree is the sum of its leaf weights: a leaf of weight \(w\) has total weight \(w\), and a tree with subtrees \(L\) and \(R\) has total weight equal to the total weight of \(L\) plus that of \(R\).

def totalWeight : HuffmanWeightTree → Real
  | .leaf weight => weight
  | .fork left right => left.totalWeight + right.totalWeight
Uses 1 · Used by 6
Statement usesHuffman weight tree
Used byErasing symbols preserves weighted path length · Erasing symbols preserves total weight · Contracting a deepest sibling pair · Weighted external path length of a Huffman weight tree · Raising one leaf weight in a bounded-height tree · Reweighting one leaf occurrence

DefinitionWeighted external path length of a Huffman weight tree#✓fully proved

For a Huffman weight tree \(T\), write \(w(T)\) for its total leaf weight. The weighted external path length \(P(T)\) of \(T\) is defined by the merge recurrence: a leaf \(T\) has \(P(T) = 0\), and a tree \(T\) with subtrees \(L\) and \(R\) has \(P(T) = P(L) + P(R) + w(L) + w(R)\).

def pathCost : HuffmanWeightTree → Real
  | .leaf _ => 0
  | .fork left right =>
      left.pathCost + right.pathCost + left.totalWeight + right.totalWeight
Uses 2 · Used by 8
Statement usesHuffman weight tree · Total leaf weight of a Huffman weight tree
Used byContracting the two least weights · Erasing symbols preserves weighted path length · Contracting a deepest sibling pair · A two-minimum merge trace gives a minimum weighted path length · Two-minimum merge costs lower-bound weighted path length · Raising one leaf weight in a bounded-height tree · Raising two leaf weights in a bounded-height tree · Reweighting one leaf occurrence

DefinitionHeight of a weight tree#✓fully proved

The height of a weight tree is the number of edges on a longest path from the root to a leaf: a leaf has height \(0\), and a fork with subtrees \(L\) and \(R\) has height \(1 + \max(\mathrm{height}(L), \mathrm{height}(R))\).

def height : HuffmanWeightTree → Nat
  | .leaf _ => 0
  | .fork left right => Nat.succ (max left.height right.height)
Uses 1 · Used by 5
Statement usesHuffman weight tree
Used byContracting the two least weights · Contracting a deepest sibling pair · Raising one leaf weight in a bounded-height tree · Raising two leaf weights in a bounded-height tree · Reweighting one leaf occurrence

InductiveWeight at a given depth#✓fully proved

For a real number \(v\), a weight tree \(T\) and a natural number \(d\), the relation "\(T\) contains \(v\) at depth \(d\)" is defined inductively: the leaf of weight \(v\) contains \(v\) at depth \(0\), and if \(L\) contains \(v\) at depth \(d\) or \(R\) contains \(v\) at depth \(d\), then the fork with left subtree \(L\) and right subtree \(R\) contains \(v\) at depth \(d + 1\). Thus it holds exactly when some leaf of \(T\) of weight \(v\) lies at depth \(d\), the root being at depth \(0\).

inductive ContainsAt (value : Real) : HuffmanWeightTree → Nat → Prop where
  | root : ContainsAt value (.leaf value) 0
  | descendLeft {left right depth}
      (h : ContainsAt value left depth) :
      ContainsAt value (.fork left right) (depth + 1)
  | descendRight {left right depth}
      (h : ContainsAt value right depth) :
      ContainsAt value (.fork left right) (depth + 1)
Uses 1 · Used by 2
Statement usesHuffman weight tree
Used byRaising one leaf weight in a bounded-height tree · Reweighting one leaf occurrence

TheoremReweighting one leaf occurrence#✓fully proved

Suppose a leaf of weight \(v\) occurs at depth \(d\) in a Huffman weight tree \(T\), and let \(r\) be a real number. Then there are a multiset \(R\) of reals and a Huffman weight tree \(T'\) such that the multiset of leaf weights of \(T\) is \(\{v\} + R\), that of \(T'\) is \(\{r\} + R\), the total leaf weight of \(T'\) is that of \(T\) plus \(r - v\), the weighted external path length of \(T'\) is that of \(T\) plus \(d(r - v)\), and \(T'\) has the same height as \(T\).

theorem ContainsAt.reweight {value replacement : Real}
    {tree : HuffmanWeightTree} {depth : Nat}
    (h : ContainsAt value tree depth) :
    ∃ (remainder : Multiset Real) (result : HuffmanWeightTree),
      tree.weights = value ::ₘ remainder ∧
      result.weights = replacement ::ₘ remainder ∧
      result.totalWeight = tree.totalWeight + (replacement - value) ∧
      result.pathCost =
        tree.pathCost + (depth : Real) * (replacement - value) ∧
      result.height = tree.height
Uses 6 · Used by 1
Statement usesHuffman weight tree · Weight at a given depth · Height of a weight tree · Weighted external path length of a Huffman weight tree · Total leaf weight of a Huffman weight tree · Multiset of leaf weights
Used byRaising one leaf weight in a bounded-height tree

TheoremRaising one leaf weight in a bounded-height tree#✓fully proved

Let \(T\) be a Huffman weight tree whose height is at most a natural number \(B\), and write \(W(T)\) for its multiset of leaf weights. Let \(v \le r\) be real numbers and let \(S\) be a multiset of reals with \(\{r\} + W(T) = \{v\} + S\). Then there is a Huffman weight tree \(T'\) with multiset of leaf weights \(S\) and height at most \(B\) whose weighted external path length is at most that of \(T\) plus \(B(r - v)\).

theorem raiseBounded {bound : Nat} (tree : HuffmanWeightTree)
    (hheight : tree.height ≤ bound) (target : Multiset Real)
    (replacement value : Real)
    (hweights : replacement ::ₘ tree.weights = value ::ₘ target)
    (hle : value ≤ replacement) :
    ∃ result : HuffmanWeightTree,
      result.weights = target ∧ result.height ≤ bound ∧
      result.pathCost ≤
        tree.pathCost + (bound : Real) * (replacement - value)
Uses 7 · Used by 1
Statement usesHuffman weight tree · Height of a weight tree · Weighted external path length of a Huffman weight tree · Multiset of leaf weights
Proof usesWeight at a given depth · Reweighting one leaf occurrence · Total leaf weight of a Huffman weight tree
Used byRaising two leaf weights in a bounded-height tree

TheoremRaising two leaf weights in a bounded-height tree#✓fully proved

Let \(T\) be a Huffman weight tree whose height is at most a natural number \(B\), and write \(W(T)\) for its multiset of leaf weights. Let \(f, s, \ell, n\) be real numbers with \(\ell \le n\), \(\ell \le f\) and \(n \le s\), and let \(S\) be a multiset of reals with \(\{f, s\} + W(T) = \{\ell, n\} + S\). Then there is a Huffman weight tree \(T'\) with multiset of leaf weights \(S\) whose weighted external path length is at most that of \(T\) plus \(B(f - \ell) + B(s - n)\).

theorem raisePair {bound : Nat} (tree : HuffmanWeightTree)
    (hheight : tree.height ≤ bound) (target : Multiset Real)
    (first second least next : Real)
    (hweights : first ::ₘ second ::ₘ tree.weights =
      least ::ₘ next ::ₘ target)
    (hleastNext : least ≤ next) (hleastFirst : least ≤ first)
    (hnextSecond : next ≤ second) :
    ∃ result : HuffmanWeightTree,
      result.weights = target ∧
      result.pathCost ≤ tree.pathCost +
        (bound : Real) * (first - least) +
        (bound : Real) * (second - next)
Uses 5 · Used by 1
Statement usesHuffman weight tree · Height of a weight tree · Weighted external path length of a Huffman weight tree · Multiset of leaf weights
Proof usesRaising one leaf weight in a bounded-height tree
Used byContracting the two least weights

TheoremContracting a deepest sibling pair#✓fully proved

Let \(T\) be a weight tree of height \(h \ge 1\). Then there are real numbers \(x\) and \(y\), a multiset \(M\) of real numbers and a real number \(c\) such that the multiset of leaf weights of \(T\) is \(\{x, y\} + M\), the path cost of \(T\) is \(c + hx + hy\), and for every real number \(z\) there is a weight tree \(T'\) of height at most \(h\) whose multiset of leaf weights is \(\{z\} + M\) and whose path cost is \(c + (h - 1)z\).

In the proof, \(x\) and \(y\) are the weights of a deepest pair of sibling leaves of \(T\), and \(T'\) replaces that pair by a single leaf of weight \(z\).

theorem exists_cherry_contraction (tree : HuffmanWeightTree)
    (hpositive : 1 ≤ tree.height) :
    ∃ (first second : Real) (remainder : Multiset Real) (baseCost : Real),
      tree.weights = first ::ₘ second ::ₘ remainder ∧
      tree.pathCost =
        baseCost + (tree.height : Real) * first +
          (tree.height : Real) * second ∧
      ∀ combined : Real, ∃ result : HuffmanWeightTree,
        result.weights = combined ::ₘ remainder ∧
        result.height ≤ tree.height ∧
        result.pathCost =
          baseCost + ((tree.height - 1 : Nat) : Real) * combined
Uses 5 · Used by 1
Statement usesHuffman weight tree · Height of a weight tree · Weighted external path length of a Huffman weight tree · Multiset of leaf weights
Proof usesTotal leaf weight of a Huffman weight tree
Used byContracting the two least weights

TheoremContracting the two least weights#✓fully proved

Let \(T\) be a weight tree, let \(a\) and \(b\) be real numbers and let \(M\) be a multiset of real numbers such that the multiset of leaf weights of \(T\) is \(\{a, b\} + M\), \(a \le b\), and \(b \le w\) for every \(w \in M\). Then there is a weight tree \(T'\) whose multiset of leaf weights is \(\{a + b\} + M\) and whose path cost satisfies \(\mathrm{cost}(T') + a + b \le \mathrm{cost}(T)\), where \(\mathrm{cost}\) denotes path cost.

The proof is a sibling exchange argument on the structural path cost.

theorem contractLeastPair (tree : HuffmanWeightTree) (least next : Real)
    (tail : Multiset Real)
    (htree : tree.weights = least ::ₘ next ::ₘ tail)
    (hleastNext : least ≤ next)
    (htail : ∀ weight ∈ tail, next ≤ weight) :
    ∃ result : HuffmanWeightTree,
      result.weights = (least + next) ::ₘ tail ∧
      result.pathCost + least + next ≤ tree.pathCost
Uses 6 · Used by 1
Statement usesHuffman weight tree · Weighted external path length of a Huffman weight tree · Multiset of leaf weights
Proof usesContracting a deepest sibling pair · Height of a weight tree · Raising two leaf weights in a bounded-height tree
Used byTwo-minimum merge costs lower-bound weighted path length

InductiveTwo-minimum merge trace#✓fully proved

The relation "\(c\) is a two-minimum merge cost of the multiset \(W\) of real weights" is defined inductively by two rules. A singleton multiset \(\{w\}\) has merge cost \(0\). If \(a \le b\), every element of the multiset \(R\) is at least \(b\), and \(c\) is a merge cost of \(\{a + b\} + R\), then \(a + b + c\) is a merge cost of \(\{a, b\} + R\). Thus a merge cost is the total cost of repeatedly replacing two smallest weights by their sum until one weight remains, each merge costing the sum of the two merged weights.

inductive MergeTrace : Multiset Real → Real → Prop where
  | singleton (weight : Real) : MergeTrace {weight} 0
  | merge {least next tailCost : Real} {rest : Multiset Real}
      (hle : least ≤ next)
      (hrest : ∀ weight ∈ rest, next ≤ weight)
      (tailTrace : MergeTrace ((least + next) ::ₘ rest) tailCost) :
      MergeTrace (least ::ₘ next ::ₘ rest) (least + next + tailCost)
Used by 3
Used byHuffman's construction follows a two-minimum merge trace · A two-minimum merge trace gives a minimum weighted path length · Two-minimum merge costs lower-bound weighted path length

TheoremTwo-minimum merge costs lower-bound weighted path length#✓fully proved

Let \(W\) be a multiset of real weights and let \(c\) be a merge cost of \(W\) certified by a two-minimum merge trace. Then every Huffman weight tree whose multiset of leaf weights is \(W\) has weighted external path length at least \(c\).

theorem MergeTrace.le_pathCost {weightBag : Multiset Real} {cost : Real}
    (trace : MergeTrace weightBag cost) (tree : HuffmanWeightTree)
    (htree : tree.weights = weightBag) : cost ≤ tree.pathCost
Uses 5 · Used by 1
Statement usesHuffman weight tree · Two-minimum merge trace · Weighted external path length of a Huffman weight tree · Multiset of leaf weights
Proof usesContracting the two least weights
Used byA two-minimum merge trace gives a minimum weighted path length

DefinitionErasing symbols from a Huffman tree#✓fully proved

Erasing the symbols of a Huffman tree gives the weight tree of the same shape: a leaf with symbol \(s\) and natural-number weight \(w\) becomes the leaf of real weight \(w\), and a fork with subtrees \(L\) and \(R\) becomes the fork whose subtrees are the erasures of \(L\) and \(R\).

def HuffmanTree.eraseSymbols {α : Type u} : HuffmanTree α → HuffmanWeightTree
  | .leaf _ weight => .leaf weight
  | .fork left right => .fork left.eraseSymbols right.eraseSymbols
Uses 2 · Used by 4
Statement usesHuffman tree · Huffman weight tree
Used byErasing symbols preserves weighted path length · Erasing symbols preserves total weight · Erasing symbols preserves leaf weights · A two-minimum merge trace gives a minimum weighted path length

TheoremErasing symbols preserves leaf weights#✓fully proved

For every Huffman tree \(T\), the multiset of leaf weights of the weight tree obtained from \(T\) by erasing its symbols is the multiset of the weights \(w\), viewed as real numbers, over the weighted leaves \((s, w)\) of \(T\).

theorem HuffmanTree.eraseSymbols_weights {α : Type u} (tree : HuffmanTree α) :
    tree.eraseSymbols.weights =
      (tree.weightedLeaves.map (fun pair => (pair.2 : Real)) : Multiset Real)
Uses 4 · Used by 1
Statement usesHuffman tree · Erasing symbols from a Huffman tree · Weighted leaves of a Huffman tree · Multiset of leaf weights
Used byA two-minimum merge trace gives a minimum weighted path length

TheoremErasing symbols preserves total weight#✓fully proved

For every Huffman tree \(T\), the total weight of the weight tree obtained from \(T\) by erasing its symbols equals the total weight of \(T\), viewed as a real number.

theorem HuffmanTree.eraseSymbols_totalWeight {α : Type u} (tree : HuffmanTree α) :
    tree.eraseSymbols.totalWeight = tree.totalWeight
Uses 4 · Used by 1
Statement usesHuffman tree · Erasing symbols from a Huffman tree · Total weight of a Huffman tree · Total leaf weight of a Huffman weight tree
Used byErasing symbols preserves weighted path length

TheoremErasing symbols preserves weighted path length#✓fully proved

For every Huffman tree \(T\), the path cost of the weight tree obtained from \(T\) by erasing its symbols equals the weighted path length of \(T\), viewed as a real number.

theorem HuffmanTree.eraseSymbols_pathCost {α : Type u} (tree : HuffmanTree α) :
    tree.eraseSymbols.pathCost = tree.weightedPathLength
Uses 7 · Used by 1
Statement usesHuffman tree · Erasing symbols from a Huffman tree · Weighted path length · Weighted external path length of a Huffman weight tree
Proof usesErasing symbols preserves total weight · Total weight of a Huffman tree · Total leaf weight of a Huffman weight tree
Used byA two-minimum merge trace gives a minimum weighted path length

DefinitionPriorities of a Huffman work forest#✓fully proved

The priorities of a list of Huffman work items form the multiset consisting of the priority of each item in the list, counted with multiplicity.

def huffmanForestPriorities {α : Type u} (forest : List (HuffmanWorkItem α)) :
    Multiset HuffmanPriority :=
  forest.map HuffmanWorkItem.priority
Uses 2 · Used by 3
Statement usesHuffman priority · Huffman work item
Used byHuffman's construction succeeds on nonempty inputs with distinct symbols · Huffman loop invariant · Huffman's construction follows a two-minimum merge trace

DefinitionWeights of a Huffman work forest#✓fully proved

The weights of a list of Huffman work items form the multiset consisting of the total leaf weight of each item's tree, taken as a real number, counted with multiplicity.

def huffmanForestWeights {α : Type u} (forest : List (HuffmanWorkItem α)) :
    Multiset Real :=
  forest.map (fun item => (item.tree.totalWeight : Real))
Uses 3 · Used by 1
Statement usesHuffman tree · Total weight of a Huffman tree · Huffman work item
Used byHuffman's construction follows a two-minimum merge trace

DefinitionCost of a Huffman work forest#✓fully proved

The cost of a list of Huffman work items is the real number obtained by summing, over the items in the list, the weighted path length of each item's tree.

def huffmanForestCost {α : Type u} (forest : List (HuffmanWorkItem α)) : Real :=
  (forest.map (fun item => (item.tree.weightedPathLength : Real))).sum
Uses 3 · Used by 1
Statement usesHuffman tree · Weighted path length · Huffman work item
Used byHuffman's construction follows a two-minimum merge trace

StructureHuffman loop invariant#✓fully proved

Let \(n\) be a natural number, \(H\) a binary min-heap of Huffman priorities and \(T\) an array of optional Huffman work items, and let \(F\) be the list of work items stored in \(T\), in array order. The invariant holds when the multiset of elements of \(H\) equals the multiset of priorities of the items of \(F\); the serial numbers of the items of \(F\) are pairwise distinct; every item of \(F\) has serial number less than \(n\); every item of \(F\) has priority weight equal to the total leaf weight of its tree; \(T\) has exactly \(n\) cells; and every item of \(F\) is stored in the cell of \(T\) whose index is its serial number.

structure HuffmanLoopInvariant {α : Type u} (nextSerial : Nat)
    (heap : MinHeap HuffmanPriority)
    (table : Array (Option (HuffmanWorkItem α))) : Prop where
  heap_eq : heap.elements = huffmanForestPriorities (huffmanTableForest table)
  serials_nodup :
    ((huffmanTableForest table).map (fun item => item.priority.serial)).Nodup
  serial_lt : ∀ item ∈ huffmanTableForest table, item.priority.serial < nextSerial
  weight_eq : ∀ item ∈ huffmanTableForest table,
    item.priority.weight = item.tree.totalWeight
  size_eq : table.size = nextSerial
  stored : ∀ item ∈ huffmanTableForest table,
    table[item.priority.serial]? = some (some item)
Uses 8 · Used by 2
Statement usesHuffman priority · Huffman tree · Total weight of a Huffman tree · Huffman work item · Binary min-heap · Elements of a binary min-heap · Priorities of a Huffman work forest · Work forest of a table
Used byHuffman's construction succeeds on nonempty inputs with distinct symbols · Huffman's construction follows a two-minimum merge trace

TheoremHuffman's construction follows a two-minimum merge trace#✓fully proved

Let \(L\) be a list of symbol–weight pairs with natural-number weights, over a symbol type with decidable equality, and suppose the Huffman construction returns the tree \(t\) on \(L\). Then the weighted path length of \(t\), as a real number, is the cost of a two-minimum merge trace for the multiset of the weights of \(L\), taken as reals: starting from that multiset, repeatedly replace two weights \(x \le y\) such that every other weight is at least \(y\) by their sum \(x + y\), until a single weight remains; the cost is the sum of all the sums \(x + y\) formed.

theorem huffman_mergeTrace {α : Type u} [DecidableEq α]
    {input : List (α × Nat)} {tree : HuffmanTree α}
    (hresult : huffman input = some tree) :
    HuffmanWeightTree.MergeTrace
      (input.map (fun pair => (pair.2 : Real)) : Multiset Real)
      tree.weightedPathLength
Uses 34 · Used by 1
Statement usesHuffman tree · Weighted path length · Two-minimum merge trace · Huffman's algorithm
Proof usesHuffman loop invariant · Huffman priority · Total weight of a Huffman tree · Result of a two-minimum extraction · Huffman work item · Binary min-heap · Elements of a binary min-heap · Elements after binary heap insertion · Empty binary min-heap · Extracting the minimum of a binary min-heap · Binary heap extraction splits off the minimum · Insertion into a binary min-heap · Extracting two minima from a Huffman heap · Extracting two minima preserves the heap's elements · Two-minimum extraction is greedy · Cost of a Huffman work forest · Priorities of a Huffman work forest · Weights of a Huffman work forest · Heap of a Huffman work forest · Bounded Huffman merge loop · Work forest of a table · The initial table holds the initial forest · Appending to the table appends to the forest · Initial Huffman forest · Numbered leaf work items · Initial Huffman table · Removing a work item by serial · Removing a serial leaves the other table entries unchanged · Removing a serial removes one work item from the forest · Removing a serial preserves the table size
Used byOptimality of Huffman coding

TheoremHuffman's construction succeeds on nonempty inputs with distinct symbols#✓fully proved

Let \(L\) be a nonempty list of symbol–weight pairs with natural-number weights, over a symbol type with decidable equality. If no symbol occurs in \(L\) more than once, then the Huffman construction returns a tree on \(L\).

theorem huffman_isSome {α : Type u} [DecidableEq α] {input : List (α × Nat)}
    (hne : input ≠ []) (hnd : (input.map Prod.fst).Nodup) :
    (huffman input).isSome
Uses 32 · Used by 1
Statement usesHuffman tree · Huffman's algorithm
Proof usesHuffman loop invariant · Huffman priority · Total weight of a Huffman tree · Result of a two-minimum extraction · Huffman work item · Binary min-heap · Elements of a binary min-heap · Elements after binary heap insertion · Empty binary min-heap · Extracting the minimum of a binary min-heap · Binary heap extraction splits off the minimum · Extraction from a binary min-heap fails exactly when it is empty · The value extracted from a binary min-heap is one of its elements · Insertion into a binary min-heap · Extracting two minima from a Huffman heap · Extracting two minima preserves the heap's elements · Priorities of a Huffman work forest · Heap of a Huffman work forest · Bounded Huffman merge loop · Work forest of a table · The initial table holds the initial forest · Appending to the table appends to the forest · Initial Huffman forest · Numbered leaf work items · Initial Huffman table · Removing a work item by serial · Removing a serial leaves the other table entries unchanged · A stored work item can be removed by its serial · Removing a serial removes one work item from the forest · Removing a serial preserves the table size
Used byHuffman's construction fails exactly on empty or repeated-symbol inputs

TheoremHuffman's construction fails exactly on empty or repeated-symbol inputs#✓fully proved

Let \(L\) be a list of symbol–weight pairs with natural-number weights, over a symbol type with decidable equality. The Huffman construction returns no tree on \(L\) if and only if \(L\) is empty or some symbol occurs in \(L\) more than once.

theorem huffman_eq_none_iff {α : Type u} [DecidableEq α]
    {input : List (α × Nat)} :
    huffman input = none ↔ input = [] ∨ ¬(input.map Prod.fst).Nodup
Uses 8
Statement usesHuffman tree · Huffman's algorithm
Proof usesHuffman work item · Heap of a Huffman work forest · Bounded Huffman merge loop · Huffman's construction succeeds on nonempty inputs with distinct symbols · Initial Huffman forest · Initial Huffman table

DefinitionAdmissible Huffman trees#✓fully proved

Given an input list of symbols with natural-number weights, a Huffman tree is admissible for the input when its list of weighted leaves, read from left to right, is a permutation of the input list: the leaves of the tree carry exactly the input's (symbol, weight) pairs, with the same multiplicities.

Every Huffman tree is a full binary tree, so admissibility imposes no further shape condition.

def HuffmanTree.Admissible {α : Type u} (tree : HuffmanTree α)
    (input : List (α × Nat)) : Prop :=
  tree.weightedLeaves.Perm input
Uses 2 · Used by 3
Statement usesHuffman tree · Weighted leaves of a Huffman tree
Used byHuffman's algorithm minimizes the encoded length · Optimality of Huffman coding · A two-minimum merge trace gives a minimum weighted path length

TheoremA two-minimum merge trace gives a minimum weighted path length#✓fully proved

Let \(L\) be a list of symbol–weight pairs with natural-number weights, and let \(t\) and \(t'\) be coding trees with symbols of the same type. Suppose the weighted path length of \(t\), as a real number, is the cost of a two-minimum merge trace for the multiset of the weights of \(L\), taken as reals (repeatedly replace two weights \(x \le y\), with every other weight at least \(y\), by \(x + y\) until one weight remains, the cost being the sum of the sums formed), and that the weighted leaves of \(t'\), listed left to right, are a permutation of \(L\). Then the weighted path length of \(t\) is at most that of \(t'\).

theorem huffman_optimal_of_mergeTrace {α : Type u}
    {input : List (α × Nat)} {tree competitor : HuffmanTree α}
    (htrace : HuffmanWeightTree.MergeTrace
      (input.map (fun pair => (pair.2 : Real)) : Multiset Real)
      tree.weightedPathLength)
    (hcompetitor : competitor.Admissible input) :
    tree.weightedPathLength ≤ competitor.weightedPathLength
Uses 11 · Used by 1
Statement usesHuffman tree · Admissible Huffman trees · Weighted path length · Two-minimum merge trace
Proof usesErasing symbols from a Huffman tree · Erasing symbols preserves weighted path length · Erasing symbols preserves leaf weights · Weighted leaves of a Huffman tree · Two-minimum merge costs lower-bound weighted path length · Weighted external path length of a Huffman weight tree · Multiset of leaf weights
Used byOptimality of Huffman coding

TheoremOptimality of Huffman coding#✓fully proved

Let \(L\) be a list of symbol–weight pairs with natural-number weights, over a symbol type with decidable equality, and suppose the Huffman construction returns the tree \(t\) on \(L\). Then every coding tree \(t'\) (a full binary tree whose leaves carry symbols and weights) whose weighted leaves, listed left to right, form a permutation of \(L\) has weighted path length at least that of \(t\).

theorem huffman_optimal {α : Type u} [DecidableEq α]
    {input : List (α × Nat)} {tree competitor : HuffmanTree α}
    (hresult : huffman input = some tree)
    (hcompetitor : competitor.Admissible input) :
    tree.weightedPathLength ≤ competitor.weightedPathLength
Uses 6 · Used by 1
Statement usesHuffman tree · Admissible Huffman trees · Weighted path length · Huffman's algorithm
Proof usesHuffman's construction follows a two-minimum merge trace · A two-minimum merge trace gives a minimum weighted path length
Used byHuffman's algorithm minimizes the encoded length

TheoremHuffman's algorithm minimizes the encoded length#✓fully proved

Let \(L\) be a list of symbol–weight pairs with natural-number weights, over a symbol type with decidable equality, and suppose Huffman's algorithm returns the tree \(t\) on \(L\). Then every Huffman tree \(t'\) that is admissible for \(L\), that is, whose weighted leaves listed from left to right form a permutation of \(L\), has encoded length at least that of \(t\).

The encoded length charges a lone leaf for a one-bit codeword; when the leaf symbols of a tree are distinct, it equals the encoder's emitted cost, the total weighted codeword length.

theorem huffman_encodedLength_optimal {α : Type u} [DecidableEq α]
    {input : List (α × Nat)} {tree competitor : HuffmanTree α}
    (hresult : huffman input = some tree)
    (hcompetitor : competitor.Admissible input) :
    tree.encodedLength ≤ competitor.encodedLength
Uses 9
Statement usesHuffman tree · Admissible Huffman trees · Encoded length of a coding tree · Huffman's algorithm
Proof usesEncoded length of a fork · Weighted leaves of a Huffman tree · Weighted path length · Optimality of Huffman coding · Huffman's construction keeps the weighted leaves
81 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.