Huffman.lean

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

1import ZlibF.Spec.Format.Huffman
2
3/-!
4# Format meta-theory: canonical Huffman codes are prefix-free
5
6An `Acceptable` code (in fact any code with all lengths at most 15 that `Fits`) is prefix-free.
7Consequence: `decodeSym` does not look beyond the code it finds, so it gives the same symbol on
8any extension of the input (`Ext`).
9-/
10
11namespace ZlibF.Spec
12
13namespace Proofs
14
15/-- `codeStart` grows at least by a factor 2 per length: the codes of length `l + j + 1` start
16after the `(codeStart l + count l) * 2^(j+1)` leaves taken by the codes of length at most `l`. -/
17theorem codeStart_ge (lens : List Nat) (l : Nat) (hl : 1 ≤ l) (j : Nat) :
18    (codeStart lens l + count lens l) * 2 ^ (j + 1) ≤ codeStart lens (l + j + 1) := by
19  induction j with
20  | zero =>
21    have : l ≠ 0 := by omega
22    simp [codeStart, this]
23  | succ j ih =>
24    have e : codeStart lens (l + (j + 1) + 1) =
25        (codeStart lens (l + j + 1) + count lens (l + j + 1)) * 2 := by
26      show codeStart lens (l + j + 1 + 1) = _
27      simp only [codeStart]
28      have : l + j + 1 ≠ 0 := by omega
29      simp
30    rw [e, Nat.pow_succ 2 (j + 1), ← Nat.mul_assoc]
31    omega
32
33theorem natToBitsMSB_length (len v : Nat) : (natToBitsMSB len v).length = len := by
34  simp [natToBitsMSB]
35
36theorem natToBitsMSB_getElem (len v i : Nat) (h : i < (natToBitsMSB len v).length) :
37    (natToBitsMSB len v)[i] = v.testBit (len - 1 - i) := by
38  simp [natToBitsMSB]
39
40/-- If the `l`-bit code of `v` is a prefix of the `l'`-bit code of `v'` (both numbers fit),
41then `v` is the top `l` bits of `v'`. -/
42theorem natToBitsMSB_prefix {l l' v v' : Nat} (hv : v < 2 ^ l) (hv' : v' < 2 ^ l')
43    (h : (natToBitsMSB l v).isPrefixOf (natToBitsMSB l' v') = true) :
44    l ≤ l' ∧ v = v' / 2 ^ (l' - l) := by
45  have hp : natToBitsMSB l v <+: natToBitsMSB l' v' := List.isPrefixOf_iff_prefix.mp h
46  have hlen := hp.length_le
47  rw [natToBitsMSB_length, natToBitsMSB_length] at hlen
48  refine ⟨hlen, ?_⟩
49  rw [← Nat.shiftRight_eq_div_pow]
50  apply Nat.eq_of_testBit_eq
51  intro j
52  rw [Nat.testBit_shiftRight]
53  by_cases hj : j < l
54  · have hi : l - 1 - j < (natToBitsMSB l v).length := by rw [natToBitsMSB_length]; omega
55    have := hp.getElem hi
56    rw [natToBitsMSB_getElem, natToBitsMSB_getElem] at this
57    have e1 : l - 1 - (l - 1 - j) = j := by omega
58    have e2 : l' - 1 - (l - 1 - j) = l' - l + j := by omega
59    rw [e1, e2] at this
60    rw [this, Nat.add_comm]
61  · have h1 : v.testBit j = false := by
62      apply Nat.testBit_lt_two_pow
63      exact Nat.lt_of_lt_of_le hv (Nat.pow_le_pow_right (by omega) (by omega))
64    have h2 : v'.testBit (l' - l + j) = false := by
65      apply Nat.testBit_lt_two_pow
66      exact Nat.lt_of_lt_of_le hv' (Nat.pow_le_pow_right (by omega) (by omega))
67    rw [h1, h2]
68
69/-- Position of a symbol of length `l` among the symbols of length `l`. -/
70abbrev rk (lens : List Nat) (l s : Nat) : Nat :=
71  ((lens.take s).filter (· == l)).length
72
73theorem getD_ne_zero_lt (lens : List Nat) (s : Nat) (hs : lens.getD s 0 ≠ 0) : s < lens.length := by
74  rcases Nat.lt_or_ge s lens.length with h | h
75  · exact h
76  · exfalso; apply hs
77    simp [List.getD_eq_getElem?_getD, List.getElem?_eq_none h]
78
79theorem getD_eq_getElem' (lens : List Nat) (s l : Nat) (h : s < lens.length)
80    (hs : lens.getD s 0 = l) : lens[s] = l := by
81  rw [← hs]; simp [List.getD_eq_getElem?_getD, h]
82
83theorem rk_lt_count (lens : List Nat) (s l : Nat) (hs : lens.getD s 0 = l) (hl : l ≠ 0) :
84    rk lens l s < count lens l := by
85  have hlt : s < lens.length := getD_ne_zero_lt lens s (by omega)
86  have hg := getD_eq_getElem' lens s l hlt hs
87  have e : lens = lens.take s ++ lens.drop s := (List.take_append_drop s lens).symm
88  have hd : lens.drop s = lens[s] :: lens.drop (s + 1) := List.drop_eq_getElem_cons hlt
89  unfold rk count
90  conv => rhs; rw [e, hd]
91  rw [List.filter_append, List.length_append, List.filter_cons]
92  simp [hg]
93
94theorem rk_strict (lens : List Nat) (s s' l : Nat) (hss : s < s') (hs : lens.getD s 0 = l)
95    (hl : l ≠ 0) : rk lens l s < rk lens l s' := by
96  have hlt : s < lens.length := getD_ne_zero_lt lens s (by omega)
97  have hg := getD_eq_getElem' lens s l hlt hs
98  unfold rk
99  obtain ⟨m, rfl⟩ : ∃ m, s' = (s + 1) + m := ⟨s' - (s + 1), by omega⟩
100  rw [List.take_add, List.filter_append, List.length_append, List.take_add_one]
101  simp [List.getElem?_eq_getElem hlt, hg]
102  omega
103
104/-- A code that `Fits` and has lengths at most 15 is prefix-free. -/
105theorem prefixFree {lens : List Nat} (h15 : ∀ x ∈ lens, x ≤ maxCodeLen) (hf : Fits lens)
106    {s s' : Nat} (hs : lens.getD s 0 ≠ 0) (hs' : lens.getD s' 0 ≠ 0)
107    (hp : (codeOf lens s).isPrefixOf (codeOf lens s') = true) : s = s' := by
108  have hlen : ∀ t, lens.getD t 0 ≠ 0 → 1 ≤ lens.getD t 0 ∧ lens.getD t 0 ≤ 15 := by
109    intro t ht
110    refine ⟨by omega, ?_⟩
111    have hl := getD_ne_zero_lt lens t ht
112    have : lens.getD t 0 = lens[t] := by simp [List.getD_eq_getElem?_getD, hl]
113    rw [this]; exact h15 _ (List.getElem_mem hl)
114  have hv : ∀ t l, lens.getD t 0 = l → l ≠ 0 → codeStart lens l + rk lens l t < 2 ^ l := by
115    intro t l hl hl0
116    obtain ⟨h1, h2⟩ := hlen t (by omega)
117    rw [hl] at h1 h2
118    have := hf l (by simp [List.mem_range'_1, maxCodeLen]; omega)
119    have := rk_lt_count lens t l hl hl0
120    omega
121  obtain ⟨l, hl⟩ : ∃ l, lens.getD s 0 = l := ⟨_, rfl⟩
122  obtain ⟨l', hl'⟩ : ∃ l', lens.getD s' 0 = l' := ⟨_, rfl⟩
123  have hl0 : l ≠ 0 := by omega
124  have hl0' : l' ≠ 0 := by omega
125  have hp' : (natToBitsMSB l (codeStart lens l + rk lens l s)).isPrefixOf
126      (natToBitsMSB l' (codeStart lens l' + rk lens l' s')) = true := by
127    simp only [codeOf, hl, hl'] at hp
128    exact hp
129  obtain ⟨hll, hveq⟩ := natToBitsMSB_prefix (hv s l hl hl0) (hv s' l' hl' hl0') hp'
130  have hlen1 : 1 ≤ l := by have := hlen s hs; omega
131  rcases Nat.lt_or_ge l l' with hlt | hge
132  · exfalso
133    obtain ⟨j, hj⟩ : ∃ j, l' = l + j + 1 := ⟨l' - l - 1, by omega⟩
134    have h1 := codeStart_ge lens l hlen1 j
135    have h2 : l' - l = j + 1 := by omega
136    rw [h2] at hveq
137    rw [← hj] at h1
138    have h3 : (codeStart lens l + count lens l) ≤ (codeStart lens l' + rk lens l' s') / 2 ^ (j + 1) := by
139      rw [Nat.le_div_iff_mul_le (Nat.two_pow_pos _)]
140      omega
141    have := rk_lt_count lens s l hl hl0
142    omega
143  · have hll' : l = l' := by omega
144    subst hll'
145    rw [Nat.sub_self, Nat.pow_zero, Nat.div_one] at hveq
146    have hr : rk lens l s = rk lens l s' := by omega
147    refine Classical.byContradiction fun hne => ?_
148    rcases Nat.lt_or_gt_of_ne hne with h | h
149    · have := rk_strict lens s s' l h hl hl0
150      omega
151    · have := rk_strict lens s' s l h hl' hl0
152      omega
153
154/-- The decoder does not read past the code it finds: it gives the same symbol on any
155extension of the input. -/
156def Ext (lens : List Nat) : Prop :=
157  ∀ (inp : List Bool) (s : Nat) (r X : List Bool),
158    decodeSym lens inp = some (s, r) → decodeSym lens (inp ++ X) = some (s, r ++ X)
159
160theorem ext_of_prefixFree {lens : List Nat}
161    (hpf : ∀ {s s' : Nat}, lens.getD s 0 ≠ 0 → lens.getD s' 0 ≠ 0 →
162      (codeOf lens s).isPrefixOf (codeOf lens s') = true → s = s') : Ext lens := by
163  intro inp s r X h
164  unfold decodeSym at h ⊢
165  split at h
166  · rename_i b hb
167    obtain ⟨hb1, as, bs, hsplit, hall⟩ := List.find?_eq_some_iff_append.mp hb
168    simp only [Option.some.injEq, Prod.mk.injEq] at h
169    obtain ⟨rfl, rfl⟩ := h
170    have hb1' := hb1
171    simp only [Bool.and_eq_true, bne_iff_ne, ne_eq] at hb1
172    obtain ⟨hne, hpre⟩ := hb1
173    have hpre' : (codeOf lens b).isPrefixOf (inp ++ X) = true := by
174      have := List.isPrefixOf_iff_prefix.mp hpre
175      exact List.isPrefixOf_iff_prefix.mpr (this.trans (List.prefix_append _ _))
176    have hnd : (as ++ b :: bs).Nodup := by rw [← hsplit]; exact List.nodup_range
177    have hfind : (List.range lens.length).find?
178        (fun s => lens.getD s 0 != 0 && (codeOf lens s).isPrefixOf (inp ++ X)) = some b := by
179      rw [hsplit, List.find?_append]
180      have hnone : as.find? (fun s => lens.getD s 0 != 0 && (codeOf lens s).isPrefixOf (inp ++ X))
181          = none := by
182        rw [List.find?_eq_none]
183        intro a ha
184        simp only [Bool.not_eq_true, Bool.and_eq_false_iff, bne_eq_false_iff_eq]
185        refine Classical.byContradiction fun hc => ?_
186        simp only [not_or, Bool.not_eq_false] at hc
187        have hc1 : lens.getD a 0 ≠ 0 := by simpa using hc.1
188        have hc2 := hc.2
189        have hab : a ≠ b := by
190          intro hab
191          subst hab
192          have := List.nodup_append.mp hnd
193          exact this.2.2 a ha a (List.mem_cons_self) rfl
194        have h1 := List.isPrefixOf_iff_prefix.mp hc2
195        have h2 := List.isPrefixOf_iff_prefix.mp hpre'
196        rcases Nat.le_total (codeOf lens a).length (codeOf lens b).length with hle | hle
197        · exact hab (hpf hc1 hne (List.isPrefixOf_iff_prefix.mpr (List.prefix_of_prefix_length_le h1 h2 hle)))
198        · exact hab (hpf hne hc1 (List.isPrefixOf_iff_prefix.mpr (List.prefix_of_prefix_length_le h2 h1 hle))).symm
199      rw [hnone]
200      have hpb : (lens.getD b 0 != 0 && (codeOf lens b).isPrefixOf (inp ++ X)) = true := by
201        rw [hpre', Bool.and_true]; exact bne_iff_ne.mpr hne
202      rw [Option.none_or]
203      simp only [List.find?_cons, hpb]
204    rw [hfind]
205    have hlenb : lens.getD b 0 ≤ inp.length := by
206      have := (List.isPrefixOf_iff_prefix.mp hpre).length_le
207      simpa [codeOf, natToBitsMSB_length] using this
208    simp only [List.drop_append_of_le_length hlenb]
209  · simp at h
210
211theorem ext_acceptable {k : CodeKind} {lens : List Nat} (h : Acceptable k lens) : Ext lens :=
212  ext_of_prefixFree fun hs hs' hp => prefixFree h.1 h.2.1 hs hs' hp
213
214theorem ext_fixedLit : Ext fixedLitLens :=
215  ext_of_prefixFree fun hs hs' hp =>
216    prefixFree (by decide +kernel) (by decide +kernel) hs hs' hp
217
218theorem ext_fixedDist : Ext fixedDistLens :=
219  ext_of_prefixFree fun hs hs' hp =>
220    prefixFree (by decide +kernel) (by decide +kernel) hs hs' hp
221
222end Proofs
223
224end ZlibF.Spec