inftrees.c.math.lean

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

1/-!
2# inftrees.c: the arithmetic of canonical codes
3
4Statements about natural numbers that the proofs about `inflate_table` use: bit reversal (`huff` is the reversed
5canonical code), the step that computes the reversed successor, the Kraft sums, and the canonical code values of
6the symbols sorted by length. Nothing here mentions the heap or the translation.
7-/
8
9namespace Zlib.Inftrees.Proofs
10
11/-! ### Bit reversal -/
12
13/-- The `n` low bits of `v` in reverse order. -/
14def rev : Nat → Nat → Nat
15  | 0, _ => 0
16  | n + 1, v => (v % 2) * 2 ^ n + rev n (v / 2)
17
18theorem rev_lt : ∀ n v, rev n v < 2 ^ n
19  | 0, _ => by simp [rev]
20  | n + 1, v => by
21    have := rev_lt n (v / 2)
22    simp only [rev, Nat.pow_succ]
23    have : v % 2 ≤ 1 := by omega
24    have h2 : v % 2 * 2 ^ n ≤ 2 ^ n := by
25      calc v % 2 * 2 ^ n ≤ 1 * 2 ^ n := Nat.mul_le_mul_right _ this
26        _ = 2 ^ n := by simp
27    omega
28
29theorem rev_mul_pow : ∀ k n w, rev (n + k) (w * 2 ^ k) = rev n w
30  | 0, n, w => by simp
31  | k + 1, n, w => by
32    have e : n + (k + 1) = (n + k) + 1 := by omega
33    rw [e, rev]
34    have h1 : w * 2 ^ (k + 1) % 2 = 0 := by
35      rw [Nat.pow_succ, ← Nat.mul_assoc]; simp [Nat.mul_mod_left]
36    have h2 : w * 2 ^ (k + 1) / 2 = w * 2 ^ k := by
37      rw [Nat.pow_succ, ← Nat.mul_assoc, Nat.mul_div_cancel _ (by omega)]
38    rw [h1, h2, rev_mul_pow k n w]; simp
39
40theorem rev_mod_pow : ∀ d R v, rev (R + d) v % 2 ^ R = rev R (v / 2 ^ d)
41  | 0, R, v => by
42    simp only [Nat.add_zero, Nat.pow_zero, Nat.div_one]
43    exact Nat.mod_eq_of_lt (rev_lt R v)
44  | d + 1, R, v => by
45    have e : R + (d + 1) = (R + d) + 1 := by omega
46    rw [e, rev]
47    have hR : 2 ^ R ∣ 2 ^ (R + d) := Nat.pow_dvd_pow 2 (by omega)
48    have h0 : v % 2 * 2 ^ (R + d) % 2 ^ R = 0 := by
49      apply Nat.mod_eq_zero_of_dvd
50      exact Nat.dvd_trans hR (Nat.dvd_mul_left _ _)
51    rw [Nat.add_mod, h0, Nat.zero_add, Nat.mod_mod, rev_mod_pow d R (v / 2)]
52    rw [Nat.div_div_eq_div_mul, Nat.pow_succ, Nat.mul_comm (2 ^ d) 2]
53
54theorem rev_inj : ∀ n a b, rev n a = rev n b → a % 2 ^ n = b % 2 ^ n
55  | 0, a, b, _ => by simp [Nat.mod_one]
56  | n + 1, a, b, h => by
57    simp only [rev] at h
58    have ha := rev_lt n (a / 2)
59    have hb := rev_lt n (b / 2)
60    have h1 : a % 2 = b % 2 := by
61      have : a % 2 < 2 := by omega
62      have : b % 2 < 2 := by omega
63      rcases (by omega : a % 2 = 0 ∨ a % 2 = 1) with h2 | h2 <;>
64        rcases (by omega : b % 2 = 0 ∨ b % 2 = 1) with h3 | h3 <;>
65        simp [h2, h3] at h <;> omega
66    rw [h1] at h
67    have h2 : rev n (a / 2) = rev n (b / 2) := by omega
68    have := rev_inj n _ _ h2
69    have e : 2 ^ (n + 1) = 2 * 2 ^ n := by rw [Nat.pow_succ, Nat.mul_comm]
70    rw [e, Nat.mod_mul, Nat.mod_mul]
71    rw [h1, this]
72
73
74/-! ### The step of `huff`
75
76`incr = 1U << e; while (huff & incr) incr >>= 1;` ends with `incr = incrLoop huff e` (0 if every bit down to bit 0
77is set). -/
78
79def incrLoop (h : Nat) : Nat → Nat
80  | 0 => if h.testBit 0 then 0 else 1
81  | e + 1 => if h.testBit (e + 1) then incrLoop h e else 2 ^ (e + 1)
82
83theorem incrLoop_mod : ∀ e h, incrLoop h e = incrLoop (h % 2 ^ (e + 1)) e
84  | 0, h => by simp [incrLoop]
85  | e + 1, h => by
86    simp only [incrLoop, Nat.testBit_mod_two_pow]
87    have := incrLoop_mod e h
88    have h2 := incrLoop_mod e (h % 2 ^ (e + 1 + 1))
89    rw [Nat.mod_mod_of_dvd _ (Nat.pow_dvd_pow 2 (by omega))] at h2
90    simp [this, h2]
91
92/-- Adding one to a number of `n + 1` bits, in the reversed representation. -/
93theorem succ_rev : ∀ n v, v < 2 ^ (n + 1) →
94    (v + 1 < 2 ^ (n + 1) → ∃ e ≤ n, incrLoop (rev (n + 1) v) n = 2 ^ e ∧
95        rev (n + 1) v % 2 ^ e + 2 ^ e = rev (n + 1) (v + 1)) ∧
96    (v + 1 = 2 ^ (n + 1) → incrLoop (rev (n + 1) v) n = 0)
97  | 0, v, hv => by
98    refine ⟨fun h1 => ?_, fun h1 => ?_⟩
99    · have : v = 0 := by simp at hv h1; omega
100      subst this
101      refine ⟨0, Nat.le_refl _, ?_, ?_⟩ <;> simp [rev, incrLoop]
102    · have : v = 1 := by simp at h1; omega
103      subst this
104      simp [rev, incrLoop]
105  | n + 1, v, hv => by
106    have hlt := rev_lt (n + 1) (v / 2)
107    have hP : 2 ^ (n + 1 + 1) = 2 * 2 ^ (n + 1) := by rw [Nat.pow_succ, Nat.mul_comm]
108    have hP' : 0 < 2 ^ (n + 1) := Nat.pow_pos (by omega)
109    have hrv : ∀ x, rev (n + 1 + 1) x = x % 2 * 2 ^ (n + 1) + rev (n + 1) (x / 2) := fun x => rfl
110    have ih := succ_rev n (v / 2) (by omega)
111    rcases (by omega : v % 2 = 0 ∨ v % 2 = 1) with h0 | h0
112    · -- the top bit is 0: incr stops at once
113      have hh : rev (n + 1 + 1) v = rev (n + 1) (v / 2) := by rw [hrv, h0]; simp
114      have hbit : (rev (n + 1 + 1) v).testBit (n + 1) = false := by
115        rw [Nat.testBit_eq_decide_div_mod_eq]
116        rw [hh]
117        have : rev (n + 1) (v / 2) / 2 ^ (n + 1) = 0 := Nat.div_eq_of_lt hlt
118        simp [this]
119      have hv1 : rev (n + 1 + 1) (v + 1) = 2 ^ (n + 1) + rev (n + 1) (v / 2) := by
120        rw [hrv]
121        have : (v + 1) % 2 = 1 := by omega
122        have : (v + 1) / 2 = v / 2 := by omega
123        simp [*]
124      refine ⟨fun _ => ⟨n + 1, Nat.le_refl _, ?_, ?_⟩, fun h1 => by omega⟩
125      · simp [incrLoop, hbit]
126      · rw [hv1, hh]
127        have : rev (n + 1) (v / 2) % 2 ^ (n + 1) = rev (n + 1) (v / 2) := Nat.mod_eq_of_lt hlt
128        omega
129    · -- the top bit is 1: look at the lower bits
130      have hh : rev (n + 1 + 1) v = 2 ^ (n + 1) + rev (n + 1) (v / 2) := by rw [hrv, h0]; simp
131      have hbit : (rev (n + 1 + 1) v).testBit (n + 1) = true := by
132        rw [Nat.testBit_eq_decide_div_mod_eq, hh]
133        have : (2 ^ (n + 1) + rev (n + 1) (v / 2)) / 2 ^ (n + 1) = 1 := by
134          rw [Nat.add_comm, Nat.add_div_right _ hP', Nat.div_eq_of_lt hlt]
135        simp [this]
136      have hmod : rev (n + 1 + 1) v % 2 ^ (n + 1) = rev (n + 1) (v / 2) := by
137        rw [hh, Nat.add_comm, Nat.add_mod_right]; exact Nat.mod_eq_of_lt hlt
138      have hloop : incrLoop (rev (n + 1 + 1) v) (n + 1) = incrLoop (rev (n + 1) (v / 2)) n := by
139        simp only [incrLoop, hbit, ite_true]
140        rw [incrLoop_mod n (rev (n + 1 + 1) v), hmod]
141      have hv1 : rev (n + 1 + 1) (v + 1) = rev (n + 1) (v / 2 + 1) := by
142        rw [hrv]
143        have : (v + 1) % 2 = 0 := by omega
144        have : (v + 1) / 2 = v / 2 + 1 := by omega
145        simp [*]
146      refine ⟨fun h1 => ?_, fun h1 => ?_⟩
147      · obtain ⟨e, he, h2, h3⟩ := ih.1 (by omega)
148        refine ⟨e, by omega, by rw [hloop]; exact h2, ?_⟩
149        rw [hv1, ← h3, hh]
150        have hd : 2 ^ e ∣ 2 ^ (n + 1) := Nat.pow_dvd_pow 2 (by omega)
151        rw [Nat.add_mod, Nat.mod_eq_zero_of_dvd hd, Nat.zero_add, Nat.mod_mod]
152      · rw [hloop]; exact ih.2 (by omega)
153
154
155/-! ### The symbols sorted by length
156
157`f s` is the length of symbol `s` (`lens[s]`); the first `n` symbols are the ones the call looks at. -/
158
159section Model
160variable (f : Nat → Nat) (n : Nat)
161
162/-- The symbols below `k` of length `l`, in increasing order. -/
163def fl (l k : Nat) : List Nat := (List.range k).filter (fun s => f s == l)
164
165/-- `count[l]` after the counting loop has looked at the symbols below `n`. -/
166def cnt (l : Nat) : Nat := (fl f l n).length
167
168/-- `work[0 ..]` after the sort loop, for the lengths `1 .. l`: the symbols sorted by (length, symbol). -/
169def wsAux : Nat → List Nat
170  | 0 => []
171  | l + 1 => wsAux l ++ fl f (l + 1) n
172
173/-- The number of symbols of length at most `l` (and at least 1). -/
174def Tc : Nat → Nat
175  | 0 => 0
176  | l + 1 => Tc l + cnt f n (l + 1)
177
178/-- Kraft: `K l = sum_{j <= l} cnt j 2^(l - j)`; `2^l - K l` is the C variable `left` after step `l`. -/
179def Kc : Nat → Nat
180  | 0 => 0
181  | l + 1 => 2 * Kc l + cnt f n (l + 1)
182
183/-- `lens[work[i]]` once the sort loop is done. -/
184def lenAt (i : Nat) : Nat := f ((wsAux f n 15).getD i 0)
185
186/-- The canonical code of the `i`-th symbol in the sorted order (RFC 1951, 3.2.2): the `k`-th of length `l` is
187`2 K(l-1) + k`. -/
188def val (i : Nat) : Nat := 2 * Kc f n (lenAt f n i - 1) + (i - Tc f n (lenAt f n i - 1))
189
190variable {f n}
191
192theorem mem_fl {l k x : Nat} : x ∈ fl f l k ↔ x < k ∧ f x = l := by
193  simp [fl]
194
195theorem wsAux_length : ∀ l, (wsAux f n l).length = Tc f n l
196  | 0 => rfl
197  | l + 1 => by simp [wsAux, Tc, cnt, wsAux_length l]
198
199theorem mem_wsAux : ∀ {l x}, x ∈ wsAux f n l ↔ x < n ∧ 1 ≤ f x ∧ f x ≤ l
200  | 0, x => by simp [wsAux]; omega
201  | l + 1, x => by
202    simp only [wsAux, List.mem_append, mem_fl, mem_wsAux (l := l)]
203    omega
204
205theorem wsAux_split {l L : Nat} (h : l ≤ L) : ∃ rest, wsAux f n L = wsAux f n l ++ rest ∧ ∀ x ∈ rest, l < f x := by
206  obtain ⟨d, rfl⟩ := Nat.exists_eq_add_of_le h
207  induction d with
208  | zero => exact ⟨[], by simp, by simp⟩
209  | succ d ih =>
210    obtain ⟨rest, h1, h2⟩ := ih (by omega)
211    refine ⟨rest ++ fl f (l + d + 1) n, by simp [wsAux, h1], ?_⟩
212    intro x hx
213    rcases List.mem_append.mp hx with hx | hx
214    · exact h2 x hx
215    · have := (mem_fl.mp hx).2; omega
216
217theorem Tc_mono {a b : Nat} (h : a ≤ b) : Tc f n a ≤ Tc f n b := by
218  obtain ⟨d, rfl⟩ := Nat.exists_eq_add_of_le h
219  induction d with
220  | zero => exact Nat.le_refl _
221  | succ d ih =>
222    have := ih (by omega)
223    show Tc f n a ≤ Tc f n (a + d) + cnt f n (a + d + 1)
224    omega
225
226/-- For `i < T 15` and `l <= 15`: the `i`-th symbol has length at most `l` iff `i < T l`. -/
227theorem lenAt_le_iff {i l : Nat} (hl : l ≤ 15) (hi : i < Tc f n 15) : lenAt f n i ≤ l ↔ i < Tc f n l := by
228  obtain ⟨rest, h1, h2⟩ := wsAux_split (f := f) (n := n) hl
229  have hlen : (wsAux f n l).length = Tc f n l := wsAux_length l
230  unfold lenAt
231  rw [h1]
232  by_cases hil : i < Tc f n l
233  · have hi' : i < (wsAux f n l).length := by omega
234    rw [List.getD_eq_getElem?_getD, List.getElem?_append_left hi', List.getElem?_eq_getElem hi']
235    have hm := List.getElem_mem hi'
236    have := (mem_wsAux.mp hm).2.2
237    simp only [Option.getD_some]
238    constructor <;> intro _ <;> omega
239  · have hge : (wsAux f n l).length ≤ i := by omega
240    have hi2 : i - (wsAux f n l).length < rest.length := by
241      have := wsAux_length (f := f) (n := n) 15
242      rw [h1, List.length_append] at this; omega
243    rw [List.getD_eq_getElem?_getD, List.getElem?_append_right hge, List.getElem?_eq_getElem hi2]
244    have hm := List.getElem_mem hi2
245    have := h2 _ hm
246    simp only [Option.getD_some]
247    constructor <;> intro _ <;> omega
248
249theorem lenAt_bounds {i : Nat} (hi : i < Tc f n 15) :
250    1 ≤ lenAt f n i ∧ lenAt f n i ≤ 15 := by
251  have hlen : (wsAux f n 15).length = Tc f n 15 := wsAux_length 15
252  have hm := List.getElem_mem (show i < (wsAux f n 15).length by omega)
253  have := mem_wsAux.mp hm
254  unfold lenAt
255  rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem (by omega)]
256  simp only [Option.getD_some]
257  omega
258
259/-- The block of lengths: `T(l-1) <= i < T l` iff the `i`-th symbol has length `l`. -/
260theorem lenAt_eq_iff {i l : Nat} (hl1 : 1 ≤ l) (hl : l ≤ 15) (hi : i < Tc f n 15) :
261    lenAt f n i = l ↔ Tc f n (l - 1) ≤ i ∧ i < Tc f n l := by
262  have a := lenAt_le_iff (f := f) (n := n) hl hi
263  have b := lenAt_le_iff (f := f) (n := n) (l := l - 1) (by omega) hi
264  omega
265
266theorem lenAt_mono {i j : Nat} (hij : i ≤ j) (hj : j < Tc f n 15) :
267    lenAt f n i ≤ lenAt f n j := by
268  have hi : i < Tc f n 15 := by omega
269  obtain ⟨b1, b2⟩ := lenAt_bounds hj
270  have a := (lenAt_le_iff (f := f) (n := n) (l := lenAt f n j - 1) (by omega) hj)
271  have b := (lenAt_le_iff (f := f) (n := n) (l := lenAt f n j) b2 hi)
272  have c := (lenAt_le_iff (f := f) (n := n) (l := lenAt f n j) b2 hj)
273  by_cases h : lenAt f n i ≤ lenAt f n j
274  · exact h
275  · exfalso
276    -- i is not in the block of lengths <= len j, so j (later) is not either
277    have : ¬ i < Tc f n (lenAt f n j) := fun h' => h (b.mpr h')
278    have := c.mp (Nat.le_refl _)
279    omega
280
281
282theorem Tc_succ' {l : Nat} (hl : 1 ≤ l) : Tc f n l = Tc f n (l - 1) + cnt f n l := by
283  obtain ⟨k, rfl⟩ : ∃ k, l = k + 1 := ⟨l - 1, by omega⟩
284  simp [Tc]
285
286theorem Kc_succ' {l : Nat} (hl : 1 ≤ l) : Kc f n l = 2 * Kc f n (l - 1) + cnt f n l := by
287  obtain ⟨k, rfl⟩ : ∃ k, l = k + 1 := ⟨l - 1, by omega⟩
288  simp [Kc]
289
290theorem Kc_gap : ∀ a d, Tc f n (a + d) = Tc f n a → Kc f n (a + d) = 2 ^ d * Kc f n a
291  | a, 0, _ => by simp
292  | a, d + 1, h => by
293    have m1 := Tc_mono (f := f) (n := n) (show a ≤ a + d by omega)
294    have e : Tc f n (a + d + 1) = Tc f n (a + d) + cnt f n (a + d + 1) := rfl
295    have h1 : Tc f n (a + d) = Tc f n a := by
296      have : a + (d + 1) = a + d + 1 := by omega
297      rw [this] at h; omega
298    have h2 : cnt f n (a + d + 1) = 0 := by
299      have : a + (d + 1) = a + d + 1 := by omega
300      rw [this] at h; omega
301    have ih := Kc_gap a d h1
302    have : a + (d + 1) = a + d + 1 := by omega
303    rw [this]
304    show 2 * Kc f n (a + d) + cnt f n (a + d + 1) = _
305    rw [h2, ih, Nat.pow_succ]
306    have : 2 ^ d * 2 * Kc f n a = 2 * (2 ^ d * Kc f n a) := by rw [Nat.mul_comm (2 ^ d) 2, Nat.mul_assoc]
307    omega
308
309/-- No code overflows its length (RFC 1951; `F-code-fits`). -/
310def Fits (f : Nat → Nat) (n : Nat) : Prop := ∀ l, 1 ≤ l → l ≤ 15 → Kc f n l ≤ 2 ^ l
311
312theorem val_lt (hfit : Fits f n) {i : Nat} (hi : i < Tc f n 15) : val f n i < 2 ^ lenAt f n i := by
313  obtain ⟨b1, b2⟩ := lenAt_bounds (f := f) (n := n) hi
314  have := (lenAt_eq_iff (f := f) (n := n) (l := lenAt f n i) b1 b2 hi).mp rfl
315  have t := Tc_succ' (f := f) (n := n) b1
316  have k := Kc_succ' (f := f) (n := n) b1
317  have := hfit _ b1 b2
318  unfold val
319  omega
320
321theorem val_succ {i : Nat} (hi : i + 1 < Tc f n 15) :
322    val f n (i + 1) = (val f n i + 1) * 2 ^ (lenAt f n (i + 1) - lenAt f n i) := by
323  have hi0 : i < Tc f n 15 := by omega
324  obtain ⟨b1, b2⟩ := lenAt_bounds (f := f) (n := n) hi0
325  obtain ⟨c1, c2⟩ := lenAt_bounds (f := f) (n := n) hi
326  have mono := lenAt_mono (f := f) (n := n) (show i ≤ i + 1 by omega) hi
327  have blk := (lenAt_eq_iff (f := f) (n := n) (l := lenAt f n i) b1 b2 hi0).mp rfl
328  have blk' := (lenAt_eq_iff (f := f) (n := n) (l := lenAt f n (i + 1)) c1 c2 hi).mp rfl
329  have t := Tc_succ' (f := f) (n := n) b1
330  have k := Kc_succ' (f := f) (n := n) b1
331  rcases Nat.eq_or_lt_of_le mono with heq | hlt
332  · rw [heq] at blk ⊢
333    simp only [val, heq, Nat.sub_self, Nat.pow_zero, Nat.mul_one]
334    omega
335  · -- the symbol i is the last of its length
336    have hge : Tc f n (lenAt f n i) ≤ i + 1 := by
337      by_cases hc : Tc f n (lenAt f n i) ≤ i + 1
338      · exact hc
339      · have := (lenAt_le_iff (f := f) (n := n) (l := lenAt f n i) b2 hi).mpr (by omega)
340        omega
341    have hT : Tc f n (lenAt f n (i + 1) - 1) = Tc f n (lenAt f n i) := by
342      have := Tc_mono (f := f) (n := n) (show lenAt f n i ≤ lenAt f n (i + 1) - 1 by omega)
343      omega
344    have hg := Kc_gap (f := f) (n := n) (lenAt f n i) (lenAt f n (i + 1) - 1 - lenAt f n i)
345      (by have e : lenAt f n i + (lenAt f n (i + 1) - 1 - lenAt f n i) = lenAt f n (i + 1) - 1 := by omega
346          rw [e]; exact hT)
347    have e : lenAt f n i + (lenAt f n (i + 1) - 1 - lenAt f n i) = lenAt f n (i + 1) - 1 := by omega
348    rw [e] at hg
349    have ep : lenAt f n (i + 1) - lenAt f n i = (lenAt f n (i + 1) - 1 - lenAt f n i) + 1 := by omega
350    have hKl : Kc f n (lenAt f n i) = 2 * Kc f n (lenAt f n i - 1) + cnt f n (lenAt f n i) := k
351    unfold val
352    rw [ep, Nat.pow_succ, hg, hT]
353    have : i + 1 - Tc f n (lenAt f n i) = 0 := by omega
354    rw [this]
355    have h3 : (2 * Kc f n (lenAt f n i - 1) + (i - Tc f n (lenAt f n i - 1)) + 1) = Kc f n (lenAt f n i) := by omega
356    rw [h3]
357    generalize 2 ^ (lenAt f n (i + 1) - 1 - lenAt f n i) = P
358    generalize Kc f n (lenAt f n i) = KK
359    simp only [Nat.add_zero]
360    rw [Nat.mul_comm KK, Nat.mul_assoc, Nat.mul_left_comm]
361
362/-- The last code of a complete code is all ones. -/
363theorem val_last (hc : Kc f n 15 = 2 ^ 15) {m : Nat} (hm : Tc f n 15 = m + 1) :
364    val f n m + 1 = 2 ^ lenAt f n m := by
365  have hi : m < Tc f n 15 := by omega
366  obtain ⟨b1, b2⟩ := lenAt_bounds (f := f) (n := n) hi
367  have blk := (lenAt_eq_iff (f := f) (n := n) (l := lenAt f n m) b1 b2 hi).mp rfl
368  have t := Tc_succ' (f := f) (n := n) b1
369  have k := Kc_succ' (f := f) (n := n) b1
370  have hTl : Tc f n (lenAt f n m) = Tc f n 15 := by
371    have := Tc_mono (f := f) (n := n) b2
372    omega
373  have hg := Kc_gap (f := f) (n := n) (lenAt f n m) (15 - lenAt f n m)
374    (by have e : lenAt f n m + (15 - lenAt f n m) = 15 := by omega
375        rw [e]; exact hTl.symm)
376  have e : lenAt f n m + (15 - lenAt f n m) = 15 := by omega
377  rw [e, hc] at hg
378  have hp : 2 ^ 15 = 2 ^ (15 - lenAt f n m) * 2 ^ lenAt f n m := by
379    rw [← Nat.pow_add]; congr 1; omega
380  have hpos : 0 < 2 ^ (15 - lenAt f n m) := Nat.pow_pos (by omega)
381  have hK : Kc f n (lenAt f n m) = 2 ^ lenAt f n m := by
382    rw [hp] at hg
383    exact (Nat.eq_of_mul_eq_mul_left hpos hg).symm
384  unfold val
385  omega
386
387
388/-- `count[l]` once the symbols before the `i`-th (in the sorted order) have been taken off. -/
389def rem (f : Nat → Nat) (n i l : Nat) : Nat := Tc f n l - max i (Tc f n (l - 1))
390
391theorem rem_zero {l : Nat} (hl : 1 ≤ l) : rem f n 0 l = cnt f n l := by
392  have := Tc_succ' (f := f) (n := n) hl
393  unfold rem; omega
394
395/-- Taking off the `i`-th symbol lowers the count of its length by one and changes no other. -/
396theorem rem_succ {i l : Nat} (hl1 : 1 ≤ l) (hl : l ≤ 15) (hi : i < Tc f n 15) :
397    rem f n (i + 1) l = rem f n i l - (if lenAt f n i = l then 1 else 0) := by
398  have a := lenAt_eq_iff (f := f) (n := n) (l := l) hl1 hl hi
399  have m1 := Tc_mono (f := f) (n := n) (show l - 1 ≤ l by omega)
400  unfold rem
401  by_cases h : lenAt f n i = l
402  · have := a.mp h
403    simp only [h, ite_true]
404    omega
405  · simp only [h, ite_false]
406    have : ¬ (Tc f n (l - 1) ≤ i ∧ i < Tc f n l) := fun hh => h (a.mpr hh)
407    omega
408
409/-! ### The sub-table sizing loop -/
410
411/-- `while (R + curr < mx) { left -= r[R + curr]; if (left <= 0) break; curr++; left <<= 1; }` with a fuel. -/
412def sizeLoop (r : Nat → Nat) (R mx : Nat) : Nat → Nat → Int → Nat × Int
413  | 0, curr, left => (curr, left)
414  | k + 1, curr, left =>
415    if R + curr < mx then
416      if left - (r (R + curr) : Int) ≤ 0 then (curr, left - (r (R + curr) : Int))
417      else sizeLoop r R mx k (curr + 1) ((left - (r (R + curr) : Int)) * 2)
418    else (curr, left)
419
420/-- The sizing loop started at `curr` with just enough fuel. -/
421def SL (r : Nat → Nat) (R mx curr : Nat) (left : Int) : Nat × Int := sizeLoop r R mx (mx - R - curr) curr left
422
423theorem SL_lt {r : Nat → Nat} {R mx curr : Nat} {left : Int} (h : R + curr < mx) :
424    SL r R mx curr left =
425      (if left - (r (R + curr) : Int) ≤ 0 then (curr, left - (r (R + curr) : Int))
426       else SL r R mx (curr + 1) ((left - (r (R + curr) : Int)) * 2)) := by
427  obtain ⟨k, hk⟩ : ∃ k, mx - R - curr = k + 1 := ⟨mx - R - curr - 1, by omega⟩
428  have hk2 : mx - R - (curr + 1) = k := by omega
429  unfold SL
430  rw [hk, hk2]
431  simp only [sizeLoop, h, ite_true]
432
433theorem SL_ge {r : Nat → Nat} {R mx curr : Nat} {left : Int} (h : mx ≤ R + curr) :
434    SL r R mx curr left = (curr, left) := by
435  have : mx - R - curr = 0 := by omega
436  unfold SL
437  rw [this]
438  simp only [sizeLoop]
439
440theorem sizeLoop_spec (r N : Nat → Nat) (R mx p d0 : Nat) (hN : ∀ d, d0 ≤ d → N (d + 1) = 2 * (N d + r d)) :
441    ∀ k curr left, d0 ≤ R + curr → R + curr ≤ mx → mx - (R + curr) ≤ k →
442      left = ((p + 1) * 2 ^ curr : Nat) - (N (R + curr) : Int) →
443      curr ≤ (sizeLoop r R mx k curr left).1 ∧ R + (sizeLoop r R mx k curr left).1 ≤ mx ∧
444      (R + (sizeLoop r R mx k curr left).1 = mx ∨
445        (p + 1) * 2 ^ (sizeLoop r R mx k curr left).1 ≤ N (R + (sizeLoop r R mx k curr left).1) +
446          r (R + (sizeLoop r R mx k curr left).1))
447  | 0, curr, left, h0, h1, h2, h3 => by
448    simp only [sizeLoop]; omega
449  | k + 1, curr, left, h0, h1, h2, h3 => by
450    simp only [sizeLoop]
451    by_cases hc : R + curr < mx
452    · simp only [hc, ite_true]
453      by_cases hb : left - (r (R + curr) : Int) ≤ 0
454      · simp only [hb, ite_true]
455        refine ⟨Nat.le_refl _, h1, Or.inr ?_⟩
456        rw [h3] at hb
457        omega
458      · simp only [hb, ite_false]
459        have := sizeLoop_spec r N R mx p d0 hN k (curr + 1) ((left - (r (R + curr) : Int)) * 2)
460          (by omega) (by omega) (by omega) (by
461            have e : R + (curr + 1) = (R + curr) + 1 := by omega
462            rw [e, hN _ h0, h3, Nat.pow_succ]
463            push_cast
464            rw [← Int.mul_assoc]
465            omega)
466        omega
467    · simp only [hc, ite_false]
468      omega
469
470
471/-- The first `R` bits of the `j`-th code, when it is longer than `R` (the index of its root entry, before reversal). -/
472def pre (f : Nat → Nat) (n R j : Nat) : Nat := val f n j / 2 ^ (lenAt f n j - R)
473
474/-- `max`: the longest length. -/
475def mxl (f : Nat → Nat) (n : Nat) : Nat := lenAt f n (Tc f n 15 - 1)
476
477/-- The sub-table sized when the code `i0` (longer than `R` bits, and the first with its prefix) opens a table:
478`curr` after the loop. -/
479def currOf (f : Nat → Nat) (n R i0 : Nat) : Nat :=
480  (SL (rem f n i0) R (mxl f n) (lenAt f n i0 - R) ((2 ^ (lenAt f n i0 - R) : Nat) : Int)).1
481
482theorem block_bound {R i0 : Nat} (hi0 : i0 < Tc f n 15) (hR : R < lenAt f n i0)
483    (halign : val f n i0 % 2 ^ (lenAt f n i0 - R) = 0) :
484    lenAt f n i0 ≤ R + currOf f n R i0 ∧ R + currOf f n R i0 ≤ mxl f n ∧
485    ∀ j, j < Tc f n 15 → R < lenAt f n j → pre f n R j = pre f n R i0 →
486      lenAt f n j ≤ R + currOf f n R i0 := by
487  obtain ⟨b1, b2⟩ := lenAt_bounds (f := f) (n := n) hi0
488  have hm : 0 < Tc f n 15 := by omega
489  have hmx : lenAt f n i0 ≤ mxl f n := lenAt_mono (f := f) (n := n) (show i0 ≤ Tc f n 15 - 1 by omega) (by omega)
490  have blk := (lenAt_eq_iff (f := f) (n := n) (l := lenAt f n i0) b1 b2 hi0).mp rfl
491  have t0 := Tc_succ' (f := f) (n := n) b1
492  have k0 := Kc_succ' (f := f) (n := n) b1
493  generalize hl0 : lenAt f n i0 = ℓ0 at *
494  generalize hv0 : val f n i0 = v0 at *
495  have hv0def : v0 = 2 * Kc f n (ℓ0 - 1) + (i0 - Tc f n (ℓ0 - 1)) := by
496    rw [← hv0, ← hl0]; rfl
497  obtain ⟨p, hp⟩ : ∃ p, v0 = p * 2 ^ (ℓ0 - R) := ⟨v0 / 2 ^ (ℓ0 - R), (Nat.div_mul_cancel (Nat.dvd_of_mod_eq_zero halign)).symm⟩
498  have hpos : 0 < 2 ^ (ℓ0 - R) := Nat.pow_pos (by omega)
499  have hpdef : pre f n R i0 = p := by
500    unfold pre; rw [hl0, hv0, hp]; exact Nat.mul_div_cancel _ hpos
501  let N : Nat → Nat := fun d => if d ≤ ℓ0 then v0 else 2 * Kc f n (d - 1)
502  have hNgt : ∀ d, ℓ0 < d → N d = 2 * Kc f n (d - 1) := fun d h => by
503    simp only [N]; rw [ite_eq_right (by omega)]
504  have hNle : ∀ d, d ≤ ℓ0 → N d = v0 := fun d h => by
505    simp only [N]; rw [ite_eq_left h]
506  have hN : ∀ d, ℓ0 ≤ d → N (d + 1) = 2 * (N d + rem f n i0 d) := by
507    intro d hd
508    rcases Nat.eq_or_lt_of_le hd with h | h
509    · subst h
510      have : N (ℓ0 + 1) = 2 * Kc f n ℓ0 := by rw [hNgt _ (by omega)]; rfl
511      have h2 : N ℓ0 = v0 := hNle _ (Nat.le_refl _)
512      have h3 : rem f n i0 ℓ0 = Tc f n ℓ0 - i0 := by unfold rem; omega
513      rw [this, h2, h3]; omega
514    · have e1 : N (d + 1) = 2 * Kc f n d := by rw [hNgt _ (by omega)]; rfl
515      have e2 : N d = 2 * Kc f n (d - 1) := hNgt _ h
516      have hd1 : 1 ≤ d := by omega
517      have h3 : rem f n i0 d = cnt f n d := by
518        have := Tc_mono (f := f) (n := n) (show ℓ0 ≤ d - 1 by omega)
519        have := Tc_succ' (f := f) (n := n) hd1
520        unfold rem; omega
521      rw [e1, e2, h3, Kc_succ' (f := f) (n := n) hd1]
522  have spec := sizeLoop_spec (rem f n i0) N R (mxl f n) p ℓ0 hN (mxl f n - R - (ℓ0 - R)) (ℓ0 - R) ((2 ^ (ℓ0 - R) : Nat) : Int)
523    (by omega) (by omega) (by omega) (by
524      have : N (R + (ℓ0 - R)) = v0 := hNle _ (by omega)
525      rw [this, hp]
526      push_cast
527      rw [Int.add_mul, Int.one_mul]; omega)
528  unfold currOf SL
529  rw [hl0]
530  generalize hc : (sizeLoop (rem f n i0) R (mxl f n) (mxl f n - R - (ℓ0 - R)) (ℓ0 - R) ((2 ^ (ℓ0 - R) : Nat) : Int)).1 = c' at spec ⊢
531  obtain ⟨s1, s2, s3⟩ := spec
532  refine ⟨by omega, s2, ?_⟩
533  intro j hj hRj hpre
534  by_cases hle : lenAt f n j ≤ R + c'
535  · exact hle
536  exfalso
537  obtain ⟨j1, j2⟩ := lenAt_bounds (f := f) (n := n) hj
538  have hjm : lenAt f n j ≤ mxl f n := lenAt_mono (f := f) (n := n) (show j ≤ Tc f n 15 - 1 by omega) (by omega)
539  have hbrk : (p + 1) * 2 ^ c' ≤ N (R + c') + rem f n i0 (R + c') := by
540    rcases s3 with h | h
541    · omega
542    · exact h
543  -- N grows past the end of the sub-tree of `p`
544  have grow : ∀ t, (p + 1) * 2 ^ (c' + 1 + t) ≤ N (R + c' + 1 + t) := by
545    intro t
546    induction t with
547    | zero =>
548      have := hN (R + c') (by omega)
549      have e : (p + 1) * 2 ^ (c' + 1 + 0) = 2 * ((p + 1) * 2 ^ c') := by
550        rw [Nat.add_zero, Nat.pow_succ, Nat.mul_comm (2 ^ c') 2, ← Nat.mul_assoc, Nat.mul_comm (p + 1) 2, Nat.mul_assoc]
551      rw [e]; simp only [Nat.add_zero]; omega
552    | succ t ih =>
553      have := hN (R + c' + 1 + t) (by omega)
554      have e : (p + 1) * 2 ^ (c' + 1 + (t + 1)) = 2 * ((p + 1) * 2 ^ (c' + 1 + t)) := by
555        rw [← Nat.add_assoc, Nat.pow_succ, Nat.mul_comm (2 ^ (c' + 1 + t)) 2, ← Nat.mul_assoc, Nat.mul_comm (p + 1) 2, Nat.mul_assoc]
556      have e2 : R + c' + 1 + (t + 1) = R + c' + 1 + t + 1 := by omega
557      rw [e2, this, e]; omega
558  have hg := grow (lenAt f n j - (R + c') - 1)
559  have e3 : R + c' + 1 + (lenAt f n j - (R + c') - 1) = lenAt f n j := by omega
560  have e4 : c' + 1 + (lenAt f n j - (R + c') - 1) = lenAt f n j - R := by omega
561  rw [e3, e4] at hg
562  have hNj : N (lenAt f n j) = 2 * Kc f n (lenAt f n j - 1) := hNgt _ (by omega)
563  have hvj : 2 * Kc f n (lenAt f n j - 1) ≤ val f n j := by unfold val; omega
564  have hge : (p + 1) * 2 ^ (lenAt f n j - R) ≤ val f n j := by omega
565  have hdiv : p + 1 ≤ val f n j / 2 ^ (lenAt f n j - R) := (Nat.le_div_iff_mul_le (Nat.pow_pos (by omega))).mpr hge
566  have : pre f n R j = val f n j / 2 ^ (lenAt f n j - R) := rfl
567  omega
568
569
570/-! ### `huff` follows the canonical code -/
571
572theorem huff_step (hfit : Fits f n) {i : Nat} (hi : i + 1 < Tc f n 15) :
573    ∃ e, e < lenAt f n i ∧ incrLoop (rev (lenAt f n i) (val f n i)) (lenAt f n i - 1) = 2 ^ e ∧
574      rev (lenAt f n i) (val f n i) % 2 ^ e + 2 ^ e = rev (lenAt f n (i + 1)) (val f n (i + 1)) := by
575  have hi0 : i < Tc f n 15 := by omega
576  obtain ⟨b1, b2⟩ := lenAt_bounds (f := f) (n := n) hi0
577  have mono := lenAt_mono (f := f) (n := n) (show i ≤ i + 1 by omega) hi
578  have hs := val_succ (f := f) (n := n) hi
579  have hl := val_lt hfit hi
580  generalize lenAt f n (i + 1) = ℓ' at *
581  generalize hv : val f n (i + 1) = v' at *
582  generalize hl0 : lenAt f n i = ℓ at *
583  generalize hv0 : val f n i = v at *
584  obtain ⟨k, rfl⟩ : ∃ k, ℓ = k + 1 := ⟨ℓ - 1, by omega⟩
585  obtain ⟨Δ, rfl⟩ : ∃ Δ, ℓ' = k + 1 + Δ := ⟨ℓ' - (k + 1), by omega⟩
586  have e1 : k + 1 + Δ - (k + 1) = Δ := by omega
587  rw [e1] at hs
588  have hvlt : v < 2 ^ (k + 1) := by
589    have := val_lt hfit hi0
590    rw [hl0, hv0] at this; exact this
591  have hlt2 : (v + 1) * 2 ^ Δ < 2 ^ (k + 1) * 2 ^ Δ := by
592    rw [← hs, ← Nat.pow_add]; exact hl
593  have hv1 : v + 1 < 2 ^ (k + 1) := Nat.lt_of_mul_lt_mul_right hlt2
594  obtain ⟨e, he, h1, h2⟩ := (succ_rev k v hvlt).1 hv1
595  refine ⟨e, by omega, ?_, ?_⟩
596  · simpa using h1
597  · rw [h2, hs, rev_mul_pow]
598
599theorem huff_last (hc : Kc f n 15 = 2 ^ 15) {m : Nat} (hm : Tc f n 15 = m + 1) :
600    incrLoop (rev (lenAt f n m) (val f n m)) (lenAt f n m - 1) = 0 := by
601  have hi : m < Tc f n 15 := by omega
602  obtain ⟨b1, b2⟩ := lenAt_bounds (f := f) (n := n) hi
603  have hl := val_last hc hm
604  generalize lenAt f n m = ℓ at *
605  generalize val f n m = v at *
606  obtain ⟨k, rfl⟩ : ∃ k, ℓ = k + 1 := ⟨ℓ - 1, by omega⟩
607  have := (succ_rev k v (by omega)).2 (by omega)
608  simpa using this
609
610/-- The low `R` bits of `huff` are the reversed prefix of the code. -/
611theorem huff_low {R j : Nat} (hR : R ≤ lenAt f n j) :
612    rev (lenAt f n j) (val f n j) % 2 ^ R = rev R (pre f n R j) := by
613  unfold pre
614  have h := rev_mod_pow (lenAt f n j - R) R (val f n j)
615  rwa [Nat.add_sub_cancel' hR] at h
616
617theorem pre_lt (hfit : Fits f n) {R j : Nat} (hj : j < Tc f n 15) (hR : R ≤ lenAt f n j) :
618    pre f n R j < 2 ^ R := by
619  unfold pre
620  have := val_lt hfit hj
621  have e : 2 ^ lenAt f n j = 2 ^ R * 2 ^ (lenAt f n j - R) := by
622    rw [← Nat.pow_add]; congr 1; omega
623  rw [e] at this
624  exact (Nat.div_lt_iff_lt_mul (Nat.pow_pos (by omega))).mpr this
625
626/-- A new root prefix starts at an aligned code. -/
627theorem align_succ (hfit : Fits f n) {R i : Nat} (hi : i + 1 < Tc f n 15) (hR : R < lenAt f n (i + 1))
628    (hnew : lenAt f n i ≤ R ∨ (R < lenAt f n i ∧ pre f n R (i + 1) ≠ pre f n R i)) :
629    val f n (i + 1) % 2 ^ (lenAt f n (i + 1) - R) = 0 := by
630  have hi0 : i < Tc f n 15 := by omega
631  obtain ⟨b1, b2⟩ := lenAt_bounds (f := f) (n := n) hi0
632  have mono := lenAt_mono (f := f) (n := n) (show i ≤ i + 1 by omega) hi
633  have hs := val_succ (f := f) (n := n) hi
634  unfold pre at hnew
635  generalize lenAt f n (i + 1) = ℓ' at *
636  generalize val f n (i + 1) = v' at *
637  generalize lenAt f n i = ℓ at *
638  generalize val f n i = v at *
639  obtain ⟨Δ, rfl⟩ : ∃ Δ, ℓ' = ℓ + Δ := ⟨ℓ' - ℓ, by omega⟩
640  have e1 : ℓ + Δ - ℓ = Δ := by omega
641  rw [e1] at hs
642  rcases hnew with h | h
643  · -- 2^(ℓ' - R) divides 2^Δ
644    have : ℓ + Δ - R ≤ Δ := Nat.sub_le_of_le_add (by omega)
645    rw [hs]
646    apply Nat.mod_eq_zero_of_dvd
647    exact Nat.dvd_mul_left_of_dvd (Nat.pow_dvd_pow 2 this) _
648  · -- the prefix changes: v + 1 crosses a multiple of 2^(ℓ - R)
649    obtain ⟨hℓ, h⟩ := h
650    have e2 : ℓ + Δ - R = Δ + (ℓ - R) := by omega
651    have hq : (v + 1) * 2 ^ Δ / 2 ^ (ℓ + Δ - R) = (v + 1) / 2 ^ (ℓ - R) := by
652      rw [e2, Nat.pow_add, Nat.mul_comm (2 ^ Δ) (2 ^ (ℓ - R))]
653      exact Nat.mul_div_mul_right _ _ (Nat.pow_pos (by omega))
654    rw [hs, hq] at h
655    have hcr : (v + 1) % 2 ^ (ℓ - R) = 0 := by
656      apply Classical.byContradiction
657      intro hne
658      apply h
659      have hP : 0 < 2 ^ (ℓ - R) := Nat.pow_pos (by omega)
660      have hlt : (v + 1) % 2 ^ (ℓ - R) ≠ 0 := hne
661      have hv1 := Nat.div_add_mod v (2 ^ (ℓ - R))
662      have hv2 := Nat.div_add_mod (v + 1) (2 ^ (ℓ - R))
663      have hr0 := Nat.mod_lt v hP
664      have hr1 := Nat.mod_lt (v + 1) hP
665      generalize 2 ^ (ℓ - R) = P at *
666      have : (v + 1) / P = v / P := by
667        rcases Nat.lt_trichotomy ((v + 1) / P) (v / P) with hlt2 | heq | hgt
668        · have := Nat.mul_le_mul_left P (show (v + 1) / P + 1 ≤ v / P by omega)
669          rw [Nat.mul_succ] at this; omega
670        · exact heq
671        · have := Nat.mul_le_mul_left P (show v / P + 1 ≤ (v + 1) / P by omega)
672          rw [Nat.mul_succ] at this; omega
673      exact this
674    -- (v+1) * 2^Δ is a multiple of 2^(Δ + (ℓ - R))
675    rw [hs, e2, Nat.pow_add]
676    apply Nat.mod_eq_zero_of_dvd
677    have := Nat.mul_dvd_mul (Nat.dvd_of_mod_eq_zero hcr) (Nat.dvd_refl (2 ^ Δ))
678    rw [Nat.mul_comm (2 ^ Δ) (2 ^ (ℓ - R))]
679    exact this
680
681
682/-! ### Counting -/
683
684theorem fl_succ (t k : Nat) : fl f t (k + 1) = fl f t k ++ (if f k = t then [k] else []) := by
685  unfold fl
686  rw [List.range_succ, List.filter_append]
687  by_cases h : f k = t <;> simp [h]
688
689theorem cnt_succ (t k : Nat) : cnt f k t = cnt f k t ∧ True := ⟨rfl, trivial⟩
690
691theorem cnt_step (t k : Nat) : cnt f (k + 1) t = cnt f k t + (if f k = t then 1 else 0) := by
692  unfold cnt
693  rw [fl_succ]
694  by_cases h : f k = t <;> simp [h]
695
696theorem cnt_le (t k : Nat) : cnt f k t ≤ k := by
697  unfold cnt fl
698  calc _ ≤ (List.range k).length := List.length_filter_le _ _
699    _ = k := by simp
700
701theorem Tc_step (k l : Nat) :
702    Tc f (k + 1) l = Tc f k l + (if 1 ≤ f k ∧ f k ≤ l then 1 else 0) := by
703  induction l with
704  | zero => simp [Tc]; omega
705  | succ l ih =>
706    show Tc f (k + 1) l + cnt f (k + 1) (l + 1) = Tc f k l + cnt f k (l + 1) + _
707    rw [ih, cnt_step]
708    split <;> split <;> split <;> omega
709
710theorem Tc_le (l : Nat) : ∀ k, Tc f k l ≤ k
711  | 0 => by
712    induction l with
713    | zero => simp [Tc]
714    | succ l ih => show Tc f 0 l + cnt f 0 (l + 1) ≤ 0; have := cnt_le (f := f) (l + 1) 0; omega
715  | k + 1 => by
716    have := Tc_le l k
717    rw [Tc_step]
718    split <;> omega
719
720
721theorem fl_succ_ne {l k : Nat} (h : f k ≠ l) : fl f l (k + 1) = fl f l k := by
722  rw [fl_succ, ite_eq_right h]; simp
723
724theorem cnt_mono {l k n : Nat} (h : k ≤ n) : cnt f k l ≤ cnt f n l := by
725  obtain ⟨d, rfl⟩ := Nat.exists_eq_add_of_le h
726  induction d with
727  | zero => exact Nat.le_refl _
728  | succ d ih =>
729    have := ih (by omega)
730    rw [← Nat.add_assoc, cnt_step]
731    split <;> omega
732
733theorem cnt_lt {l k n : Nat} (h : k < n) (hf : f k = l) : cnt f k l < cnt f n l := by
734  have := cnt_mono (f := f) (l := l) (show k + 1 ≤ n by omega)
735  rw [cnt_step, ite_eq_left hf] at this
736  omega
737
738theorem fl_getD_new {l k : Nat} (hf : f k = l) :
739    (fl f l (k + 1)).getD (cnt f k l) 0 = k := by
740  rw [fl_succ, ite_eq_left hf]
741  have : (fl f l k).length = cnt f k l := rfl
742  simp [List.getD_eq_getElem?_getD, List.getElem?_append_right (Nat.le_of_eq this), this]
743
744theorem fl_getD_old {l k j : Nat} (hf : f k = l) (hj : j < cnt f k l) :
745    (fl f l (k + 1)).getD j 0 = (fl f l k).getD j 0 := by
746  rw [fl_succ, ite_eq_left hf]
747  have : (fl f l k).length = cnt f k l := rfl
748  simp [List.getD_eq_getElem?_getD, List.getElem?_append_left (show j < (fl f l k).length by omega)]
749
750theorem rev_zero : ∀ n, rev n 0 = 0
751  | 0 => rfl
752  | n + 1 => by simp [rev, rev_zero n]
753
754theorem val_zero (h : 0 < Tc f n 15) : val f n 0 = 0 := by
755  obtain ⟨b1, b2⟩ := lenAt_bounds (f := f) (n := n) h
756  have blk := (lenAt_eq_iff (f := f) (n := n) (l := lenAt f n 0) b1 b2 h).mp rfl
757  have hT : Tc f n (0 + (lenAt f n 0 - 1)) = Tc f n 0 := by
758    have : Tc f n 0 = 0 := rfl
759    simp only [Nat.zero_add]; omega
760  have := Kc_gap (f := f) (n := n) 0 (lenAt f n 0 - 1) hT
761  have hK0 : Kc f n 0 = 0 := rfl
762  rw [hK0, Nat.mul_zero] at this
763  unfold val
764  simp only [Nat.zero_add] at this
765  rw [this]
766  omega
767
768
769/-! ### The canonical code is prefix-free -/
770
771/-- Later codes are above the end of the interval of an earlier one: `(v_i + 1) 2^(l_j - l_i) <= v_j`. -/
772theorem val_ge {i : Nat} : ∀ d, i + 1 + d < Tc f n 15 →
773    (val f n i + 1) * 2 ^ (lenAt f n (i + 1 + d) - lenAt f n i) ≤ val f n (i + 1 + d)
774  | 0, h => by
775    have := val_succ (f := f) (n := n) (i := i) (by omega)
776    simp only [Nat.add_zero]; omega
777  | d + 1, h => by
778    have ih := val_ge (i := i) d (by omega)
779    have hs := val_succ (f := f) (n := n) (i := i + 1 + d) (by omega)
780    have m1 := lenAt_mono (f := f) (n := n) (show i ≤ i + 1 + d by omega) (by omega)
781    have m2 := lenAt_mono (f := f) (n := n) (show i + 1 + d ≤ i + 1 + d + 1 by omega) (by omega)
782    have e : i + 1 + (d + 1) = i + 1 + d + 1 := by omega
783    rw [e, hs]
784    have hp : 2 ^ (lenAt f n (i + 1 + d + 1) - lenAt f n i) =
785        2 ^ (lenAt f n (i + 1 + d) - lenAt f n i) * 2 ^ (lenAt f n (i + 1 + d + 1) - lenAt f n (i + 1 + d)) := by
786      rw [← Nat.pow_add]; congr 1; omega
787    rw [hp, ← Nat.mul_assoc]
788    exact Nat.mul_le_mul_right _ (by
789      have := Nat.mul_le_mul_right (2 ^ 0) ih
790      omega)
791
792/-- No canonical code is a prefix of a later one. -/
793theorem prefix_free {i j : Nat} (hij : i < j) (hj : j < Tc f n 15) :
794    val f n j / 2 ^ (lenAt f n j - lenAt f n i) ≠ val f n i := by
795  obtain ⟨d, rfl⟩ : ∃ d, j = i + 1 + d := ⟨j - i - 1, by omega⟩
796  have h := val_ge (f := f) (n := n) (i := i) d hj
797  have hpos : 0 < 2 ^ (lenAt f n (i + 1 + d) - lenAt f n i) := Nat.pow_pos (by omega)
798  intro heq
799  have : val f n (i + 1 + d) / 2 ^ (lenAt f n (i + 1 + d) - lenAt f n i) ≥ val f n i + 1 :=
800    (Nat.le_div_iff_mul_le hpos).mpr h
801  omega
802
803
804/-- The sets of table indices that two different codes fill are disjoint: the indices that fill the entries of the
805`i`-th code are those `x` with `x mod 2^l_i = rev l_i v_i` (the first `l_i` bits that the decoder reads). -/
806theorem entries_disjoint (hfit : Fits f n) {i j : Nat} (hij : i < j) (hj : j < Tc f n 15) (x : Nat) :
807    ¬ (x % 2 ^ lenAt f n i = rev (lenAt f n i) (val f n i) ∧ x % 2 ^ lenAt f n j = rev (lenAt f n j) (val f n j)) := by
808  rintro ⟨h1, h2⟩
809  have hi : i < Tc f n 15 := by omega
810  have m := lenAt_mono (f := f) (n := n) (show i ≤ j by omega) hj
811  obtain ⟨Δ, hΔ⟩ : ∃ Δ, lenAt f n j = lenAt f n i + Δ := ⟨lenAt f n j - lenAt f n i, by omega⟩
812  have hd : lenAt f n j - lenAt f n i = Δ := by omega
813  have h3 : x % 2 ^ lenAt f n i = rev (lenAt f n i) (val f n j / 2 ^ Δ) := by
814    have e1 : x % 2 ^ lenAt f n i = (x % 2 ^ lenAt f n j) % 2 ^ lenAt f n i :=
815      (Nat.mod_mod_of_dvd _ (Nat.pow_dvd_pow 2 (by omega))).symm
816    rw [e1, h2]
817    have := rev_mod_pow Δ (lenAt f n i) (val f n j)
818    rw [← hΔ] at this
819    exact this
820  have h4 := rev_inj _ _ _ (h1.symm.trans h3)
821  have vi := val_lt hfit hi
822  have vj := val_lt hfit hj
823  have hlt : val f n j / 2 ^ Δ < 2 ^ lenAt f n i := by
824    apply (Nat.div_lt_iff_lt_mul (Nat.pow_pos (by omega))).mpr
825    rw [← Nat.pow_add, ← hΔ]; exact vj
826  rw [Nat.mod_eq_of_lt vi, Nat.mod_eq_of_lt hlt] at h4
827  exact prefix_free (f := f) (n := n) hij hj (by rw [hd]; exact h4.symm)
828
829
830/-- The reversed code is its root part plus `2^R` times the sub-table part. -/
831theorem rev_split {R j : Nat} (hR : R ≤ lenAt f n j) :
832    rev (lenAt f n j) (val f n j) = rev R (pre f n R j) + 2 ^ R * (rev (lenAt f n j) (val f n j) / 2 ^ R) := by
833  have h := huff_low (f := f) (n := n) (R := R) (j := j) hR
834  have := Nat.mod_add_div (rev (lenAt f n j) (val f n j)) (2 ^ R)
835  omega
836
837/-- Two different codes under the same root prefix fill different entries of their sub-table: the entries of the
838`j`-th code are `hd_j + 2^(l_j - R) t` with `hd_j = rev l_j v_j / 2^R`. -/
839theorem block_disjoint (hfit : Fits f n) {R i j : Nat} (hij : j < i) (hi : i < Tc f n 15)
840    (hRj : R < lenAt f n j) (hp : pre f n R j = pre f n R i) (t t' : Nat) :
841    rev (lenAt f n j) (val f n j) / 2 ^ R + 2 ^ (lenAt f n j - R) * t' ≠
842      rev (lenAt f n i) (val f n i) / 2 ^ R + 2 ^ (lenAt f n i - R) * t := by
843  intro heq
844  have hj : j < Tc f n 15 := by omega
845  have mono := lenAt_mono (f := f) (n := n) (show j ≤ i by omega) hi
846  have sj := rev_split (f := f) (n := n) (R := R) (j := j) (by omega)
847  have si := rev_split (f := f) (n := n) (R := R) (j := i) (by omega)
848  have lj := rev_lt (lenAt f n j) (val f n j)
849  have li := rev_lt (lenAt f n i) (val f n i)
850  apply entries_disjoint hfit hij hi (rev R (pre f n R i) + 2 ^ R * (rev (lenAt f n j) (val f n j) / 2 ^ R + 2 ^ (lenAt f n j - R) * t'))
851  have ej : 2 ^ R * 2 ^ (lenAt f n j - R) = 2 ^ lenAt f n j := by rw [← Nat.pow_add]; congr 1; omega
852  have ei : 2 ^ R * 2 ^ (lenAt f n i - R) = 2 ^ lenAt f n i := by rw [← Nat.pow_add]; congr 1; omega
853  constructor
854  · -- modulo 2^l_j
855    have : rev R (pre f n R i) + 2 ^ R * (rev (lenAt f n j) (val f n j) / 2 ^ R + 2 ^ (lenAt f n j - R) * t') =
856        rev (lenAt f n j) (val f n j) + 2 ^ lenAt f n j * t' := by
857      rw [← hp] at *
858      rw [Nat.mul_add, ← Nat.mul_assoc, ej]
859      omega
860    rw [this, Nat.add_mul_mod_self_left]
861    exact Nat.mod_eq_of_lt lj
862  · rw [heq]
863    have : rev R (pre f n R i) + 2 ^ R * (rev (lenAt f n i) (val f n i) / 2 ^ R + 2 ^ (lenAt f n i - R) * t) =
864        rev (lenAt f n i) (val f n i) + 2 ^ lenAt f n i * t := by
865      rw [Nat.mul_add, ← Nat.mul_assoc, ei]
866      omega
867    rw [this, Nat.add_mul_mod_self_left]
868    exact Nat.mod_eq_of_lt li
869
870end Model
871
872end Zlib.Inftrees.Proofs