Run-length encoding

DefinitionRun-length compression from a pending run#✓fully proved

For a bit \(c\), a natural number \(r\) and a finite bit list \(w\), the compression \(C(c, r, w)\) of \(w\) from the pending run \((c, r)\) is the list of natural numbers defined by recursion on \(w\). If \(w\) is empty, \(C(c, r, w)\) is the one-entry list \((r)\). If \(w\) is a bit \(b\) followed by a list \(w'\), then \(C(c, r, w)\) is \(r\) followed by \(C(\lnot c, 1, w')\) when \(b \ne c\); it is \(255\), then \(0\), followed by \(C(c, 1, w')\) when \(b = c\) and \(r = 255\); otherwise it is \(C(c, r + 1, w')\).

Here \(c\) is the bit of the current run and \(r\) is its length so far.

def compressFrom : Bool → Nat → List Bool → List Nat
  | _, run, [] => [run]
  | old, run, bit :: rest =>
      if bit != old then run :: compressFrom (!old) 1 rest
      else if run = 255 then 255 :: 0 :: compressFrom old 1 rest
      else compressFrom old (run + 1) rest

Used by 4

Used byRun-length compression · Compression from a short pending run emits counts at most 255 · Run-length expansion inverts compression · Expansion recovers the pending run and the input

DefinitionRun-length compression#✓fully proved

The run-length compression of a finite bit list \(w\) is \(C(0, 0, w)\), the compression of \(w\) from an empty pending run of zero bits. It lists the lengths of the maximal runs of \(w\), alternating between zeros and ones and starting with a possibly empty run of zeros; a run of length \(n > 255\) is written as \(255, 0, 255, 0, \dots, 255, 0, m\) with \(1 \le m \le 255\).

def compress (bits : List Bool) : List Nat :=
  compressFrom false 0 bits

Uses 1 · Used by 2

Statement usesRun-length compression from a pending run

Used byRun lengths fit in 8 bits · Run-length expansion inverts compression

DefinitionRun-length expansion from a starting bit#✓fully proved

For a bit \(c\) and a list \((n_1, \dots, n_k)\) of natural numbers, the expansion \(E(c, (n_1, \dots, n_k))\) is the bit list obtained by concatenating, for \(i = 1, \dots, k\) in order, \(n_i\) copies of \(c\) when \(i\) is odd and \(n_i\) copies of \(\lnot c\) when \(i\) is even.

def expandFrom : Bool → List Nat → List Bool
  | _, [] => []
  | bit, count :: rest => List.replicate count bit ++ expandFrom (!bit) rest

Used by 4

Used byRun-length expansion · Run-length expansion inverts compression · Expansion recovers the pending run and the input · Length of an expansion from a starting bit

DefinitionRun-length expansion#✓fully proved

The run-length expansion of a list \((n_1, \dots, n_k)\) of natural numbers is \(E(0, (n_1, \dots, n_k))\), the expansion from the zero bit: the bit list obtained by concatenating, for \(i = 1, \dots, k\) in order, \(n_i\) zeros when \(i\) is odd and \(n_i\) ones when \(i\) is even.

def expand (counts : List Nat) : List Bool :=
  expandFrom false counts

Uses 1 · Used by 2

Statement usesRun-length expansion from a starting bit

Used byRun-length expansion inverts compression · Length of a run-length expansion

TheoremCompression from a short pending run emits counts at most 255#✓fully proved

For every bit \(c\), every natural number \(r \le 255\) and every finite bit list \(w\), every entry of the compression \(C(c, r, w)\) of \(w\) from the pending run \((c, r)\) is at most \(255\).

theorem compressFrom_le (old : Bool) (run : Nat) (legal : run ≤ 255) (bits : List Bool) :
    ∀ count ∈ compressFrom old run bits, count ≤ 255

Uses 1 · Used by 1

Statement usesRun-length compression from a pending run

Used byRun lengths fit in 8 bits

TheoremRun lengths fit in 8 bits#✓fully proved

For every finite bit list \(w\), every entry of the run-length compression of \(w\) is at most \(255\).

theorem compress_le (bits : List Bool) : ∀ count ∈ compress bits, count ≤ 255

Uses 2

Statement usesRun-length compression

Proof usesCompression from a short pending run emits counts at most 255

TheoremLength of an expansion from a starting bit#✓fully proved

For every bit \(c\) and every list \((n_1, \dots, n_k)\) of natural numbers, the expansion \(E(c, (n_1, \dots, n_k))\) has length \(n_1 + \dots + n_k\).

theorem expandFrom_length (bit : Bool) (counts : List Nat) :
    (expandFrom bit counts).length = counts.sum

Uses 1 · Used by 1

Statement usesRun-length expansion from a starting bit

Used byLength of a run-length expansion

TheoremLength of a run-length expansion#✓fully proved

For every list \((n_1, \dots, n_k)\) of natural numbers, the run-length expansion of \((n_1, \dots, n_k)\) has length \(n_1 + \dots + n_k\).

theorem expand_length (counts : List Nat) : (expand counts).length = counts.sum

Uses 2

Statement usesRun-length expansion

Proof usesLength of an expansion from a starting bit

TheoremExpansion recovers the pending run and the input#✓fully proved

For every bit \(c\), every natural number \(r\) and every finite bit list \(w\), the expansion from the starting bit \(c\) of the compression \(C(c, r, w)\) is the list of \(r\) copies of \(c\) followed by \(w\).

theorem expandFrom_compressFrom (old : Bool) (run : Nat) (bits : List Bool) :
    expandFrom old (compressFrom old run bits) = List.replicate run old ++ bits

Uses 2 · Used by 1

Statement usesRun-length compression from a pending run · Run-length expansion from a starting bit

Used byRun-length expansion inverts compression

TheoremRun-length expansion inverts compression#✓fully proved

For every finite bit list \(w\), the run-length expansion of the run-length compression of \(w\) is \(w\).

theorem expand_compress (bits : List Bool) : expand (compress bits) = bits

Uses 5

Statement usesRun-length compression · Run-length expansion

Proof usesRun-length compression from a pending run · Run-length expansion from a starting bit · Expansion recovers the pending run and the input

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.