inftrees.c.canon.lean

本页保留 Lean 源码及行号。点击行号可定位语句，点击 import 中的模块名可查看依赖。

1/-!
2# The canonical construction in the list model
3
4Pure mathematics about the lengths `ls`, migrated from an earlier development: the allocation order, the Kraft
5sums `K`, the canonical code values `cv`, `H = rev (L j) (cv j)` (the table index of the first entry of code `j`),
6the group widths of the sub-tables (`look`, `width`) and the closed form `desc` of the table geometry. The names are
7in the namespace `Zlib.Inftrees.Canon` so that they do not clash with the model used by the main proof.
8-/
9
10/-!
11# Bit reversal and the backwards increment of inflate_table
12
13Pure mathematics. `rev k x` reverses the low `k` bits of `x`; inflate_table
14keeps the current canonical code `x` of length `k` bit-reversed in `huff`
15(DEFLATE sends Huffman codes most-significant bit first, while table indices
16are read least-significant bit first). The C "backwards increment" turns
17`rev k x` into `rev k (x + 1)`.
18-/
19set_option autoImplicit false
20
21namespace Zlib.Inftrees.Canon
22
23/-- Reverse the low `k` bits of `x`. -/
24def rev : Nat → Nat → Nat
25  | 0, _ => 0
26  | k + 1, x => rev k (x / 2) + (x % 2) * 2 ^ k
27
28theorem rev_zero (x : Nat) : rev 0 x = 0 := rfl
29
30theorem rev_succ (k x : Nat) : rev (k + 1) x = rev k (x / 2) + (x % 2) * 2 ^ k := rfl
31
32theorem rev_lt (k x : Nat) : rev k x < 2 ^ k := by
33  induction k generalizing x with
34  | zero => simp [rev]
35  | succ k ih =>
36    rw [rev_succ, Nat.pow_succ]
37    have := ih (x / 2)
38    have : x % 2 ≤ 1 := by omega
39    have : (x % 2) * 2 ^ k ≤ 2 ^ k := by
40      calc (x % 2) * 2 ^ k ≤ 1 * 2 ^ k := Nat.mul_le_mul_right _ this
41        _ = 2 ^ k := Nat.one_mul _
42    omega
43
44theorem rev_split (a b x : Nat) :
45    rev (a + b) x = rev a (x / 2 ^ b) + rev b (x % 2 ^ b) * 2 ^ a := by
46  induction b generalizing x with
47  | zero => simp [rev]
48  | succ b ih =>
49    rw [show a + (b + 1) = (a + b) + 1 by omega, rev_succ, ih, rev_succ]
50    have h1 : x / 2 / 2 ^ b = x / 2 ^ (b + 1) := by
51      rw [Nat.div_div_eq_div_mul, Nat.pow_succ, Nat.mul_comm]
52    have h2 : x % 2 ^ (b + 1) / 2 = x / 2 % 2 ^ b := by
53      rw [Nat.pow_succ, Nat.mul_comm, Nat.mod_mul_right_div_self]
54    have h3 : x % 2 ^ (b + 1) % 2 = x % 2 := by
55      rw [Nat.pow_succ, Nat.mod_mul_left_mod]
56    rw [h1, h2, h3, Nat.pow_add 2 a b, Nat.add_mul, Nat.mul_assoc, Nat.mul_comm (2 ^ b) (2 ^ a)]
57    omega
58
59theorem rev_mod (k x : Nat) : rev k (x % 2 ^ k) = rev k x := by
60  induction k generalizing x with
61  | zero => rfl
62  | succ k ih =>
63    rw [rev_succ, rev_succ]
64    have h2 : x % 2 ^ (k + 1) / 2 = x / 2 % 2 ^ k := by
65      rw [Nat.pow_succ, Nat.mul_comm, Nat.mod_mul_right_div_self]
66    have h3 : x % 2 ^ (k + 1) % 2 = x % 2 := by
67      rw [Nat.pow_succ, Nat.mod_mul_left_mod]
68    rw [h2, h3, ih]
69
70theorem rev_of_zero (k : Nat) : rev k 0 = 0 := by
71  induction k with
72  | zero => rfl
73  | succ k ih => simp [rev_succ, ih]
74
75/-- Appending low zero bits (a code shifted left by `d`) adds high zero bits
76to the reversed value. -/
77theorem rev_shift (k d x : Nat) : rev (k + d) (x * 2 ^ d) = rev k x := by
78  rw [rev_split, Nat.mul_div_cancel _ (Nat.two_pow_pos d), Nat.mul_mod_left, rev_of_zero]
79  simp
80
81theorem rev_two_pow (i : Nat) : rev (i + 1) (2 ^ i) = 1 := by
82  have := rev_split 1 i (2 ^ i)
83  rw [show 1 + i = i + 1 by omega] at this
84  rw [this, Nat.div_self (Nat.two_pow_pos i), Nat.mod_self, rev_of_zero]
85  simp [rev]
86
87/-- Bit `k-1-i` of `rev k x` is bit `i` of `x`. -/
88theorem rev_bit (k i x : Nat) (hi : i < k) :
89    rev k x / 2 ^ (k - 1 - i) % 2 = x / 2 ^ i % 2 := by
90  have hs := rev_split (k - 1 - i) (i + 1) x
91  rw [show k - 1 - i + (i + 1) = k by omega] at hs
92  rw [hs]
93  have hlt := rev_lt (k - 1 - i) (x / 2 ^ (i + 1))
94  rw [Nat.add_mul_div_right _ _ (Nat.two_pow_pos _), Nat.div_eq_of_lt hlt, Nat.zero_add]
95  rw [rev_succ]
96  have hlt2 := rev_lt i (x % 2 ^ (i + 1) / 2)
97  have : (x % 2 ^ (i + 1)) % 2 = x / 2 ^ i % 2 ∨ True := Or.inr trivial
98  -- rev (i+1) y % 2 is the top bit of y
99  have htop : ∀ (j y : Nat), y < 2 ^ (j + 1) → rev (j + 1) y % 2 = y / 2 ^ j := by
100    intro j
101    induction j with
102    | zero => intro y hy; simp [rev] at *; omega
103    | succ j ih =>
104      intro y hy
105      rw [rev_succ, Nat.pow_succ]
106      have hy2 : y / 2 < 2 ^ (j + 1) := by
107        rw [Nat.pow_succ] at hy ⊢; omega
108      have := ih (y / 2) hy2
109      have hpar : (rev (j + 1) (y / 2) + y % 2 * (2 ^ j * 2)) % 2 = rev (j + 1) (y / 2) % 2 := by
110        rw [Nat.add_mod]; simp [← Nat.mul_assoc, Nat.mul_mod_left]
111      rw [hpar, this, Nat.div_div_eq_div_mul, Nat.mul_comm]
112  have hy : x % 2 ^ (i + 1) < 2 ^ (i + 1) := Nat.mod_lt _ (Nat.two_pow_pos _)
113  have ht := htop i (x % 2 ^ (i + 1)) hy
114  rw [← rev_succ, ht]
115  rw [Nat.pow_succ, Nat.mod_mul_right_div_self]
116
117/-- Backwards increment, carry case: if bits `0..i-1` of `x` are ones and bit
118`i` is zero (`i < k`), then `rev k (x+1)` keeps the top `k-1-i` reversed bits
119and sets bit `k-1-i`. -/
120theorem rev_succ_of_trailing (k i x : Nat) (hi : i < k)
121    (hlow : x % 2 ^ i = 2 ^ i - 1) (hbit : x / 2 ^ i % 2 = 0) :
122    rev k (x + 1) = rev k x % 2 ^ (k - 1 - i) + 2 ^ (k - 1 - i) := by
123  have hk : k = (k - 1 - i) + (i + 1) := by omega
124  have hs1 := rev_split (k - 1 - i) (i + 1) x
125  have hs2 := rev_split (k - 1 - i) (i + 1) (x + 1)
126  rw [← hk] at hs1 hs2
127  have hp : 0 < 2 ^ i := Nat.two_pow_pos i
128  have hm : x % 2 ^ (i + 1) = 2 ^ i - 1 := by
129    have := Nat.mod_add_div (x % 2 ^ (i + 1)) (2 ^ i)
130    have e1 : x % 2 ^ (i + 1) % 2 ^ i = x % 2 ^ i := by
131      rw [Nat.pow_succ, Nat.mod_mul_right_mod]
132    have e2 : x % 2 ^ (i + 1) / 2 ^ i = x / 2 ^ i % 2 := by
133      rw [Nat.pow_succ, Nat.mod_mul_right_div_self]
134    rw [e1, e2, hbit, hlow] at this
135    omega
136  have hq : (x + 1) / 2 ^ (i + 1) = x / 2 ^ (i + 1) := by
137    have := Nat.div_add_mod x (2 ^ (i + 1))
138    have hp2 : 2 ^ (i + 1) = 2 * 2 ^ i := by rw [Nat.pow_succ, Nat.mul_comm]
139    have : x + 1 = 2 ^ (i + 1) * (x / 2 ^ (i + 1)) + 2 ^ i := by omega
140    rw [this, Nat.mul_add_div (Nat.two_pow_pos _), Nat.div_eq_of_lt (Nat.pow_lt_pow_right (by decide) (by omega))]
141    simp
142  have hr : (x + 1) % 2 ^ (i + 1) = 2 ^ i := by
143    have := Nat.div_add_mod x (2 ^ (i + 1))
144    have hp2 : 2 ^ (i + 1) = 2 * 2 ^ i := by rw [Nat.pow_succ, Nat.mul_comm]
145    have : x + 1 = 2 ^ (i + 1) * (x / 2 ^ (i + 1)) + 2 ^ i := by omega
146    rw [this, Nat.mul_add_mod, Nat.mod_eq_of_lt (Nat.pow_lt_pow_right (by decide) (by omega))]
147  rw [hs2, hq, hr, rev_two_pow, Nat.one_mul, hs1]
148  have hlt := rev_lt (k - 1 - i) (x / 2 ^ (i + 1))
149  rw [Nat.add_mul_mod_self_right, Nat.mod_eq_of_lt hlt]
150
151/-- Backwards increment, overflow case: all `k` bits ones. -/
152theorem rev_all_ones (k x : Nat) (hlow : x % 2 ^ k = 2 ^ k - 1) (hx : x < 2 ^ k) :
153    x + 1 = 2 ^ k := by
154  rw [Nat.mod_eq_of_lt hx] at hlow
155  have := Nat.two_pow_pos k
156  omega
157
158/-- Extending the low run of ones by one bit. -/
159theorem low_ones_succ (x i : Nat) (hlow : x % 2 ^ i = 2 ^ i - 1) (hbit : x / 2 ^ i % 2 = 1) :
160    x % 2 ^ (i + 1) = 2 ^ (i + 1) - 1 := by
161  have := Nat.mod_add_div (x % 2 ^ (i + 1)) (2 ^ i)
162  have e1 : x % 2 ^ (i + 1) % 2 ^ i = x % 2 ^ i := by
163    rw [Nat.pow_succ, Nat.mod_mul_right_mod]
164  have e2 : x % 2 ^ (i + 1) / 2 ^ i = x / 2 ^ i % 2 := by
165    rw [Nat.pow_succ, Nat.mod_mul_right_div_self]
166  rw [e1, e2, hbit, hlow] at this
167  have hp2 : 2 ^ (i + 1) = 2 * 2 ^ i := by rw [Nat.pow_succ, Nat.mul_comm]
168  have := Nat.two_pow_pos i
169  omega
170
171/-! ## Bitwise helpers -/
172
173theorem and_two_pow (x p : Nat) : x &&& 2 ^ p = if x / 2 ^ p % 2 = 1 then 2 ^ p else 0 := by
174  apply Nat.eq_of_testBit_eq
175  intro j
176  rw [Nat.testBit_and, Nat.testBit_two_pow]
177  split
178  · rename_i hb
179    rw [Nat.testBit_two_pow]
180    by_cases hj : p = j
181    · subst hj; simp [Nat.testBit_eq_decide_div_mod_eq, hb]
182    · simp [hj]
183  · rename_i hb
184    simp only [Nat.zero_testBit]
185    by_cases hj : p = j
186    · subst hj; simp [Nat.testBit_eq_decide_div_mod_eq]; omega
187    · simp [hj]
188
189end Zlib.Inftrees.Canon
190
191/-!
192# Allocation order of the code lengths (counting sort in inflate_table)
193
194Pure mathematics, independent of the C translation. For a length vector
195`ls` (entries `0..15`), `symsOf ls l` lists the symbols of length `l` in
196increasing order and `ord ls` concatenates them for `l = 1..15`. This is the
197order in which inflate_table's counting sort leaves the symbols in `work[]`,
198and the order in which its main loop assigns canonical codes.
199-/
200set_option autoImplicit false
201
202namespace Zlib.Inftrees.Canon
203
204/-- Symbols of length `l`, increasing. -/
205def symsOf (ls : List Nat) (l : Nat) : List Nat :=
206  (List.range ls.length).filter fun s => ls.getD s 0 == l
207
208/-- Number of symbols with nonzero length below `l` (`offs[l]` in the C). -/
209def offL (ls : List Nat) (l : Nat) : Nat :=
210  ((List.range l).map fun l' => if l' = 0 then 0 else ls.count l').sum
211
212/-- Allocation order: lengths 1..15, increasing symbol within a length. -/
213def ord (ls : List Nat) : List Nat :=
214  (List.range 15).flatMap fun i => symsOf ls (i + 1)
215
216/-- Number of coded (nonzero-length) symbols. -/
217def nz (ls : List Nat) : Nat := (ord ls).length
218
219/-- `j`-th symbol in allocation order. -/
220def sy (ls : List Nat) (j : Nat) : Nat := (ord ls).getD j 0
221
222/-- Length of the `j`-th symbol in allocation order. -/
223def L (ls : List Nat) (j : Nat) : Nat := ls.getD (sy ls j) 0
224
225/-! ## Filter/count over ranges -/
226
227theorem countP_range_succ (p : Nat → Bool) (k : Nat) :
228    (List.range (k + 1)).countP p = (List.range k).countP p + (if p k then 1 else 0) := by
229  rw [List.range_succ, List.countP_append]
230  simp [List.countP_cons]
231
232theorem filter_range_getElem? (p : Nat → Bool) (n k : Nat) (hk : k < n) (hp : p k = true) :
233    ((List.range n).filter p)[(List.range k).countP p]? = some k := by
234  induction n with
235  | zero => omega
236  | succ n ih =>
237    rw [List.range_succ, List.filter_append]
238    by_cases hkn : k < n
239    · rw [List.getElem?_append_left]
240      · exact ih hkn
241      · have : (List.range k).countP p < (List.range (k + 1)).countP p := by
242          rw [countP_range_succ]; simp [hp]
243        have h2 : (List.range (k + 1)).countP p ≤ (List.range n).countP p := by
244          apply List.Sublist.countP_le
245          exact (List.range_sublist).mpr (by omega)
246        rw [← List.countP_eq_length_filter]
247        omega
248    · have hk' : k = n := by omega
249      subst hk'
250      rw [List.getElem?_append_right (by simp [List.countP_eq_length_filter])]
251      simp [hp, List.countP_eq_length_filter]
252
253theorem filter_range_length (p : Nat → Bool) (n : Nat) :
254    ((List.range n).filter p).length = (List.range n).countP p :=
255  (List.countP_eq_length_filter).symm
256
257theorem countP_range_getD (ls : List Nat) (l k : Nat) (hk : k ≤ ls.length) :
258    (List.range k).countP (fun s => ls.getD s 0 == l) = (ls.take k).count l := by
259  induction k with
260  | zero => simp
261  | succ k ih =>
262    rw [countP_range_succ, ih (by omega)]
263    rw [List.take_add_one]
264    rw [List.count_append]
265    have hk' : k < ls.length := by omega
266    simp [List.getElem?_eq_getElem hk', List.getD_eq_getElem?_getD, List.count_singleton]
267
268theorem symsOf_length (ls : List Nat) (l : Nat) : (symsOf ls l).length = ls.count l := by
269  unfold symsOf
270  rw [filter_range_length, countP_range_getD ls l _ (Nat.le_refl _), List.take_length]
271
272/-- Position of symbol `k` within `symsOf`. -/
273theorem symsOf_getElem? (ls : List Nat) (l k : Nat) (hk : k < ls.length)
274    (hl : ls.getD k 0 = l) : (symsOf ls l)[(ls.take k).count l]? = some k := by
275  unfold symsOf
276  rw [← countP_range_getD ls l k (by omega)]
277  exact filter_range_getElem? _ _ _ hk (by simp only [beq_iff_eq]; exact hl)
278
279theorem mem_symsOf (ls : List Nat) (l s : Nat) :
280    s ∈ symsOf ls l ↔ s < ls.length ∧ ls.getD s 0 = l := by
281  simp [symsOf]
282
283/-! ## flatMap over a range -/
284
285theorem sum_range_le (g : Nat → Nat) (j m : Nat) (h : j ≤ m) :
286    ((List.range j).map g).sum ≤ ((List.range m).map g).sum := by
287  induction m with
288  | zero => have : j = 0 := by omega
289            subst this; exact Nat.le_refl _
290  | succ m ih =>
291    by_cases hj : j = m + 1
292    · subst hj; exact Nat.le_refl _
293    · have := ih (by omega)
294      rw [List.range_succ, List.map_append, List.sum_append]
295      simp only [List.map_cons, List.map_nil, List.sum_cons, List.sum_nil]
296      omega
297
298theorem flatMap_range_getElem? (f : Nat → List Nat) (m j r : Nat) (hj : j < m)
299    (hr : r < (f j).length) :
300    ((List.range m).flatMap f)[((List.range j).map fun i => (f i).length).sum + r]? =
301      (f j)[r]? := by
302  induction m with
303  | zero => omega
304  | succ m ih =>
305    rw [List.range_succ, List.flatMap_append]
306    by_cases hjm : j < m
307    · rw [List.getElem?_append_left]
308      · exact ih hjm
309      · have hsub : ((List.range j).map fun i => (f i).length).sum + (f j).length ≤
310            ((List.range m).flatMap f).length := by
311          rw [List.length_flatMap]
312          have h1 := sum_range_le (fun i => (f i).length) (j + 1) m (by omega)
313          rw [List.range_succ, List.map_append, List.sum_append] at h1
314          simpa using h1
315        omega
316    · have : j = m := by omega
317      subst this
318      rw [List.getElem?_append_right]
319      · simp [List.length_flatMap]
320      · simp [List.length_flatMap]
321
322end Zlib.Inftrees.Canon
323
324
325/-!
326# Length intervals of the allocation order
327
328Pure mathematics: allocation index `j` has length `l` exactly when
329`offL l ≤ j < offL (l+1)`; lengths are nondecreasing along the order; the
330counting sort places symbol `s` of length `l` at `offL l + #{s' < s : ls[s'] = l}`.
331-/
332set_option autoImplicit false
333
334namespace Zlib.Inftrees.Canon
335
336theorem offL_succ (ls : List Nat) (l : Nat) :
337    offL ls (l + 1) = offL ls l + (if l = 0 then 0 else ls.count l) := by
338  unfold offL
339  rw [List.range_succ, List.map_append, List.sum_append]
340  simp
341
342theorem offL_zero (ls : List Nat) : offL ls 0 = 0 := rfl
343theorem offL_one (ls : List Nat) : offL ls 1 = 0 := by simp [offL_succ, offL_zero]
344
345theorem offL_succ_pos (ls : List Nat) {l : Nat} (hl : 1 ≤ l) :
346    offL ls (l + 1) = offL ls l + ls.count l := by
347  rw [offL_succ]; simp; omega
348
349theorem offL_mono (ls : List Nat) {a b : Nat} (h : a ≤ b) : offL ls a ≤ offL ls b := by
350  induction b with
351  | zero => have : a = 0 := by omega
352            subst this; exact Nat.le_refl _
353  | succ b ih =>
354    by_cases hab : a = b + 1
355    · subst hab; exact Nat.le_refl _
356    · have := ih (by omega); rw [offL_succ]; omega
357
358theorem offL_eq_sum (ls : List Nat) (j : Nat) :
359    offL ls (j + 1) = ((List.range j).map fun i => ls.count (i + 1)).sum := by
360  induction j with
361  | zero => exact offL_one ls
362  | succ j ih =>
363    rw [offL_succ_pos ls (by omega), ih, List.range_succ, List.map_append, List.sum_append]
364    simp
365
366theorem nz_eq (ls : List Nat) : nz ls = offL ls 16 := by
367  unfold nz ord
368  rw [List.length_flatMap, offL_eq_sum]
369  simp [symsOf_length]
370
371theorem ord_getElem? (ls : List Nat) (l r : Nat) (hl1 : 1 ≤ l) (hl : l ≤ 15)
372    (hr : r < ls.count l) : (ord ls)[offL ls l + r]? = (symsOf ls l)[r]? := by
373  unfold ord
374  have hj : l - 1 < 15 := by omega
375  have hlen : r < (symsOf ls (l - 1 + 1)).length := by
376    rw [symsOf_length]; rw [show l - 1 + 1 = l by omega]; exact hr
377  have := flatMap_range_getElem? (fun i => symsOf ls (i + 1)) 15 (l - 1) r hj hlen
378  simp only [symsOf_length] at this
379  rw [← offL_eq_sum, show l - 1 + 1 = l by omega] at this
380  exact this
381
382theorem exists_len (ls : List Nat) (j : Nat) (m : Nat) (hj : j < offL ls (m + 1)) :
383    ∃ l, 1 ≤ l ∧ l ≤ m ∧ offL ls l ≤ j ∧ j < offL ls (l + 1) := by
384  induction m with
385  | zero => rw [offL_one] at hj; omega
386  | succ m ih =>
387    by_cases h : j < offL ls (m + 1)
388    · obtain ⟨l, h1, h2, h3, h4⟩ := ih h
389      exact ⟨l, h1, by omega, h3, h4⟩
390    · exact ⟨m + 1, by omega, by omega, by omega, hj⟩
391
392theorem sy_of_interval (ls : List Nat) {j l : Nat} (hl1 : 1 ≤ l) (hl : l ≤ 15)
393    (h1 : offL ls l ≤ j) (h2 : j < offL ls (l + 1)) :
394    sy ls j < ls.length ∧ ls.getD (sy ls j) 0 = l := by
395  rw [offL_succ_pos ls hl1] at h2
396  have hr : j - offL ls l < ls.count l := by omega
397  have hg := ord_getElem? ls l (j - offL ls l) hl1 hl hr
398  rw [show offL ls l + (j - offL ls l) = j by omega] at hg
399  have hlen : j - offL ls l < (symsOf ls l).length := by rw [symsOf_length]; exact hr
400  have hm : (symsOf ls l)[j - offL ls l] ∈ symsOf ls l := List.getElem_mem hlen
401  rw [List.getElem?_eq_getElem hlen] at hg
402  have hsy : sy ls j = (symsOf ls l)[j - offL ls l] := by
403    unfold sy; rw [List.getD_eq_getElem?_getD, hg]; rfl
404  rw [hsy]
405  exact (mem_symsOf ls l _).mp hm
406
407/-- Lengths are bounded by 15 (the C precondition). -/
408def Bounded (ls : List Nat) : Prop := ∀ l ∈ ls, l ≤ 15
409
410theorem count_eq_zero_of_gt (ls : List Nat) (hb : Bounded ls) (l : Nat) (hl : 15 < l) :
411    ls.count l = 0 := by
412  apply List.count_eq_zero_of_not_mem
413  intro hm; have := hb l hm; omega
414
415theorem L_interval (ls : List Nat) {j : Nat} (hj : j < nz ls) :
416    1 ≤ L ls j ∧ L ls j ≤ 15 ∧ offL ls (L ls j) ≤ j ∧ j < offL ls (L ls j + 1) ∧
417      sy ls j < ls.length := by
418  rw [nz_eq] at hj
419  obtain ⟨l, h1, h2, h3, h4⟩ := exists_len ls j 15 hj
420  obtain ⟨hs, hg⟩ := sy_of_interval ls h1 (by omega) h3 h4
421  have : L ls j = l := hg
422  rw [this]
423  exact ⟨h1, h2, h3, h4, hs⟩
424
425theorem L_eq_of_interval (ls : List Nat) {j l : Nat} (hl1 : 1 ≤ l) (hl : l ≤ 15)
426    (h1 : offL ls l ≤ j) (h2 : j < offL ls (l + 1)) : L ls j = l :=
427  (sy_of_interval ls hl1 hl h1 h2).2
428
429theorem L_mono (ls : List Nat) {j j' : Nat} (hjj : j ≤ j') (hj' : j' < nz ls) :
430    L ls j ≤ L ls j' := by
431  obtain ⟨_, _, a3, _, _⟩ := L_interval ls (show j < nz ls by omega)
432  obtain ⟨_, _, _, b4, _⟩ := L_interval ls hj'
433  refine Classical.byContradiction fun hc => ?_
434  have := offL_mono ls (show L ls j' + 1 ≤ L ls j by omega)
435  omega
436
437/-- Indices of codes with length at most `l` are exactly `[0, offL (l+1))`. -/
438theorem lt_offL_iff (ls : List Nat) {j l : Nat} (hj : j < nz ls) :
439    j < offL ls (l + 1) ↔ L ls j ≤ l := by
440  obtain ⟨_, _, a3, a4, _⟩ := L_interval ls hj
441  constructor
442  · intro h
443    refine Classical.byContradiction fun hc => ?_
444    have := offL_mono ls (show l + 1 ≤ L ls j by omega)
445    omega
446  · intro h
447    have := offL_mono ls (show L ls j + 1 ≤ l + 1 by omega)
448    omega
449
450theorem count_take_lt (ls : List Nat) {s l : Nat} (hs : s < ls.length) (hls : ls.getD s 0 = l) :
451    (ls.take s).count l < ls.count l := by
452  have hsplit := congrArg (fun xs : List Nat => xs.count l) (List.take_append_drop s ls)
453  simp only [List.count_append] at hsplit
454  rw [List.drop_eq_getElem_cons hs] at hsplit
455  have : ls[s] = l := by
456    rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hs] at hls; exact hls
457  simp [this, List.count_cons] at hsplit
458  omega
459
460/-- Counting sort position: symbol `s` of length `l` sits at
461`offL l + #{s' < s : ls[s'] = l}`. -/
462theorem sy_sorted (ls : List Nat) {s l : Nat} (hs : s < ls.length) (hl1 : 1 ≤ l) (hl : l ≤ 15)
463    (hls : ls.getD s 0 = l) : sy ls (offL ls l + (ls.take s).count l) = s := by
464  have hr := count_take_lt ls hs hls
465  unfold sy
466  rw [List.getD_eq_getElem?_getD, ord_getElem? ls l _ hl1 hl hr, symsOf_getElem? ls l s hs hls]
467  rfl
468
469end Zlib.Inftrees.Canon
470
471
472/-!
473# Kraft prefix sums and canonical code values along the allocation order
474
475Pure mathematics. `K ls j` is the left-aligned (15-bit) start of the `j`-th
476canonical code; `cv ls j` its numeric code value; `H ls j` the bit-reversed
477value inflate_table keeps in `huff`. `krAt` is the C's left recurrence.
478-/
479set_option autoImplicit false
480
481namespace Zlib.Inftrees.Canon
482
483def K (ls : List Nat) (j : Nat) : Nat := ((List.range j).map fun i => 2 ^ (15 - L ls i)).sum
484
485def cv (ls : List Nat) (j : Nat) : Nat := K ls j / 2 ^ (15 - L ls j)
486
487def H (ls : List Nat) (j : Nat) : Nat := rev (L ls j) (cv ls j)
488
489/-- `krAt l = Σ_{1 ≤ l' ≤ l} count l' * 2^(l - l')`, the C's
490`left <<= 1; left -= count[len]` recurrence with `left = 2^l - krAt l`. -/
491def krAt (ls : List Nat) : Nat → Nat
492  | 0 => 0
493  | l + 1 => 2 * krAt ls l + ls.count (l + 1)
494
495/-- Remaining codes of length `l` at or after allocation index `a`. -/
496def cntGE (ls : List Nat) (a l : Nat) : Nat := offL ls (l + 1) - max a (offL ls l)
497
498theorem K_succ (ls : List Nat) (j : Nat) : K ls (j + 1) = K ls j + 2 ^ (15 - L ls j) := by
499  unfold K; rw [List.range_succ, List.map_append, List.sum_append]; simp
500
501theorem K_zero (ls : List Nat) : K ls 0 = 0 := rfl
502
503theorem K_mono (ls : List Nat) {j j' : Nat} (h : j ≤ j') : K ls j ≤ K ls j' := by
504  induction j' with
505  | zero => have : j = 0 := by omega
506            subst this; exact Nat.le_refl _
507  | succ j' ih =>
508    by_cases hj : j = j' + 1
509    · subst hj; exact Nat.le_refl _
510    · have := ih (by omega); rw [K_succ]; have := Nat.two_pow_pos (15 - L ls j'); omega
511
512theorem K_strict (ls : List Nat) {j j' : Nat} (h : j < j') : K ls j < K ls j' := by
513  have h1 := K_mono ls (show j + 1 ≤ j' by omega)
514  have h2 := K_succ ls j
515  have := Nat.two_pow_pos (15 - L ls j)
516  omega
517
518/-- Prefix sums are multiples of `2^(15-l)` when all earlier lengths are `≤ l`. -/
519theorem dvd_K (ls : List Nat) (j l : Nat) (h : ∀ i < j, L ls i ≤ l) :
520    2 ^ (15 - l) ∣ K ls j := by
521  induction j with
522  | zero => exact Nat.dvd_zero _
523  | succ j ih =>
524    rw [K_succ]
525    refine Nat.dvd_add (ih fun i hi => h i (by omega)) ?_
526    exact Nat.pow_dvd_pow 2 (by have := h j (by omega); omega)
527
528theorem dvd_K_self (ls : List Nat) {j : Nat} (hj : j < nz ls) :
529    2 ^ (15 - L ls j) ∣ K ls j :=
530  dvd_K ls j _ fun i hi => L_mono ls (by omega) hj
531
532/-- Codes of one length are consecutive multiples. -/
533theorem K_offL_add (ls : List Nat) {l : Nat} (hl1 : 1 ≤ l) (hl : l ≤ 15) (r : Nat)
534    (hr : r ≤ ls.count l) : K ls (offL ls l + r) = K ls (offL ls l) + r * 2 ^ (15 - l) := by
535  induction r with
536  | zero => simp
537  | succ r ih =>
538    rw [← Nat.add_assoc, K_succ, ih (by omega)]
539    have h2 : offL ls l + r < offL ls (l + 1) := by rw [offL_succ_pos ls hl1]; omega
540    rw [L_eq_of_interval ls hl1 hl (by omega) h2, Nat.succ_mul]
541    omega
542
543theorem krAt_K (ls : List Nat) (l : Nat) (hl : l ≤ 15) :
544    krAt ls l * 2 ^ (15 - l) = K ls (offL ls (l + 1)) := by
545  induction l with
546  | zero => simp [krAt, offL_one, K_zero]
547  | succ l ih =>
548    rw [krAt, offL_succ_pos ls (show 1 ≤ l + 1 by omega),
549      K_offL_add ls (by omega) hl _ (Nat.le_refl _), ← ih (by omega)]
550    have hp : 2 ^ (15 - l) = 2 * 2 ^ (15 - (l + 1)) := by
551      rw [show 15 - l = (15 - (l + 1)) + 1 by omega, Nat.pow_succ, Nat.mul_comm]
552    rw [hp, Nat.add_mul, Nat.mul_comm 2 (krAt ls l), Nat.mul_assoc]
553
554/-- Total Kraft sum (in units of 2^-15) of the coded symbols. -/
555theorem krAt15 (ls : List Nat) : krAt ls 15 = K ls (nz ls) := by
556  have := krAt_K ls 15 (by omega)
557  simp at this
558  rw [nz_eq]; exact this
559
560theorem krAt_mono (ls : List Nat) (a b : Nat) (h : a ≤ b) :
561    krAt ls a * 2 ^ (b - a) ≤ krAt ls b := by
562  induction b with
563  | zero => have : a = 0 := by omega
564            subst this; simp
565  | succ b ih =>
566    by_cases hab : a = b + 1
567    · subst hab; simp
568    · have := ih (by omega)
569      rw [krAt, show b + 1 - a = (b - a) + 1 by omega, Nat.pow_succ]
570      rw [← Nat.mul_assoc]
571      omega
572
573/-! ## Canonical values -/
574
575theorem cv_mul (ls : List Nat) {j : Nat} (hj : j < nz ls) :
576    cv ls j * 2 ^ (15 - L ls j) = K ls j := Nat.div_mul_cancel (dvd_K_self ls hj)
577
578theorem cv_succ (ls : List Nat) {j : Nat} (hj : j + 1 < nz ls) :
579    cv ls (j + 1) = (cv ls j + 1) * 2 ^ (L ls (j + 1) - L ls j) := by
580  have hm := L_mono ls (show j ≤ j + 1 by omega) hj
581  have h15 := (L_interval ls hj).2.1
582  show K ls (j + 1) / 2 ^ (15 - L ls (j + 1)) = _
583  rw [K_succ, ← cv_mul ls (show j < nz ls by omega)]
584  have hp : 2 ^ (15 - L ls j) = 2 ^ (L ls (j + 1) - L ls j) * 2 ^ (15 - L ls (j + 1)) := by
585    rw [← Nat.pow_add]; congr 1; omega
586  rw [show cv ls j * 2 ^ (15 - L ls j) + 2 ^ (15 - L ls j) = (cv ls j + 1) * 2 ^ (15 - L ls j)
587    by rw [Nat.succ_mul], hp, ← Nat.mul_assoc, Nat.mul_div_cancel _ (Nat.two_pow_pos _)]
588
589theorem H_succ (ls : List Nat) {j : Nat} (hj : j + 1 < nz ls) :
590    H ls (j + 1) = rev (L ls j) (cv ls j + 1) := by
591  have hm := L_mono ls (show j ≤ j + 1 by omega) hj
592  show rev (L ls (j + 1)) (cv ls (j + 1)) = _
593  rw [cv_succ ls hj]
594  have := rev_shift (L ls j) (L ls (j + 1) - L ls j) (cv ls j + 1)
595  rw [show L ls j + (L ls (j + 1) - L ls j) = L ls (j + 1) by omega] at this
596  exact this
597
598theorem H_zero (ls : List Nat) : H ls 0 = 0 := by
599  unfold H cv; rw [K_zero, Nat.zero_div, rev_of_zero]
600
601/-- A valid (not over-subscribed) code has room for every code value. -/
602theorem cv_succ_le (ls : List Nat) {j : Nat} (hj : j < nz ls)
603    (hk : K ls (j + 1) ≤ 2 ^ 15) : cv ls j + 1 ≤ 2 ^ L ls j := by
604  have h15 := (L_interval ls hj).2.1
605  rw [K_succ, ← cv_mul ls hj] at hk
606  have hp : 2 ^ 15 = 2 ^ L ls j * 2 ^ (15 - L ls j) := by rw [← Nat.pow_add]; congr 1; omega
607  rw [hp, show cv ls j * 2 ^ (15 - L ls j) + 2 ^ (15 - L ls j) =
608    (cv ls j + 1) * 2 ^ (15 - L ls j) by rw [Nat.succ_mul]] at hk
609  exact Nat.le_of_mul_le_mul_right hk (Nat.two_pow_pos _)
610
611theorem H_lt (ls : List Nat) (j : Nat) : H ls j < 2 ^ L ls j := rev_lt _ _
612
613/-! ## Remaining counts -/
614
615theorem cntGE_zero (ls : List Nat) {l : Nat} (hl : 1 ≤ l) : cntGE ls 0 l = ls.count l := by
616  unfold cntGE; rw [offL_succ_pos ls hl]; simp
617
618/-- Decrement of `count[len]` after processing allocation index `j`. -/
619theorem cntGE_succ (ls : List Nat) {j l : Nat} (hj : j < nz ls) (hl : 1 ≤ l) :
620    cntGE ls (j + 1) l = if l = L ls j then cntGE ls j l - 1 else cntGE ls j l := by
621  obtain ⟨a1, a2, a3, a4, _⟩ := L_interval ls hj
622  unfold cntGE
623  split
624  · rename_i he; subst he; omega
625  · rename_i hne
626    rcases Nat.lt_or_gt_of_ne hne with hlt | hgt
627    · have := offL_mono ls (show l + 1 ≤ L ls j by omega); omega
628    · have := offL_mono ls (show L ls j + 1 ≤ l by omega); omega
629
630theorem cntGE_self (ls : List Nat) {j : Nat} (hj : j < nz ls) :
631    cntGE ls j (L ls j) = offL ls (L ls j + 1) - j := by
632  obtain ⟨_, _, a3, _, _⟩ := L_interval ls hj
633  unfold cntGE; congr 1; omega
634
635end Zlib.Inftrees.Canon
636
637
638/-!
639# Root groups, the sub-table lookahead and the table descriptor sequence
640
641Pure mathematics. With root width `root`, the codes longer than `root` fall
642into groups by their first `root` bits, `grp j = K j / 2^(15-root)`. When the
643main loop of inflate_table reaches the first code of a group it computes the
644sub-table width with the `count[]` lookahead (`look`), advances `next` past the
645previous table, and grows `used`. `desc ls root mx i` is the
646(drop, curr, base, used, low) state in force while code `i` is written.
647
648For a complete code (`K (nz) = 2^15`) every code of a group fits its
649sub-table: `L i ≤ root + curr` (`look_covers`).
650-/
651set_option autoImplicit false
652
653namespace Zlib.Inftrees.Canon
654
655def grp (ls : List Nat) (root j : Nat) : Nat := K ls j / 2 ^ (15 - root)
656
657/-- The C lookahead
658```c
659while (curr + drop < max) { left -= count[curr + drop]; if (left <= 0) break;
660                            curr++; left <<= 1; }
661```
662with `count[l] = cntGE a l` and a fuel bound. -/
663def look (ls : List Nat) (a root mx : Nat) : Nat → Int → Nat → Nat
664  | c, _, 0 => c
665  | c, left, f + 1 =>
666    if c + root < mx then
667      if left - (cntGE ls a (c + root) : Int) ≤ 0 then c
668      else look ls a root mx (c + 1) (2 * (left - (cntGE ls a (c + root) : Int))) f
669    else c
670
671/-- The sub-table width chosen for a group starting at allocation index `a`. -/
672def width (ls : List Nat) (a root mx : Nat) : Nat :=
673  look ls a root mx (L ls a - root) (2 ^ (L ls a - root) : Nat) 16
674
675structure Desc where
676  drop : Nat
677  curr : Nat
678  base : Nat
679  used : Nat
680  low : Nat
681  deriving Repr
682
683/-- A new sub-table starts at code `i+1`. -/
684def startsAt (ls : List Nat) (root i : Nat) : Prop :=
685  root < L ls (i + 1) ∧ (L ls i ≤ root ∨ grp ls root (i + 1) ≠ grp ls root i)
686
687instance (ls : List Nat) (root i : Nat) : Decidable (startsAt ls root i) := by
688  unfold startsAt; infer_instance
689
690/-- Table descriptor in force while code `i` is written. -/
691def desc (ls : List Nat) (root mx : Nat) : Nat → Desc
692  | 0 => ⟨0, root, 0, 2 ^ root, 2 ^ 32 - 1⟩
693  | i + 1 =>
694    let d := desc ls root mx i
695    if startsAt ls root i then
696      ⟨root, width ls (i + 1) root mx, d.base + 2 ^ d.curr,
697        d.used + 2 ^ width ls (i + 1) root mx, rev root (grp ls root (i + 1))⟩
698    else d
699
700/-! ## Hypotheses shared by the lemmas below -/
701
702/-- Accepted complete code with root in `[min, max]`. -/
703structure CompleteCode (ls : List Nat) (root mx : Nat) : Prop where
704  pos : 0 < nz ls
705  complete : K ls (nz ls) = 2 ^ 15
706  root_pos : 1 ≤ root
707  root_le : root ≤ mx
708  mx_eq : mx = L ls (nz ls - 1)
709  min_le : L ls 0 ≤ root
710
711theorem CompleteCode.L_le_mx {ls : List Nat} {root mx : Nat} (hc : CompleteCode ls root mx)
712    {i : Nat} (hi : i < nz ls) : L ls i ≤ mx := by
713  rw [hc.mx_eq]; exact L_mono ls (by omega) (by have := hc.pos; omega)
714
715theorem CompleteCode.mx_le {ls : List Nat} {root mx : Nat} (hc : CompleteCode ls root mx) :
716    mx ≤ 15 := by
717  rw [hc.mx_eq]; exact (L_interval ls (by have := hc.pos; omega)).2.1
718
719theorem CompleteCode.K_lt {ls : List Nat} {root mx : Nat} (hc : CompleteCode ls root mx)
720    {i : Nat} (hi : i < nz ls) : K ls (i + 1) ≤ 2 ^ 15 := by
721  rw [← hc.complete]; exact K_mono ls (by omega)
722
723theorem grp_lt {ls : List Nat} {root mx : Nat} (hc : CompleteCode ls root mx)
724    {i : Nat} (hi : i < nz ls) : grp ls root i < 2 ^ root := by
725  have hk : K ls i < 2 ^ 15 := by
726    have := hc.K_lt hi; have := K_strict ls (show i < i + 1 by omega); omega
727  have hr15 : root ≤ 15 := Nat.le_trans hc.root_le hc.mx_le
728  have hp : 2 ^ 15 = 2 ^ root * 2 ^ (15 - root) := by rw [← Nat.pow_add]; congr 1; omega
729  unfold grp
730  rw [Nat.div_lt_iff_lt_mul (Nat.two_pow_pos _), ← hp]
731  exact hk
732
733theorem grp_mono (ls : List Nat) (root : Nat) {i j : Nat} (h : i ≤ j) :
734    grp ls root i ≤ grp ls root j :=
735  Nat.div_le_div_right (K_mono ls h)
736
737/-! ## Alignment of group starts -/
738
739/-- A long code that starts a group begins on a root-slot boundary. -/
740theorem start_aligned {ls : List Nat} {root mx : Nat} (hc : CompleteCode ls root mx)
741    {i : Nat} (hi : i + 1 < nz ls) (hs : startsAt ls root i) :
742    K ls (i + 1) = grp ls root (i + 1) * 2 ^ (15 - root) := by
743  have hr15 : root ≤ 15 := Nat.le_trans hc.root_le hc.mx_le
744  obtain ⟨hlong, hcase⟩ := hs
745  by_cases hshort : L ls i ≤ root
746  · have hd : 2 ^ (15 - root) ∣ K ls (i + 1) := by
747      apply dvd_K
748      intro j hj
749      exact Nat.le_trans (L_mono ls (show j ≤ i by omega) (by omega)) hshort
750    unfold grp; exact (Nat.div_mul_cancel hd).symm
751  · have hne : grp ls root (i + 1) ≠ grp ls root i := by
752      rcases hcase with h | h
753      · exact absurd h hshort
754      · exact h
755    have hi' : i < nz ls := by omega
756    have hL15 := (L_interval ls hi').2.1
757    -- u = 2^(15 - L i), U = 2^(15 - root) = t * u
758    have hU : 2 ^ (15 - root) = 2 ^ (L ls i - root) * 2 ^ (15 - L ls i) := by
759      rw [← Nat.pow_add]; congr 1; omega
760    have hKi := cv_mul ls hi'
761    have hKs := K_succ ls i
762    have hq_le : grp ls root (i + 1) * 2 ^ (15 - root) ≤ K ls (i + 1) := Nat.div_mul_le_self _ _
763    have hgi : grp ls root i < grp ls root (i + 1) := by
764      have := grp_mono ls root (show i ≤ i + 1 by omega); omega
765    have hlt : K ls i < grp ls root (i + 1) * 2 ^ (15 - root) := by
766      unfold grp at hgi
767      exact (Nat.div_lt_iff_lt_mul (Nat.two_pow_pos _)).mp hgi
768    -- divide everything by u
769    generalize hu : 2 ^ (15 - L ls i) = u at hU hKi hKs
770    generalize ht : 2 ^ (L ls i - root) = t at hU
771    generalize hq : grp ls root (i + 1) = q at hq_le hlt ⊢
772    have hupos : 0 < u := by rw [← hu]; exact Nat.two_pow_pos _
773    rw [hU] at hq_le hlt
774    rw [hKs, ← hKi] at hq_le
775    rw [← hKi] at hlt
776    rw [hKs, ← hKi, hU]
777    -- q * (t * u) ≤ cv * u + u and cv * u < q * (t * u)
778    have h1 : q * t ≤ cv ls i + 1 := by
779      have : q * t * u ≤ (cv ls i + 1) * u := by
780        rw [Nat.mul_assoc, Nat.succ_mul]; exact hq_le
781      exact Nat.le_of_mul_le_mul_right this hupos
782    have h2 : cv ls i < q * t := by
783      have : cv ls i * u < q * t * u := by rw [Nat.mul_assoc]; exact hlt
784      exact Nat.lt_of_mul_lt_mul_right this
785    have h3 : q * t = cv ls i + 1 := by omega
786    rw [← Nat.mul_assoc, h3, Nat.succ_mul]
787
788end Zlib.Inftrees.Canon
789
790
791/-!
792# The sub-table lookahead covers its group
793
794Pure mathematics. For a complete code, the width `look` chooses for a group
795starting at allocation index `a` accommodates every code of the group, and
796(for the canonical-table bridge) is attained by some code of the group.
797-/
798set_option autoImplicit false
799
800namespace Zlib.Inftrees.Canon
801
802theorem K_range (ls : List Nat) {l x : Nat} (hl1 : 1 ≤ l) (hl : l ≤ 15)
803    (h1 : offL ls l ≤ x) (h2 : x ≤ offL ls (l + 1)) :
804    K ls x = K ls (offL ls l) + (x - offL ls l) * 2 ^ (15 - l) := by
805  have := K_offL_add ls hl1 hl (x - offL ls l) (by rw [offL_succ_pos ls hl1] at h2; omega)
806  rwa [show offL ls l + (x - offL ls l) = x by omega] at this
807
808/-- Coverage by codes from `a` of length `< root + c`. -/
809def cov (ls : List Nat) (a root c : Nat) : Nat := K ls (max a (offL ls (root + c))) - K ls a
810
811theorem cov_step (ls : List Nat) {a root c : Nat} (ha : a < nz ls)
812    (hc : L ls a ≤ root + c) (h15 : root + c ≤ 15) :
813    cov ls a root (c + 1) = cov ls a root c + cntGE ls a (root + c) * 2 ^ (15 - (root + c)) := by
814  obtain ⟨a1, _, _, a4, _⟩ := L_interval ls ha
815  have hl1 : 1 ≤ root + c := by omega
816  have hmono := offL_mono ls (show L ls a + 1 ≤ root + c + 1 by omega)
817  have hmono2 := offL_mono ls (show root + c ≤ root + c + 1 by omega)
818  have hmax1 : max a (offL ls (root + (c + 1))) = offL ls (root + c + 1) := by
819    rw [show root + (c + 1) = root + c + 1 by omega]; omega
820  have hK1 := K_range ls hl1 h15 (x := offL ls (root + c + 1)) hmono2 (Nat.le_refl _)
821  have hK2 := K_range ls hl1 h15 (x := max a (offL ls (root + c))) (by omega) (by omega)
822  have hKa := K_mono ls (show a ≤ max a (offL ls (root + c)) by omega)
823  unfold cov cntGE
824  rw [hmax1, hK1, hK2]
825  have hsub : offL ls (root + c + 1) - offL ls (root + c) =
826      (offL ls (root + c + 1) - max a (offL ls (root + c))) +
827        (max a (offL ls (root + c)) - offL ls (root + c)) := by omega
828  rw [hsub, Nat.add_mul]
829  rw [hK2] at hKa
830  omega
831
832theorem cov_init (ls : List Nat) {a root : Nat} (ha : a < nz ls) (hr : root ≤ L ls a) :
833    cov ls a root (L ls a - root) = 0 := by
834  obtain ⟨_, _, a3, _, _⟩ := L_interval ls ha
835  unfold cov
836  rw [show root + (L ls a - root) = L ls a by omega, show max a (offL ls (L ls a)) = a by omega]
837  simp
838
839theorem look_spec (ls : List Nat) {a root mx : Nat} (ha : a < nz ls) (hmx : mx ≤ 15) :
840    ∀ (f c : Nat) (left : Int), L ls a ≤ root + c → c + root ≤ mx → mx - root - c ≤ f →
841      left * (2 ^ (15 - root - c) : Nat) = ((2 ^ (15 - root) : Nat) : Int) - (cov ls a root c : Int) →
842      0 < left →
843      c ≤ look ls a root mx c left f ∧ look ls a root mx c left f + root ≤ mx ∧
844      (look ls a root mx c left f + root = mx ∨
845        2 ^ (15 - root) ≤ cov ls a root (look ls a root mx c left f + 1)) ∧
846      (c < look ls a root mx c left f →
847        cov ls a root (look ls a root mx c left f) < 2 ^ (15 - root)) := by
848  intro f
849  induction f with
850  | zero =>
851    intro c left h1 h2 h3 _ _
852    simp only [look]
853    exact ⟨Nat.le_refl _, h2, Or.inl (by omega), fun h => absurd h (Nat.lt_irrefl _)⟩
854  | succ f ih =>
855    intro c left h1 h2 h3 hinv hpos
856    simp only [look]
857    by_cases hlt : c + root < mx
858    · rw [ite_eq_left hlt]
859      have hstep := cov_step ls ha h1 (by omega)
860      have hp : (2 ^ (15 - root - c) : Nat) = 2 ^ (15 - (root + c)) := by congr 1; omega
861      -- new left times 2^(15-root-c)
862      have hinv' : (left - (cntGE ls a (c + root) : Int)) * (2 ^ (15 - root - c) : Nat) =
863          ((2 ^ (15 - root) : Nat) : Int) - (cov ls a root (c + 1) : Int) := by
864        have e1 : ((cov ls a root (c + 1) : Nat) : Int) = (cov ls a root c : Int) +
865            (cntGE ls a (root + c) : Int) * ((2 ^ (15 - (root + c)) : Nat) : Int) := by
866          rw [hstep]; push_cast; rfl
867        rw [Int.sub_mul, hinv, e1, show c + root = root + c by omega, hp]
868        generalize (cntGE ls a (root + c) : Int) * ((2 ^ (15 - (root + c)) : Nat) : Int) = M
869        omega
870      by_cases hle : left - (cntGE ls a (c + root) : Int) ≤ 0
871      · rw [ite_eq_left hle]
872        refine ⟨Nat.le_refl _, by omega, Or.inr ?_, fun h => absurd h (Nat.lt_irrefl _)⟩
873        have hnn : (0 : Int) ≤ (2 ^ (15 - root - c) : Nat) := Int.natCast_nonneg _
874        have := Int.mul_le_mul_of_nonneg_right hle hnn
875        rw [hinv'] at this
876        omega
877      · rw [ite_eq_right hle]
878        have hp2 : (2 ^ (15 - root - c) : Nat) = 2 * 2 ^ (15 - root - (c + 1)) := by
879          rw [show 15 - root - c = (15 - root - (c + 1)) + 1 by omega, Nat.pow_succ, Nat.mul_comm]
880        have hinv2 : 2 * (left - (cntGE ls a (c + root) : Int)) * (2 ^ (15 - root - (c + 1)) : Nat) =
881            ((2 ^ (15 - root) : Nat) : Int) - (cov ls a root (c + 1) : Int) := by
882          rw [← hinv', hp2]; push_cast; rw [Int.mul_comm 2, Int.mul_assoc]
883        obtain ⟨r1, r2, r3, r4⟩ := ih (c + 1) _ (by omega) (by omega) (by omega) hinv2 (by omega)
884        refine ⟨by omega, r2, r3, ?_⟩
885        intro _
886        by_cases hcr : c + 1 < look ls a root mx (c + 1) (2 * (left - (cntGE ls a (c + root) : Int))) f
887        · exact r4 hcr
888        · have heq : look ls a root mx (c + 1) (2 * (left - (cntGE ls a (c + root) : Int))) f = c + 1 := by omega
889          rw [heq]
890          have hpos2 : (0 : Int) < (2 ^ (15 - root - c) : Nat) := by
891            exact Int.natCast_pos.mpr (Nat.two_pow_pos _)
892          have := Int.mul_pos (show (0 : Int) < left - (cntGE ls a (c + root) : Int) by omega) hpos2
893          rw [hinv'] at this
894          omega
895    · rw [ite_eq_right hlt]
896      refine ⟨Nat.le_refl _, h2, Or.inl (by omega), fun h => absurd h (Nat.lt_irrefl _)⟩
897
898/-- Result facts for the width of a group starting at `a` (a long code). -/
899theorem width_spec (ls : List Nat) {a root mx : Nat} (ha : a < nz ls) (hmx : mx ≤ 15)
900    (hlong : root < L ls a) (hLmx : L ls a ≤ mx) :
901    L ls a - root ≤ width ls a root mx ∧ width ls a root mx + root ≤ mx ∧
902      (width ls a root mx + root = mx ∨ 2 ^ (15 - root) ≤ cov ls a root (width ls a root mx + 1)) ∧
903      (L ls a - root < width ls a root mx →
904        cov ls a root (width ls a root mx) < 2 ^ (15 - root)) := by
905  unfold width
906  apply look_spec ls ha hmx 16 _ _ (by omega) (by omega) (by omega) _ (by
907    have := Nat.two_pow_pos (L ls a - root); omega)
908  rw [cov_init ls ha (by omega)]
909  have hp : 2 ^ (L ls a - root) * 2 ^ (15 - root - (L ls a - root)) = 2 ^ (15 - root) := by
910    rw [← Nat.pow_add]; congr 1; omega
911  rw [show ((0 : Nat) : Int) = 0 from rfl, Int.sub_zero]
912  exact_mod_cast hp
913
914/-- Every code of the group fits the chosen sub-table width. -/
915theorem look_covers {ls : List Nat} {root mx : Nat} (hc : CompleteCode ls root mx)
916    {a : Nat} (ha : a + 1 < nz ls) (hs : startsAt ls root a) {i : Nat}
917    (hi1 : a + 1 ≤ i) (hi : i < nz ls) (hg : grp ls root i = grp ls root (a + 1)) :
918    L ls i ≤ root + width ls (a + 1) root mx := by
919  have hmx := hc.mx_le
920  obtain ⟨w1, w2, w3, _⟩ := width_spec ls ha hmx hs.1 (hc.L_le_mx ha)
921  rcases w3 with heq | hcov
922  · have := hc.L_le_mx hi; omega
923  · refine Classical.byContradiction fun hcon => ?_
924    have hal := start_aligned hc ha hs
925    have hge : max (a + 1) (offL ls (root + (width ls (a + 1) root mx + 1))) ≤ i := by
926      have : ¬ i < offL ls (root + width ls (a + 1) root mx + 1) := by
927        rw [lt_offL_iff ls hi]; omega
928      rw [show root + (width ls (a + 1) root mx + 1) = root + width ls (a + 1) root mx + 1 by omega]
929      omega
930    have hKi := K_mono ls hge
931    unfold cov at hcov
932    have hka := K_mono ls (show a + 1 ≤ max (a + 1) (offL ls (root + (width ls (a + 1) root mx + 1)))
933      by omega)
934    -- K i ≥ (grp (a+1) + 1) * 2^(15-root), contradicting grp i = grp (a+1)
935    have hK : (grp ls root (a + 1) + 1) * 2 ^ (15 - root) ≤ K ls i := by
936      rw [Nat.succ_mul, ← hal]; omega
937    have : grp ls root (a + 1) + 1 ≤ grp ls root i := by
938      unfold grp
939      exact (Nat.le_div_iff_mul_le (Nat.two_pow_pos _)).mpr hK
940    omega
941
942end Zlib.Inftrees.Canon
943
944
945/-!
946# Properties of the table descriptor sequence
947
948Pure mathematics: shape of `desc` (root table while codes are short; one
949sub-table per group afterwards), `used = base + 2^curr`, monotonicity, and
950the facts the main loop needs for in-bounds writes. Also the reversed group
951index read from `huff & mask`, and `rev` injectivity.
952-/
953set_option autoImplicit false
954
955namespace Zlib.Inftrees.Canon
956
957theorem rev_one (b : Nat) : rev 1 b = b % 2 := by simp [rev]
958
959theorem rev_rev (k x : Nat) : rev k (rev k x) = x % 2 ^ k := by
960  induction k generalizing x with
961  | zero => simp [rev, Nat.mod_one]
962  | succ k ih =>
963    have hs := rev_split 1 k (rev (k + 1) x)
964    rw [show 1 + k = k + 1 by omega] at hs
965    have hlt := rev_lt k (x / 2)
966    have hb : x % 2 < 2 := Nat.mod_lt _ (by decide)
967    have h1 : (rev k (x / 2) + x % 2 * 2 ^ k) / 2 ^ k = x % 2 := by
968      rw [Nat.add_mul_div_right _ _ (Nat.two_pow_pos k), Nat.div_eq_of_lt hlt]; simp
969    have h2 : (rev k (x / 2) + x % 2 * 2 ^ k) % 2 ^ k = rev k (x / 2) := by
970      rw [Nat.add_mul_mod_self_right, Nat.mod_eq_of_lt hlt]
971    rw [hs, rev_one, show rev (k + 1) x = rev k (x / 2) + x % 2 * 2 ^ k from rev_succ k x,
972      h1, h2, ih, Nat.mod_mod, Nat.pow_one]
973    -- x % 2 + (x / 2 % 2^k) * 2 = x % 2^(k+1)
974    have := Nat.mod_add_div (x % 2 ^ (k + 1)) 2
975    have e1 : x % 2 ^ (k + 1) % 2 = x % 2 := by rw [Nat.pow_succ, Nat.mod_mul_left_mod]
976    have e2 : x % 2 ^ (k + 1) / 2 = x / 2 % 2 ^ k := by
977      rw [Nat.pow_succ, Nat.mul_comm, Nat.mod_mul_right_div_self]
978    rw [e1, e2] at this
979    omega
980
981theorem rev_inj {k x y : Nat} (hx : x < 2 ^ k) (hy : y < 2 ^ k) (h : rev k x = rev k y) :
982    x = y := by
983  have := congrArg (rev k) h
984  rw [rev_rev, rev_rev, Nat.mod_eq_of_lt hx, Nat.mod_eq_of_lt hy] at this
985  exact this
986
987/-- `huff & mask` of a long code is the reversed root prefix (its group). -/
988theorem H_mod_root (ls : List Nat) {root j : Nat} (hj : j < nz ls) (hr : root ≤ L ls j) :
989    H ls j % 2 ^ root = rev root (grp ls root j) := by
990  have h15 := (L_interval ls hj).2.1
991  unfold H
992  have hs := rev_split root (L ls j - root) (cv ls j)
993  rw [show root + (L ls j - root) = L ls j by omega] at hs
994  rw [hs, Nat.add_mul_mod_self_right, Nat.mod_eq_of_lt (rev_lt _ _)]
995  congr 1
996  unfold grp cv
997  rw [Nat.div_div_eq_div_mul, ← Nat.pow_add]
998  congr 2; omega
999
1000/-- `huff >> root` of a long code. -/
1001theorem H_div_root (ls : List Nat) {root j : Nat} (hj : j < nz ls) (hr : root ≤ L ls j) :
1002    H ls j / 2 ^ root = rev (L ls j - root) (cv ls j % 2 ^ (L ls j - root)) := by
1003  unfold H
1004  have hs := rev_split root (L ls j - root) (cv ls j)
1005  rw [show root + (L ls j - root) = L ls j by omega] at hs
1006  rw [hs, Nat.add_mul_div_right _ _ (Nat.two_pow_pos _), Nat.div_eq_of_lt (rev_lt _ _)]
1007  simp
1008
1009theorem desc_used (ls : List Nat) (root mx : Nat) (i : Nat) :
1010    (desc ls root mx i).used = (desc ls root mx i).base + 2 ^ (desc ls root mx i).curr := by
1011  induction i with
1012  | zero => simp [desc]
1013  | succ i ih =>
1014    simp only [desc]
1015    split
1016    · simp only; rw [ih]
1017    · exact ih
1018
1019theorem desc_used_mono (ls : List Nat) (root mx : Nat) {i j : Nat} (h : i ≤ j) :
1020    (desc ls root mx i).used ≤ (desc ls root mx j).used := by
1021  induction j with
1022  | zero => have : i = 0 := by omega
1023            subst this; exact Nat.le_refl _
1024  | succ j ih =>
1025    by_cases hij : i = j + 1
1026    · subst hij; exact Nat.le_refl _
1027    · have := ih (by omega)
1028      simp only [desc]
1029      split
1030      · simp only; have := Nat.two_pow_pos (width ls (j + 1) root mx); omega
1031      · exact this
1032
1033theorem desc_short (ls : List Nat) {root mx i : Nat} (hi : i < nz ls) (hs : L ls i ≤ root) :
1034    desc ls root mx i = desc ls root mx 0 := by
1035  induction i with
1036  | zero => rfl
1037  | succ i ih =>
1038    have hm := L_mono ls (show i ≤ i + 1 by omega) hi
1039    simp only [desc]
1040    rw [ite_eq_right (by intro h; exact absurd h.1 (by omega))]
1041    exact ih (by omega) (by omega)
1042
1043/-- A long code's descriptor is the one set up at the start of its group. -/
1044theorem desc_long {ls : List Nat} {root mx : Nat} (hmin : L ls 0 ≤ root) {i : Nat}
1045    (hi : i < nz ls) (hl : root < L ls i) :
1046    ∃ a, a + 1 ≤ i ∧ startsAt ls root a ∧ grp ls root (a + 1) = grp ls root i ∧
1047      (desc ls root mx i).drop = root ∧ (desc ls root mx i).curr = width ls (a + 1) root mx ∧
1048      (desc ls root mx i).low = rev root (grp ls root i) := by
1049  induction i with
1050  | zero => omega
1051  | succ i ih =>
1052    simp only [desc]
1053    by_cases hs : startsAt ls root i
1054    · rw [ite_eq_left hs]
1055      exact ⟨i, Nat.le_refl _, hs, rfl, rfl, rfl, rfl⟩
1056    · rw [ite_eq_right hs]
1057      have hli : root < L ls i ∧ grp ls root (i + 1) = grp ls root i := by
1058        unfold startsAt at hs
1059        refine Classical.byContradiction fun hc => hs ⟨hl, ?_⟩
1060        by_cases h1 : L ls i ≤ root
1061        · exact Or.inl h1
1062        · exact Or.inr fun he => hc ⟨by omega, he⟩
1063      obtain ⟨a, ha, hsa, hga, hd, hc, hlow⟩ := ih (by omega) hli.1
1064      exact ⟨a, by omega, hsa, by rw [hga, hli.2], hd, hc, by rw [hlow, hli.2]⟩
1065
1066/-- Safety core: every code fits the table it is written into. -/
1067theorem desc_fits {ls : List Nat} {root mx : Nat} (hc : CompleteCode ls root mx) {i : Nat}
1068    (hi : i < nz ls) :
1069    (desc ls root mx i).drop ≤ L ls i ∧
1070      L ls i - (desc ls root mx i).drop ≤ (desc ls root mx i).curr ∧
1071      (desc ls root mx i).curr ≤ 15 ∧ (desc ls root mx i).drop ≤ root := by
1072  have hmx := hc.mx_le
1073  have hr15 : root ≤ 15 := Nat.le_trans hc.root_le hmx
1074  by_cases hs : L ls i ≤ root
1075  · rw [desc_short ls hi hs]; simp [desc]; omega
1076  · obtain ⟨a, ha, hsa, hga, hd, hcur, _⟩ := desc_long (mx := mx) hc.min_le hi (by omega)
1077    have hcov := look_covers hc (show a + 1 < nz ls by omega) hsa (show a + 1 ≤ i from ha) hi hga.symm
1078    have hw := width_spec ls (show a + 1 < nz ls by omega) hmx hsa.1 (hc.L_le_mx (by omega))
1079    rw [hd, hcur]
1080    omega
1081
1082end Zlib.Inftrees.Canon