参考文档 / ZLIB × LEAN
trees.c.heap.pq.lean
此页源文件快照 ·
7ab9a57c04eefed3 · 对应提交的原文 ↗本页保留 Lean 源码及行号。点击行号可定位语句，点击 import 中的模块名可查看依赖。
1import ZlibF.Proof.«trees.c.heap.base»
2
3/-!
4# trees.c: `pqdownheap` and `pqremove`
5
6The priority queue is `s->heap[1 .. heap_len]`, ordered by `smaller` (frequency, then depth). `pqd` is the pure
7model of `pqdownheap`; `ws_pqdownheap` says the translation computes it, with every index inside the arrays.
8-/
9
10namespace Zlib.Trees.Proofs
11open C Zlib.Trees
12
13/-! ### Checked `int` arithmetic -/
14
15theorem ofInt_toInt' (x : Int) (h1 : -2147483648 ≤ x) (h2 : x ≤ 2147483647) : (Int32.ofInt x).toInt = x := by
16 rw [Int32.toInt_ofInt]
17 have : Int32.size = 4294967296 := rfl
18 rw [this, Int.bmod_eq_of_le] <;> omega
19
20section arith
21variable {h0 : Heap} {id : Nat} {d : DeflateState}
22
23theorem ws_ck (x : Int) (h1 : -2147483648 ≤ x) (h2 : x ≤ 2147483647) :
24 WS h0 id (ck x) d (fun v d' => v.toInt = x ∧ d' = d) :=
25 WS.of_eq (by simp [ck, h1, h2]) ⟨ofInt_toInt' x h1 h2, rfl⟩
26
27theorem ws_iadd (a b : Int32) (h1 : -2147483648 ≤ a.toInt + b.toInt) (h2 : a.toInt + b.toInt ≤ 2147483647) :
28 WS h0 id (iadd a b) d (fun v d' => v.toInt = a.toInt + b.toInt ∧ d' = d) := ws_ck _ h1 h2
29
30theorem ws_isub (a b : Int32) (h1 : -2147483648 ≤ a.toInt - b.toInt) (h2 : a.toInt - b.toInt ≤ 2147483647) :
31 WS h0 id (isub a b) d (fun v d' => v.toInt = a.toInt - b.toInt ∧ d' = d) := ws_ck _ h1 h2
32
33theorem ws_shl1 (x : Int32) (h1 : 0 ≤ x.toInt) (h2 : x.toInt * 2 ≤ 2147483647) :
34 WS h0 id (shl1 x) d (fun v d' => v.toInt = x.toInt * 2 ∧ d' = d) := by
35 have : ¬ x.toInt < 0 := by omega
36 unfold shl1
37 simp only [this, ite_false]
38 exact ws_ck _ (by omega) h2
39
40theorem ws_heapAt (i : Int32) (h1 : 0 ≤ i.toInt) (h2 : i.toInt < d.heap.size) :
41 WS h0 id (heapAt (Sp id) i) d (fun v d' => v = d.heap[i.toInt.toNat]! ∧ d' = d) := by
42 unfold heapAt
43 refine WS.bind' ws_pHeap fun p d1 ⟨hp, hd⟩ => ?_
44 subst hp; subst hd
45 exact ws_index_heap _ h1 h2
46
47theorem ws_heapSet (i : Int32) (v : Int32) (h1 : 0 ≤ i.toInt) (h2 : i.toInt < d.heap.size) :
48 WS h0 id (heapSet (Sp id) i v) d (fun _ d' => d' = { d with heap := d.heap.set! i.toInt.toNat v }) := by
49 unfold heapSet
50 refine WS.bind' ws_pHeap fun p d1 ⟨hp, hd⟩ => ?_
51 subst hp; subst hd
52 exact ws_setAt_heap _ _ h1 h2
53
54end arith
55
56/-! ### The order `smaller` -/
57
58/-- `smaller(tree, n, m, depth)` on the arrays. -/
59def sm (T : Array CtData) (D : Array UInt8) (n m : Int32) : Bool :=
60 decide ((T[n.toInt.toNat]!).fc < (T[m.toInt.toNat]!).fc) ||
61 ((T[n.toInt.toNat]!).fc == (T[m.toInt.toNat]!).fc && decide (D[n.toInt.toNat]! ≤ D[m.toInt.toNat]!))
62
63/-- `x` is a node of the tree `T` with a depth entry. -/
64def NV (T : Array CtData) (D : Array UInt8) (x : Int32) : Prop :=
65 0 ≤ x.toInt ∧ x.toInt < T.size ∧ x.toInt < D.size
66
67theorem ws_smaller {h0 : Heap} {id : Nat} {d : DeflateState} (k : TK) (n m : Int32)
68 (hn : NV (k.arr d) d.depth n) (hm : NV (k.arr d) d.depth m) :
69 WS h0 id (smaller (Ptr.ref (k.ref id) 0) n m (Ptr.ref (BRef.dstate_depth id) 0)) d
70 (fun v d' => v = sm (k.arr d) d.depth n m ∧ d' = d) := by
71 obtain ⟨hn0, hn1, hn2⟩ := hn
72 obtain ⟨hm0, hm1, hm2⟩ := hm
73 unfold smaller
74 refine WS.bind' (ws_getFc k _ hn0 hn1) fun fn d1 ⟨hfn, hd1⟩ => ?_
75 subst hd1
76 refine WS.bind' (ws_getFc k _ hm0 hm1) fun fm d1 ⟨hfm, hd1⟩ => ?_
77 subst hd1
78 subst hfn; subst hfm
79 refine WS.ite' (fun hlt => ?_) (fun hnlt => ?_)
80 · refine WS.pure' ⟨?_, rfl⟩
81 simp only [sm, hlt, decide_true, Bool.true_or]
82 · refine WS.ite' (fun heq => ?_) (fun hne => ?_)
83 · refine WS.bind' (ws_index_depth _ hn0 hn2) fun dn d1 ⟨hdn, hd1⟩ => ?_
84 subst hd1
85 refine WS.bind' (ws_index_depth _ hm0 hm2) fun dm d1 ⟨hdm, hd1⟩ => ?_
86 subst hd1
87 subst hdn; subst hdm
88 refine WS.pure' ⟨?_, rfl⟩
89 simp only [sm, hnlt, heq, decide_false, Bool.false_or, Bool.true_and]
90 · refine WS.pure' ⟨?_, rfl⟩
91 have hne' : ((k.arr d1)[n.toInt.toNat]!.fc == (k.arr d1)[m.toInt.toNat]!.fc) = false := by simpa using hne
92 simp only [sm, hnlt, hne', decide_false, Bool.false_or, Bool.false_and]
93
94
95@[simp] theorem tk_arr_heap (tk : TK) (d : DeflateState) (a : Array Int32) : tk.arr { d with heap := a } = tk.arr d := by
96 cases tk <;> rfl
97
98/-- The common tail of one pass of the loop of `pqdownheap`, for the child `jj` that was chosen. -/
99theorem ws_pq_cont {h0 : Heap} {id : Nat} (tk : TK) (kk jj v : Int32) (e : DeflateState)
100 (hk1 : 1 ≤ kk.toInt) (hk2 : kk.toInt < e.heap.size) (hj1 : 1 ≤ jj.toInt) (hj2 : jj.toInt < e.heap.size)
101 (hj3 : jj.toInt ≤ 1000000000)
102 (hnj : NV (tk.arr e) e.depth (e.heap[jj.toInt.toNat]!)) (hnv : NV (tk.arr e) e.depth v) :
103 WS h0 id (do
104 let hj ← heapAt (Sp id) jj
105 let dp ← pDepth (Sp id)
106 let b ← smaller (Ptr.ref (tk.ref id) 0) v hj dp
107 if b = true then pure (kk, jj, true) else do
108 heapSet (Sp id) kk hj
109 let j2 ← shl1 jj
110 pure (jj, j2, false)) e
111 (fun st e' =>
112 (sm (tk.arr e) e.depth v e.heap[jj.toInt.toNat]! = true ∧ st = (kk, jj, true) ∧ e' = e) ∨
113 (sm (tk.arr e) e.depth v e.heap[jj.toInt.toNat]! = false ∧ st.1 = jj ∧ st.2.1.toInt = 2 * jj.toInt ∧
114 st.2.2 = false ∧ e' = { e with heap := e.heap.set! kk.toInt.toNat e.heap[jj.toInt.toNat]! })) := by
115 refine WS.bind' (ws_heapAt jj (by omega) hj2) fun hj e1 ⟨hhj, he1⟩ => ?_
116 subst e1; subst hhj
117 refine WS.bind' ws_pDepth fun dp e1 ⟨hdp, he1⟩ => ?_
118 subst e1; subst hdp
119 refine WS.bind' (ws_smaller tk v _ hnv hnj) fun b e1 ⟨hb, he1⟩ => ?_
120 subst e1; subst hb
121 cases hsm : sm (tk.arr e) e.depth v e.heap[jj.toInt.toNat]!
122 · simp only [Bool.false_eq_true, ite_false]
123 refine WS.bind' (ws_heapSet kk _ (by omega) hk2) fun _ e1 he1 => ?_
124 subst e1
125 refine WS.bind' (ws_shl1 jj (by omega) (by omega)) fun j2 e1 ⟨hj2', he1⟩ => ?_
126 subst e1
127 refine WS.pure' (Or.inr ⟨trivial, rfl, ?_, rfl, rfl⟩)
128 show j2.toInt = 2 * jj.toInt
129 omega
130 · simp only [ite_true]
131 exact WS.pure' (Or.inl ⟨trivial, rfl, rfl⟩)
132
133end Zlib.Trees.Proofs