DeflateCodes.lean

Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.

1import Std
2
3/-!
4# Canonical Huffman code assignment
5
6The recurrence and symbol ordering follow RFC 1951 and the reference
7`zlib-formal` proof of `gen_codes`. Values are unbounded natural numbers.
8-/
9
10namespace Zlib.Trees.Math
11
12/-- First canonical code of each length. -/
13def nextCode (bl : Nat → Nat) : Nat → Nat
14  | 0 => 0
15  | b + 1 => (nextCode bl b + bl b) * 2
16
17/-- Number of earlier symbols with the selected length. -/
18def countBefore (len : Nat → Nat) (l n : Nat) : Nat :=
19  ((List.range n).filter (fun m => len m = l)).length
20
21theorem countBefore_succ (len : Nat → Nat) (l n : Nat) :
22    countBefore len l (n + 1) = countBefore len l n + (if len n = l then 1 else 0) := by
23  unfold countBefore
24  rw [List.range_succ, List.filter_append]
25  by_cases h : len n = l <;> simp [h]
26
27@[simp] theorem countBefore_zero (len : Nat → Nat) (l : Nat) : countBefore len l 0 = 0 := rfl
28
29/-- Canonical code before reversal for transmission. -/
30def canonicalCode (bl len : Nat → Nat) (n : Nat) : Nat :=
31  nextCode bl (len n) + countBefore len (len n) n
32
33/-- Reverse exactly the low `k` bits. -/
34def reverseLowBits (c : Nat) : Nat → Nat
35  | 0 => 0
36  | k + 1 => 2 * reverseLowBits c k + (c / 2 ^ k) % 2
37
38theorem reverseLowBits_mod (c k : Nat) :
39    reverseLowBits (c % 2 ^ k) k = reverseLowBits c k := by
40  induction k generalizing c with
41  | zero => rfl
42  | succ k ih =>
43    simp only [reverseLowBits]
44    have h1 : c % 2 ^ (k + 1) % 2 ^ k = c % 2 ^ k := by
45      rw [Nat.pow_succ, Nat.mod_mul_right_mod]
46    have h2 : c % 2 ^ (k + 1) / 2 ^ k % 2 = c / 2 ^ k % 2 := by
47      rw [Nat.pow_succ, Nat.mod_mul_right_div_self, Nat.mod_mod]
48    rw [← ih (c % 2 ^ (k + 1)), h1, ih, h2]
49
50theorem reverseLowBits_mod_of_le (c k m : Nat) (hk : k ≤ m) :
51    reverseLowBits (c % 2 ^ m) k = reverseLowBits c k := by
52  rw [← reverseLowBits_mod (c % 2 ^ m) k, ← reverseLowBits_mod c k]
53  congr 1
54  obtain ⟨d, rfl⟩ : ∃ d, m = k + d := ⟨m - k, by omega⟩
55  rw [Nat.pow_add, Nat.mod_mul_right_mod]
56
57/-- Value stored by zlib for a symbol with positive length. -/
58def storedCode (bl len : Nat → Nat) (n : Nat) : Nat :=
59  reverseLowBits (canonicalCode bl len n) (len n)
60
61
62/-- Reversing exactly k low bits produces a value that fits in k bits. -/
63theorem reverseLowBits_lt (c k : Nat) : reverseLowBits c k < 2 ^ k := by
64  induction k with
65  | zero => simp only [reverseLowBits, Nat.pow_zero]; omega
66  | succ k ih =>
67    rw [reverseLowBits, Nat.pow_succ]
68    have hb : c / 2 ^ k % 2 < 2 := Nat.mod_lt _ (by omega)
69    omega
70
71/-- The value stored for a symbol fits its declared length. This bound
72uses the low-bit reversal alone, and does not assume a valid code count. -/
73theorem storedCode_lt (bl len : Nat → Nat) (n : Nat) : storedCode bl len n < 2 ^ len n :=
74  reverseLowBits_lt _ _
75
76
77/-- Bit i of the reversed value is bit k-1-i of the original value. -/
78theorem reverseLowBits_testBit (c k i : Nat) (hi : i < k) :
79    (reverseLowBits c k).testBit i = c.testBit (k - 1 - i) := by
80  induction k generalizing i with
81  | zero => omega
82  | succ k ih =>
83    have hb : c / 2 ^ k % 2 < 2 ^ 1 := by change c / 2 ^ k % 2 < 2; omega
84    have hbit := Nat.testBit_two_pow_mul_add (reverseLowBits c k) hb i
85    change (2 * reverseLowBits c k + c / 2 ^ k % 2).testBit i = _ at hbit
86    rw [reverseLowBits, hbit]
87    by_cases hi0 : i = 0
88    · subst i
89      rw [ite_eq_left (by omega), show k + 1 - 1 - 0 = k by omega]
90      simp only [Nat.testBit_eq_decide_div_mod_eq, Nat.pow_zero, Nat.div_one, Nat.mod_mod]
91    · rw [ite_eq_right (by omega), ih (i - 1) (by omega)]
92      congr 1
93      omega
94
95/-- Reading a reversed code least-significant bit first gives the original
96code most-significant bit first. -/
97theorem reverseLowBits_wire (c k : Nat) :
98    (List.range k).map (fun i => (reverseLowBits c k).testBit i) =
99      (List.range k).map (fun i => c.testBit (k - 1 - i)) := by
100  apply List.map_congr_left
101  intro i hi
102  exact reverseLowBits_testBit c k i (List.mem_range.mp hi)
103
104end Zlib.Trees.Math