DeflateTreeScan.lean

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

1import Std
2
3/-! # Counting the leaves inserted by the first `build_tree` scan -/
4
5namespace Zlib.Trees.Math
6
7/-- Number of positive-frequency symbols below the scan position. -/
8def scanCount (fr : Nat → UInt16) : Nat → Nat
9  | 0 => 0
10  | k + 1 => scanCount fr k + if fr k ≠ 0 then 1 else 0
11
12/-- Largest positive-frequency symbol below the scan position, or `-1`. -/
13def scanMax (fr : Nat → UInt16) : Nat → Int
14  | 0 => -1
15  | k + 1 => if fr k ≠ 0 then k else scanMax fr k
16
17theorem scanCount_le (fr : Nat → UInt16) (k : Nat) : scanCount fr k ≤ k := by
18  induction k with
19  | zero => exact Nat.le_refl _
20  | succ k ih => simp only [scanCount]; split <;> omega
21
22theorem scanMax_bounds (fr : Nat → UInt16) (k : Nat) :
23    -1 ≤ scanMax fr k ∧ scanMax fr k < k := by
24  induction k with
25  | zero => simp [scanMax]
26  | succ k ih => simp only [scanMax]; split <;> omega
27
28/-- The selected maximum is exact, including the all-zero case. -/
29theorem scanMax_spec (fr : Nat → UInt16) (k : Nat) :
30    (scanMax fr k = -1 ∧ ∀ m < k, fr m = 0) ∨
31    (∃ u : Nat, scanMax fr k = u ∧ u < k ∧ fr u ≠ 0 ∧
32      ∀ m, u < m → m < k → fr m = 0) := by
33  induction k with
34  | zero => exact Or.inl ⟨rfl, by omega⟩
35  | succ k ih =>
36    simp only [scanMax]
37    by_cases hk : fr k ≠ 0
38    · rw [ite_eq_left hk]
39      exact Or.inr ⟨k, rfl, by omega, hk, by omega⟩
40    · rw [ite_eq_right hk]
41      rcases ih with ⟨he, hz⟩ | ⟨u, he, hu, hf, hz⟩
42      · refine Or.inl ⟨he, ?_⟩
43        intro m hm
44        by_cases heq : m = k
45        · subst m; simpa using hk
46        · exact hz m (by omega)
47      · refine Or.inr ⟨u, he, by omega, hf, ?_⟩
48        intro m hm1 hm2
49        by_cases heq : m = k
50        · subst m; simpa using hk
51        · exact hz m hm1 (by omega)
52
53end Zlib.Trees.Math