trees.c.heap.gbmath.lean

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

1
2/-!
3# Pure facts behind `gen_bitlen`
4
5* `rs F n = Σ_{i<n} F i` and its algebra (congruence, additivity, single
6  point, swap, image/reindexing, counting).
7* The clamped-depth identity of a Huffman tree laid out as `build_tree` lays
8  it out (`kraft_clamped`): with `ovf` the number of nodes whose depth exceeds
9  `L`, the clamped Kraft sum of the leaves is `2^L + ovf/2`, `ovf` is even, and
10  `bl_count[L] ≥ ovf/2 + 1` when `ovf > 0`.
11* One round of the overflow fix-up lowers the Kraft sum by exactly one.
12
13Everything here is about natural numbers; no heap.
14-/
15
16namespace Zlib.Trees.Proofs.GB
17
18/-! ## Finite sums -/
19
20/-- `rs F n = F 0 + … + F (n-1)`. -/
21def rs (F : Nat → Nat) : Nat → Nat
22  | 0 => 0
23  | n + 1 => rs F n + F n
24
25@[simp] theorem rs_zero (F : Nat → Nat) : rs F 0 = 0 := rfl
26theorem rs_succ (F : Nat → Nat) (n : Nat) : rs F (n + 1) = rs F n + F n := rfl
27
28theorem rs_congr {F G : Nat → Nat} {n : Nat} (h : ∀ i < n, F i = G i) : rs F n = rs G n := by
29  induction n with
30  | zero => rfl
31  | succ n ih => rw [rs_succ, rs_succ, ih (fun i hi => h i (by omega)), h n (by omega)]
32
33theorem rs_add (F G : Nat → Nat) (n : Nat) : rs (fun i => F i + G i) n = rs F n + rs G n := by
34  induction n with
35  | zero => rfl
36  | succ n ih => rw [rs_succ, rs_succ, rs_succ, ih]; omega
37
38theorem rs_mul (c : Nat) (F : Nat → Nat) (n : Nat) : rs (fun i => c * F i) n = c * rs F n := by
39  induction n with
40  | zero => simp
41  | succ n ih => rw [rs_succ, rs_succ, ih, Nat.mul_add]
42
43theorem rs_le {F G : Nat → Nat} {n : Nat} (h : ∀ i < n, F i ≤ G i) : rs F n ≤ rs G n := by
44  induction n with
45  | zero => simp
46  | succ n ih =>
47    rw [rs_succ, rs_succ]
48    have := ih (fun i hi => h i (by omega)); have := h n (by omega); omega
49
50theorem rs_eq_zero {F : Nat → Nat} {n : Nat} (h : ∀ i < n, F i = 0) : rs F n = 0 := by
51  induction n with
52  | zero => rfl
53  | succ n ih => rw [rs_succ, ih (fun i hi => h i (by omega)), h n (by omega)]
54
55theorem rs_zero_of {F : Nat → Nat} {n : Nat} (h : rs F n = 0) : ∀ i < n, F i = 0 := by
56  induction n with
57  | zero => intro i hi; omega
58  | succ n ih =>
59    rw [rs_succ] at h
60    intro i hi
61    by_cases e : i = n
62    · subst e; omega
63    · exact ih (by omega) i (by omega)
64
65theorem le_rs {F : Nat → Nat} {n i : Nat} (hi : i < n) : F i ≤ rs F n := by
66  induction n with
67  | zero => omega
68  | succ n ih =>
69    rw [rs_succ]
70    by_cases e : i = n
71    · subst e; omega
72    · have := ih (by omega); omega
73
74theorem rs_const (c n : Nat) : rs (fun _ => c) n = c * n := by
75  induction n with
76  | zero => simp
77  | succ n ih => rw [rs_succ, ih, Nat.mul_succ]
78
79/-- Splitting a range. -/
80theorem rs_split (F : Nat → Nat) (a b : Nat) : rs F (a + b) = rs F a + rs (fun i => F (a + i)) b := by
81  induction b with
82  | zero => rfl
83  | succ b ih => rw [← Nat.add_assoc, rs_succ, rs_succ, ih, Nat.add_assoc]
84
85/-- Sum of a function supported at one point. -/
86theorem rs_single (G : Nat → Nat) (k n : Nat) :
87    rs (fun i => if i = k then G i else 0) n = if k < n then G k else 0 := by
88  induction n with
89  | zero => simp
90  | succ n ih =>
91    rw [rs_succ, ih]
92    by_cases e : n = k
93    · subst e; simp
94    · rw [ite_eq_right e]
95      by_cases h1 : k < n
96      · rw [ite_eq_left h1, ite_eq_left (by omega)]; rfl
97      · rw [ite_eq_right h1, ite_eq_right (by omega)]
98
99theorem rs_single' (G : Nat → Nat) (k n : Nat) (hk : k < n) :
100    rs (fun i => if k = i then G i else 0) n = G k := by
101  rw [rs_congr (G := fun i => if i = k then G i else 0) (fun i _ => by
102    by_cases e : i = k
103    · subst e; simp
104    · rw [ite_eq_right (Ne.symm e), ite_eq_right e])]
105  rw [rs_single, ite_eq_left hk]
106
107theorem rs_swap (F : Nat → Nat → Nat) (m n : Nat) :
108    rs (fun b => rs (fun p => F b p) m) n = rs (fun p => rs (fun b => F b p) n) m := by
109  induction n with
110  | zero => simp only [rs_zero]; exact (rs_eq_zero (fun _ _ => rfl)).symm
111  | succ n ih =>
112    rw [rs_succ, ih]
113    rw [show (fun p => rs (fun b => F b p) (n + 1)) = (fun p => rs (fun b => F b p) n + F n p) from rfl]
114    rw [rs_add]
115
116/-- Changing one term. -/
117theorem rs_upd {F G : Nat → Nat} {n k : Nat} (hk : k < n) (h : ∀ i < n, i ≠ k → F i = G i) :
118    rs F n + G k = rs G n + F k := by
119  induction n with
120  | zero => omega
121  | succ n ih =>
122    rw [rs_succ, rs_succ]
123    by_cases e : k = n
124    · subst e
125      rw [rs_congr (fun i hi => h i (by omega) (by omega))]; omega
126    · have := ih (by omega) (fun i hi hne => h i (by omega) hne)
127      rw [h n (by omega) (Ne.symm e)]; omega
128
129/-- All terms `≤ 1` and the sum is `n`: every term is `1`. -/
130theorem rs_all_one {F : Nat → Nat} {n : Nat} (hle : ∀ i < n, F i ≤ 1) (hs : rs F n = n) :
131    ∀ i < n, F i = 1 := by
132  induction n with
133  | zero => intro i hi; omega
134  | succ n ih =>
135    rw [rs_succ] at hs
136    have h1 := hle n (by omega)
137    have h2 : rs F n ≤ n := by
138      have := rs_le (n := n) (G := fun _ => 1) (fun i hi => hle i (by omega)); rw [rs_const] at this; omega
139    intro i hi
140    by_cases e : i = n
141    · subst e; omega
142    · exact ih (fun j hj => hle j (by omega)) (by omega) i (by omega)
143
144/-- Indicator. -/
145def ind (p : Prop) [Decidable p] : Nat := if p then 1 else 0
146
147theorem ind_le (p : Prop) [Decidable p] : ind p ≤ 1 := by unfold ind; split <;> omega
148
149/-! ## Counting and reindexing -/
150
151/-- Number of `i < m` with `P i = v`. -/
152def cnt (P : Nat → Nat) (m v : Nat) : Nat := rs (fun i => if P i = v then 1 else 0) m
153
154/-- **Image lemma.** Summing `F ∘ P` over `i < m` is summing `F v` weighted by
155the multiplicity of `v` among `P 0, …, P (m-1)`. -/
156theorem rs_image (P F : Nat → Nat) (m N : Nat) (hP : ∀ i < m, P i < N) :
157    rs (fun i => F (P i)) m = rs (fun v => cnt P m v * F v) N := by
158  induction m with
159  | zero =>
160    simp only [rs_zero]
161    exact (rs_eq_zero (fun v _ => by simp [cnt])).symm
162  | succ m ih =>
163    rw [rs_succ, ih (fun i hi => hP i (by omega))]
164    have e : (fun v => cnt P (m + 1) v * F v) =
165        (fun v => cnt P m v * F v + (if v = P m then F v else 0)) := by
166      funext v; simp only [cnt, rs_succ]
167      by_cases e : P m = v
168      · subst e; simp [Nat.add_mul]
169      · rw [ite_eq_right e, ite_eq_right (Ne.symm e)]; simp
170    rw [e, rs_add, rs_single, ite_eq_left (hP m (by omega))]
171
172theorem cnt_le_one (P : Nat → Nat) (m v : Nat)
173    (hinj : ∀ i j, i < m → j < m → P i = P j → i = j) : cnt P m v ≤ 1 := by
174  induction m with
175  | zero => simp [cnt]
176  | succ m ih =>
177    simp only [cnt, rs_succ] at *
178    have ih' := ih (fun i j hi hj e => hinj i j (by omega) (by omega) e)
179    by_cases e : P m = v
180    · rw [ite_eq_left e]
181      have : rs (fun i => if P i = v then 1 else 0) m = 0 := rs_eq_zero (fun i hi => by
182        rw [ite_eq_right]; intro e'; have := hinj i m (by omega) (by omega) (e'.trans e.symm); omega)
183      omega
184    · rw [ite_eq_right e]; omega
185
186theorem cnt_pos {P : Nat → Nat} {m v i : Nat} (hi : i < m) (e : P i = v) : 1 ≤ cnt P m v := by
187  have := le_rs (F := fun i => if P i = v then 1 else 0) hi
188  simp only [e, ite_true] at this; exact this
189
190theorem cnt_zero {P : Nat → Nat} {m v : Nat} (h : ∀ i < m, P i ≠ v) : cnt P m v = 0 :=
191  rs_eq_zero (fun i hi => by rw [ite_eq_right (h i hi)])
192
193theorem cnt_exists {P : Nat → Nat} {m v : Nat} (h : 1 ≤ cnt P m v) : ∃ i < m, P i = v := by
194  by_cases hx : ∃ i < m, P i = v
195  · exact hx
196  · have := cnt_zero (P := P) (m := m) (v := v) (fun i hi e => hx ⟨i, hi, e⟩); omega
197
198/-- Pigeonhole: an injective map from `m` points into `N` values has `m ≤ N`. -/
199theorem inj_le (P : Nat → Nat) (m N : Nat) (hP : ∀ i < m, P i < N)
200    (hinj : ∀ i j, i < m → j < m → P i = P j → i = j) : m ≤ N := by
201  have := rs_image P (fun _ => 1) m N hP
202  rw [rs_const] at this
203  have h2 : rs (fun v => cnt P m v * 1) N ≤ rs (fun _ => 1) N :=
204    rs_le (fun v _ => by have := cnt_le_one P m v hinj; omega)
205  rw [rs_const] at h2; omega
206
207/-- An injective self-map of `[0, n)` hits every point. -/
208theorem inj_surj (P : Nat → Nat) (n : Nat) (hP : ∀ i < n, P i < n)
209    (hinj : ∀ i j, i < n → j < n → P i = P j → i = j) : ∀ v < n, ∃ i < n, P i = v := by
210  have h1 := rs_image P (fun _ => 1) n n hP
211  rw [rs_const] at h1
212  have := rs_all_one (F := fun v => cnt P n v) (n := n) (fun v _ => cnt_le_one P n v hinj)
213    (by rw [← rs_congr (F := fun v => cnt P n v * 1) (fun v _ => by simp)]; omega)
214  intro v hv
215  exact cnt_exists (by rw [this v hv]; exact Nat.le_refl 1)
216
217/-- Reindexing by a bijection of `[0, n)`. -/
218theorem rs_perm (σ F : Nat → Nat) (n : Nat) (hσ : ∀ i < n, σ i < n)
219    (hinj : ∀ i j, i < n → j < n → σ i = σ j → i = j) : rs (fun i => F (σ i)) n = rs F n := by
220  rw [rs_image σ F n n hσ]
221  apply rs_congr
222  intro v hv
223  obtain ⟨i, hi, e⟩ := inj_surj σ n hσ hinj v hv
224  have h1 := cnt_pos (P := σ) hi e
225  have h2 := cnt_le_one σ n v hinj
226  rw [show cnt σ n v = 1 by omega, Nat.one_mul]
227
228/-- Regrouping a sum by the value of a key `f i < B`. -/
229theorem rs_regroup (Q : Nat → Prop) [DecidablePred Q] (f W : Nat → Nat) (m B : Nat)
230    (hf : ∀ i < m, Q i → f i < B) :
231    rs (fun i => if Q i then W (f i) else 0) m =
232      rs (fun b => rs (fun i => if Q i ∧ f i = b then 1 else 0) m * W b) B := by
233  have e1 : (fun b => rs (fun i => if Q i ∧ f i = b then 1 else 0) m * W b) =
234      (fun b => rs (fun i => if Q i ∧ f i = b then W b else 0) m) := by
235    funext b
236    rw [Nat.mul_comm, ← rs_mul]
237    apply rs_congr; intro i _; split <;> simp
238  rw [e1, rs_swap]
239  apply rs_congr
240  intro i hi
241  by_cases hq : Q i
242  · rw [ite_eq_left hq]
243    rw [rs_congr (G := fun b => if f i = b then W b else 0) (fun b _ => by
244      by_cases e : f i = b
245      · rw [ite_eq_left ⟨hq, e⟩, ite_eq_left e]
246      · rw [ite_eq_right (fun h => e h.2), ite_eq_right e])]
247    rw [rs_single' W (f i) B (hf i hi hq)]
248  · rw [ite_eq_right hq]
249    exact (rs_eq_zero (fun b _ => by rw [ite_eq_right (fun h => hq h.1)])).symm
250
251/-- Pairing: `F (t/2)` summed over `t < 2J`... in the `gen_bitlen` order,
252position offset `i` belongs to pair `(2J-1-i)/2`. -/
253theorem rs_pair (F : Nat → Nat) (J : Nat) :
254    rs (fun i => F ((2 * J - 1 - i) / 2)) (2 * J) = 2 * rs F J := by
255  induction J with
256  | zero => simp
257  | succ J ih =>
258    rw [show 2 * (J + 1) = 2 + 2 * J by omega, rs_split]
259    rw [rs_congr (F := fun i => F ((2 + 2 * J - 1 - (2 + i)) / 2)) (G := fun i => F ((2 * J - 1 - i) / 2))
260      (fun i hi => by congr 1; omega)]
261    rw [ih, rs_succ]
262    simp only [rs_succ, rs_zero]
263    rw [show (2 + 2 * J - 1 - 0) / 2 = J by omega, show (2 + 2 * J - 1 - 1) / 2 = J by omega]
264    omega
265
266theorem rs_ind_add (p q : Nat → Prop) [DecidablePred p] [DecidablePred q] (n : Nat)
267    (h : ∀ i < n, ¬ (p i ∧ q i)) :
268    rs (fun i => if p i ∨ q i then 1 else 0) n =
269      rs (fun i => if p i then 1 else 0) n + rs (fun i => if q i then 1 else 0) n := by
270  rw [← rs_add]; apply rs_congr; intro i hi
271  have := h i hi
272  by_cases a : p i <;> by_cases b : q i <;> simp_all
273
274end Zlib.Trees.Proofs.GB