DeflateBlIndex.lean

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

1import Std.Tactic
2
3/-! # The descending search for the last bit-length code rank
4
5The recursive maximum follows the reference EmitBlTree argument. The lower
6bound two reflects the actual loop; a four-code header needs a used rank at
7least three, established separately from the caller's constructed trees.
8-/
9
10namespace Zlib.Trees.Proofs.Math
11
12def blMaxIdx (used : Nat → Bool) : Nat → Nat
13  | 0 => 0
14  | m + 1 => if m + 1 < 3 then m + 1 else if used (m + 1) then m + 1 else blMaxIdx used m
15
16theorem blMaxIdx_le (used : Nat → Bool) (m : Nat) : blMaxIdx used m ≤ m := by
17  induction m with
18  | zero => exact Nat.le_refl _
19  | succ m ih => unfold blMaxIdx; split <;> (try split) <;> omega
20
21theorem blMaxIdx_ge (used : Nat → Bool) (m : Nat) (hm : 2 ≤ m) : 2 ≤ blMaxIdx used m := by
22  induction m with
23  | zero => omega
24  | succ m ih =>
25    unfold blMaxIdx
26    split
27    · omega
28    · split
29      · omega
30      · exact ih (by omega)
31
32theorem blMaxIdx_step (used : Nat → Bool) (m : Nat) (hm : 3 ≤ m) :
33    blMaxIdx used m = if used m then m else blMaxIdx used (m - 1) := by
34  rw [show m = (m - 1) + 1 by omega]
35  simp only [blMaxIdx, ite_eq_right (show ¬ m - 1 + 1 < 3 by omega)]
36  simp only [Nat.add_sub_cancel]
37
38/-- Every rank omitted by the returned index has zero length. -/
39theorem blMaxIdx_suffix (used : Nat → Bool) (m k : Nat)
40    (hk : blMaxIdx used m < k) (hkm : k ≤ m) : used k = false := by
41  induction m with
42  | zero => have := blMaxIdx_le used 0; omega
43  | succ m ih =>
44    simp only [blMaxIdx] at hk
45    split at hk
46    · omega
47    · split at hk
48      · omega
49      · rename_i hu
50        by_cases heq : k = m + 1
51        · subst k; exact Bool.eq_false_iff.mpr hu
52        · exact ih hk (by omega)
53
54/-- A used rank at least three forces enough transmitted header entries. -/
55theorem blMaxIdx_ge_of_used (used : Nat → Bool) (m k : Nat)
56    (hk3 : 3 ≤ k) (hkm : k ≤ m) (hu : used k = true) : k ≤ blMaxIdx used m := by
57  by_cases hle : k ≤ blMaxIdx used m
58  · exact hle
59  · have hf := blMaxIdx_suffix used m k (by omega) hkm
60    rw [hu] at hf
61    contradiction
62
63end Zlib.Trees.Proofs.Math