inftrees.c.cover.root.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.tile»
2
3/-!
4# Covering of the root table
5
6Pure arithmetic over the canonical model. A root cell `y < 2^R` is read with the next `R` input bits, the first bit
7being the lowest bit of `y`. The 15-bit word that starts with those bits is `z = rev R y * 2^(15 - R)`, so the cell is
8decided by the tile of `[0, 2^15)` that contains `z`: a code of length `l ≤ R` whose tile contains `z` fills `y`
9(`y % 2^l = H j`, the cells `H j + 2^l * k` that the C writes with `drop = 0`); a code with `l > R` places a link at
10`y = H j % 2^R` (`low` in the C).
11-/
12set_option autoImplicit false
13
14namespace Zlib.Inftrees.Proofs.Cover
15open Zlib.Inftrees.Canon
16
17/-- The `j`-th code (allocation order) is short and fills the root cell `y`. -/
18def ShortAt (ls : List Nat) (R y j : Nat) : Prop := j < nz ls ∧ L ls j ≤ R ∧ y % 2 ^ L ls j = H ls j
19
20/-- The `j`-th code is longer than the root and its link sits at the root cell `y`. -/
21def LongAt (ls : List Nat) (R y j : Nat) : Prop := j < nz ls ∧ R < L ls j ∧ H ls j % 2 ^ R = y
22
23theorem rev_div_short (R l y : Nat) (hl : l ≤ R) :
24    Canon.rev R y / 2 ^ (R - l) = Canon.rev l (y % 2 ^ l) := by
25  have hs := rev_split (R - l) l y
26  rw [show R - l + l = R by omega] at hs
27  rw [hs, Nat.add_mul_div_right _ _ (two_pow_pos' _), Nat.div_eq_of_lt (rev_lt _ _)]
28  simp
29
30/-- The word `z` of a root cell, seen at the length of a short code. -/
31theorem short_div {R l y : Nat} (hR : R ≤ 15) (hl : l ≤ R) :
32    Canon.rev R y * 2 ^ (15 - R) / 2 ^ (15 - l) = Canon.rev l (y % 2 ^ l) := by
33  have hp : 2 ^ (15 - l) = 2 ^ (15 - R) * 2 ^ (R - l) := by rw [← Nat.pow_add]; congr 1; omega
34  rw [hp, ← Nat.div_div_eq_div_mul, Nat.mul_div_cancel _ (two_pow_pos' _), rev_div_short R l y hl]
35
36/-- A short code covers the root cell `y` exactly when its tile contains the word of `y`. -/
37theorem short_iff {ls : List Nat} (hF : Fit ls) {R y j : Nat} (hR : R ≤ 15) (hj : j < nz ls) (hl : L ls j ≤ R) :
38    InTile ls j (Canon.rev R y * 2 ^ (15 - R)) ↔ y % 2 ^ L ls j = H ls j := by
39  rw [inTile_iff_div ls hj, short_div hR hl]
40  have hc := cv_lt hF hj
41  unfold H
42  constructor
43  · intro h
44    rw [← h, rev_rev, Nat.mod_mod]
45  · intro h
46    rw [h, rev_rev, Nat.mod_eq_of_lt hc]
47
48/-- A tile of a code longer than the root lies inside the block of `2^(15 - R)` points that contains it: the group
49`grp` of the code is the block number of any point of its tile. -/
50theorem long_grp {ls : List Nat} {R j z : Nat} (hj : j < nz ls) (hR : R < L ls j) (h : InTile ls j z) :
51    grp ls R j = z / 2 ^ (15 - R) := by
52  have h15 := (L_interval ls hj).2.1
53  have hd := (inTile_iff_div ls hj z).mp h
54  have hp : 2 ^ (15 - R) = 2 ^ (15 - L ls j) * 2 ^ (L ls j - R) := by
55    rw [← Nat.pow_add]; congr 1; omega
56  unfold grp
57  rw [hp, ← Nat.div_div_eq_div_mul, ← Nat.div_div_eq_div_mul, hd]
58  unfold cv; rfl
59
60/-- The bounds of the tile of a short code in units of the root cell. -/
61theorem short_units {ls : List Nat} {R j : Nat} (hR : R ≤ 15) (hj : j < nz ls) (hl : L ls j ≤ R) :
62    K ls j = (cv ls j * 2 ^ (R - L ls j)) * 2 ^ (15 - R) ∧
63    K ls (j + 1) = (cv ls j * 2 ^ (R - L ls j) + 2 ^ (R - L ls j)) * 2 ^ (15 - R) := by
64  have hp : 2 ^ (15 - L ls j) = 2 ^ (R - L ls j) * 2 ^ (15 - R) := by
65    rw [← Nat.pow_add]; congr 1; omega
66  have hm := cv_mul ls hj
67  rw [hp] at hm
68  refine ⟨by rw [← hm, Nat.mul_assoc], ?_⟩
69  rw [K_succ, ← hm, hp, Nat.add_mul, Nat.mul_assoc]
70
71/-- A long code whose link is at `y` belongs to the block `rev R y`. -/
72theorem long_grp_eq {ls : List Nat} (hF : Fit ls) {R y j : Nat} (hR : R ≤ 15) (h : LongAt ls R y j) :
73    grp ls R j = Canon.rev R y := by
74  obtain ⟨hj, hl, hy⟩ := h
75  rw [← hy, H_mod_root ls hj (by omega), rev_rev, Nat.mod_eq_of_lt (grp_lt' hF hR hj)]
76
77/-- **Root covering.** Every cell `y < 2^R` of the root table is, for a code that is not over-subscribed, in
78exactly one of three states: filled by exactly one short code (and no link at `y`); a link of the group of long codes
79`rev R y` (and no short code fills it); or not written at all, which happens only beyond the Kraft sum
80(`K nz ≤ rev R y * 2^(15 - R)`, impossible for a complete code). -/
81inductive RootCell (ls : List Nat) (R y : Nat) : Prop
82  | short (j : Nat) : ShortAt ls R y j → (∀ j', ShortAt ls R y j' → j' = j) → (∀ j', ¬ LongAt ls R y j') →
83      RootCell ls R y
84  | long (j : Nat) : LongAt ls R y j → (∀ j', ¬ ShortAt ls R y j') → RootCell ls R y
85  | free : (∀ j', ¬ ShortAt ls R y j') → (∀ j', ¬ LongAt ls R y j') → K ls (nz ls) ≤ Canon.rev R y * 2 ^ (15 - R) →
86      RootCell ls R y
87
88/-- **Root covering (list model).** For lengths that are not over-subscribed (`Fit`) and `R ≤ 15`, every root cell
89`y < 2^R` is in one of the three states of `RootCell`. -/
90theorem root_cover {ls : List Nat} (hF : Fit ls) {R : Nat} (hR : R ≤ 15) {y : Nat} (hy : y < 2 ^ R) :
91    RootCell ls R y := by
92  generalize hr : Canon.rev R y = r
93  have hrlt : r < 2 ^ R := hr ▸ rev_lt _ _
94  have hshort : ∀ j, ShortAt ls R y j ↔ j < nz ls ∧ L ls j ≤ R ∧ InTile ls j (r * 2 ^ (15 - R)) := by
95    intro j
96    constructor
97    · rintro ⟨hj, hl, h⟩; exact ⟨hj, hl, hr ▸ (short_iff hF hR hj hl).mpr h⟩
98    · rintro ⟨hj, hl, h⟩; exact ⟨hj, hl, (short_iff hF hR hj hl).mp (hr ▸ h)⟩
99  by_cases hz : r * 2 ^ (15 - R) < K ls (nz ls)
100  · obtain ⟨j, hj, hjt⟩ := tile_exists ls hz
101    have t1 := hjt.1
102    have t2 := hjt.2
103    by_cases hl : L ls j ≤ R
104    · refine RootCell.short j ⟨hj, hl, (short_iff hF hR hj hl).mp (hr ▸ hjt)⟩ ?_ ?_
105      · intro j' hj'
106        obtain ⟨hj1, hl1, h1⟩ := (hshort j').mp hj'
107        exact tile_unique ls h1 hjt
108      · intro j' hlong
109        have hg := long_grp_eq hF hR hlong
110        obtain ⟨hj', hRl, _⟩ := hlong
111        have hk1 : r * 2 ^ (15 - R) ≤ K ls j' := by
112          rw [hr] at hg; rw [← hg]; exact Nat.div_mul_le_self _ _
113        have hk2 : K ls j' < (r + 1) * 2 ^ (15 - R) := by
114          rw [hr] at hg; rw [← hg, Nat.succ_mul]; exact Nat.lt_div_mul_add (two_pow_pos' _)
115        obtain ⟨u1, u2⟩ := short_units (ls := ls) hR hj hl
116        have hb := hjt.1
117        have hb2 := hjt.2
118        rw [u1] at hb; rw [u2] at hb2
119        have e1 : cv ls j * 2 ^ (R - L ls j) ≤ r := Nat.le_of_mul_le_mul_right hb (two_pow_pos' _)
120        have e2 : r < cv ls j * 2 ^ (R - L ls j) + 2 ^ (R - L ls j) :=
121          Nat.lt_of_mul_lt_mul_right hb2
122        have e3 : (r + 1) * 2 ^ (15 - R) ≤ K ls (j + 1) := by
123          rw [u2]; exact Nat.mul_le_mul_right _ e2
124        by_cases hjj : j' < j
125        · have := K_strict ls hjj; omega
126        · by_cases hje : j' = j
127          · subst hje; omega
128          · have := K_mono ls (show j + 1 ≤ j' by omega); omega
129    · refine RootCell.long j ⟨hj, by omega, ?_⟩ ?_
130      · have hg := long_grp (R := R) hj (by omega) hjt
131        rw [Nat.mul_div_cancel _ (two_pow_pos' _)] at hg
132        rw [H_mod_root ls hj (by omega), hg, ← hr, rev_rev, Nat.mod_eq_of_lt hy]
133      · intro j' hj'
134        obtain ⟨hj1, hl1, h1⟩ := (hshort j').mp hj'
135        have := tile_unique ls h1 hjt
136        subst this
137        omega
138  · refine RootCell.free ?_ ?_ (by rw [hr]; omega)
139    · intro j' hj'
140      obtain ⟨hj1, hl1, h1⟩ := (hshort j').mp hj'
141      exact not_inTile_of_ge ls hj1 (by omega) h1
142    · intro j' hlong
143      have hg := long_grp_eq hF hR hlong
144      have hj' := hlong.1
145      have hk1 : r * 2 ^ (15 - R) ≤ K ls j' := by
146        rw [hr] at hg; rw [← hg]; exact Nat.div_mul_le_self _ _
147      have := K_strict ls (show j' < nz ls from hj')
148      omega
149
150end Zlib.Inftrees.Proofs.Cover