inftrees.c.cover.fn.lean

本页保留 Lean 源码及行号。点击行号可定位语句，点击 import 中的模块名可查看依赖。

1import ZlibF.Proof.«inftrees.c.cover.group»
2import ZlibF.Proof.«inftrees.c.canonbridge»
3
4/-!
5# The covering lemmas in the model of the main proof
6
7`inftrees.c.canonbridge` identifies the canonical model (`ls = lensOf f n`: `Canon.L`, `Canon.K`, `Canon.H`,
8`Canon.grp`) with the model that the main loop of `inflate_table` is proved in (`lenAt`, `val`, `pre`, `Tc`, `Kc`).
9This module restates the covering lemmas of `inftrees.c.cover.root` and `.group` in that model.
10-/
11set_option autoImplicit false
12
13namespace Zlib.Inftrees.Proofs.Cover
14
15theorem nz_eq_Tc (f : Nat → Nat) (n : Nat) : Canon.nz (lensOf f n) = Tc f n 15 := by
16  unfold Canon.nz; rw [ord_eq]; exact wsAux_length 15
17
18/-- Last tile of a code that is not over-subscribed. -/
19theorem K_top {f : Nat → Nat} {n : Nat} (hpos : 0 < Tc f n 15) :
20    ∃ m, Tc f n 15 = m + 1 ∧
21      Canon.K (lensOf f n) (Tc f n 15) = (val f n m + 1) * 2 ^ (15 - lenAt f n m) := by
22  obtain ⟨m, hm⟩ : ∃ m, Tc f n 15 = m + 1 := ⟨Tc f n 15 - 1, by omega⟩
23  refine ⟨m, hm, ?_⟩
24  have hlt : m < Tc f n 15 := by omega
25  rw [hm, Canon.K_succ, K_eq f n m hlt, L_eq f n hlt, Nat.add_mul, Nat.one_mul]
26
27theorem fit_of_fits {f : Nat → Nat} {n : Nat} (hfit : Fits f n) : Fit (lensOf f n) := by
28  show Canon.K (lensOf f n) (Canon.nz (lensOf f n)) ≤ 2 ^ 15
29  rw [nz_eq_Tc]
30  by_cases hpos : 0 < Tc f n 15
31  · obtain ⟨m, hm, hK⟩ := K_top hpos
32    rw [hK]
33    have hlt : m < Tc f n 15 := by omega
34    have h1 := val_lt hfit hlt
35    obtain ⟨b1, b2⟩ := lenAt_bounds (f := f) (n := n) hlt
36    have hp : 2 ^ 15 = 2 ^ lenAt f n m * 2 ^ (15 - lenAt f n m) := by rw [← Nat.pow_add]; congr 1; omega
37    rw [hp]
38    exact Nat.mul_le_mul_right _ h1
39  · have : Tc f n 15 = 0 := by omega
40    rw [this]; simp [Canon.K_zero]
41
42theorem complete_of_Kc {f : Nat → Nat} {n : Nat} (hc : Kc f n 15 = 2 ^ 15) :
43    Canon.K (lensOf f n) (Canon.nz (lensOf f n)) = 2 ^ 15 := by
44  rw [nz_eq_Tc]
45  have hpos : 0 < Tc f n 15 := by
46    refine Classical.byContradiction fun h => ?_
47    have h0 : Tc f n 15 = 0 := by omega
48    have : Kc f n 15 = 0 := by
49      have := Kc_gap (f := f) (n := n) 0 15 (by simpa [Tc] using h0)
50      simpa [Kc] using this
51    have : (2 : Nat) ^ 15 = 0 := by omega
52    exact absurd this (by decide)
53  obtain ⟨m, hm, hK⟩ := K_top hpos
54  rw [hK, val_last hc hm]
55  have hlt : m < Tc f n 15 := by omega
56  obtain ⟨b1, b2⟩ := lenAt_bounds (f := f) (n := n) hlt
57  rw [← Nat.pow_add]; congr 1; omega
58
59/-! ### The three predicates in the model of the main proof -/
60
61/-- The `j`-th symbol in sorted order fills the root cell `y` (a code of at most `R` bits whose bit-reversed value
62`rev l v` is `y` modulo `2^l`; the C writes `table[huff + k * 2^l]`, `k < 2^(R - l)`). -/
63def ShortAtF (f : Nat → Nat) (n R y j : Nat) : Prop :=
64  j < Tc f n 15 ∧ lenAt f n j ≤ R ∧ y % 2 ^ lenAt f n j = rev (lenAt f n j) (val f n j)
65
66/-- The `j`-th symbol is longer than `R` bits and its link sits at the root cell `y = rev R (pre j)` (the `low` of
67the C). -/
68def LongAtF (f : Nat → Nat) (n R y j : Nat) : Prop :=
69  j < Tc f n 15 ∧ R < lenAt f n j ∧ rev R (pre f n R j) = y
70
71/-- The `j`-th symbol is longer than `R` bits and belongs to the group `p` of the root link `rev R p`
72(`pre j = val j / 2^(l - R)`, `e.p j` in the main loop). -/
73def GroupF (f : Nat → Nat) (n R p j : Nat) : Prop := j < Tc f n 15 ∧ R < lenAt f n j ∧ pre f n R j = p
74
75theorem grp_eq_pre {f : Nat → Nat} {n R j : Nat} (hj : j < Tc f n 15) (hR : R ≤ lenAt f n j) :
76    Canon.grp (lensOf f n) R j = pre f n R j := by
77  obtain ⟨b1, b2⟩ := lenAt_bounds (f := f) (n := n) hj
78  unfold Canon.grp pre
79  rw [K_eq f n j hj]
80  have hp : 2 ^ (15 - R) = 2 ^ (15 - lenAt f n j) * 2 ^ (lenAt f n j - R) := by
81    rw [← Nat.pow_add]; congr 1; omega
82  rw [hp, ← Nat.div_div_eq_div_mul, Nat.mul_div_cancel _ (two_pow_pos' _)]
83
84theorem shortAt_iff (f : Nat → Nat) (n R y j : Nat) : ShortAt (lensOf f n) R y j ↔ ShortAtF f n R y j := by
85  unfold ShortAt ShortAtF
86  rw [nz_eq_Tc]
87  constructor
88  · rintro ⟨hj, hl, h⟩
89    rw [L_eq f n hj] at hl h
90    rw [H_eq f n hj] at h
91    exact ⟨hj, hl, h⟩
92  · rintro ⟨hj, hl, h⟩
93    refine ⟨hj, by rw [L_eq f n hj]; exact hl, ?_⟩
94    rw [L_eq f n hj, H_eq f n hj]; exact h
95
96theorem longAt_iff (f : Nat → Nat) (n R y j : Nat) : LongAt (lensOf f n) R y j ↔ LongAtF f n R y j := by
97  unfold LongAt LongAtF
98  rw [nz_eq_Tc]
99  constructor
100  · rintro ⟨hj, hl, h⟩
101    rw [L_eq f n hj] at hl
102    refine ⟨hj, hl, ?_⟩
103    rw [← h, Canon.H_mod_root _ (by rw [nz_eq_Tc]; exact hj) (by rw [L_eq f n hj]; omega),
104      grp_eq_pre hj (by omega), canon_rev_eq]
105  · rintro ⟨hj, hl, h⟩
106    refine ⟨hj, by rw [L_eq f n hj]; exact hl, ?_⟩
107    rw [Canon.H_mod_root _ (by rw [nz_eq_Tc]; exact hj) (by rw [L_eq f n hj]; omega),
108      grp_eq_pre hj (by omega), canon_rev_eq, h]
109
110theorem group_iff (f : Nat → Nat) (n R p j : Nat) : Group (lensOf f n) R p j ↔ GroupF f n R p j := by
111  unfold Group GroupF
112  rw [nz_eq_Tc]
113  constructor
114  · rintro ⟨hj, hl, h⟩
115    rw [L_eq f n hj] at hl
116    exact ⟨hj, hl, by rw [← grp_eq_pre hj (by omega)]; exact h⟩
117  · rintro ⟨hj, hl, h⟩
118    exact ⟨hj, by rw [L_eq f n hj]; exact hl, by rw [grp_eq_pre hj (by omega)]; exact h⟩
119
120/-! ### Root covering -/
121
122/-- A root cell of a complete code: filled by exactly one short code, or the link of a group of long codes (and then
123filled by no short code). -/
124def RootCellC (f : Nat → Nat) (n R y : Nat) : Prop :=
125  (∃ j, ShortAtF f n R y j ∧ (∀ j', ShortAtF f n R y j' → j' = j) ∧ ∀ j', ¬ LongAtF f n R y j') ∨
126  ((∃ j, LongAtF f n R y j) ∧ ∀ j', ¬ ShortAtF f n R y j')
127
128/-- **Root covering (translation model).** For lengths that are not over-subscribed (`Fits`), every root cell
129`y < 2^R` (`R ≤ 15`) is covered as in `RootCellC`, or by nothing at all. -/
130theorem root_cover_fn {f : Nat → Nat} {n R y : Nat} (hfit : Fits f n) (hR : R ≤ 15) (hy : y < 2 ^ R) :
131    RootCellC f n R y ∨ ((∀ j, ¬ ShortAtF f n R y j) ∧ ∀ j, ¬ LongAtF f n R y j) := by
132  have hs := fun j => shortAt_iff f n R y j
133  have hl := fun j => longAt_iff f n R y j
134  rcases root_cover (fit_of_fits hfit) hR hy with ⟨j, h1, h2, h3⟩ | ⟨j, h1, h2⟩ | ⟨h1, h2, _⟩
135  · exact Or.inl (Or.inl ⟨j, (hs j).mp h1, fun j' h => h2 j' ((hs j').mpr h), fun j' h => h3 j' ((hl j').mpr h)⟩)
136  · exact Or.inl (Or.inr ⟨⟨j, (hl j).mp h1⟩, fun j' h => h2 j' ((hs j').mpr h)⟩)
137  · exact Or.inr ⟨fun j' h => h1 j' ((hs j').mpr h), fun j' h => h2 j' ((hl j').mpr h)⟩
138
139/-- **Root covering of a complete code (translation model).** No root cell stays unwritten. -/
140theorem root_cover_complete_fn {f : Nat → Nat} {n R y : Nat} (hfit : Fits f n) (hc : Kc f n 15 = 2 ^ 15)
141    (hR : R ≤ 15) (hy : y < 2 ^ R) : RootCellC f n R y := by
142  have hs := fun j => shortAt_iff f n R y j
143  have hl := fun j => longAt_iff f n R y j
144  rcases root_cover (fit_of_fits hfit) hR hy with ⟨j, h1, h2, h3⟩ | ⟨j, h1, h2⟩ | ⟨h1, h2, h3⟩
145  · exact Or.inl ⟨j, (hs j).mp h1, fun j' h => h2 j' ((hs j').mpr h), fun j' h => h3 j' ((hl j').mpr h)⟩
146  · exact Or.inr ⟨⟨j, (hl j).mp h1⟩, fun j' h => h2 j' ((hs j').mpr h)⟩
147  · exfalso
148    rw [complete_of_Kc hc] at h3
149    have h4 : Canon.rev R y * 2 ^ (15 - R) < 2 ^ 15 := by
150      have hp : 2 ^ 15 = 2 ^ R * 2 ^ (15 - R) := by rw [← Nat.pow_add]; congr 1; omega
151      rw [hp]
152      exact Nat.mul_lt_mul_of_pos_right (Canon.rev_lt _ _) (two_pow_pos' _)
153    omega
154
155/-- The link of a long code is at a cell below `2^R`, and the codes of one group share the cell. -/
156theorem longAtF_lt {f : Nat → Nat} {n R y j : Nat} (h : LongAtF f n R y j) : y < 2 ^ R := h.2.2 ▸ rev_lt _ _
157
158/-! ### Group covering -/
159
160/-- **Group covering (translation model, residue form).** For a complete code, a group `p` of long codes (`j0` is
161one) and a sub-table width `c` with `R + c ≤ 15` that holds every code of the group (`lenAt j ≤ R + c`), every cell
162`t` of the sub-table is covered by exactly one code `j` of the group: `t % 2^(lenAt j - R)` is `rev (lenAt j) (val j) >> R`. -/
163theorem group_cover_fn {f : Nat → Nat} {n R p j0 : Nat} (hc : Kc f n 15 = 2 ^ 15) (hR : R ≤ 15)
164    (hg0 : GroupF f n R p j0) {c : Nat} (hRc : R + c ≤ 15) (hcl : ∀ j, GroupF f n R p j → lenAt f n j ≤ R + c)
165    (t : Nat) :
166    ∃ j, GroupF f n R p j ∧ t % 2 ^ (lenAt f n j - R) = rev (lenAt f n j) (val f n j) / 2 ^ R ∧
167      ∀ j', GroupF f n R p j' → t % 2 ^ (lenAt f n j' - R) = rev (lenAt f n j') (val f n j') / 2 ^ R → j' = j := by
168  have hcl' : ∀ j, Group (lensOf f n) R p j → Canon.L (lensOf f n) j ≤ R + c := by
169    intro j hj
170    have := (group_iff f n R p j).mp hj
171    rw [L_eq f n this.1]; exact hcl j this
172  have hH : ∀ j, GroupF f n R p j → Canon.H (lensOf f n) j = rev (lenAt f n j) (val f n j) :=
173    fun j hj => H_eq f n hj.1
174  obtain ⟨j, hj, hm, hu⟩ := group_cover (complete_of_Kc hc) hR ((group_iff f n R p j0).mpr hg0) hRc hcl' t
175  have hjF := (group_iff f n R p j).mp hj
176  refine ⟨j, hjF, ?_, ?_⟩
177  · rw [← hH j hjF, ← L_eq f n hjF.1]; exact hm
178  · intro j' hj' heq
179    refine hu j' ((group_iff f n R p j').mpr hj') ?_
180    rw [hH j' hj', L_eq f n hj'.1]; exact heq
181
182/-- **Group covering, index form (translation model).** Same hypotheses, and `t < 2^c`: the cell `t` is written
183by exactly one code `j` of the group, as `next[(huff >> drop) + 2^(lenAt j - R) * t']` with `huff = rev (lenAt j) (val j)`,
184`drop = R`, `t' < 2^(R + c - lenAt j)` (the fill loop of the C). -/
185theorem group_cover_idx_fn {f : Nat → Nat} {n R p j0 : Nat} (hc : Kc f n 15 = 2 ^ 15) (hR : R ≤ 15)
186    (hg0 : GroupF f n R p j0) {c : Nat} (hRc : R + c ≤ 15) (hcl : ∀ j, GroupF f n R p j → lenAt f n j ≤ R + c)
187    {t : Nat} (ht : t < 2 ^ c) :
188    ∃ j, GroupF f n R p j ∧
189      (∃ t', t' < 2 ^ (R + c - lenAt f n j) ∧
190        t = rev (lenAt f n j) (val f n j) / 2 ^ R + 2 ^ (lenAt f n j - R) * t') ∧
191      ∀ j' t', GroupF f n R p j' →
192        t = rev (lenAt f n j') (val f n j') / 2 ^ R + 2 ^ (lenAt f n j' - R) * t' → j' = j := by
193  have hcl' : ∀ j, Group (lensOf f n) R p j → Canon.L (lensOf f n) j ≤ R + c := by
194    intro j hj
195    have := (group_iff f n R p j).mp hj
196    rw [L_eq f n this.1]; exact hcl j this
197  have hH : ∀ j, GroupF f n R p j → Canon.H (lensOf f n) j = rev (lenAt f n j) (val f n j) :=
198    fun j hj => H_eq f n hj.1
199  obtain ⟨j, hj, ⟨t', ht', he⟩, hu⟩ :=
200    group_cover_idx (complete_of_Kc hc) hR ((group_iff f n R p j0).mpr hg0) hRc hcl' ht
201  have hjF := (group_iff f n R p j).mp hj
202  have hLj := L_eq f n hjF.1
203  refine ⟨j, hjF, ⟨t', by rw [← hLj]; exact ht', ?_⟩, ?_⟩
204  · rw [← hH j hjF, ← hLj]; exact he
205  · intro j' t'' hj' heq
206    refine hu j' t'' ((group_iff f n R p j').mpr hj') ?_
207    rw [hH j' hj', L_eq f n hj'.1]; exact heq
208
209/-- The cell index `rev l v >> R + 2^(l - R) * t'` that a code of the group writes is inside the sub-table. -/
210theorem cell_lt_fn {f : Nat → Nat} {n R p j c : Nat} (hg : GroupF f n R p j) (hl : lenAt f n j ≤ R + c) {t' : Nat}
211    (ht' : t' < 2 ^ (R + c - lenAt f n j)) :
212    rev (lenAt f n j) (val f n j) / 2 ^ R + 2 ^ (lenAt f n j - R) * t' < 2 ^ c := by
213  have hG := (group_iff f n R p j).mpr hg
214  have hLj := L_eq f n hg.1
215  have := cell_lt (c := c) hG (by rw [hLj]; exact hl) (t' := t') (by rw [hLj]; exact ht')
216  rw [H_eq f n hg.1, hLj] at this
217  exact this
218
219/-! ### The incomplete code that the main loop accepts -/
220
221/-- **The single code of length 1** (the only incomplete code with symbols that `inflate_table` builds a table
222for: `Tc = 1`, `lenAt 0 = 1`, hence `R = 1`): the root cell `0` is filled by it and cell `1` is covered by no code,
223neither short nor long. The C writes cell `1` after the loop, the entry `op = 64, bits = len - drop = 1, val = 0`
224(`invalid_leaf`). Every other incomplete code makes `inflate_table` return `-1` before the first write, and the empty
225code (`max = 0`) is handled before the loop (two entries `op = 64, bits = 1, val = 0`). -/
226theorem root_single_fn {f : Nat → Nat} {n : Nat} (hT : Tc f n 15 = 1) (hl : lenAt f n 0 = 1) :
227    ShortAtF f n 1 0 0 ∧ (∀ j, ¬ ShortAtF f n 1 1 j) ∧ ∀ y j, ¬ LongAtF f n 1 y j := by
228  have h0 : val f n 0 = 0 := val_zero (by omega)
229  refine ⟨⟨by omega, by omega, by rw [hl, h0]; simp [rev]⟩, ?_, ?_⟩
230  · rintro j ⟨hj, _, h⟩
231    have : j = 0 := by omega
232    subst this
233    rw [hl, h0] at h
234    simp [rev] at h
235  · rintro y j ⟨hj, hR, _⟩
236    have : j = 0 := by omega
237    subst this
238    omega
239
240end Zlib.Inftrees.Proofs.Cover