inftrees.c.cover.tile.lean

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

1import ZlibF.Proof.«inftrees.c.canon»
2
3/-!
4# Kraft tiles of a canonical code
5
6Pure arithmetic over the canonical model (`Zlib.Inftrees.Canon`). The code word of the `j`-th symbol in allocation
7order owns the *tile* `[K j, K j + 2^(15 - L j))` of `[0, 2^15)`. For a code that is not over-subscribed the tiles
8are disjoint and consecutive, so they cover exactly `[0, K nz)`. A point `z` is in the tile of `j` exactly when
9`z / 2^(15 - L j) = cv j`, i.e. when the code word of `j` is a prefix of the 15-bit word `z`.
10-/
11set_option autoImplicit false
12
13namespace Zlib.Inftrees.Proofs.Cover
14open Zlib.Inftrees.Canon
15
16/-- The code is not over-subscribed (`Σ 2^(15 - l) ≤ 2^15`). -/
17abbrev Fit (ls : List Nat) : Prop := K ls (nz ls) ≤ 2 ^ 15
18
19/-- `z` lies in the tile of the `j`-th code. -/
20abbrev InTile (ls : List Nat) (j z : Nat) : Prop := K ls j ≤ z ∧ z < K ls (j + 1)
21
22theorem two_pow_pos' (n : Nat) : 0 < 2 ^ n := Nat.two_pow_pos n
23
24theorem inTile_iff_div (ls : List Nat) {j : Nat} (hj : j < nz ls) (z : Nat) :
25    InTile ls j z ↔ z / 2 ^ (15 - L ls j) = cv ls j := by
26  have hm := cv_mul ls hj
27  have hp := two_pow_pos' (15 - L ls j)
28  unfold InTile
29  rw [K_succ]
30  constructor
31  · rintro ⟨h1, h2⟩
32    apply Nat.le_antisymm
33    · apply Nat.le_of_lt_succ
34      rw [Nat.div_lt_iff_lt_mul hp]
35      rw [Nat.succ_mul]; omega
36    · rw [Nat.le_div_iff_mul_le hp]; omega
37  · intro h
38    have h1 := Nat.div_mul_le_self z (2 ^ (15 - L ls j))
39    have h2 := Nat.lt_div_mul_add (a := z) hp
40    rw [h] at h1 h2
41    omega
42
43/-- A point of `[0, K nz)` is in exactly one tile. -/
44theorem tile_exists (ls : List Nat) {z : Nat} (hz : z < K ls (nz ls)) :
45    ∃ j, j < nz ls ∧ InTile ls j z := by
46  have : ∀ n, n ≤ nz ls → z < K ls n → ∃ j, j < nz ls ∧ InTile ls j z := by
47    intro n
48    induction n with
49    | zero => intro _ h; exact absurd h (by simp [K_zero])
50    | succ n ih =>
51      intro hn h
52      by_cases hz' : z < K ls n
53      · exact ih (by omega) hz'
54      · exact ⟨n, by omega, by omega, h⟩
55  exact this _ (Nat.le_refl _) hz
56
57theorem tile_unique (ls : List Nat) {j j' z : Nat}
58    (h : InTile ls j z) (h' : InTile ls j' z) : j = j' := by
59  by_cases hlt : j < j'
60  · have := K_mono ls (show j + 1 ≤ j' by omega); omega
61  · by_cases hgt : j' < j
62    · have := K_mono ls (show j' + 1 ≤ j by omega); omega
63    · omega
64
65/-- Outside `[0, K nz)` there is no tile. -/
66theorem not_inTile_of_ge (ls : List Nat) {j z : Nat} (hj : j < nz ls) (hz : K ls (nz ls) ≤ z) :
67    ¬ InTile ls j z := by
68  intro h
69  have := K_mono ls (show j + 1 ≤ nz ls by omega)
70  omega
71
72/-- No code of a non-over-subscribed set reaches `2^15`. -/
73theorem cv_lt {ls : List Nat} (hF : Fit ls) {j : Nat} (hj : j < nz ls) : cv ls j < 2 ^ L ls j := by
74  have h := cv_succ_le ls hj (Nat.le_trans (K_mono ls (show j + 1 ≤ nz ls by omega)) hF)
75  omega
76
77theorem K_lt {ls : List Nat} (hF : Fit ls) {j : Nat} (hj : j < nz ls) : K ls j < 2 ^ 15 := by
78  have := K_strict ls (show j < nz ls by omega)
79  omega
80
81/-- The first `R` bits of a code that is longer than `R` (the group of the root table). -/
82theorem grp_lt' {ls : List Nat} (hF : Fit ls) {R : Nat} (hR : R ≤ 15) {j : Nat} (hj : j < nz ls) :
83    grp ls R j < 2 ^ R := by
84  have hk := K_lt hF hj
85  have hp : 2 ^ 15 = 2 ^ R * 2 ^ (15 - R) := by rw [← Nat.pow_add]; congr 1; omega
86  unfold grp
87  rw [Nat.div_lt_iff_lt_mul (two_pow_pos' _), ← hp]
88  exact hk
89
90end Zlib.Inftrees.Proofs.Cover