DeflateHeapRemove.lean

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

1import ZlibF.Math.DeflateHeap
2import ZlibF.Proof.«trees.c.heap.pqrun»
3
4/-! # Removing a binary-heap root: exact entries and finite sums -/
5
6namespace Zlib.Trees.Proofs
7
8/-- A heap permutation preserves any natural-valued sum of its entries. -/
9theorem PermOn.sum {A H : Nat → Int32} {len : Nat} (hp : PermOn A H len) (F : Int32 → Nat) :
10    GB.rs (fun i => F (A (i + 1))) len = GB.rs (fun i => F (H (i + 1))) len := by
11  obtain ⟨σ, hr, hinj, he⟩ := hp
12  let P : Nat → Nat := fun i => σ (i + 1) - 1
13  have hP : ∀ i < len, P i < len := by
14    intro i hi
15    have := hr (i + 1) (by omega) (by omega)
16    dsimp only [P]; omega
17  have hPi : ∀ i j, i < len → j < len → P i = P j → i = j := by
18    intro i j hi hj hij
19    have ha := hr (i + 1) (by omega) (by omega)
20    have hb := hr (j + 1) (by omega) (by omega)
21    have hs : σ (i + 1) = σ (j + 1) := by dsimp only [P] at hij; omega
22    have := hinj (i + 1) (j + 1) (by omega) (by omega) (by omega) (by omega) hs
23    omega
24  have heq : GB.rs (fun i => F (A (i + 1))) len =
25      GB.rs (fun i => (fun j => F (H (j + 1))) (P i)) len := by
26    apply GB.rs_congr
27    intro i hi
28    have ha := hr (i + 1) (by omega) (by omega)
29    rw [he (i + 1) (by omega) (by omega)]
30    dsimp only [P]
31    congr 2
32    omega
33  rw [heq]
34  exact GB.rs_perm P (fun j => F (H (j + 1))) len hP hPi
35
36/-- Removing the root loses exactly that entry, for any natural-valued
37observation. This does not assume unique node values. -/
38theorem PermOn.removed_sum {A H : Nat → Int32} {len : Nat}
39    (hp : PermOn A (Hm H len) (len - 1)) (h2 : 2 ≤ len) (F : Int32 → Nat) :
40    GB.rs (fun i => F (A (i + 1))) (len - 1) + F (H 1) =
41      GB.rs (fun i => F (H (i + 1))) len := by
42  rw [hp.sum F]
43  have hm : len - 1 = 1 + (len - 2) := by omega
44  have hl : len = (len - 1) + 1 := by omega
45  rw [hl, GB.rs_succ]
46  rw [show len - 1 + 1 = len by omega]
47  rw [hm, GB.rs_split, GB.rs_split]
48  simp only [GB.rs_succ, GB.rs_zero, Nat.zero_add, Hm]
49  have heq : GB.rs (fun i => F (if 1 + i + 1 = 1 then H len else H (1 + i + 1))) (len - 2) =
50      GB.rs (fun i => F (H (1 + i + 1))) (len - 2) := by
51    apply GB.rs_congr
52    intro i hi
53    rw [ite_eq_right (by omega)]
54  rw [heq, ite_eq_left trivial]
55  omega
56
57/-- Every remaining entry came from a non-root old position. -/
58theorem PermOn.removed_origin {A H : Nat → Int32} {len : Nat}
59    (hp : PermOn A (Hm H len) (len - 1)) (h2 : 2 ≤ len)
60    (q : Nat) (hq1 : 1 ≤ q) (hq2 : q ≤ len - 1) :
61    ∃ i : Nat, 2 ≤ i ∧ i ≤ len ∧ A q = H i := by
62  obtain ⟨σ, hr, hinj, he⟩ := hp
63  have hs := hr q hq1 hq2
64  have hv := he q hq1 hq2
65  dsimp only [Hm] at hv
66  by_cases heq : σ q = 1
67  · exact ⟨len, h2, Nat.le_refl _, by simpa [heq] using hv⟩
68  · exact ⟨σ q, by omega, by omega, by simpa only [ite_eq_right heq] using hv⟩
69
70/-- Every old non-root entry remains present after deletion and sift-down. -/
71theorem PermOn.removed_preimage {A H : Nat → Int32} {len : Nat}
72    (hp : PermOn A (Hm H len) (len - 1)) (h2 : 2 ≤ len)
73    (i : Nat) (hi1 : 2 ≤ i) (hi2 : i ≤ len) :
74    ∃ q : Nat, 1 ≤ q ∧ q ≤ len - 1 ∧ A q = H i := by
75  by_cases heq : i = len
76  · obtain ⟨q, hq1, hq2, hq⟩ := hp.preimage 1 (by omega) (by omega)
77    exact ⟨q, hq1, hq2, by simpa [Hm, heq] using hq⟩
78  · obtain ⟨q, hq1, hq2, hq⟩ := hp.preimage i (by omega) (by omega)
79    exact ⟨q, hq1, hq2, by simpa only [Hm, ite_eq_right (show i ≠ 1 by omega)] using hq⟩
80
81/-- Root deletion and permutation preserve distinctness and exclude the
82removed root from every populated slot. -/
83theorem PermOn.removed_injective {A H : Nat → Int32} {len : Nat}
84    (hp : PermOn A (Hm H len) (len - 1)) (h2 : 2 ≤ len)
85    (hinj : ∀ i j, 1 ≤ i → i ≤ len → 1 ≤ j → j ≤ len → H i = H j → i = j) :
86    (∀ q, 1 ≤ q → q ≤ len - 1 → A q ≠ H 1) ∧
87      ∀ q q', 1 ≤ q → q ≤ len - 1 → 1 ≤ q' → q' ≤ len - 1 → A q = A q' → q = q' := by
88  have hmap : ∀ i, 1 ≤ i → i ≤ len - 1 → 2 ≤ (if i = 1 then len else i) ∧ (if i = 1 then len else i) ≤ len := by
89    intro i hi1 hi2
90    split <;> omega
91  constructor
92  · intro q hq1 hq2 hroot
93    obtain ⟨i, hi1, hi2, hqi⟩ := hp.removed_origin h2 q hq1 hq2
94    have heq := hinj i 1 (by omega) hi2 (by omega) (by omega) (hqi.symm.trans hroot)
95    omega
96  · obtain ⟨σ, hr, hσ, he⟩ := hp
97    intro q q' hq1 hq2 hq'1 hq'2 hqq
98    have hs := hr q hq1 hq2
99    have hs' := hr q' hq'1 hq'2
100    have ha := hmap (σ q) hs.1 hs.2
101    have hb := hmap (σ q') hs'.1 hs'.2
102    have hvals : H (if σ q = 1 then len else σ q) = H (if σ q' = 1 then len else σ q') := by
103      have hqa := he q hq1 hq2
104      have hqb := he q' hq'1 hq'2
105      dsimp only [Hm] at hqa hqb
106      simpa only [apply_ite] using hqa.symm.trans (hqq.trans hqb)
107    have hi := hinj _ _ (by omega) ha.2 (by omega) hb.2 hvals
108    have heq : σ q = σ q' := by split at hi <;> split at hi <;> omega
109    exact hσ q q' hq1 hq2 hq'1 hq'2 heq
110
111/-- Replacing the root removes its old observation and adds the new one. -/
112theorem replace_root_sum (H : Nat → Int32) (node : Int32) (len : Nat) (h1 : 1 ≤ len) (F : Int32 → Nat) :
113    GB.rs (fun i => F (if i + 1 = 1 then node else H (i + 1))) len + F (H 1) =
114      GB.rs (fun i => F (H (i + 1))) len + F node := by
115  have h := GB.rs_upd (F := fun i => F (if i + 1 = 1 then node else H (i + 1)))
116    (G := fun i => F (H (i + 1))) (n := len) (k := 0) (by omega) (by
117      intro i hi hne
118      rw [ite_eq_right (by omega)])
119  simpa using h
120
121
122/-- Reindexing a queue preserves distinctness of its entries. -/
123theorem PermOn.injective {A H : Nat → Int32} {len : Nat} (hp : PermOn A H len)
124    (hi : ∀ i j, 1 ≤ i → i ≤ len → 1 ≤ j → j ≤ len → H i = H j → i = j) :
125    ∀ i j, 1 ≤ i → i ≤ len → 1 ≤ j → j ≤ len → A i = A j → i = j := by
126  obtain ⟨σ, hr, hs, he⟩ := hp
127  intro i j hi1 hi2 hj1 hj2 hij
128  apply hs i j hi1 hi2 hj1 hj2
129  apply hi _ _ (hr i hi1 hi2).1 (hr i hi1 hi2).2 (hr j hj1 hj2).1 (hr j hj1 hj2).2
130  rw [← he i hi1 hi2, ← he j hj1 hj2]
131  exact hij
132
133end Zlib.Trees.Proofs