DeflateTreeForce.lean

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

1import ZlibF.Math.DeflateTreeScan
2
3/-! # Fresh dummy leaves for the two-leaf repair in `build_tree` -/
4
5namespace Zlib.Trees.Math
6
7def forceNode (m : Int) : Nat := if m < 2 then (m + 1).toNat else 0
8
9def forceMax (m : Int) : Int := if m < 2 then m + 1 else m
10
11def forceFreq (fr : Nat → UInt16) (m : Int) (v : Nat) : UInt16 :=
12  if v = forceNode m then 1 else fr v
13
14theorem scanCount_pos (fr : Nat → UInt16) (N a : Nat) (ha : a < N) (hf : fr a ≠ 0) :
15    1 ≤ scanCount fr N := by
16  induction N with
17  | zero => omega
18  | succ N ih =>
19    simp only [scanCount]
20    by_cases heq : a = N
21    · subst a; rw [ite_eq_left hf]; omega
22    · have h := ih (by omega); split <;> omega
23
24theorem scanCount_two (fr : Nat → UInt16) (N a b : Nat)
25    (ha : a < N) (hb : b < N) (hab : a ≠ b) (hfa : fr a ≠ 0) (hfb : fr b ≠ 0) :
26    2 ≤ scanCount fr N := by
27  induction N with
28  | zero => omega
29  | succ N ih =>
30    simp only [scanCount]
31    by_cases hea : a = N
32    · subst a
33      have h := scanCount_pos fr N b (by omega) hfb
34      rw [ite_eq_left hfa]; omega
35    · by_cases heb : b = N
36      · subst b
37        have h := scanCount_pos fr N a (by omega) hfa
38        rw [ite_eq_left hfb]; omega
39      · have h := ih (by omega) (by omega)
40        split <;> omega
41
42theorem scanCount_congr (fr gr : Nat → UInt16) (N : Nat) (h : ∀ v < N, fr v = gr v) :
43    scanCount fr N = scanCount gr N := by
44  induction N with
45  | zero => rfl
46  | succ N ih => simp only [scanCount, ih (by intro v hv; exact h v (by omega)), h N (by omega)]
47
48theorem scanMax_congr (fr gr : Nat → UInt16) (N : Nat) (h : ∀ v < N, fr v = gr v) :
49    scanMax fr N = scanMax gr N := by
50  induction N with
51  | zero => rfl
52  | succ N ih => simp only [scanMax, ih (by intro v hv; exact h v (by omega)), h N (by omega)]
53
54theorem scanMax_eq (fr : Nat → UInt16) (N a : Nat) (ha : a < N) (hf : fr a ≠ 0)
55    (hz : ∀ v, a < v → v < N → fr v = 0) : scanMax fr N = a := by
56  rcases scanMax_spec fr N with ⟨hm, hzero⟩ | ⟨u, hm, hu, hfu, hzero⟩
57  · exact False.elim (hf (hzero a ha))
58  · have heq : u = a := by
59      by_cases hlt : u < a
60      · exact False.elim (hf (hzero a hlt ha))
61      · by_cases hgt : a < u
62        · exact False.elim (hfu (hz u hgt hu))
63        · omega
64    simpa only [heq] using hm
65
66/-- With at most one used leaf, zlib chooses a fresh leaf inside the actual
67alphabet. An alphabet of at least three symbols includes the `max_code = 1`
68case, where the chosen leaf is symbol 2. -/
69theorem forceNode_fresh (fr : Nat → UInt16) (N : Nat) (hN : 3 ≤ N)
70    (hc : scanCount fr N ≤ 1) :
71    forceNode (scanMax fr N) < N ∧ fr (forceNode (scanMax fr N)) = 0 := by
72  rcases scanMax_spec fr N with ⟨hm, hz⟩ | ⟨u, hm, hu, hf, hz⟩
73  · rw [hm]
74    have heq : forceNode (-1) = 0 := rfl
75    rw [heq]
76    exact ⟨by omega, hz 0 (by omega)⟩
77  · rw [hm]
78    by_cases hsmall : (u : Int) < 2
79    · have hnode : forceNode (u : Int) = u + 1 := by simp only [forceNode, ite_eq_left hsmall]; omega
80      rw [hnode]
81      exact ⟨by omega, hz (u + 1) (by omega) (by omega)⟩
82    · have hnode : forceNode (u : Int) = 0 := by simp only [forceNode, ite_eq_right hsmall]
83      rw [hnode]
84      refine ⟨by omega, ?_⟩
85      apply Classical.byContradiction
86      intro hzero
87      have htwo := scanCount_two fr N 0 u (by omega) hu (by omega) hzero hf
88      omega
89
90theorem scanCount_set_one (fr : Nat → UInt16) (N node : Nat) (hn : node < N) (hz : fr node = 0) :
91    scanCount (fun v => if v = node then 1 else fr v) N = scanCount fr N + 1 := by
92  induction N with
93  | zero => omega
94  | succ N ih =>
95    by_cases heq : node = N
96    · subst node
97      have hpre : scanCount (fun v => if v = N then 1 else fr v) N = scanCount fr N :=
98        scanCount_congr (fun v => if v = N then 1 else fr v) fr N (by intro v hv; rw [ite_eq_right (by omega)])
99      simp [scanCount, hpre, hz]
100    · have hpre := ih (by omega)
101      simp only [scanCount, hpre, ite_eq_right (Ne.symm heq)]
102      split <;> omega
103
104theorem scanCount_force (fr : Nat → UInt16) (N : Nat) (hN : 3 ≤ N) (hc : scanCount fr N ≤ 1) :
105    scanCount (forceFreq fr (scanMax fr N)) N = scanCount fr N + 1 := by
106  obtain ⟨hn, hz⟩ := forceNode_fresh fr N hN hc
107  exact scanCount_set_one fr N _ hn hz
108
109/-- The control variable updated by zlib remains the exact maximum after
110adding the fresh leaf. -/
111theorem scanMax_force (fr : Nat → UInt16) (N : Nat) (hN : 3 ≤ N) (hc : scanCount fr N ≤ 1) :
112    scanMax (forceFreq fr (scanMax fr N)) N = forceMax (scanMax fr N) := by
113  obtain ⟨hn, hz⟩ := forceNode_fresh fr N hN hc
114  rcases scanMax_spec fr N with ⟨hm, hzero⟩ | ⟨u, hm, hu, hfu, hzero⟩
115  · rw [hm]
116    change scanMax (fun v => if v = 0 then 1 else fr v) N = 0
117    exact scanMax_eq _ N 0 (by omega) (by simp) (by
118      intro v hv hvN; rw [ite_eq_right (by omega)]; exact hzero v hvN)
119  · rw [hm]
120    by_cases hsmall : (u : Int) < 2
121    · have hnode : forceNode (u : Int) = u + 1 := by simp only [forceNode, ite_eq_left hsmall]; omega
122      simp only [forceMax, ite_eq_left hsmall]
123      have heq := scanMax_eq (forceFreq fr u) N (u + 1) (by omega)
124        (by simp [forceFreq, hnode]) (by
125          intro v hv hvN
126          rw [show forceFreq fr u v = fr v by simp [forceFreq, hnode, show v ≠ u + 1 by omega]]
127          exact hzero v (by omega) hvN)
128      simpa using heq
129    · have hnode : forceNode (u : Int) = 0 := by simp only [forceNode, ite_eq_right hsmall]
130      simp only [forceMax, ite_eq_right hsmall]
131      exact scanMax_eq (forceFreq fr u) N u hu
132        (by simpa only [forceFreq, hnode, ite_eq_right (show u ≠ 0 by omega)] using hfu) (by
133          intro v hv hvN
134          rw [show forceFreq fr u v = fr v by simp [forceFreq, hnode, show v ≠ 0 by omega]]
135          exact hzero v hv hvN)
136
137end Zlib.Trees.Math