trees.c.heap.pqrun.lean

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

1import ZlibF.Proof.«trees.c.heap.pq»
2import ZlibF.Proof.«trees.c.heap.ord»
3
4/-!
5# trees.c: `pqdownheap` keeps the heap order
6
7The loop invariant and the hole lemmas (`HoleInv`, `hole_step`, ...) are those of the earlier attempt
8(`Proofs/trees/PqDownHeapOrd.lean`), restated for the record `d` of the new heap model.
9-/
10
11namespace Zlib.Trees.Proofs
12open C Zlib.Trees
13
14theorem sm_eq (T : Array CtData) (D : Array UInt8) :
15    sm T D = smallerB (fun n => (T[n]!).fc) (fun n => D[n]!) := rfl
16
17theorem sm_ok (T : Array CtData) (D : Array UInt8) : KeyOK (sm T D) := by
18  rw [sm_eq]; exact smallerB_ok _ _
19
20/-- The heap array with the pending value `v` in the hole `K`. -/
21def wh (hp : Array Int32) (K : Nat) (v : Int32) : Nat → Int32 := fun i => if i = K then v else hp[i]!
22
23theorem ws_pqdownheap {h0 : Heap} {id : Nat} (tk : TK) (d : DeflateState) (kk : Int32) (k0 len : Nat)
24    (hk : kk.toInt = k0) (hk1 : 1 ≤ k0) (hk2 : k0 ≤ len) (hlen : d.heap_len.toInt = len)
25    (hsz : len < d.heap.size) (hbig : d.heap.size ≤ 1000000)
26    (hval : ∀ i, 1 ≤ i → i ≤ len → NV (tk.arr d) d.depth d.heap[i]!)
27    (hheap : HeapOK (sm (tk.arr d) d.depth) (fun i => d.heap[i]!) len k0) :
28    WS h0 id (pqdownheap (Sp id) (Ptr.ref (tk.ref id) 0) kk) d (fun _ d' =>
29      ∃ hp', d' = { d with heap := hp' } ∧ hp'.size = d.heap.size ∧
30        (∀ i, ¬ (1 ≤ i ∧ i ≤ len) → hp'[i]! = d.heap[i]!) ∧
31        PermOn (fun i => hp'[i]!) (fun i => d.heap[i]!) len ∧
32        HeapOK (sm (tk.arr d) d.depth) (fun i => hp'[i]!) len (k0 - 1)) := by
33  have kOK := sm_ok (tk.arr d) d.depth
34  unfold pqdownheap
35  simp only []
36  refine WS.bind' (ws_heapAt kk (by omega) (by omega)) fun v d1 ⟨hv, hd1⟩ => ?_
37  subst d1
38  refine WS.bind' (ws_shl1 kk (by omega) (by omega)) fun j d1 ⟨hj, hd1⟩ => ?_
39  subst d1
40  have hv' : v = d.heap[k0]! := by rw [hv]; congr 1; omega
41  have hnv : NV (tk.arr d) d.depth v := by rw [hv']; exact hval k0 hk1 hk2
42  let H : Nat → Int32 := fun i => d.heap[i]!
43  let Inv : Int32 × Int32 × Bool → DeflateState → Prop := fun st e => ∃ (K : Nat) (hpc : Array Int32),
44    e = { d with heap := hpc } ∧ hpc.size = d.heap.size ∧ (∀ i, ¬ (1 ≤ i ∧ i ≤ len) → hpc[i]! = d.heap[i]!) ∧
45    st.1.toInt = K ∧ k0 ≤ K ∧ K ≤ len ∧ (st.2.2 = false → st.2.1.toInt = 2 * K) ∧
46    PermOn (wh hpc K v) H len ∧ HoleInv (sm (tk.arr d) d.depth) (wh hpc K v) len k0 K ∧
47    (st.2.2 = true → ∃ j', MinChild (sm (tk.arr d) d.depth) (wh hpc K v) len K j' ∧
48      sm (tk.arr d) d.depth (wh hpc K v K) (wh hpc K v j') = true)
49  let Q : Int32 × Int32 × Bool → DeflateState → Prop := fun st e => ∃ (K : Nat) (hpc : Array Int32),
50    e = { d with heap := hpc } ∧ hpc.size = d.heap.size ∧ (∀ i, ¬ (1 ≤ i ∧ i ≤ len) → hpc[i]! = d.heap[i]!) ∧
51    st.1.toInt = K ∧ k0 ≤ K ∧ K ≤ len ∧ PermOn (wh hpc K v) H len ∧
52    HeapOK (sm (tk.arr d) d.depth) (wh hpc K v) len (k0 - 1)
53  let μ : Int32 × Int32 × Bool → DeflateState → Nat := fun st _ => if st.2.2 then 0 else 4000000 - st.2.1.toInt.toNat
54  have hf : ∀ st e, μ st e < fuel := fun st e => by
55    unfold μ; split <;> simp only [fuel] <;> omega
56  have hwh0 : wh d.heap k0 v = H := by
57    funext i; simp only [wh, H]; split <;> simp_all
58  have hI0 : Inv (kk, j, false) d :=
59    ⟨k0, d.heap, rfl, rfl, fun _ _ => rfl, hk, Nat.le_refl _, hk2, fun _ => by simp only; omega,
60      by rw [hwh0]; exact PermOn.refl _ _, by rw [hwh0]; exact hole_init hheap, fun e => by simp at e⟩
61  refine WS.bind' (Q := Q) (WS.cwhile2 (id := id) Inv μ Q ?_ hI0 (hf _ d)) ?_
62  · -- one step
63    rintro ⟨kk', jj, bb⟩ e ⟨K, hpc, he, hsz', hfr, hK, hK1, hK2, hj', hp, hhole, hbrk⟩
64    subst he
65    simp only at hK hj' hbrk
66    have hvalA : ∀ i, 1 ≤ i → i ≤ len → NV (tk.arr d) d.depth (wh hpc K v i) := by
67      obtain ⟨σ, hr, -, hee⟩ := hp
68      intro i h1 h2
69      have := hee i h1 h2
70      have h3 : wh hpc K v i = d.heap[σ i]! := this
71      rw [h3]; exact hval _ (hr i h1 h2).1 (hr i h1 h2).2
72    cases bb with
73    | true =>
74      refine WS.pure' (Or.inl ⟨rfl, ?_⟩)
75      obtain ⟨j', hm, hkey⟩ := hbrk rfl
76      exact ⟨K, hpc, rfl, hsz', hfr, hK, hK1, hK2, hp, hole_break kOK ⟨hk1, hK1⟩ hhole hm hkey⟩
77    | false =>
78      have hj'' : jj.toInt = 2 * K := hj' rfl
79      refine WS.bind' ws_rd fun l e1 ⟨hl, he1⟩ => ?_
80      subst e1; subst hl
81      by_cases hleaf : 2 * K ≤ len
82      · -- the body runs
83        refine WS.pure' (Or.inr ⟨?_, ?_⟩)
84        · simp only [decide_eq_true_eq]
85          show jj.toInt ≤ d.heap_len.toInt
86          omega
87        refine WS.bind' ws_rd fun l e1 ⟨hl, he1⟩ => ?_
88        subst e1; subst hl
89        dsimp only
90        have hK573 : K < hpc.size := by omega
91        have hvK : NV (tk.arr d) d.depth v := hnv
92        -- the common tail, for the chosen child `j1 = J`
93        have tail : ∀ (j1 : Int32) (J : Nat), j1.toInt = J → MinChild (sm (tk.arr d) d.depth) (wh hpc K v) len K J →
94            WS h0 id (do
95              let hj ← heapAt (Sp id) j1
96              let dp ← pDepth (Sp id)
97              let b ← smaller (Ptr.ref (tk.ref id) 0) v hj dp
98              if b = true then pure (kk', j1, true) else do
99                heapSet (Sp id) kk' hj
100                let j2 ← shl1 j1
101                pure (j1, j2, false)) { d with heap := hpc }
102              (fun st e2 => Inv st e2 ∧ μ st e2 < μ (kk', jj, false) { d with heap := hpc }) := by
103          intro j1 J hJ hm
104          have hJK : J ≠ K := by have := hm.1; omega
105          have hJ1 : 1 ≤ J ∧ J ≤ len := ⟨by have := hm.2.1; omega, hm.2.2.1⟩
106          have hK1' : 1 ≤ K := by omega
107          have hJsz : J < hpc.size := by omega
108          have hJv : (wh hpc K v J) = hpc[J]! := by simp [wh, hJK]
109          have hnJ : NV (tk.arr d) d.depth hpc[J]! := by rw [← hJv]; exact hvalA J hJ1.1 hJ1.2
110          have hjtn : j1.toInt.toNat = J := by omega
111          have hnJ' : NV (tk.arr { d with heap := hpc }) ({ d with heap := hpc }).depth
112              (({ d with heap := hpc }).heap[j1.toInt.toNat]!) := by
113            rw [tk_arr_heap]; show NV (tk.arr d) d.depth hpc[j1.toInt.toNat]!; rw [hjtn]; exact hnJ
114          have hnv' : NV (tk.arr { d with heap := hpc }) ({ d with heap := hpc }).depth v := by
115            rw [tk_arr_heap]; exact hnv
116          refine WS.mono (ws_pq_cont (h0 := h0) (id := id) tk kk' j1 v { d with heap := hpc }
117            (by show 1 ≤ kk'.toInt; omega) (by show kk'.toInt < hpc.size; omega)
118            (by show 1 ≤ j1.toInt; omega) (by show j1.toInt < hpc.size; omega) (by omega) hnJ' hnv') ?_
119          intro st e2 hq
120          rcases hq with ⟨hsm, hst, he2⟩ | ⟨hsm, hst1, hst2, hst3, he2⟩
121          · subst hst; subst he2
122            simp only [hjtn] at hsm
123            refine ⟨⟨K, hpc, rfl, hsz', hfr, hK, hK1, hK2, fun e => by simp at e, hp, hhole,
124              fun _ => ⟨J, hm, ?_⟩⟩, ?_⟩
125            · simpa [wh, hJK] using hsm
126            · simp only [μ, ite_true, Bool.false_eq_true, ite_false, Int32.toNatClampNeg]; omega
127          · have hkK : kk'.toInt.toNat = K := by omega
128            simp only [hjtn, hkK] at he2
129            subst he2
130            simp only [hjtn] at hsm
131            have hsw : wh (hpc.set! K hpc[J]!) J v = swapAt (wh hpc K v) K J := by
132              funext i
133              simp only [wh, swapAt, getD_set hpc K i _ hK573]
134              by_cases e1 : i = J
135              · subst e1; simp [hJK]
136              · by_cases e2 : i = K
137                · subst e2; simp [e1]; intro h; omega
138                · simp [e1, e2]
139            have hkey : sm (tk.arr d) d.depth (wh hpc K v K) (wh hpc K v J) = false := by
140              simpa [wh, hJK] using hsm
141            refine ⟨⟨J, hpc.set! K hpc[J]!, rfl, by rw [size_set!]; exact hsz', ?_, by rw [hst1]; exact hJ, by have := hm.1; omega, hJ1.2,
142              fun _ => by omega, ?_, ?_, fun e => by rw [hst3] at e; simp at e⟩, ?_⟩
143            · intro i hi
144              rw [getD_set hpc K i _ hK573, ite_eq_right (by omega)]; exact hfr i hi
145            · rw [hsw]; exact hp.swap ⟨hK1', hK2⟩ hJ1
146            · rw [hsw]
147              exact hole_step kOK ⟨hk1, hK1⟩ hhole hm hkey
148            · simp only [μ, hst3, ite_true, Bool.false_eq_true, ite_false, Int32.toNatClampNeg]
149              have := hm.1
150              have h1 : st.2.1.toInt = 2 * (J : Int) := by omega
151              omega
152        have hNVe : ∀ x, NV (tk.arr d) d.depth x →
153            NV (tk.arr { d with heap := hpc }) ({ d with heap := hpc }).depth x :=
154          fun x hx => by rw [tk_arr_heap]; exact hx
155        have hAe : ∀ i, i ≠ K → wh hpc K v i = hpc[i]! := fun i hi => by simp [wh, hi]
156        have h1i : (1 : Int32).toInt = 1 := rfl
157        have refl : ∀ x, sm (tk.arr d) d.depth x x = true := fun x => (kOK.total x x).elim (fun h => h) (fun h => h)
158        by_cases h2 : 2 * K < len
159        · have hlt : jj.toInt < d.heap_len.toInt := by omega
160          refine WS.ite' (fun _ => ?_) (fun hn => absurd hlt hn)
161          refine WS.bind' (ws_iadd jj 1 (by rw [h1i]; omega) (by rw [h1i]; omega)) fun j1 e1 ⟨hj1, he1⟩ => ?_
162          subst e1
163          have hi1 : j1.toInt.toNat = 2 * K + 1 := by rw [h1i] at hj1; omega
164          have hi0 : jj.toInt.toNat = 2 * K := by omega
165          refine WS.bind' (ws_heapAt j1 (by rw [h1i] at hj1; omega) (by show j1.toInt < (hpc.size : Int); rw [h1i] at hj1; omega))
166            fun a e1 ⟨ha, he1⟩ => ?_
167          subst e1
168          refine WS.bind' (ws_heapAt jj (by omega) (by show jj.toInt < (hpc.size : Int); omega)) fun b e1 ⟨hb, he1⟩ => ?_
169          subst e1
170          refine WS.bind' ws_pDepth fun dp e1 ⟨hdp, he1⟩ => ?_
171          subst e1; subst hdp
172          have hv1 : NV (tk.arr d) d.depth hpc[2 * K + 1]! := by
173            rw [← hAe _ (by omega)]; exact hvalA _ (by omega) (by omega)
174          have hv0 : NV (tk.arr d) d.depth hpc[2 * K]! := by
175            rw [← hAe _ (by omega)]; exact hvalA _ (by omega) (by omega)
176          have ha' : a = hpc[2 * K + 1]! := by rw [ha]; show hpc[j1.toInt.toNat]! = _; rw [hi1]
177          have hb' : b = hpc[2 * K]! := by rw [hb]; show hpc[jj.toInt.toNat]! = _; rw [hi0]
178          subst ha'; subst hb'
179          refine WS.bind' (ws_smaller tk _ _ (hNVe _ hv1) (hNVe _ hv0)) fun s1 e1 ⟨hs1, he1⟩ => ?_
180          subst e1
181          by_cases hs : sm (tk.arr d) d.depth hpc[2 * K + 1]! hpc[2 * K]! = true
182          · have hs1' : s1 = true := by rw [hs1]; simpa using hs
183            subst hs1'
184            simp only [ite_true]
185            refine WS.bind' (ws_iadd jj 1 (by rw [h1i]; omega) (by rw [h1i]; omega)) fun j1' e1 ⟨hj1', he1⟩ => ?_
186            subst e1
187            refine tail j1' (2 * K + 1) (by rw [h1i] at hj1'; omega) ⟨by omega, by omega, by omega, ?_⟩
188            intro c hc h2c hlc
189            have : c = 2 * K ∨ c = 2 * K + 1 := by omega
190            rcases this with rfl | rfl
191            · rw [hAe _ (by omega), hAe _ (by omega)]; exact hs
192            · exact refl _
193          · have hs1' : s1 = false := by rw [hs1]; simpa using hs
194            subst hs1'
195            simp only [Bool.false_eq_true, ite_false]
196            refine tail jj (2 * K) (by omega) ⟨by omega, by omega, by omega, ?_⟩
197            intro c hc h2c hlc
198            have : c = 2 * K ∨ c = 2 * K + 1 := by omega
199            rcases this with rfl | rfl
200            · exact refl _
201            · rcases kOK.total (wh hpc K v (2 * K)) (wh hpc K v (2 * K + 1)) with e | e
202              · exact e
203              · rw [hAe _ (by omega), hAe _ (by omega)] at e; exact absurd e hs
204        · have hnlt : ¬ jj.toInt < d.heap_len.toInt := by omega
205          refine WS.ite' (fun hn => absurd hn hnlt) (fun _ => ?_)
206          refine tail jj (2 * K) (by omega) ⟨by omega, by omega, by omega, ?_⟩
207          intro c hc h2c hlc
208          have : c = 2 * K := by omega
209          subst this
210          exact refl _
211      · refine WS.pure' (Or.inl ⟨?_, ?_⟩)
212        · simp only [decide_eq_false_iff_not]
213          show ¬ (jj.toInt ≤ d.heap_len.toInt)
214          omega
215        · exact ⟨K, hpc, rfl, hsz', hfr, hK, hK1, hK2, hp, hole_leaf ⟨hk1, hK1⟩ hhole (by omega)⟩
216  · rintro ⟨kk', jj, bb⟩ e ⟨K, hpc, he, hsz', hfr, hK, hK1, hK2, hp, hok⟩
217    subst he
218    simp only at hK
219    have hKs : K < hpc.size := by omega
220    refine WS.mono (ws_heapSet kk' v (by omega) (by show kk'.toInt < (hpc.size : Int); omega)) ?_
221    intro _ e2 he2
222    have hkn : kk'.toInt.toNat = K := by omega
223    simp only [hkn] at he2
224    subst he2
225    have hw : (fun i => (hpc.set! K v)[i]!) = wh hpc K v := by
226      funext i; simp only [wh, getD_set hpc K i v hKs]
227    refine ⟨hpc.set! K v, rfl, by rw [size_set!]; exact hsz', ?_, by rw [hw]; exact hp, by rw [hw]; exact hok⟩
228    intro i hi
229    rw [getD_set hpc K i v hKs, ite_eq_right (by omega)]; exact hfr i hi
230
231@[simp] theorem tk_arr_heap_len (tk : TK) (d : DeflateState) (a : Int32) : tk.arr { d with heap_len := a } = tk.arr d := by
232  cases tk <;> rfl
233
234/-- `pqremove`: the smallest node is returned and the heap, one shorter, has its order again. `Hm H len` is the heap
235with its last entry moved to the top, which `pqdownheap` then repairs. -/
236def Hm (H : Nat → Int32) (len : Nat) : Nat → Int32 := fun i => if i = 1 then H len else H i
237
238theorem ws_pqremove {h0 : Heap} {id : Nat} (tk : TK) (d : DeflateState) (len : Nat)
239    (hlen : d.heap_len.toInt = len) (h2 : 2 ≤ len) (hsz : len < d.heap.size) (hbig : d.heap.size ≤ 1000000)
240    (hval : ∀ i, 1 ≤ i → i ≤ len → NV (tk.arr d) d.depth d.heap[i]!)
241    (hheap : HeapOK (sm (tk.arr d) d.depth) (fun i => d.heap[i]!) len 0) :
242    WS h0 id (pqremove (Sp id) (Ptr.ref (tk.ref id) 0)) d (fun top d' =>
243      top = d.heap[1]! ∧ ∃ (hl' : Int32) (hp' : Array Int32), hl'.toInt = (len : Int) - 1 ∧
244        d' = { d with heap := hp', heap_len := hl' } ∧ hp'.size = d.heap.size ∧
245        (∀ i, ¬ (1 ≤ i ∧ i ≤ len - 1) → hp'[i]! = d.heap[i]!) ∧
246        PermOn (fun i => hp'[i]!) (Hm (fun i => d.heap[i]!) len) (len - 1) ∧
247        HeapOK (sm (tk.arr d) d.depth) (fun i => hp'[i]!) (len - 1) 0) := by
248  have kOK := sm_ok (tk.arr d) d.depth
249  unfold pqremove
250  refine WS.bind' (ws_heapAt 1 (by decide) (by show (1 : Int) < d.heap.size; omega)) fun top d1 ⟨htop, hd1⟩ => ?_
251  subst d1
252  refine WS.bind' ws_rd fun l d1 ⟨hl, hd1⟩ => ?_
253  subst d1; subst l
254  refine WS.bind' (ws_heapAt d.heap_len (by omega) (by omega)) fun v d1 ⟨hv, hd1⟩ => ?_
255  subst d1
256  refine WS.bind' (ws_isub d.heap_len 1 (by have : (1 : Int32).toInt = 1 := rfl; omega)
257    (by have : (1 : Int32).toInt = 1 := rfl; omega)) fun hl' d1 ⟨hhl', hd1⟩ => ?_
258  subst d1
259  have h1i : (1 : Int32).toInt = 1 := rfl
260  refine WS.bind' (ws_md (fun e => { e with heap_len := hl' })) fun _ d1 hd1 => ?_
261  subst hd1
262  refine WS.bind' (ws_heapSet 1 v (by decide) (by show (1 : Int) < d.heap.size; omega)) fun _ d1 hd1 => ?_
263  subst hd1
264  have hvi : v = d.heap[len]! := by rw [hv]; congr 1; omega
265  have hhl' : hl'.toInt = (len : Int) - 1 := by omega
266  have hnode : ∀ i, 1 ≤ i → i ≤ len - 1 → NV (tk.arr d) d.depth
267      ({ ({ d with heap_len := hl' } : DeflateState) with heap := d.heap.set! (1 : Int32).toInt.toNat v }).heap[i]! := by
268    intro i h1 h3
269    show NV (tk.arr d) d.depth (d.heap.set! (1 : Int32).toInt.toNat v)[i]!
270    rw [getD_set _ _ _ _ (by rw [h1i]; show 1 < d.heap.size; omega)]
271    split
272    · rw [hvi]; exact hval len (by omega) (Nat.le_refl _)
273    · exact hval i h1 (by omega)
274  have e1n : (1 : Int32).toInt.toNat = 1 := rfl
275  have hheap2 : HeapOK (sm (tk.arr d) d.depth) (fun i => (d.heap.set! 1 v)[i]!) (len - 1) 1 := by
276    intro c h2c hlc hc
277    have hs1 : 1 < d.heap.size := by omega
278    simp only [getD_set d.heap 1 _ v hs1]
279    rw [ite_eq_right (by omega), ite_eq_right (by omega)]
280    exact hheap c h2c (by omega) (by omega)
281  have key := ws_pqdownheap (h0 := h0) (id := id) tk
282    { ({ d with heap_len := hl' } : DeflateState) with heap := d.heap.set! (1 : Int32).toInt.toNat v } 1 1 (len - 1)
283    (by rw [h1i]; rfl) (Nat.le_refl _) (by omega) (by show hl'.toInt = _; omega)
284    (by show len - 1 < (d.heap.set! _ v).size; rw [size_set!]; omega)
285    (by show (d.heap.set! _ v).size ≤ _; rw [size_set!]; omega)
286    (fun i h1 h3 => by rw [tk_arr_heap, tk_arr_heap_len]; exact hnode i h1 h3)
287    (by rw [tk_arr_heap, tk_arr_heap_len, e1n]; exact hheap2)
288  refine WS.bind' key fun _ d1 ⟨hp', hd1, hsz', hfr, hperm, hok⟩ => ?_
289  subst hd1
290  refine WS.pure' ⟨?_, hl', hp', ?_, rfl, ?_, ?_, ?_, ?_⟩
291  · rw [htop, e1n]
292  · omega
293  · simpa using hsz'
294  · intro i hi
295    have := hfr i hi
296    simp only [e1n, getD_set d.heap 1 i v (by omega : 1 < d.heap.size)] at this
297    rw [this, ite_eq_right (by omega)]
298  · have hw : (fun i => (d.heap.set! 1 v)[i]!) = Hm (fun i => d.heap[i]!) len := by
299      funext i; simp only [Hm]; rw [getD_set d.heap 1 i v (by omega : 1 < d.heap.size), hvi]
300    have hperm' : PermOn (fun i => hp'[i]!) (fun i => (d.heap.set! 1 v)[i]!) (len - 1) := hperm
301    rw [hw] at hperm'; exact hperm'
302  · rw [tk_arr_heap, tk_arr_heap_len] at hok; exact hok
303
304/-! ### Heap-level statements -/
305
306/-- **`pqdownheap`, correct and safe.** Called on the heap `heap[1 .. len]`, `len = heap_len`, with the hole at
307`k0 ∈ [1, len]`. Precondition: `len` is the current `heap_len`, the heap array has more than `len` entries (the C
308array has `HEAP_SIZE = 573`), the nodes `heap[1..len]` index `tree` and `depth` (in `build_tree` they are below
309`2 * elems + 1 ≤ 573`), and the heap order holds for every parent `> k0` (`build_tree` calls it for `k0 = heap_len/2`
310down to 1, and for `k0 = 1` after replacing the root). Result: no fault; only `heap[1..len]` changes; the new
311heap is a permutation of the old one and the order holds for every parent `> k0 - 1`. `tk` says which tree array
312`tree` points to (`dyn_ltree`, `dyn_dtree` or `bl_tree` of the same state). -/
313theorem pqdownheap_correct {h : Heap} {id : Nat} {d : DeflateState} (hd : h.dstates id = some d) (tk : TK)
314    (kk : Int32) (k0 len : Nat) (hk : kk.toInt = k0) (hk1 : 1 ≤ k0) (hk2 : k0 ≤ len) (hlen : d.heap_len.toInt = len)
315    (hsz : len < d.heap.size) (hbig : d.heap.size ≤ 1000000)
316    (hval : ∀ i, 1 ≤ i → i ≤ len → NV (tk.arr d) d.depth d.heap[i]!)
317    (hheap : HeapOK (sm (tk.arr d) d.depth) (fun i => d.heap[i]!) len k0) :
318    ∃ hp', pqdownheap (Sp id) (Ptr.ref (tk.ref id) 0) kk h = .ok ((), setD h id { d with heap := hp' }) ∧
319      hp'.size = d.heap.size ∧ (∀ i, ¬ (1 ≤ i ∧ i ≤ len) → hp'[i]! = d.heap[i]!) ∧
320      PermOn (fun i => hp'[i]!) (fun i => d.heap[i]!) len ∧
321      HeapOK (sm (tk.arr d) d.depth) (fun i => hp'[i]!) len (k0 - 1) := by
322  have := ws_pqdownheap (h0 := h) (id := id) tk d kk k0 len hk hk1 hk2 hlen hsz hbig hval hheap
323  obtain ⟨_, d', e, hp', rfl, hr⟩ := this
324  rw [setD_self hd] at e
325  exact ⟨hp', e, hr⟩
326
327/-- **`pqdownheap` does not fault**: the preconditions of `pqdownheap_correct` (hole `k0 ∈ [1, heap_len]`, nodes of
328`heap[1..heap_len]` inside `tree` and `depth`, heap order for parents `> k0`) give a run to the end; every index is
329inside the arrays. -/
330theorem pqdownheap_safe {h : Heap} {id : Nat} {d : DeflateState} (hd : h.dstates id = some d) (tk : TK)
331    (kk : Int32) (k0 len : Nat) (hk : kk.toInt = k0) (hk1 : 1 ≤ k0) (hk2 : k0 ≤ len) (hlen : d.heap_len.toInt = len)
332    (hsz : len < d.heap.size) (hbig : d.heap.size ≤ 1000000)
333    (hval : ∀ i, 1 ≤ i → i ≤ len → NV (tk.arr d) d.depth d.heap[i]!)
334    (hheap : HeapOK (sm (tk.arr d) d.depth) (fun i => d.heap[i]!) len k0) :
335    ∃ h', pqdownheap (Sp id) (Ptr.ref (tk.ref id) 0) kk h = .ok ((), h') := by
336  obtain ⟨hp', e, -⟩ := pqdownheap_correct hd tk kk k0 len hk hk1 hk2 hlen hsz hbig hval hheap
337  exact ⟨_, e⟩
338
339/-- **`pqremove`, correct and safe.** Called with `heap_len = len ≥ 2` (the loop of `build_tree` runs while
340`heap_len ≥ 2`), the heap order holding everywhere. It returns `heap[1]`, the smallest node, sets `heap_len` to
341`len - 1`, and leaves `heap[1 .. len-1]` a heap, a permutation of the old `heap[2..len]`. -/
342theorem pqremove_correct {h : Heap} {id : Nat} {d : DeflateState} (hd : h.dstates id = some d) (tk : TK) (len : Nat)
343    (hlen : d.heap_len.toInt = len) (h2 : 2 ≤ len) (hsz : len < d.heap.size) (hbig : d.heap.size ≤ 1000000)
344    (hval : ∀ i, 1 ≤ i → i ≤ len → NV (tk.arr d) d.depth d.heap[i]!)
345    (hheap : HeapOK (sm (tk.arr d) d.depth) (fun i => d.heap[i]!) len 0) :
346    ∃ (hl' : Int32) (hp' : Array Int32), hl'.toInt = (len : Int) - 1 ∧
347      pqremove (Sp id) (Ptr.ref (tk.ref id) 0) h = .ok (d.heap[1]!, setD h id { d with heap := hp', heap_len := hl' }) ∧
348      hp'.size = d.heap.size ∧ (∀ i, ¬ (1 ≤ i ∧ i ≤ len - 1) → hp'[i]! = d.heap[i]!) ∧
349      PermOn (fun i => hp'[i]!) (Hm (fun i => d.heap[i]!) len) (len - 1) ∧
350      HeapOK (sm (tk.arr d) d.depth) (fun i => hp'[i]!) (len - 1) 0 := by
351  have := ws_pqremove (h0 := h) (id := id) tk d len hlen h2 hsz hbig hval hheap
352  obtain ⟨top, d', e, htop, hl', hp', hh, rfl, hr⟩ := this
353  rw [setD_self hd] at e
354  subst htop
355  exact ⟨hl', hp', hh, e, hr⟩
356
357/-- **`pqremove` does not fault**: `heap_len ≥ 2`, the nodes of `heap[1..heap_len]` inside `tree` and `depth`, the
358heap order everywhere (see `pqremove_correct`). -/
359theorem pqremove_safe {h : Heap} {id : Nat} {d : DeflateState} (hd : h.dstates id = some d) (tk : TK) (len : Nat)
360    (hlen : d.heap_len.toInt = len) (h2 : 2 ≤ len) (hsz : len < d.heap.size) (hbig : d.heap.size ≤ 1000000)
361    (hval : ∀ i, 1 ≤ i → i ≤ len → NV (tk.arr d) d.depth d.heap[i]!)
362    (hheap : HeapOK (sm (tk.arr d) d.depth) (fun i => d.heap[i]!) len 0) :
363    ∃ (top : Int32) (h' : Heap), pqremove (Sp id) (Ptr.ref (tk.ref id) 0) h = .ok (top, h') := by
364  obtain ⟨_, _, _, e, -⟩ := pqremove_correct hd tk len hlen h2 hsz hbig hval hheap
365  exact ⟨_, _, e⟩
366
367end Zlib.Trees.Proofs