DeflateKraft.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.gbsym»
2import ZlibF.Math.DeflateCodes
3import ZlibF.Proof.«inftrees.c.link»
4
5/-! # From the compressor's exact Kraft sum to format-valid code lengths -/
6
7namespace Zlib.Trees.Proofs.GB
8
9/-- The decoder's count and the compressor's bounded sum count the same
10symbol indices. -/
11theorem decoder_count_rs (len : Nat → Nat) (N b : Nat) :
12    Zlib.Inftrees.Proofs.cnt len N b = rs (fun i => if len i = b then 1 else 0) N := by
13  rw [← countBefore_rs]
14  unfold countBefore Zlib.Inftrees.Proofs.cnt Zlib.Inftrees.Proofs.fl
15  congr 1
16
17/-- The decoder's cumulative Kraft recurrence is the symbol-level Kraft
18sum, with lengths zero and lengths beyond the current level omitted. -/
19theorem decoder_kraft_rs (len : Nat → Nat) (N l : Nat) :
20    Zlib.Inftrees.Proofs.Kc len N l =
21      rs (fun i => if 1 ≤ len i ∧ len i ≤ l then 2 ^ (l - len i) else 0) N := by
22  induction l with
23  | zero =>
24    rw [Zlib.Inftrees.Proofs.Kc]
25    symm
26    exact rs_eq_zero (fun i hi => by rw [ite_eq_right (by omega)])
27  | succ l ih =>
28    rw [Zlib.Inftrees.Proofs.Kc, ih, decoder_count_rs, ← rs_mul, ← rs_add]
29    apply rs_congr
30    intro i hi
31    by_cases he : len i = l + 1
32    · rw [ite_eq_right (by omega), ite_eq_left he, ite_eq_left (by omega), he, Nat.sub_self, Nat.pow_zero]
33    · by_cases hb : 1 ≤ len i ∧ len i ≤ l
34      · rw [ite_eq_left hb, ite_eq_right he, ite_eq_left (by omega)]
35        rw [show l + 1 - len i = (l - len i) + 1 by omega, Nat.pow_succ]
36        omega
37      · rw [ite_eq_right hb, ite_eq_right he, ite_eq_right (by omega)]
38
39/-- A prefix Kraft sum scaled to a later level is bounded by the complete
40symbol sum at that level. -/
41theorem decoder_kraft_scaled (len : Nat → Nat) (N l L : Nat) (hl : l ≤ L) :
42    Zlib.Inftrees.Proofs.Kc len N l * 2 ^ (L - l) ≤
43      rs (fun i => if len i ≠ 0 then 2 ^ (L - len i) else 0) N := by
44  rw [decoder_kraft_rs, Nat.mul_comm, ← rs_mul]
45  apply rs_le
46  intro i hi
47  by_cases hb : 1 ≤ len i ∧ len i ≤ l
48  · rw [ite_eq_left hb, ite_eq_left (by omega), ← Nat.pow_add]
49    have he : L - l + (l - len i) = L - len i := by omega
50    rw [he]
51    exact Nat.le_refl _
52  · rw [ite_eq_right hb, Nat.mul_zero]
53    omega
54
55/-- Scaling an exact Kraft sum retains exactness when every symbol length
56fits the earlier level. -/
57theorem symbol_kraft_scale (len : Nat → Nat) (N L M : Nat) (hLM : L ≤ M)
58    (hlen : ∀ i < N, len i ≤ L)
59    (hk : rs (fun i => if len i ≠ 0 then 2 ^ (L - len i) else 0) N = 2 ^ L) :
60    rs (fun i => if len i ≠ 0 then 2 ^ (M - len i) else 0) N = 2 ^ M := by
61  have hs : rs (fun i => if len i ≠ 0 then 2 ^ (M - len i) else 0) N =
62      2 ^ (M - L) * rs (fun i => if len i ≠ 0 then 2 ^ (L - len i) else 0) N := by
63    rw [← rs_mul]
64    apply rs_congr
65    intro i hi
66    have hli := hlen i hi
67    by_cases hz : len i = 0
68    · rw [ite_eq_right (by omega), ite_eq_right (by omega), Nat.mul_zero]
69    · rw [ite_eq_left hz, ite_eq_left hz, ← Nat.pow_add]
70      congr 1
71      omega
72  rw [hs, hk, ← Nat.pow_add, show M - L + L = M by omega]
73
74/-- Exact Kraft equality and bounded lengths imply the independent
75format's Fits and Complete predicates, for any of its three code kinds. -/
76theorem format_code_complete (len : Nat → Nat) (N L : Nat) (hL : L ≤ 15)
77    (hlen : ∀ i < N, len i ≤ L)
78    (hk : rs (fun i => if len i ≠ 0 then 2 ^ (L - len i) else 0) N = 2 ^ L) :
79    ∀ kind : ZlibF.Spec.CodeKind, ZlibF.Spec.Acceptable kind (Zlib.Inftrees.Proofs.lensOf len N) := by
80  have h15 : ∀ i < N, len i ≤ 15 := fun i hi => Nat.le_trans (hlen i hi) hL
81  have hk15 := symbol_kraft_scale len N L 15 hL hlen hk
82  have hfit : Zlib.Inftrees.Proofs.Fits len N := by
83    intro l hl1 hl15
84    have hs := decoder_kraft_scaled len N l 15 hl15
85    rw [hk15] at hs
86    have hpow : 2 ^ 15 = 2 ^ l * 2 ^ (15 - l) := by
87      rw [← Nat.pow_add, show l + (15 - l) = 15 by omega]
88    rw [hpow] at hs
89    exact Nat.le_of_mul_le_mul_right hs (Nat.two_pow_pos _)
90  have hfull : Zlib.Inftrees.Proofs.Kc len N 15 = 2 ^ 15 := by
91    rw [decoder_kraft_rs, ← hk15]
92    apply rs_congr
93    intro i hi
94    have hv := h15 i hi
95    by_cases hz : len i = 0
96    · rw [ite_eq_right (by omega), ite_eq_right (by omega)]
97    · rw [ite_eq_left (by omega), ite_eq_left hz]
98  intro kind
99  refine ⟨?_, (Zlib.Inftrees.Proofs.fits_iff len N).mpr hfit,
100    Or.inl ((Zlib.Inftrees.Proofs.complete_iff len N).mpr hfull)⟩
101  intro x hx
102  simp only [Zlib.Inftrees.Proofs.lensOf, List.mem_map] at hx
103  obtain ⟨i, hi, rfl⟩ := hx
104  exact h15 i (List.mem_range.mp hi)
105
106
107/-- Rank within the earlier symbols is the format's rank in the length
108list prefix. Symbol order is unchanged by the representation conversion. -/
109theorem canonical_rank_format (len : Nat → Nat) (N v l : Nat) (hv : v ≤ N) :
110    Zlib.Trees.Math.countBefore len l v =
111      (((Zlib.Inftrees.Proofs.lensOf len N).take v).filter (· == l)).length := by
112  unfold Zlib.Trees.Math.countBefore Zlib.Inftrees.Proofs.lensOf
113  rw [← List.map_take, List.take_range, Nat.min_eq_left hv, List.filter_map, List.length_map]
114  rfl
115
116/-- Actual count values with a zero length-zero count induce the independent
117format's starting-code recurrence. -/
118theorem canonical_start_format (len bl : Nat → Nat) (N : Nat) (h0 : bl 0 = 0)
119    (hc : ∀ b, 1 ≤ b → b < 16 → bl b = ZlibF.Spec.count (Zlib.Inftrees.Proofs.lensOf len N) b) :
120    ∀ b, b ≤ 15 → Zlib.Trees.Math.nextCode bl b = ZlibF.Spec.codeStart (Zlib.Inftrees.Proofs.lensOf len N) b := by
121  intro b
122  induction b with
123  | zero => intro hb; rfl
124  | succ b ih =>
125    intro hb
126    rw [Zlib.Trees.Math.nextCode, ZlibF.Spec.codeStart, ih (by omega)]
127    by_cases hb0 : b = 0
128    · subst b
129      rw [h0, ite_eq_left rfl]
130    · rw [ite_eq_right hb0, hc b (by omega) (by omega)]
131
132/-- Exact stored-code bits coincide with the independent format code for
133that symbol. This establishes meaning of the bits, separately from Fits. -/
134theorem stored_bits_format (len bl : Nat → Nat) (N v : Nat) (hv : v < N) (hl : len v ≤ 15)
135    (h0 : bl 0 = 0)
136    (hc : ∀ b, 1 ≤ b → b < 16 → bl b = ZlibF.Spec.count (Zlib.Inftrees.Proofs.lensOf len N) b) :
137    (List.range (len v)).map (fun i => (Zlib.Trees.Math.storedCode bl len v).testBit i) =
138      ZlibF.Spec.codeOf (Zlib.Inftrees.Proofs.lensOf len N) v := by
139  unfold Zlib.Trees.Math.storedCode
140  rw [Zlib.Trees.Math.reverseLowBits_wire]
141  have hlen : (Zlib.Inftrees.Proofs.lensOf len N).getD v 0 = len v := by
142    simp [Zlib.Inftrees.Proofs.lensOf, List.getD_eq_getElem?_getD, hv]
143  unfold ZlibF.Spec.codeOf Zlib.Trees.Math.canonicalCode
144  rw [hlen, canonical_start_format len bl N h0 hc _ hl, canonical_rank_format len N v (len v) (by omega)]
145  rfl
146
147end Zlib.Trees.Proofs.GB