trees.c.heap.gbsym.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.gbclk»
2
3/-!
4# trees.c: the symbol-level view of the lengths (pure)
5
6`countBefore`, `kraftSum`, `bitCost` and the bridge `gb_symbolic` from per-position facts to them, copied from the
7earlier attempt (`Spec/trees/Build.lean`, `GenBitlen.lean`).
8-/
9
10namespace Zlib.Trees.Proofs.GB
11open Zlib.Trees.Proofs.GB
12
13/-- Number of symbols `m < n` with length `l`. -/
14def countBefore (len : Nat → Nat) (l n : Nat) : Nat := ((List.range n).filter (fun m => len m = l)).length
15
16
17theorem countBefore_succ (len : Nat → Nat) (l n : Nat) :
18    countBefore len l (n + 1) = countBefore len l n + (if len n = l then 1 else 0) := by
19  unfold countBefore
20  rw [List.range_succ, List.filter_append]
21  by_cases h : len n = l <;> simp [h]
22
23theorem countBefore_zero (len : Nat → Nat) (l : Nat) : countBefore len l 0 = 0 := rfl
24
25/-- Kraft sum scaled by `2 ^ maxlen` over the nonzero lengths `len n`, `n < N`. -/
26def kraftSum (len : Nat → Nat) (N maxlen : Nat) : Nat :=
27  ((List.range N).filter (fun n => len n ≠ 0)).foldl (fun acc n => acc + 2 ^ (maxlen - len n)) 0
28
29
30/-- **Exact bit cost** accumulated by `gen_bitlen` into `opt_len`
31(resp. `static_len` with the static lengths `slen`): `Σ_{n ≤ maxc} fr n * (len n + xbits n)`,
32where `xbits n = extra[n - base]` for `n ≥ base` and `0` otherwise. `build_tree`
33first subtracts 1 from `opt_len` (and `slen n` from `static_len`) for each
34symbol it forces to frequency 1, so its net effect on `opt_len` is
35`bitCost fr' len xbits maxc - #forced` modulo `2^64`, with `fr'` the frequencies
36after forcing. -/
37def bitCost (fr len xbits : Nat → Nat) (maxc : Nat) : Nat :=
38  (List.range (maxc + 1)).foldl (fun acc n => acc + fr n * (len n + xbits n)) 0
39
40
41theorem foldl_filter_add (p : Nat → Prop) [DecidablePred p] (F : Nat → Nat) (l : List Nat) (a : Nat) :
42    (l.filter (fun n => decide (p n))).foldl (fun acc n => acc + F n) a =
43      l.foldl (fun acc n => acc + if p n then F n else 0) a := by
44  induction l generalizing a with
45  | nil => rfl
46  | cons x l ih =>
47    by_cases hx : p x
48    · simp only [List.filter_cons, hx, decide_true, ite_true, List.foldl_cons]; exact ih _
49    · simp only [List.filter_cons, hx, decide_false, Bool.false_eq_true, ite_false, List.foldl_cons, Nat.add_zero]
50      exact ih _
51
52theorem foldl_range_add (F : Nat → Nat) (N : Nat) : (List.range N).foldl (fun acc n => acc + F n) 0 = rs F N := by
53  induction N with
54  | zero => rfl
55  | succ N ih => rw [List.range_succ, List.foldl_append, ih]; rfl
56
57theorem kraftSum_rs (len : Nat → Nat) (N L : Nat) :
58    kraftSum len N L = rs (fun n => if len n ≠ 0 then 2 ^ (L - len n) else 0) N := by
59  unfold kraftSum
60  rw [foldl_filter_add (fun n => len n ≠ 0) (fun n => 2 ^ (L - len n)), foldl_range_add]
61
62theorem bitCost_rs (fr len xb : Nat → Nat) (maxc : Nat) :
63    bitCost fr len xb maxc = rs (fun n => fr n * (len n + xb n)) (maxc + 1) := by
64  unfold bitCost; rw [foldl_range_add]
65
66theorem countBefore_rs (len : Nat → Nat) (l n : Nat) :
67    countBefore len l n = rs (fun m => if len m = l then 1 else 0) n := by
68  induction n with
69  | zero => rfl
70  | succ n ih => rw [countBefore_succ, ih, rs_succ]
71
72
73/-- From per-position facts about node lengths `ln` to the symbol-level targets. -/
74theorem gb_symbolic {H : Nat → Nat} {hm J elems maxc L : Nat} {fr : Nat → UInt16} {xb : Nat → Nat} {sl : Nat → UInt16}
75    (S : PShape H hm J elems maxc) (hT : ∀ v ≤ maxc, fr v ≠ 0 ↔ ∃ q, hm < q ∧ q < 573 ∧ H q = v)
76    (ln : Nat → Nat) (C : Nat → Nat)
77    (hln : ∀ i < 2 * J, H (hm + 1 + i) ≤ maxc → 1 ≤ ln (H (hm + 1 + i)) ∧ ln (H (hm + 1 + i)) ≤ L)
78    (hk : rs (fun i => if H (hm + 1 + i) ≤ maxc then 2 ^ (L - ln (H (hm + 1 + i))) else 0) (2 * J) = 2 ^ L)
79    (hc : ∀ x, 1 ≤ x → blP H hm maxc ln (2 * J) x = C x) :
80    let len := fun v => if v ≤ maxc ∧ fr v ≠ 0 then ln v else 0
81    (∀ n, (maxc < n ∨ fr n = 0) → len n = 0) ∧
82    (∀ n ≤ maxc, fr n ≠ 0 → 1 ≤ len n ∧ len n ≤ L ∧ len n = ln n) ∧
83    kraftSum len (maxc + 1) L = 2 ^ L ∧
84    (∀ x, 1 ≤ x → countBefore len x (maxc + 1) = C x) ∧
85    bitCost (fun n => (fr n).toNat) len xb maxc = costP H hm maxc (fun n => (fr n).toNat) ln xb (2 * J) ∧
86    bitCost (fun n => (fr n).toNat) (fun n => (sl n).toNat) xb maxc =
87      costP H hm maxc (fun n => (fr n).toNat) (fun n => (sl n).toNat) xb (2 * J) := by
88  intro len
89  have hm_eq := S.hm_eq
90  have hleafln : ∀ n ≤ maxc, fr n ≠ 0 → 1 ≤ ln n ∧ ln n ≤ L := by
91    intro n hn hf
92    obtain ⟨q, h1, h2, e⟩ := (hT n hn).mp hf
93    have := hln (q - hm - 1) (by omega) (by rw [show hm + 1 + (q - hm - 1) = q by omega, e]; exact hn)
94    rwa [show hm + 1 + (q - hm - 1) = q by omega, e] at this
95  have hlen_t : ∀ n ≤ maxc, fr n ≠ 0 → len n = ln n := fun n hn hf => by simp only [len]; rw [ite_eq_left ⟨hn, hf⟩]
96  have hlen_f : ∀ n, ¬ (n ≤ maxc ∧ fr n ≠ 0) → len n = 0 := fun n h => by simp only [len]; rw [ite_eq_right h]
97  refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩
98  · intro n h
99    apply hlen_f n
100    intro h'
101    rcases h with h | h
102    · omega
103    · exact h'.2 h
104  · intro n hn hf
105    rw [hlen_t n hn hf]
106    exact ⟨(hleafln n hn hf).1, (hleafln n hn hf).2, rfl⟩
107  · rw [kraftSum_rs, ← hk, S.leaf_sum (fun v => fr v ≠ 0) hT (fun v => 2 ^ (L - ln v))]
108    apply rs_congr; intro n hn
109    by_cases hf : fr n ≠ 0
110    · rw [hlen_t n (by omega) hf, ite_eq_left (by have := hleafln n (by omega) hf; omega), ite_eq_left hf]
111    · rw [hlen_f n (fun h => hf h.2), ite_eq_right (by simp), ite_eq_right hf]
112  · intro x hx
113    rw [countBefore_rs, ← hc x hx]
114    have e3 : blP H hm maxc ln (2 * J) x = rs (fun i => if H (hm + 1 + i) ≤ maxc then
115        (fun v => if ln v = x then 1 else 0) (H (hm + 1 + i)) else 0) (2 * J) := by
116      unfold blP; apply rs_congr; intro i _
117      by_cases a : H (hm + 1 + i) ≤ maxc
118      · rw [ite_eq_left a]
119        by_cases b : ln (H (hm + 1 + i)) = x
120        · rw [ite_eq_left ⟨a, b⟩]; simp only; rw [ite_eq_left b]
121        · rw [ite_eq_right (fun h => b h.2)]; simp only; rw [ite_eq_right b]
122      · rw [ite_eq_right (fun h => a h.1), ite_eq_right a]
123    rw [e3, S.leaf_sum (fun v => fr v ≠ 0) hT (fun v => if ln v = x then 1 else 0)]
124    apply rs_congr; intro n hn
125    by_cases hf : fr n ≠ 0
126    · rw [hlen_t n (by omega) hf, ite_eq_left hf]
127    · rw [hlen_f n (fun h => hf h.2), ite_eq_right (by omega), ite_eq_right hf]
128  · rw [bitCost_rs]; unfold costP
129    rw [S.leaf_sum (fun v => fr v ≠ 0) hT (fun v => (fr v).toNat * (ln v + xb v))]
130    apply rs_congr; intro n hn
131    by_cases hf : fr n ≠ 0
132    · rw [hlen_t n (by omega) hf, ite_eq_left hf]
133    · rw [ite_eq_right hf]; simp only [Decidable.not_not] at hf; rw [hf]; simp
134  · rw [bitCost_rs]; unfold costP
135    rw [S.leaf_sum (fun v => fr v ≠ 0) hT (fun v => (fr v).toNat * ((sl v).toNat + xb v))]
136    apply rs_congr; intro n hn
137    by_cases hf : fr n ≠ 0
138    · rw [ite_eq_left hf]
139    · rw [ite_eq_right hf]; simp only [Decidable.not_not] at hf; rw [hf]; simp
140
141end Zlib.Trees.Proofs.GB