inftrees.c.cover.group.lean

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

1import ZlibF.Proof.«inftrees.c.cover.root»
2
3/-!
4# Covering of a sub-table
5
6Pure arithmetic over the canonical model. The long codes whose first `R` bits are the block `p` (`grp = p`) form the
7group of one root link. For a complete code they tile the block `[p * 2^(15-R), (p+1) * 2^(15-R))`. A sub-table with
8`2^c` cells is read with the `c` bits that follow the root bits; the cell `t` is decided by the tile that contains
9`z = p * 2^(15-R) + rev c t * 2^(15-R-c)`. The code `j` of the group (`e = L j - R ≤ c`) fills the cells
10`t = H j / 2^R + 2^e * t'`, `t' < 2^(c - e)`, which is what the C writes (`next[(huff >> drop) + fill]`).
11-/
12set_option autoImplicit false
13
14namespace Zlib.Inftrees.Proofs.Cover
15open Zlib.Inftrees.Canon
16
17/-- The `j`-th code is longer than the root and in the group of block `p`. -/
18def Group (ls : List Nat) (R p j : Nat) : Prop := j < nz ls ∧ R < L ls j ∧ grp ls R j = p
19
20theorem z_div (R c p t e : Nat) (hRc : R + c ≤ 15) (hec : e ≤ c) :
21    (p * 2 ^ (15 - R) + Canon.rev c t * 2 ^ (15 - R - c)) / 2 ^ (15 - R - e) =
22      p * 2 ^ e + Canon.rev e (t % 2 ^ e) := by
23  have h1 : 2 ^ (15 - R - e) = 2 ^ (15 - R - c) * 2 ^ (c - e) := by
24    rw [← Nat.pow_add]; congr 1; omega
25  have h2 : p * 2 ^ (15 - R) = (p * 2 ^ e) * 2 ^ (15 - R - e) := by
26    rw [Nat.mul_assoc, ← Nat.pow_add]; congr 2; omega
27  rw [h2, h1, show (p * 2 ^ e) * (2 ^ (15 - R - c) * 2 ^ (c - e)) =
28      (2 ^ (15 - R - c) * 2 ^ (c - e)) * (p * 2 ^ e) from Nat.mul_comm _ _,
29    Nat.mul_add_div (Nat.mul_pos (two_pow_pos' _) (two_pow_pos' _)),
30    Nat.mul_comm (Canon.rev c t), Nat.mul_div_mul_left _ _ (two_pow_pos' _), rev_div_short c e t hec]
31
32theorem z_lt (R c p t : Nat) (hRc : R + c ≤ 15) :
33    p * 2 ^ (15 - R) + Canon.rev c t * 2 ^ (15 - R - c) < (p + 1) * 2 ^ (15 - R) := by
34  have h : Canon.rev c t * 2 ^ (15 - R - c) < 2 ^ (15 - R) := by
35    have hp : 2 ^ (15 - R) = 2 ^ c * 2 ^ (15 - R - c) := by rw [← Nat.pow_add]; congr 1; omega
36    rw [hp]
37    exact Nat.mul_lt_mul_of_pos_right (rev_lt _ _) (two_pow_pos' _)
38  rw [Nat.succ_mul]; omega
39
40theorem z_div_root (R c p t : Nat) (hRc : R + c ≤ 15) :
41    (p * 2 ^ (15 - R) + Canon.rev c t * 2 ^ (15 - R - c)) / 2 ^ (15 - R) = p := by
42  have h := z_lt R c p t hRc
43  have := two_pow_pos' (15 - R)
44  rw [Nat.add_comm, Nat.add_mul_div_right _ _ this, Nat.div_eq_of_lt]
45  · simp
46  · rw [Nat.succ_mul] at h; omega
47
48/-- `cv` of a code of the group, split at the root. -/
49theorem cv_group {ls : List Nat} {R p j : Nat} (hg : Group ls R p j) :
50    cv ls j = p * 2 ^ (L ls j - R) + cv ls j % 2 ^ (L ls j - R) := by
51  obtain ⟨hj, hl, hp⟩ := hg
52  have h15 := (L_interval ls hj).2.1
53  have hq : cv ls j / 2 ^ (L ls j - R) = p := by
54    rw [← hp]; unfold grp cv
55    rw [Nat.div_div_eq_div_mul, ← Nat.pow_add]
56    congr 2; omega
57  have := Nat.div_add_mod (cv ls j) (2 ^ (L ls j - R))
58  rw [hq, Nat.mul_comm (2 ^ (L ls j - R)) p] at this
59  omega
60
61/-- **Group covering (list model, residue form).** For a complete code, a group `p` of long codes (`j0` is one) and a
62width `c` with `R + c ≤ 15` that holds every code of the group, every cell `t` of the sub-table is covered by exactly
63one code `j` of the group: `t % 2^(L j - R) = H j / 2^R`. -/
64theorem group_cover {ls : List Nat} (hcomp : K ls (nz ls) = 2 ^ 15) {R p j0 : Nat} (hR : R ≤ 15)
65    (hg0 : Group ls R p j0) {c : Nat} (hRc : R + c ≤ 15) (hcl : ∀ j, Group ls R p j → L ls j ≤ R + c)
66    (t : Nat) :
67    ∃ j, Group ls R p j ∧ t % 2 ^ (L ls j - R) = H ls j / 2 ^ R ∧
68      ∀ j', Group ls R p j' → t % 2 ^ (L ls j' - R) = H ls j' / 2 ^ R → j' = j := by
69  have hF : Fit ls := by show K ls (nz ls) ≤ 2 ^ 15; omega
70  obtain ⟨hj0, hl0, hp0⟩ := hg0
71  have hplt : p < 2 ^ R := hp0 ▸ grp_lt' hF hR hj0
72  generalize hz : p * 2 ^ (15 - R) + Canon.rev c t * 2 ^ (15 - R - c) = z
73  have hzlt : z < (p + 1) * 2 ^ (15 - R) := hz ▸ z_lt R c p t hRc
74  have hzdiv : z / 2 ^ (15 - R) = p := hz ▸ z_div_root R c p t hRc
75  have hzge : p * 2 ^ (15 - R) ≤ z := by rw [← hz]; omega
76  have hpow : 2 ^ 15 = 2 ^ R * 2 ^ (15 - R) := by rw [← Nat.pow_add]; congr 1; omega
77  have hzK : z < K ls (nz ls) := by
78    rw [hcomp, hpow]
79    have : (p + 1) * 2 ^ (15 - R) ≤ 2 ^ R * 2 ^ (15 - R) := Nat.mul_le_mul_right _ hplt
80    omega
81  obtain ⟨j, hj, hjt⟩ := tile_exists ls hzK
82  have t1 := hjt.1
83  have t2 := hjt.2
84  have hlong : R < L ls j := by
85    refine Classical.byContradiction fun hl => ?_
86    have hl' : L ls j ≤ R := by omega
87    obtain ⟨u1, u2⟩ := short_units (ls := ls) hR hj hl'
88    have hk0a : p * 2 ^ (15 - R) ≤ K ls j0 := by rw [← hp0]; exact Nat.div_mul_le_self _ _
89    have hk0b : K ls j0 < (p + 1) * 2 ^ (15 - R) := by
90      rw [← hp0, Nat.succ_mul]; exact Nat.lt_div_mul_add (two_pow_pos' _)
91    rw [u1] at t1; rw [u2] at t2
92    have e1 : cv ls j * 2 ^ (R - L ls j) ≤ p := by
93      have : (cv ls j * 2 ^ (R - L ls j)) * 2 ^ (15 - R) < (p + 1) * 2 ^ (15 - R) := by omega
94      have := Nat.lt_of_mul_lt_mul_right this
95      omega
96    have e2 : p < cv ls j * 2 ^ (R - L ls j) + 2 ^ (R - L ls j) := by
97      have : p * 2 ^ (15 - R) < (cv ls j * 2 ^ (R - L ls j) + 2 ^ (R - L ls j)) * 2 ^ (15 - R) := by omega
98      exact Nat.lt_of_mul_lt_mul_right this
99    have e3 : K ls j ≤ K ls j0 := by
100      rw [u1]; exact Nat.le_trans (Nat.mul_le_mul_right _ e1) hk0a
101    have e4 : K ls j0 < K ls (j + 1) := by
102      rw [u2]
103      exact Nat.lt_of_lt_of_le hk0b (Nat.mul_le_mul_right _ e2)
104    by_cases hjj : j0 < j
105    · have := K_strict ls hjj; omega
106    · by_cases hje : j0 = j
107      · subst hje; omega
108      · have := K_mono ls (show j + 1 ≤ j0 by omega); omega
109  have hgrp : grp ls R j = p := by rw [long_grp hj hlong hjt, hzdiv]
110  have hgj : Group ls R p j := ⟨hj, hlong, hgrp⟩
111  have h15 := (L_interval ls hj).2.1
112  have hec := hcl j hgj
113  have hzval : ∀ j', Group ls R p j' → z / 2 ^ (15 - L ls j') = p * 2 ^ (L ls j' - R) +
114      Canon.rev (L ls j' - R) (t % 2 ^ (L ls j' - R)) := by
115    intro j' hj'
116    have hl := hcl j' hj'
117    have hl15 := (L_interval ls hj'.1).2.1
118    have hRl := hj'.2.1
119    rw [← hz, show 15 - L ls j' = 15 - R - (L ls j' - R) by omega]
120    exact z_div R c p t (L ls j' - R) hRc (by omega)
121  have hHdiv : ∀ j', Group ls R p j' → H ls j' / 2 ^ R = Canon.rev (L ls j' - R) (cv ls j' % 2 ^ (L ls j' - R)) :=
122    fun j' hj' => H_div_root ls hj'.1 (by have := hj'.2.1; omega)
123  refine ⟨j, hgj, ?_, ?_⟩
124  · rw [hHdiv j hgj]
125    have hcv := (inTile_iff_div ls hj z).mp hjt
126    rw [hzval j hgj] at hcv
127    have hm : cv ls j % 2 ^ (L ls j - R) = Canon.rev (L ls j - R) (t % 2 ^ (L ls j - R)) := by
128      rw [← hcv, Nat.add_comm, Nat.add_mul_mod_self_right, Nat.mod_eq_of_lt (rev_lt _ _)]
129    rw [hm, rev_rev, Nat.mod_mod]
130  · intro j' hj' heq
131    have e1 : Canon.rev (L ls j' - R) (t % 2 ^ (L ls j' - R)) = cv ls j' % 2 ^ (L ls j' - R) := by
132      rw [heq, hHdiv j' hj', rev_rev, Nat.mod_mod]
133    refine tile_unique ls ((inTile_iff_div ls hj'.1 z).mpr ?_) hjt
134    rw [hzval j' hj', e1]; exact (cv_group hj').symm
135
136/-- The first entry index of a code of the group inside its sub-table is below `2^(L j - R)`. -/
137theorem first_lt {ls : List Nat} {R p j : Nat} (hg : Group ls R p j) : H ls j / 2 ^ R < 2 ^ (L ls j - R) := by
138  obtain ⟨hj, hl, _⟩ := hg
139  have h15 := (L_interval ls hj).2.1
140  rw [Nat.div_lt_iff_lt_mul (two_pow_pos' _), ← Nat.pow_add, show L ls j - R + R = L ls j by omega]
141  exact H_lt ls j
142
143/-- The cells that a code of the group writes lie inside the sub-table of `2^c` cells. -/
144theorem cell_lt {ls : List Nat} {R p j c : Nat} (hg : Group ls R p j) (hl : L ls j ≤ R + c) {t' : Nat}
145    (ht' : t' < 2 ^ (R + c - L ls j)) : H ls j / 2 ^ R + 2 ^ (L ls j - R) * t' < 2 ^ c := by
146  have h1 := first_lt hg
147  have hR := hg.2.1
148  have hp : 2 ^ c = 2 ^ (L ls j - R) * 2 ^ (R + c - L ls j) := by
149    rw [← Nat.pow_add]; congr 1; omega
150  rw [hp]
151  have : 2 ^ (L ls j - R) * (t' + 1) ≤ 2 ^ (L ls j - R) * 2 ^ (R + c - L ls j) :=
152    Nat.mul_le_mul_left _ ht'
153  rw [Nat.mul_succ] at this
154  omega
155
156/-- **Group covering, in the index form of the C.** For a complete code, a group `p` of long codes (one of them is
157`j0`) and a sub-table width `c` with `R + c ≤ 15` that holds every code of the group (`L j ≤ R + c`, which
158`inflate_table` ensures with `look`), every cell `t < 2^c` of the sub-table is written by exactly one code `j` of the
159group, as `next[H j / 2^R + 2^(L j - R) * t']` with `t' < 2^(R + c - L j)`. (`H j / 2^R` is `huff >> drop` of the
160code at the time it is written.) -/
161theorem group_cover_idx {ls : List Nat} (hcomp : K ls (nz ls) = 2 ^ 15) {R p j0 : Nat} (hR : R ≤ 15)
162    (hg0 : Group ls R p j0) {c : Nat} (hRc : R + c ≤ 15) (hcl : ∀ j, Group ls R p j → L ls j ≤ R + c)
163    {t : Nat} (ht : t < 2 ^ c) :
164    ∃ j, Group ls R p j ∧ (∃ t', t' < 2 ^ (R + c - L ls j) ∧ t = H ls j / 2 ^ R + 2 ^ (L ls j - R) * t') ∧
165      ∀ j' t', Group ls R p j' → t = H ls j' / 2 ^ R + 2 ^ (L ls j' - R) * t' → j' = j := by
166  obtain ⟨j, hg, hm, hu⟩ := group_cover hcomp hR hg0 hRc hcl t
167  have hmodeq : ∀ j' t', Group ls R p j' → (H ls j' / 2 ^ R + 2 ^ (L ls j' - R) * t') % 2 ^ (L ls j' - R) =
168      H ls j' / 2 ^ R := by
169    intro j' t' hj'
170    rw [Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt (first_lt hj')]
171  refine ⟨j, hg, ⟨t / 2 ^ (L ls j - R), ?_, ?_⟩, ?_⟩
172  · have hl := hcl j hg
173    have hR' := hg.2.1
174    have hp : 2 ^ c = 2 ^ (L ls j - R) * 2 ^ (R + c - L ls j) := by
175      rw [← Nat.pow_add]; congr 1; omega
176    rw [hp] at ht
177    exact Nat.div_lt_of_lt_mul ht
178  · have := Nat.mod_add_div t (2 ^ (L ls j - R))
179    rw [hm] at this; omega
180  · intro j' t' hj' heq
181    apply hu j' hj'
182    rw [heq, hmodeq j' t' hj']
183
184end Zlib.Inftrees.Proofs.Cover