DeflateHeap.lean

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

1import ZlibF.Proof.«trees.c.heap.ord»
2import ZlibF.Proof.«trees.c.heap.gbmath»
3
4/-!
5# Finite permutations of binary-heap entries
6
7The existing `PermOn` and finite-range pigeonhole theorem are reused here.
8These lemmas concern functions and bounded indices; they do not execute or
9modify a heap.
10-/
11
12namespace Zlib.Trees.Proofs
13
14/-- Compose permutations of the same populated heap interval. -/
15theorem PermOn.trans' {A B D : Nat → Int32} {len : Nat}
16    (h1 : PermOn A B len) (h2 : PermOn B D len) : PermOn A D len := by
17  obtain ⟨σ, hr, hi, he⟩ := h1
18  obtain ⟨τ, hr', hi', he'⟩ := h2
19  refine ⟨τ ∘ σ, fun i a b => hr' _ (hr i a b).1 (hr i a b).2,
20    fun i i' a b c d e => ?_, fun i a b => ?_⟩
21  · exact hi i i' a b c d (hi' _ _ (hr i a b).1 (hr i a b).2 (hr i' c d).1 (hr i' c d).2 e)
22  · simp only [Function.comp]; rw [he i a b, he' _ (hr i a b).1 (hr i a b).2]
23
24/-- A bounded injective reindexing also preserves every old entry. -/
25theorem PermOn.preimage {A H : Nat → Int32} {len : Nat} (hp : PermOn A H len)
26    (i : Nat) (hi1 : 1 ≤ i) (hi2 : i ≤ len) :
27    ∃ j : Nat, 1 ≤ j ∧ j ≤ len ∧ A j = H i := by
28  obtain ⟨σ, hr, hj, he⟩ := hp
29  let P : Nat → Nat := fun q => σ (q + 1) - 1
30  have hP : ∀ q < len, P q < len := by
31    intro q hq
32    have := hr (q + 1) (by omega) (by omega)
33    dsimp only [P]; omega
34  have hPi : ∀ q q', q < len → q' < len → P q = P q' → q = q' := by
35    intro q q' hq hq' heq
36    have ha := hr (q + 1) (by omega) (by omega)
37    have hb := hr (q' + 1) (by omega) (by omega)
38    have hs : σ (q + 1) = σ (q' + 1) := by dsimp only [P] at heq; omega
39    have := hj (q + 1) (q' + 1) (by omega) (by omega) (by omega) (by omega) hs
40    omega
41  obtain ⟨q, hq, heq⟩ := GB.inj_surj P len hP hPi (i - 1) (by omega)
42  refine ⟨q + 1, by omega, by omega, ?_⟩
43  rw [he (q + 1) (by omega) (by omega)]
44  have := hr (q + 1) (by omega) (by omega)
45  have hs : σ (q + 1) = i := by dsimp only [P] at heq; omega
46  rw [hs]
47
48/-- Every populated entry is above the root in the comparison preorder. -/
49theorem HeapOK.root_min {key : Int32 → Int32 → Bool} {H : Nat → Int32} {len : Nat}
50    (hk : KeyOK key) (ho : HeapOK key H len 0) :
51    ∀ q, 1 ≤ q → q ≤ len → key (H 1) (H q) = true := by
52  intro q
53  induction q using Nat.strongRecOn with
54  | _ q ih =>
55    intro hq1 hq2
56    by_cases heq : q = 1
57    · subst q
58      rcases hk.total (H 1) (H 1) with h | h <;> exact h
59    · have hq : 2 ≤ q := by omega
60      have hp : key (H 1) (H (q / 2)) = true :=
61        ih (q / 2) (by omega) (by omega) (by omega)
62      exact hk.trans _ _ _ hp (ho q hq hq2 (by omega))
63
64end Zlib.Trees.Proofs