trees.c.heap.gbtree.lean

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

1import ZlibF.Proof.«trees.c.heap.gbmath»
2
3/-!
4# The tree layout of `build_tree` and its clamped depths (pure)
5
6`PShape H hm J elems maxc` is the layout `build_tree` leaves in
7`heap[hm .. HEAP_SIZE)`; `Clamped … cl` says `cl` is the clamped depth that the
8first pass of `gen_bitlen` computes. Proved: the clamped Kraft identity
9(`kraft_clamped`), `bl_count[L] = exact + overflow/2` (`blC_top`), some node has
10exact depth `L` when `overflow > 0` (`exactC_pos`), and the fix-up round facts.
11-/
12
13namespace Zlib.Trees.Proofs.GB
14
15/-- The `Dad` of the node at heap position `p`: positions `572-2j` and `571-2j`
16hold the two children of node `elems + j`. -/
17def dadP (elems p : Nat) : Nat := elems + (572 - p) / 2
18
19/-- Pure shape of the tree that `build_tree` leaves in `heap[hm .. 573)`: `J ≥ 1`
20internal nodes `elems .. elems+J-1`, root `elems+J-1` at `hm = 572 - 2J`, node
21`elems+j` placed below its children `572-2j`, `571-2j`, all other entries symbols
22`≤ maxc < elems`, all entries distinct. -/
23structure PShape (H : Nat → Nat) (hm J elems maxc : Nat) : Prop where
24  hm_eq : hm + 2 * J + 1 = 573
25  J1 : 1 ≤ J
26  maxc_lt : maxc < elems
27  inj : ∀ q q', hm ≤ q → q < 573 → hm ≤ q' → q' < 573 → H q = H q' → q = q'
28  kind : ∀ q, hm ≤ q → q < 573 → H q ≤ maxc ∨ (elems ≤ H q ∧ H q < elems + J)
29  root : H hm = elems + J - 1
30  appears : ∀ j < J, ∃ q, hm ≤ q ∧ q < 571 - 2 * j ∧ H q = elems + j
31
32/-- `cl` is the clamped depth: `0` at the root, `min (cl dad + 1) L` elsewhere. -/
33structure Clamped (H : Nat → Nat) (hm J elems L : Nat) (cl : Nat → Nat) : Prop where
34  root : cl (H hm) = 0
35  step : ∀ i < 2 * J, cl (H (hm + 1 + i)) = min (cl (dadP elems (hm + 1 + i)) + 1) L
36
37section tree
38variable {H : Nat → Nat} {hm J elems maxc L : Nat} {cl : Nat → Nat}
39
40theorem PShape.dadP_eq (S : PShape H hm J elems maxc) (i : Nat) (hi : i < 2 * J) :
41    dadP elems (hm + 1 + i) = elems + (2 * J - 1 - i) / 2 := by
42  have := S.hm_eq; unfold dadP; congr 2; omega
43
44theorem Clamped.le_all (S : PShape H hm J elems maxc) (C : Clamped H hm J elems L cl) (q : Nat)
45    (h1 : hm ≤ q) (h2 : q < 573) : cl (H q) ≤ L := by
46  by_cases e : q = hm
47  · subst e; rw [C.root]; omega
48  · have := C.step (q - hm - 1) (by have := S.hm_eq; omega)
49    rw [show hm + 1 + (q - hm - 1) = q by omega] at this
50    rw [this]; exact Nat.min_le_right _ _
51
52theorem Clamped.dad_le (S : PShape H hm J elems maxc) (C : Clamped H hm J elems L cl) (i : Nat)
53    (hi : i < 2 * J) : cl (dadP elems (hm + 1 + i)) ≤ L := by
54  rw [S.dadP_eq i hi]
55  obtain ⟨q, h1, h2, e⟩ := S.appears ((2 * J - 1 - i) / 2) (by omega)
56  rw [← e]; exact C.le_all S q h1 (by omega)
57
58/-- The internal nodes, counted through the heap positions, are `elems .. elems+J-1`. -/
59theorem PShape.internal_sum (S : PShape H hm J elems maxc) (F : Nat → Nat) :
60    rs (fun i => if elems ≤ H (hm + i) then F (H (hm + i)) else 0) (2 * J + 1) =
61      rs (fun j => F (elems + j)) J := by
62  have hm_eq := S.hm_eq
63  have hP : ∀ i < 2 * J + 1, H (hm + i) < elems + J := by
64    intro i hi
65    rcases S.kind (hm + i) (by omega) (by omega) with h | h
66    · have := S.maxc_lt; omega
67    · exact h.2
68  have := rs_image (fun i => H (hm + i)) (fun v => if elems ≤ v then F v else 0) (2 * J + 1) (elems + J) hP
69  rw [this, rs_split]
70  rw [rs_eq_zero (fun v hv => by rw [ite_eq_right (by omega), Nat.mul_zero])]
71  rw [Nat.zero_add]
72  apply rs_congr
73  intro j hj
74  rw [ite_eq_left (by omega)]
75  obtain ⟨q, h1, h2, e⟩ := S.appears j hj
76  have c1 := cnt_pos (P := fun i => H (hm + i)) (m := 2 * J + 1) (i := q - hm) (by omega)
77    (by show H (hm + (q - hm)) = _; rw [show hm + (q - hm) = q by omega, e])
78  have c2 := cnt_le_one (fun i => H (hm + i)) (2 * J + 1) (elems + j)
79    (fun a b ha hb e => by have := S.inj (hm + a) (hm + b) (by omega) (by omega) (by omega) (by omega) e; omega)
80  rw [show cnt (fun i => H (hm + i)) (2 * J + 1) (elems + j) = 1 by omega, Nat.one_mul]
81
82/-- Weight of one open child slot below a node of clamped depth `x` (scaled by `2^(L+1)`). -/
83def slot (L x : Nat) : Nat := if x < L then 2 ^ (L - x) else 1
84
85theorem local_leaf (L d : Nat) (hL : 1 ≤ L) (hd : d ≤ L) :
86    2 * 2 ^ (L - min (d + 1) L) = slot L d + ind (d = L) := by
87  by_cases e : d = L
88  · rw [show min (d + 1) L = L by omega]
89    unfold slot ind
90    rw [ite_eq_right (show ¬ d < L by omega), ite_eq_left e, Nat.sub_self]
91  · rw [show min (d + 1) L = d + 1 by omega]
92    unfold slot ind
93    rw [ite_eq_left (show d < L by omega), ite_eq_right e]
94    rw [show L - d = (L - (d + 1)) + 1 by omega, Nat.pow_succ]; omega
95
96theorem local_int (L d : Nat) (hL : 1 ≤ L) (hd : d ≤ L) :
97    2 * slot L (min (d + 1) L) = slot L d + ind (d = L) := by
98  by_cases e : d = L
99  · rw [show min (d + 1) L = L by omega]
100    unfold slot ind
101    rw [ite_eq_right (Nat.lt_irrefl _), ite_eq_right (show ¬ d < L by omega), ite_eq_left e]
102  · by_cases e2 : d + 1 = L
103    · rw [show min (d + 1) L = L by omega]
104      unfold slot ind
105      rw [ite_eq_right (Nat.lt_irrefl _), ite_eq_left (show d < L by omega), ite_eq_right e, show L - d = 1 by omega]
106    · rw [show min (d + 1) L = d + 1 by omega]
107      unfold slot ind
108      rw [ite_eq_left (show d + 1 < L by omega), ite_eq_left (show d < L by omega), ite_eq_right e]
109      rw [show L - d = (L - (d + 1)) + 1 by omega, Nat.pow_succ]; omega
110
111/-- Clamped Kraft sum of the leaves, scaled by `2^L`. -/
112def kraftC (H : Nat → Nat) (hm J maxc L : Nat) (cl : Nat → Nat) : Nat :=
113  rs (fun i => if H (hm + 1 + i) ≤ maxc then 2 ^ (L - cl (H (hm + 1 + i))) else 0) (2 * J)
114
115/-- Number of nodes whose (clamped) parent depth is already `L`: `gen_bitlen`'s `overflow`. -/
116def ovfC (H : Nat → Nat) (hm J elems L : Nat) (cl : Nat → Nat) : Nat :=
117  rs (fun i => if cl (dadP elems (hm + 1 + i)) = L then 1 else 0) (2 * J)
118
119theorem PShape.internal_tail (S : PShape H hm J elems maxc) (C : Clamped H hm J elems L cl) (F : Nat → Nat) :
120    F 0 + rs (fun i => if elems ≤ H (hm + 1 + i) then F (cl (H (hm + 1 + i))) else 0) (2 * J) =
121      rs (fun j => F (cl (elems + j))) J := by
122  have hint := S.internal_sum (fun v => F (cl v))
123  rw [show 2 * J + 1 = 1 + 2 * J by omega, rs_split] at hint
124  simp only [rs_succ, rs_zero, Nat.add_zero, Nat.zero_add] at hint
125  rw [S.root, ite_eq_left (by have := S.J1; omega)] at hint
126  rw [show elems + J - 1 = H hm by rw [S.root], C.root] at hint
127  rw [← hint]
128  congr 1
129  apply rs_congr; intro i _; rw [Nat.add_assoc]
130
131/-- **Clamped Kraft identity.** `2 · Σ_leaves 2^(L - cl) = 2^(L+1) + overflow`. -/
132theorem kraft_clamped (S : PShape H hm J elems maxc) (C : Clamped H hm J elems L cl) (hL : 1 ≤ L) :
133    2 * kraftC H hm J maxc L cl = 2 ^ (L + 1) + ovfC H hm J elems L cl := by
134  have hm_eq := S.hm_eq
135  have hloc : ∀ i < 2 * J,
136      (if H (hm + 1 + i) ≤ maxc then 2 * 2 ^ (L - cl (H (hm + 1 + i))) else 0) +
137        2 * (if elems ≤ H (hm + 1 + i) then slot L (cl (H (hm + 1 + i))) else 0) =
138      slot L (cl (dadP elems (hm + 1 + i))) + (if cl (dadP elems (hm + 1 + i)) = L then 1 else 0) := by
139    intro i hi
140    have hd := C.dad_le S i hi
141    rw [C.step i hi]
142    have hk := S.kind (hm + 1 + i) (by omega) (by omega)
143    have := S.maxc_lt
144    by_cases hl : H (hm + 1 + i) ≤ maxc
145    · rw [ite_eq_left hl, ite_eq_right (by omega)]
146      have := local_leaf L _ hL hd; unfold ind at this; omega
147    · rw [ite_eq_right hl, ite_eq_left (by omega)]
148      have := local_int L _ hL hd; unfold ind at this; omega
149  have hsum := rs_congr hloc
150  rw [rs_add, rs_add, rs_mul] at hsum
151  have hpair : rs (fun i => slot L (cl (dadP elems (hm + 1 + i)))) (2 * J) =
152      2 * rs (fun j => slot L (cl (elems + j))) J := by
153    rw [rs_congr (G := fun i => (fun j => slot L (cl (elems + j))) ((2 * J - 1 - i) / 2))
154      (fun i hi => by simp only; rw [S.dadP_eq i hi])]
155    exact rs_pair (fun j => slot L (cl (elems + j))) J
156  have hint := S.internal_tail C (slot L)
157  have hs0 : slot L 0 = 2 ^ L := by unfold slot; rw [ite_eq_left (show 0 < L by omega), Nat.sub_zero]
158  rw [hs0] at hint
159  have hleaf : rs (fun i => if H (hm + 1 + i) ≤ maxc then 2 * 2 ^ (L - cl (H (hm + 1 + i))) else 0) (2 * J) =
160      2 * kraftC H hm J maxc L cl := by
161    unfold kraftC; rw [← rs_mul]; apply rs_congr; intro i _; split <;> simp
162  unfold ovfC
163  rw [Nat.pow_succ]
164  omega
165
166/-- Nodes at exact depth `L`: their parent has clamped depth `L - 1`. -/
167def exactC (H : Nat → Nat) (hm J elems L : Nat) (cl : Nat → Nat) : Nat :=
168  rs (fun i => if cl (dadP elems (hm + 1 + i)) + 1 = L then 1 else 0) (2 * J)
169
170/-- Leaves of clamped depth `b` (`bl_count[b]` after the first pass). -/
171def blC (H : Nat → Nat) (hm J maxc : Nat) (cl : Nat → Nat) (b : Nat) : Nat :=
172  rs (fun i => if H (hm + 1 + i) ≤ maxc ∧ cl (H (hm + 1 + i)) = b then 1 else 0) (2 * J)
173
174/-- `bl_count[L] = #(nodes of exact depth L) + overflow / 2`, and `overflow` is even. -/
175theorem blC_top (S : PShape H hm J elems maxc) (C : Clamped H hm J elems L cl) (hL : 1 ≤ L) :
176    ovfC H hm J elems L cl % 2 = 0 ∧
177    blC H hm J maxc cl L = exactC H hm J elems L cl + ovfC H hm J elems L cl / 2 := by
178  have hm_eq := S.hm_eq
179  have hloc : ∀ i < 2 * J,
180      (if H (hm + 1 + i) ≤ maxc ∧ cl (H (hm + 1 + i)) = L then 1 else 0) +
181        (if elems ≤ H (hm + 1 + i) then (if cl (H (hm + 1 + i)) = L then 1 else 0) else 0) =
182      (if cl (dadP elems (hm + 1 + i)) + 1 = L then 1 else 0) +
183        (if cl (dadP elems (hm + 1 + i)) = L then 1 else 0) := by
184    intro i hi
185    have hd := C.dad_le S i hi
186    have hk := S.kind (hm + 1 + i) (by omega) (by omega)
187    have := S.maxc_lt
188    rw [C.step i hi]
189    by_cases hl : H (hm + 1 + i) ≤ maxc
190    · rw [ite_eq_right (show ¬ elems ≤ H (hm + 1 + i) by omega)]
191      by_cases a : cl (dadP elems (hm + 1 + i)) + 1 = L
192      · rw [ite_eq_left ⟨hl, by omega⟩, ite_eq_left a, ite_eq_right (by omega)]
193      · by_cases b : cl (dadP elems (hm + 1 + i)) = L
194        · rw [ite_eq_left ⟨hl, by omega⟩, ite_eq_right a, ite_eq_left b]
195        · rw [ite_eq_right (fun h => by omega), ite_eq_right a, ite_eq_right b]
196    · rw [ite_eq_right (fun h => hl h.1), ite_eq_left (by omega)]
197      by_cases a : cl (dadP elems (hm + 1 + i)) + 1 = L
198      · rw [ite_eq_left (by omega), ite_eq_left a, ite_eq_right (by omega)]
199      · by_cases b : cl (dadP elems (hm + 1 + i)) = L
200        · rw [ite_eq_left (by omega), ite_eq_right a, ite_eq_left b]
201        · rw [ite_eq_right (by omega), ite_eq_right a, ite_eq_right b]
202  have hsum := rs_congr hloc
203  rw [rs_add, rs_add] at hsum
204  have hpair : rs (fun i => if cl (dadP elems (hm + 1 + i)) = L then 1 else 0) (2 * J) =
205      2 * rs (fun j => if cl (elems + j) = L then 1 else 0) J := by
206    rw [rs_congr (G := fun i => (fun j => if cl (elems + j) = L then 1 else 0) ((2 * J - 1 - i) / 2))
207      (fun i hi => by simp only; rw [S.dadP_eq i hi])]
208    exact rs_pair (fun j => if cl (elems + j) = L then 1 else 0) J
209  have hint := S.internal_tail C (fun x => if x = L then 1 else 0)
210  rw [ite_eq_right (by omega), Nat.zero_add] at hint
211  unfold blC exactC ovfC
212  constructor <;> omega
213
214/-- If some node overflows, some node has exact depth `L`. -/
215theorem exactC_pos (S : PShape H hm J elems maxc) (C : Clamped H hm J elems L cl) (hL : 1 ≤ L)
216    (hov : 0 < ovfC H hm J elems L cl) : 0 < exactC H hm J elems L cl := by
217  have hm_eq := S.hm_eq
218  have key0 : ∀ n i, i < n → i < 2 * J → cl (dadP elems (hm + 1 + i)) = L →
219      ∃ i' < 2 * J, cl (dadP elems (hm + 1 + i')) + 1 = L := by
220    intro n
221    induction n with
222    | zero => intro i hi; omega
223    | succ n ihn =>
224      intro i hin hi hcl
225      have ih : ∀ i', i' < i → i' < 2 * J → cl (dadP elems (hm + 1 + i')) = L →
226          ∃ i' < 2 * J, cl (dadP elems (hm + 1 + i')) + 1 = L :=
227        fun i' h1 => ihn i' (by omega)
228      rw [S.dadP_eq i hi] at hcl
229      obtain ⟨q, h1, h2, e⟩ := S.appears ((2 * J - 1 - i) / 2) (by omega)
230      rw [← e] at hcl
231      have hq : q ≠ hm := by intro e'; subst e'; rw [C.root] at hcl; omega
232      obtain ⟨i', rfl⟩ : ∃ i', q = hm + 1 + i' := ⟨q - hm - 1, by omega⟩
233      have hq' : i' < i := by omega
234      have := C.step i' (by omega)
235      rw [hcl] at this
236      have hd := C.dad_le S i' (by omega)
237      by_cases a : cl (dadP elems (hm + 1 + i')) + 1 = L
238      · exact ⟨i', by omega, a⟩
239      · exact ih i' hq' (by omega) (by omega)
240  obtain ⟨i, hi, hcl⟩ : ∃ i < 2 * J, cl (dadP elems (hm + 1 + i)) = L := by
241    by_cases hx : ∃ i < 2 * J, cl (dadP elems (hm + 1 + i)) = L
242    · exact hx
243    · have := rs_eq_zero (F := fun i => if cl (dadP elems (hm + 1 + i)) = L then 1 else 0) (n := 2 * J)
244        (fun i hi => by rw [ite_eq_right (fun e => hx ⟨i, hi, e⟩)])
245      unfold ovfC at hov; omega
246  obtain ⟨i', hi', e'⟩ := key0 (i + 1) i (by omega) hi hcl
247  have := le_rs (F := fun i => if cl (dadP elems (hm + 1 + i)) + 1 = L then 1 else 0) hi'
248  simp only [e', ite_true] at this
249  unfold exactC; omega
250
251/-- No leaf has clamped depth `0`. -/
252theorem blC_zero (S : PShape H hm J elems maxc) (C : Clamped H hm J elems L cl) (hL : 1 ≤ L) :
253    blC H hm J maxc cl 0 = 0 := by
254  unfold blC
255  apply rs_eq_zero; intro i hi
256  rw [ite_eq_right]; rintro ⟨-, e⟩; rw [C.step i hi] at e; omega
257
258theorem blC_high (S : PShape H hm J elems maxc) (C : Clamped H hm J elems L cl) (b : Nat) (hb : L < b) :
259    blC H hm J maxc cl b = 0 := by
260  have hm_eq := S.hm_eq
261  unfold blC
262  apply rs_eq_zero; intro i hi
263  rw [ite_eq_right]; rintro ⟨-, e⟩; have := C.le_all S (hm + 1 + i) (by omega) (by omega); omega
264
265/-- The clamped Kraft sum regrouped by length. -/
266theorem kraftC_eq (S : PShape H hm J elems maxc) (C : Clamped H hm J elems L cl) :
267    kraftC H hm J maxc L cl = rs (fun b => blC H hm J maxc cl b * 2 ^ (L - b)) (L + 1) := by
268  have hm_eq := S.hm_eq
269  unfold kraftC blC
270  exact rs_regroup (fun i => H (hm + 1 + i) ≤ maxc) (fun i => cl (H (hm + 1 + i))) (fun b => 2 ^ (L - b))
271    (2 * J) (L + 1) (fun i hi _ => by have := C.le_all S (hm + 1 + i) (by omega) (by omega); omega)
272
273/-- Number of leaves. -/
274def nLeaves (H : Nat → Nat) (hm J maxc : Nat) : Nat :=
275  rs (fun i => if H (hm + 1 + i) ≤ maxc then 1 else 0) (2 * J)
276
277theorem blC_total (S : PShape H hm J elems maxc) (C : Clamped H hm J elems L cl) :
278    rs (fun b => blC H hm J maxc cl b) (L + 1) = nLeaves H hm J maxc := by
279  have hm_eq := S.hm_eq
280  have := rs_regroup (fun i => H (hm + 1 + i) ≤ maxc) (fun i => cl (H (hm + 1 + i))) (fun _ => 1)
281    (2 * J) (L + 1) (fun i hi _ => by have := C.le_all S (hm + 1 + i) (by omega) (by omega); omega)
282  unfold nLeaves blC
283  rw [this]; apply rs_congr; intro b _; simp
284
285/-- Summing over the leaves (by position) is summing over the symbols in the tree. -/
286theorem PShape.leaf_sum (S : PShape H hm J elems maxc) (T : Nat → Prop) [DecidablePred T]
287    (hT : ∀ v ≤ maxc, T v ↔ ∃ q, hm < q ∧ q < 573 ∧ H q = v) (F : Nat → Nat) :
288    rs (fun i => if H (hm + 1 + i) ≤ maxc then F (H (hm + 1 + i)) else 0) (2 * J) =
289      rs (fun v => if T v then F v else 0) (maxc + 1) := by
290  have hm_eq := S.hm_eq
291  have hlt := S.maxc_lt
292  have hP : ∀ i < 2 * J, H (hm + 1 + i) < elems + J := by
293    intro i hi
294    rcases S.kind (hm + 1 + i) (by omega) (by omega) with h | h
295    · omega
296    · exact h.2
297  have := rs_image (fun i => H (hm + 1 + i)) (fun v => if v ≤ maxc then F v else 0) (2 * J) (elems + J) hP
298  rw [this, show elems + J = (maxc + 1) + (elems + J - (maxc + 1)) by omega, rs_split]
299  rw [rs_eq_zero (F := fun i => cnt (fun i => H (hm + 1 + i)) (2 * J) (maxc + 1 + i) *
300      (if maxc + 1 + i ≤ maxc then F (maxc + 1 + i) else 0)) (fun v _ => by rw [ite_eq_right (by omega), Nat.mul_zero]),
301    Nat.add_zero]
302  apply rs_congr
303  intro v hv
304  rw [ite_eq_left (by omega)]
305  have hinj : ∀ a b, a < 2 * J → b < 2 * J → H (hm + 1 + a) = H (hm + 1 + b) → a = b :=
306    fun a b ha hb e => by
307      have := S.inj (hm + 1 + a) (hm + 1 + b) (by omega) (by omega) (by omega) (by omega) e; omega
308  have c2 := cnt_le_one (fun i => H (hm + 1 + i)) (2 * J) v hinj
309  by_cases ht : T v
310  · rw [ite_eq_left ht]
311    obtain ⟨q, h1, h2, e⟩ := (hT v (by omega)).mp ht
312    have c1 := cnt_pos (P := fun i => H (hm + 1 + i)) (m := 2 * J) (i := q - hm - 1) (by omega)
313      (by show H (hm + 1 + (q - hm - 1)) = _; rw [show hm + 1 + (q - hm - 1) = q by omega, e])
314    rw [show cnt (fun i => H (hm + 1 + i)) (2 * J) v = 1 by omega, Nat.one_mul]
315  · rw [ite_eq_right ht]
316    have : cnt (fun i => H (hm + 1 + i)) (2 * J) v = 0 := cnt_zero (fun i hi e =>
317      ht ((hT v (by omega)).mpr ⟨hm + 1 + i, by omega, by omega, e⟩))
318    rw [this, Nat.zero_mul]
319
320theorem nLeaves_le (S : PShape H hm J elems maxc) : nLeaves H hm J maxc ≤ maxc + 1 := by
321  classical
322  have hl := S.leaf_sum (fun v => ∃ q, hm < q ∧ q < 573 ∧ H q = v) (fun _ _ => Iff.rfl) (fun _ => 1)
323  unfold nLeaves
324  rw [hl]
325  have := rs_le (n := maxc + 1) (F := fun v => if (∃ q, hm < q ∧ q < 573 ∧ H q = v) then 1 else 0)
326    (G := fun _ => 1) (fun v _ => by split <;> omega)
327  rw [rs_const] at this; omega
328
329end tree
330
331/-! ## One round of the overflow fix-up -/
332
333/-- Kraft sum of the counts `c b` (`b = 0 .. L`), scaled by `2^L`. -/
334def kc (c : Nat → Nat) (L : Nat) : Nat := rs (fun b => c b * 2 ^ (L - b)) (L + 1)
335
336theorem ind_mul (p : Prop) [Decidable p] (x : Nat) : ind p * x = if p then x else 0 := by
337  unfold ind; split <;> simp
338
339theorem rs_ind_eq (k n : Nat) (hk : k < n) : rs (fun x => ind (x = k)) n = 1 := by
340  rw [rs_congr (F := fun x => ind (x = k)) (G := fun x => if x = k then 1 else 0) (fun x _ => rfl),
341    rs_single, ite_eq_left hk]
342
343/-- One round: `c[b]--`, `c[b+1] += 2`, `c[L]--` lowers the Kraft sum by one
344and keeps the total. -/
345theorem round_kraft (c c' : Nat → Nat) (L b : Nat) (hb : b + 1 ≤ L)
346    (h : ∀ x ≤ L, c' x + ind (x = b) + ind (x = L) = c x + 2 * ind (x = b + 1)) :
347    kc c' L + 1 = kc c L ∧ rs c' (L + 1) = rs c (L + 1) := by
348  have e1 := rs_congr (n := L + 1) (F := fun x => (c' x + ind (x = b) + ind (x = L)) * 2 ^ (L - x))
349    (G := fun x => (c x + 2 * ind (x = b + 1)) * 2 ^ (L - x)) (fun x hx => by rw [h x (by omega)])
350  simp only [Nat.add_mul, Nat.mul_assoc] at e1
351  rw [rs_add, rs_add, rs_add] at e1
352  simp only [ind_mul] at e1
353  rw [rs_single _ _ _, rs_single _ _ _, ite_eq_left (by omega), ite_eq_left (by omega)] at e1
354  have e3 : rs (fun i => 2 * (if i = b + 1 then 2 ^ (L - i) else 0)) (L + 1) = 2 * 2 ^ (L - (b + 1)) := by
355    rw [rs_mul, rs_single, ite_eq_left (by omega)]
356  rw [e3] at e1
357  have e4 : 2 ^ (L - b) = 2 * 2 ^ (L - (b + 1)) := by
358    rw [show L - b = (L - (b + 1)) + 1 by omega, Nat.pow_succ]; omega
359  rw [e4, Nat.sub_self, Nat.pow_zero] at e1
360  refine ⟨by unfold kc; omega, ?_⟩
361  have e2 := rs_congr (n := L + 1) (F := fun x => c' x + ind (x = b) + ind (x = L))
362    (G := fun x => c x + 2 * ind (x = b + 1)) (fun x hx => h x (by omega))
363  rw [rs_add, rs_add, rs_add, rs_mul] at e2
364  rw [rs_ind_eq b _ (by omega), rs_ind_eq L _ (by omega), rs_ind_eq (b + 1) _ (by omega)] at e2
365  omega
366
367/-- While the Kraft sum exceeds `2^L` and there are at most `2^L` leaves, some
368length `1 ≤ b < L` is in use. -/
369theorem exists_short (c : Nat → Nat) (L R : Nat) (hR : 1 ≤ R) (hk : kc c L = 2 ^ L + R)
370    (htot : rs c (L + 1) ≤ 2 ^ L) (h0 : c 0 = 0) : ∃ b, 1 ≤ b ∧ b < L ∧ c b ≠ 0 := by
371  by_cases hx : ∃ b, 1 ≤ b ∧ b < L ∧ c b ≠ 0
372  · exact hx
373  · exfalso
374    have z : rs (fun b => c b * 2 ^ (L - b)) L = 0 := rs_eq_zero (fun b hb => by
375      by_cases e : b = 0
376      · subst e; rw [h0, Nat.zero_mul]
377      · have : c b = 0 := by
378          by_cases e' : c b = 0
379          · exact e'
380          · exact absurd ⟨b, by omega, hb, e'⟩ hx
381        rw [this, Nat.zero_mul])
382    unfold kc at hk
383    rw [rs_succ, z, Nat.sub_self, Nat.pow_zero, Nat.mul_one, Nat.zero_add] at hk
384    have := le_rs (F := c) (n := L + 1) (i := L) (by omega)
385    omega
386
387end Zlib.Trees.Proofs.GB