InflateTableGeometry.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.step»
2import ZlibF.Proof.«inftrees.c.cover.root»
3
4/-!
5# Disjoint cells in the actual decode-table layout
6
7The existing descriptor vocabulary lives with the constructor proof. These
8lemmas are heap-free: separate allocation intervals first, then use canonical
9prefix uniqueness inside an interval.
10-/
11
12namespace Zlib.Inftrees.Proofs
13open Zlib.Inftrees.Canon
14set_option autoImplicit false
15
16theorem desc_regions (ls : List Nat) (root mx : Nat) {i j : Nat} (order : i ≤ j) :
17    desc ls root mx i = desc ls root mx j ∨
18      (desc ls root mx i).used ≤ (desc ls root mx j).base := by
19  induction j with
20  | zero => have : i = 0 := by omega
21            subst i
22            exact Or.inl rfl
23  | succ j ih =>
24    by_cases same : i = j + 1
25    · subst i
26      exact Or.inl rfl
27    · have previous := ih (by omega)
28      by_cases start : startsAt ls root j
29      · rw [desc_succ_of_starts ls root mx j start]
30        dsimp only
31        right
32        rcases previous with equal | separated
33        · rw [equal, desc_used]
34          exact Nat.le_refl _
35        · have := Nat.two_pow_pos (desc ls root mx j).curr
36          omega
37      · rw [desc_succ_of_not ls root mx j start]
38        exact previous
39
40theorem gAddr_in_region {ls : List Nat} {root mx i m : Nat}
41    (code : CompleteCode ls root mx) (index : i < nz ls)
42    (copy : m < gReps ls root mx i) :
43    (desc ls root mx i).base ≤ gAddr ls root mx i m ∧
44      gAddr ls root mx i m < (desc ls root mx i).used := by
45  obtain ⟨drop, fits, _, _⟩ := desc_fits code index
46  have power : 2 ^ (L ls i - (desc ls root mx i).drop) *
47      2 ^ (desc ls root mx i).drop = 2 ^ L ls i := by
48    rw [← Nat.pow_add]
49    congr 1
50    omega
51  have quotient : H ls i / 2 ^ (desc ls root mx i).drop <
52      2 ^ (L ls i - (desc ls root mx i).drop) := by
53    rw [Nat.div_lt_iff_lt_mul (Nat.two_pow_pos _), power]
54    exact Canon.H_lt ls i
55  have capacity : 2 ^ ((desc ls root mx i).curr -
56      (L ls i - (desc ls root mx i).drop)) *
57      2 ^ (L ls i - (desc ls root mx i).drop) = 2 ^ (desc ls root mx i).curr := by
58    rw [← Nat.pow_add]
59    congr 1
60    omega
61  have count := Nat.mul_le_mul_right
62    (2 ^ (L ls i - (desc ls root mx i).drop)) (Nat.succ_le_of_lt copy)
63  change (m + 1) * _ ≤ 2 ^ ((desc ls root mx i).curr -
64    (L ls i - (desc ls root mx i).drop)) * _ at count
65  rw [capacity, Nat.add_mul, Nat.one_mul] at count
66  rw [desc_used]
67  unfold gAddr
68  constructor
69  · exact Nat.le_trans (Nat.le_add_right _ _) (Nat.le_add_right _ _)
70  · have localBound : H ls i / 2 ^ (desc ls root mx i).drop +
71        m * 2 ^ (L ls i - (desc ls root mx i).drop) < 2 ^ (desc ls root mx i).curr := by
72      calc
73        _ < 2 ^ (L ls i - (desc ls root mx i).drop) +
74            m * 2 ^ (L ls i - (desc ls root mx i).drop) := Nat.add_lt_add_right quotient _
75        _ = m * 2 ^ (L ls i - (desc ls root mx i).drop) +
76            2 ^ (L ls i - (desc ls root mx i).drop) := Nat.add_comm _ _
77        _ ≤ _ := count
78    simpa only [Nat.add_assoc] using Nat.add_lt_add_left localBound (desc ls root mx i).base
79
80theorem desc_residue {ls : List Nat} {root mx i : Nat}
81    (code : CompleteCode ls root mx) (index : i < nz ls) :
82    H ls i % 2 ^ (desc ls root mx i).drop =
83      (desc ls root mx i).low % 2 ^ (desc ls root mx i).drop := by
84  by_cases short : L ls i ≤ root
85  · rw [desc_short ls index short]
86    simp [desc, Nat.mod_one]
87  · obtain ⟨a, _, _, _, drop, _, low⟩ := desc_long (mx := mx) code.min_le index (by omega)
88    rw [drop, low, H_mod_root ls index (by omega),
89      Nat.mod_eq_of_lt (Canon.rev_lt _ _)]
90
91theorem replicated_residue (value len drop m : Nat) (inside : value < 2 ^ len)
92    (le : drop ≤ len) :
93    (value % 2 ^ drop + 2 ^ drop * (value / 2 ^ drop + m * 2 ^ (len - drop))) %
94      2 ^ len = value := by
95  have factor : 2 ^ drop * 2 ^ (len - drop) = 2 ^ len := by
96    rw [← Nat.pow_add]
97    congr 1
98    omega
99  have decompose := Nat.mod_add_div value (2 ^ drop)
100  rw [Nat.mul_add, ← Nat.mul_assoc, Nat.mul_comm (2 ^ drop) m,
101    Nat.mul_assoc, factor]
102  rw [show value % 2 ^ drop + (2 ^ drop * (value / 2 ^ drop) + m * 2 ^ len) =
103    value + m * 2 ^ len by omega]
104  rw [Nat.add_mul_mod_self_right, Nat.mod_eq_of_lt inside]
105
106theorem canonical_prefix_unique {ls : List Nat} (fit : Cover.Fit ls)
107    {i j value : Nat} (hi : i < nz ls) (hj : j < nz ls)
108    (left : value % 2 ^ L ls i = H ls i) (right : value % 2 ^ L ls j = H ls j) : i = j := by
109  have ti := (Cover.short_iff fit (R := 15) (by omega) hi (L_interval ls hi).2.1).mpr left
110  have tj := (Cover.short_iff fit (R := 15) (by omega) hj (L_interval ls hj).2.1).mpr right
111  exact Cover.tile_unique ls ti tj
112
113/-- Every root cell covered by a short code is one of that code's actual
114replicated write addresses, with the replica index in range. -/
115theorem short_root_replica {ls : List Nat} {root mx i cell : Nat}
116    (index : i < nz ls) (short : L ls i ≤ root) (inside : cell < 2 ^ root)
117    (residue : cell % 2 ^ L ls i = H ls i) :
118    ∃ replica, replica < gReps ls root mx i ∧ gAddr ls root mx i replica = cell := by
119  refine ⟨cell / 2 ^ L ls i, ?_, ?_⟩
120  · unfold gReps
121    rw [desc_short ls index short]
122    simp only [desc, Nat.sub_zero]
123    rw [Nat.div_lt_iff_lt_mul (Nat.two_pow_pos _), ← Nat.pow_add]
124    have exponent : root - L ls i + L ls i = root := by omega
125    rwa [exponent]
126  · unfold gAddr
127    rw [desc_short ls index short]
128    simp only [desc, Nat.pow_zero, Nat.div_one, Nat.sub_zero, Nat.zero_add]
129    have decompose := Nat.mod_add_div cell (2 ^ L ls i)
130    rw [residue] at decompose
131    simpa only [Nat.mul_comm] using decompose
132
133theorem gAddr_unique {ls : List Nat} {root mx i j m n : Nat}
134    (code : CompleteCode ls root mx) (hi : i < nz ls) (hj : j < nz ls)
135    (hm : m < gReps ls root mx i) (hn : n < gReps ls root mx j)
136    (same : gAddr ls root mx i m = gAddr ls root mx j n) : i = j ∧ m = n := by
137  have ri := gAddr_in_region code hi hm
138  have rj := gAddr_in_region code hj hn
139  have descriptors : desc ls root mx i = desc ls root mx j := by
140    by_cases order : i ≤ j
141    · rcases desc_regions ls root mx order with equal | separated
142      · exact equal
143      · omega
144    · rcases desc_regions ls root mx (by omega : j ≤ i) with equal | separated
145      · exact equal.symm
146      · omega
147  have dropI := (desc_fits code hi).1
148  have dropJ := (desc_fits code hj).1
149  have residueI := desc_residue code hi
150  have residueJ := desc_residue code hj
151  rw [← descriptors] at dropJ residueJ
152  have low : H ls i % 2 ^ (desc ls root mx i).drop =
153      H ls j % 2 ^ (desc ls root mx i).drop := residueI.trans residueJ.symm
154  have localSame : H ls i / 2 ^ (desc ls root mx i).drop +
155      m * 2 ^ (L ls i - (desc ls root mx i).drop) =
156      H ls j / 2 ^ (desc ls root mx i).drop +
157      n * 2 ^ (L ls j - (desc ls root mx i).drop) := by
158    unfold gAddr at same
159    rw [← descriptors] at same
160    omega
161  let value := H ls i % 2 ^ (desc ls root mx i).drop +
162    2 ^ (desc ls root mx i).drop *
163      (H ls i / 2 ^ (desc ls root mx i).drop +
164        m * 2 ^ (L ls i - (desc ls root mx i).drop))
165  have left : value % 2 ^ L ls i = H ls i :=
166    replicated_residue _ _ _ _ (Canon.H_lt ls i) dropI
167  have right : value % 2 ^ L ls j = H ls j := by
168    dsimp only [value]
169    rw [low, localSame]
170    exact replicated_residue _ _ _ _ (Canon.H_lt ls j) dropJ
171  have fit : Cover.Fit ls := Nat.le_of_eq code.complete
172  have equal := canonical_prefix_unique fit hi hj left right
173  subst j
174  refine ⟨rfl, ?_⟩
175  unfold gAddr at same
176  have product : m * 2 ^ (L ls i - (desc ls root mx i).drop) =
177      n * 2 ^ (L ls i - (desc ls root mx i).drop) := by omega
178  exact Nat.eq_of_mul_eq_mul_right (Nat.two_pow_pos _) product
179
180theorem startsAt_group_strict {ls : List Nat} {root a b : Nat}
181    (ha : a < nz ls) (hb : b < nz ls) (ordered : a < b)
182    (long : root < L ls a) (positive : 1 ≤ b) (start : startsAt ls root (b - 1)) :
183    grp ls root a < grp ls root b := by
184  have monotone := grp_mono ls root (Nat.le_of_lt ordered)
185  by_cases strict : grp ls root a < grp ls root b
186  · exact strict
187  exfalso
188  have equal : grp ls root a = grp ls root b := by omega
189  have left := grp_mono ls root (by omega : a ≤ b - 1)
190  have right := grp_mono ls root (by omega : b - 1 ≤ b)
191  have lengths := L_mono ls (by omega : a ≤ b - 1) (by omega : b - 1 < nz ls)
192  unfold startsAt at start
193  rw [show b - 1 + 1 = b by omega] at start
194  rcases start.2 with short | changed
195  · omega
196  · apply changed
197    omega
198
199theorem gSlot_unique {ls : List Nat} {root mx a b : Nat}
200    (code : CompleteCode ls root mx) (ha0 : 1 ≤ a) (ha : a < nz ls)
201    (sa : startsAt ls root (a - 1)) (hb0 : 1 ≤ b) (hb : b < nz ls)
202    (sb : startsAt ls root (b - 1)) (same : gSlot ls root a = gSlot ls root b) : a = b := by
203  have sameGroup : grp ls root a = grp ls root b :=
204    Canon.rev_inj (grp_lt code ha) (grp_lt code hb) same
205  have la : root < L ls a := by
206    have := sa.1
207    simpa only [show a - 1 + 1 = a by omega] using this
208  have lb : root < L ls b := by
209    have := sb.1
210    simpa only [show b - 1 + 1 = b by omega] using this
211  by_cases order : a < b
212  · have := startsAt_group_strict ha hb order la hb0 sb
213    omega
214  · by_cases reverse : b < a
215    · have := startsAt_group_strict hb ha reverse lb ha0 sa
216      omega
217    · omega
218
219theorem gSlot_ne_gAddr {ls : List Nat} {root mx a i m : Nat}
220    (code : CompleteCode ls root mx) (positive : 1 ≤ a) (ha : a < nz ls)
221    (start : startsAt ls root (a - 1)) (hi : i < nz ls)
222    (hm : m < gReps ls root mx i) : gSlot ls root a ≠ gAddr ls root mx i m := by
223  intro same
224  have rootBound : gSlot ls root a < 2 ^ root := Canon.rev_lt _ _
225  by_cases short : L ls i ≤ root
226  · have residue : gAddr ls root mx i m % 2 ^ L ls i = H ls i := by
227      unfold gAddr
228      rw [desc_short ls hi short]
229      simp only [desc, Nat.zero_add, Nat.pow_zero, Nat.div_one, Nat.sub_zero]
230      rw [Nat.add_mul_mod_self_right, Nat.mod_eq_of_lt (Canon.H_lt ls i)]
231    have shortAt : Cover.ShortAt ls root (gSlot ls root a) i :=
232      ⟨hi, short, by rw [same]; exact residue⟩
233    have long : root < L ls a := by
234      have := start.1
235      simpa only [show a - 1 + 1 = a by omega] using this
236    have longAt : Cover.LongAt ls root (gSlot ls root a) a := by
237      refine ⟨ha, long, ?_⟩
238      rw [Canon.H_mod_root ls ha (by omega)]
239      rfl
240    have cover := Cover.root_cover (Nat.le_of_eq code.complete)
241      (Nat.le_trans code.root_le code.mx_le) rootBound
242    cases cover with
243    | short j _ _ noLong => exact noLong a longAt
244    | long j _ noShort => exact noShort i shortAt
245    | free noShort _ _ => exact noShort i shortAt
246  · have region := gAddr_in_region code hi hm
247    obtain ⟨_, _, _, _, drop, _, _⟩ := desc_long (mx := mx) code.min_le hi (by omega)
248    have baseBound : 2 ^ root ≤ (desc ls root mx i).base := by
249      rcases desc_regions ls root mx (i := 0) (j := i) (by omega) with equal | separated
250      · have sameDrop := congrArg Desc.drop equal
251        simp only [desc] at sameDrop
252        rw [drop] at sameDrop
253        have := code.root_pos
254        omega
255      · exact separated
256    omega
257
258/-- Complete canonical codes have disjoint replicated leaves and link
259slots in the constructor's existing concrete descriptor layout. -/
260theorem geometry_complete {ls : List Nat} {root mx : Nat}
261    (code : CompleteCode ls root mx) : GeoOK ls root mx := by
262  constructor
263  · intro i j m n hi hj hm hn same
264    exact gAddr_unique code hi hj hm hn same
265  · intro a i m positive ha start hi hm
266    exact gSlot_ne_gAddr code positive ha start hi hm
267  · intro a b ha0 ha sa hb0 hb sb same
268    exact gSlot_unique code ha0 ha sa hb0 hb sb same
269
270/-- The accepted incomplete single-symbol case has one leaf family and
271no subtable links. It does not require a complete Kraft partition. -/
272theorem geometry_single {ls : List Nat} {root mx : Nat} (single : nz ls = 1) :
273    GeoOK ls root mx := by
274  constructor
275  · intro i j m n hi hj hm hn same
276    have iz : i = 0 := by omega
277    have jz : j = 0 := by omega
278    subst i
279    subst j
280    refine ⟨rfl, ?_⟩
281    simp only [gAddr, desc, Nat.zero_add, Nat.pow_zero, Nat.div_one, Nat.sub_zero] at same
282    exact Nat.eq_of_mul_eq_mul_right (Nat.two_pow_pos _) (Nat.add_left_cancel same)
283  · intro a i m positive ha start hi hm
284    omega
285  · intro a b ha0 ha sa hb0 hb sb same
286    omega
287
288end Zlib.Inftrees.Proofs