DeflateForest.lean

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

1import ZlibF.Proof.«trees.c.heap.gbtree»
2
3/-! # Queue and descending tail as one finite sequence of tree nodes -/
4
5namespace Zlib.Trees.Proofs.GB
6
7/-- Enumerate the active queue, then the descending tail. -/
8def poolAt (H : Nat → Nat) (len i : Nat) : Nat :=
9  if i < len then H (i + 1) else H (572 - (i - len))
10
11/-- Observe all active queue entries and all retained tail entries. -/
12def poolSum (H : Nat → Nat) (len tail : Nat) (F : Nat → Nat) : Nat :=
13  rs (fun i => F (H (i + 1))) len + rs (fun i => F (H (572 - i))) tail
14
15/-- The two sums are exactly one bounded sequence sum. -/
16theorem poolSum_eq_rs (H : Nat → Nat) (len tail : Nat) (F : Nat → Nat) :
17    poolSum H len tail F = rs (fun i => F (poolAt H len i)) (len + tail) := by
18  rw [rs_split]
19  unfold poolSum
20  congr 1
21  · apply rs_congr
22    intro i hi
23    simp only [poolAt, hi, ite_true]
24  · apply rs_congr
25    intro i hi
26    simp only [poolAt, show ¬ len + i < len by omega, ite_false, Nat.add_sub_cancel_left]
27
28/-- Two distinct summands fit inside the whole sum. -/
29theorem two_le_rs (F : Nat → Nat) (m i j : Nat) (hi : i < m) (hj : j < m) (hne : i ≠ j) :
30    F i + F j ≤ rs F m := by
31  let G := fun q => if q = i then 0 else F q
32  have hu := rs_upd (F := F) (G := G) (n := m) (k := i) hi (by
33    intro q hq hqi
34    dsimp only [G]
35    rw [ite_eq_right hqi])
36  have hjG := le_rs (F := G) hj
37  have hGi : G i = 0 := by simp only [G, ite_true]
38  have hGj : G j = F j := by simp only [G, ite_eq_right (Ne.symm hne)]
39  rw [hGi] at hu
40  rw [hGj] at hjG
41  omega
42
43/-- At most one occurrence of every value implies distinct entries. -/
44theorem injective_of_counts (P : Nat → Nat) (m : Nat) (hc : ∀ v, cnt P m v ≤ 1) :
45    ∀ i j, i < m → j < m → P i = P j → i = j := by
46  intro i j hi hj heq
47  by_cases hne : i = j
48  · exact hne
49  exfalso
50  have htwo := two_le_rs (fun q => if P q = P i then 1 else 0) m i j hi hj hne
51  have hcnt := hc (P i)
52  have hji := heq.symm
53  simp only [hji, ite_true] at htwo
54  unfold cnt at hcnt
55  omega
56
57/-- The queue/tail index map hits only active heap positions. -/
58theorem poolAt_position (H : Nat → Nat) (K j i : Nat) (hK : K ≤ 286) (hj : j < K) (hi : i < K + j) :
59    ∃ q : Nat, ((1 ≤ q ∧ q ≤ K - j) ∨ (573 - 2 * j ≤ q ∧ q < 573)) ∧ poolAt H (K - j) i = H q := by
60  by_cases hq : i < K - j
61  · exact ⟨i + 1, Or.inl ⟨by omega, by omega⟩, by simp only [poolAt, hq, ite_true]⟩
62  · refine ⟨572 - (i - (K - j)), Or.inr ⟨by omega, by omega⟩, ?_⟩
63    simp only [poolAt, hq, ite_false]
64
65/-- Every active heap position has a bounded queue/tail sequence index. -/
66theorem poolAt_preimage (H : Nat → Nat) (K j q : Nat) (hK : K ≤ 286) (hj : j < K)
67    (hq : (1 ≤ q ∧ q ≤ K - j) ∨ (573 - 2 * j ≤ q ∧ q < 573)) :
68    ∃ i : Nat, i < K + j ∧ poolAt H (K - j) i = H q := by
69  rcases hq with hq | hq
70  · refine ⟨q - 1, by omega, ?_⟩
71    simp only [poolAt, show q - 1 < K - j by omega, ite_true, show q - 1 + 1 = q by omega]
72  · refine ⟨K - j + (572 - q), by omega, ?_⟩
73    simp only [poolAt, show ¬ K - j + (572 - q) < K - j by omega, ite_false, Nat.add_sub_cancel_left,
74      show 572 - (572 - q) = q by omega]
75
76/-- A heap position's sequence index is unique. -/
77theorem poolAt_index_injective (K j : Nat) (hK : K ≤ 286) (hj : j < K) :
78    ∀ i i', i < K + j → i' < K + j →
79      (if i < K - j then i + 1 else 572 - (i - (K - j))) =
80      (if i' < K - j then i' + 1 else 572 - (i' - (K - j))) → i = i' := by
81  intro i i' hi hi' heq
82  split at heq <;> split at heq <;> omega
83
84
85/-- Two child stores enlarge the descending tail, while the queue count
86loses those two children and gains their fresh parent. -/
87theorem poolSum_step (H E : Nat → Nat) (K j n m node : Nat)
88    (hK : K ≤ 286) (hj : j + 1 < K)
89    (hn : E (572 - 2 * j) = n) (hm : E (571 - 2 * j) = m)
90    (hframe : ∀ i < 2 * j, E (572 - i) = H (572 - i))
91    (hqueue : ∀ F : Nat → Nat,
92      rs (fun i => F (E (i + 1))) (K - j - 1) + F n + F m =
93        rs (fun i => F (H (i + 1))) (K - j) + F node)
94    (F : Nat → Nat) :
95    poolSum E (K - (j + 1)) (2 * (j + 1)) F = poolSum H (K - j) (2 * j) F + F node := by
96  have htail : rs (fun i => F (E (572 - i))) (2 * (j + 1)) =
97      rs (fun i => F (H (572 - i))) (2 * j) + F n + F m := by
98    rw [show 2 * (j + 1) = 2 * j + 1 + 1 by omega, rs_succ, rs_succ]
99    rw [rs_congr (fun i hi => congrArg F (hframe i hi)), hn,
100      show 572 - (2 * j + 1) = 571 - 2 * j by omega, hm]
101  have hq := hqueue F
102  unfold poolSum
103  rw [htail, show K - (j + 1) = K - j - 1 by omega]
104  omega
105
106/-- Exact pool observations imply exact multiplicities. -/
107theorem pool_counts (H H0 : Nat → Nat) (len tail K N j : Nat)
108    (hsum : ∀ F : Nat → Nat, poolSum H len tail F =
109      rs (fun i => F (H0 (i + 1))) K + rs (fun i => F (N + i)) j) (v : Nat) :
110    cnt (poolAt H len) (len + tail) v = cnt (fun i => H0 (i + 1)) K v + cnt (fun i => N + i) j v := by
111  simpa only [poolSum_eq_rs, cnt] using hsum (fun q => if q = v then 1 else 0)
112
113/-- Initially distinct leaf nodes below N and the distinct internal range
114N..N+j have no repeated values in the complete pool. -/
115theorem pool_unique (H H0 : Nat → Nat) (len tail K N j : Nat)
116    (hinit : ∀ i < K, H0 (i + 1) < N)
117    (hinj : ∀ i i', i < K → i' < K → H0 (i + 1) = H0 (i' + 1) → i = i')
118    (hsum : ∀ F : Nat → Nat, poolSum H len tail F =
119      rs (fun i => F (H0 (i + 1))) K + rs (fun i => F (N + i)) j) :
120    ∀ i i', i < len + tail → i' < len + tail → poolAt H len i = poolAt H len i' → i = i' := by
121  apply injective_of_counts
122  intro v
123  rw [pool_counts H H0 len tail K N j hsum v]
124  by_cases hv : v < N
125  · have hz : cnt (fun i => N + i) j v = 0 := cnt_zero (fun i hi => by omega)
126    rw [hz, Nat.add_zero]
127    exact cnt_le_one _ _ _ hinj
128  · have hz : cnt (fun i => H0 (i + 1)) K v = 0 := cnt_zero (fun i hi => by have := hinit i hi; omega)
129    rw [hz, Nat.zero_add]
130    exact cnt_le_one _ _ _ (fun i i' hi hi' he => by omega)
131
132/-- Each pool value is either an original leaf or an already created
133internal node. This follows from counts, without a membership assumption. -/
134theorem pool_origin (H H0 : Nat → Nat) (len tail K N j : Nat)
135    (hsum : ∀ F : Nat → Nat, poolSum H len tail F =
136      rs (fun i => F (H0 (i + 1))) K + rs (fun i => F (N + i)) j)
137    (i : Nat) (hi : i < len + tail) :
138    (∃ q < K, H0 (q + 1) = poolAt H len i) ∨ (N ≤ poolAt H len i ∧ poolAt H len i < N + j) := by
139  classical
140  by_cases hleaf : ∃ q < K, H0 (q + 1) = poolAt H len i
141  · exact Or.inl hleaf
142  right
143  by_cases hint : N ≤ poolAt H len i ∧ poolAt H len i < N + j
144  · exact hint
145  exfalso
146  have hc := cnt_pos (P := poolAt H len) hi rfl
147  rw [pool_counts H H0 len tail K N j hsum (poolAt H len i)] at hc
148  have hz1 : cnt (fun q => H0 (q + 1)) K (poolAt H len i) = 0 := cnt_zero (fun q hq he => hleaf ⟨q, hq, he⟩)
149  have hz2 : cnt (fun q => N + q) j (poolAt H len i) = 0 := cnt_zero (fun q hq he => hint (by omega))
150  omega
151
152/-- Every already created internal node occurs in the pool. -/
153theorem pool_internal (H H0 : Nat → Nat) (len tail K N j : Nat)
154    (hsum : ∀ F : Nat → Nat, poolSum H len tail F =
155      rs (fun i => F (H0 (i + 1))) K + rs (fun i => F (N + i)) j)
156    (a : Nat) (ha : a < j) : ∃ i < len + tail, poolAt H len i = N + a := by
157  apply cnt_exists
158  rw [pool_counts H H0 len tail K N j hsum (N + a)]
159  have hc := cnt_pos (P := fun i => N + i) ha rfl
160  omega
161
162/-- Every active heap position has a bounded sequence index that maps
163back to that exact position, independently of the node values. -/
164theorem pool_position_preimage (K j q : Nat) (hK : K ≤ 286) (hj : j < K)
165    (hq : (1 ≤ q ∧ q ≤ K - j) ∨ (573 - 2 * j ≤ q ∧ q < 573)) :
166    ∃ i : Nat, i < K + j ∧ (if i < K - j then i + 1 else 572 - (i - (K - j))) = q := by
167  rcases hq with hq | hq
168  · refine ⟨q - 1, by omega, ?_⟩
169    rw [ite_eq_left (by omega)]
170    omega
171  · refine ⟨K - j + (572 - q), by omega, ?_⟩
172    rw [ite_eq_right (by omega)]
173    omega
174
175/-- Distinct sequence values yield distinct active heap positions. -/
176theorem pool_heap_injective (H : Nat → Nat) (K j : Nat) (hK : K ≤ 286) (hj : j < K)
177    (hinj : ∀ i i', i < K + j → i' < K + j → poolAt H (K - j) i = poolAt H (K - j) i' → i = i') :
178    ∀ q q', ((1 ≤ q ∧ q ≤ K - j) ∨ (573 - 2 * j ≤ q ∧ q < 573)) →
179      ((1 ≤ q' ∧ q' ≤ K - j) ∨ (573 - 2 * j ≤ q' ∧ q' < 573)) → H q = H q' → q = q' := by
180  intro q q' hq hq' heq
181  obtain ⟨i, hi, hpos⟩ := pool_position_preimage K j q hK hj hq
182  obtain ⟨i', hi', hpos'⟩ := pool_position_preimage K j q' hK hj hq'
183  have hval : ∀ k, poolAt H (K - j) k = H (if k < K - j then k + 1 else 572 - (k - (K - j))) := by
184    intro k
185    unfold poolAt
186    split <;> rfl
187  have heqi : poolAt H (K - j) i = poolAt H (K - j) i' := by rw [hval, hval, hpos, hpos']; exact heq
188  have hii := hinj i i' hi hi' heqi
189  rw [hii] at hpos
190  omega
191
192
193/-- Every original leaf remains in the complete pool. -/
194theorem pool_leaf (H H0 : Nat → Nat) (len tail K N j : Nat)
195    (hsum : ∀ F : Nat → Nat, poolSum H len tail F =
196      rs (fun i => F (H0 (i + 1))) K + rs (fun i => F (N + i)) j)
197    (a : Nat) (ha : a < K) : ∃ i < len + tail, poolAt H len i = H0 (a + 1) := by
198  apply cnt_exists
199  rw [pool_counts H H0 len tail K N j hsum (H0 (a + 1))]
200  have hc := cnt_pos (P := fun i => H0 (i + 1)) ha rfl
201  omega
202
203end Zlib.Trees.Proofs.GB