trees.c.heap.ord.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.base»
2
3/-!
4# Binary heaps ordered by `smaller` (pure)
5
6Migrated from the earlier attempt (its `Spec/trees/Build.lean`), unchanged except for the namespace. The heap is
7`heap[1 .. heap_len]` (children of `p` are `2p`, `2p+1`), ordered by zlib's `smaller` macro: `key a b` iff
8`Freq[a] < Freq[b]`, or equal frequencies and `depth[a] ≤ depth[b]` (a total preorder). `HeapOK key H len k`: the
9heap property holds for every parent `> k`; `HoleInv` is the invariant of the sift-down loop.
10-/
11
12namespace Zlib.Trees.Proofs
13
14/-- zlib's `smaller(tree, n, m, depth)` on node values. -/
15def smallerB (fr : Nat → UInt16) (dp : Nat → UInt8) (a b : Int32) : Bool :=
16  decide (fr a.toInt.toNat < fr b.toInt.toNat) ||
17    (fr a.toInt.toNat == fr b.toInt.toNat && decide (dp a.toInt.toNat ≤ dp b.toInt.toNat))
18
19/-- A total preorder. -/
20structure KeyOK (key : Int32 → Int32 → Bool) : Prop where
21  total : ∀ a b, key a b = true ∨ key b a = true
22  trans : ∀ a b c, key a b = true → key b c = true → key a c = true
23
24theorem smallerB_ok (fr : Nat → UInt16) (dp : Nat → UInt8) : KeyOK (smallerB fr dp) := by
25  constructor
26  · intro a b
27    simp only [smallerB, Bool.or_eq_true, decide_eq_true_eq, Bool.and_eq_true, beq_iff_eq,
28      UInt16.lt_iff_toNat_lt, ← UInt16.toNat_inj, UInt8.le_iff_toNat_le]
29    omega
30  · intro a b c
31    simp only [smallerB, Bool.or_eq_true, decide_eq_true_eq, Bool.and_eq_true, beq_iff_eq,
32      UInt16.lt_iff_toNat_lt, ← UInt16.toNat_inj, UInt8.le_iff_toNat_le]
33    omega
34
35/-- Heap property for every parent `p > k` (in `1 .. len`). -/
36def HeapOK (key : Int32 → Int32 → Bool) (H : Nat → Int32) (len k : Nat) : Prop :=
37  ∀ c, 2 ≤ c → c ≤ len → k < c / 2 → key (H (c / 2)) (H c) = true
38
39/-- `H'` on `1 .. len` is a permutation of `H` on `1 .. len`. -/
40def PermOn (H' H : Nat → Int32) (len : Nat) : Prop :=
41  ∃ σ : Nat → Nat, (∀ i, 1 ≤ i → i ≤ len → 1 ≤ σ i ∧ σ i ≤ len) ∧
42    (∀ i i', 1 ≤ i → i ≤ len → 1 ≤ i' → i' ≤ len → σ i = σ i' → i = i') ∧
43    ∀ i, 1 ≤ i → i ≤ len → H' i = H (σ i)
44
45theorem PermOn.refl (H : Nat → Int32) (len : Nat) : PermOn H H len :=
46  ⟨id, fun i a b => ⟨a, b⟩, fun i i' _ _ _ _ e => e, fun _ _ _ => rfl⟩
47
48/-- Swap positions `a`, `b`. -/
49def swapAt (A : Nat → Int32) (a b : Nat) : Nat → Int32 :=
50  fun i => if i = a then A b else if i = b then A a else A i
51
52theorem PermOn.swap {A H : Nat → Int32} {len : Nat} (hp : PermOn A H len) {a b : Nat}
53    (ha : 1 ≤ a ∧ a ≤ len) (hb : 1 ≤ b ∧ b ≤ len) : PermOn (swapAt A a b) H len := by
54  obtain ⟨σ, hr, hi, he⟩ := hp
55  let τ : Nat → Nat := fun i => if i = a then b else if i = b then a else i
56  refine ⟨σ ∘ τ, ?_, ?_, ?_⟩
57  · intro i h1 h2; simp only [Function.comp, τ]; split
58    · exact hr b hb.1 hb.2
59    · split
60      · exact hr a ha.1 ha.2
61      · exact hr i h1 h2
62  · intro i i' h1 h2 h3 h4 e
63    simp only [Function.comp, τ] at e
64    have hτ : ∀ x, 1 ≤ x → x ≤ len → 1 ≤ τ x ∧ τ x ≤ len := by
65      intro x h1 h2; simp only [τ]; split
66      · exact hb
67      · split
68        · exact ha
69        · exact ⟨h1, h2⟩
70    have := hi _ _ (hτ i h1 h2).1 (hτ i h1 h2).2 (hτ i' h3 h4).1 (hτ i' h3 h4).2 e
71    simp only [τ] at this
72    split at this <;> split at this <;> (try split at this) <;> (try split at this) <;> omega
73  · intro i h1 h2; simp only [Function.comp, τ, swapAt]; split
74    · exact he b hb.1 hb.2
75    · split
76      · exact he a ha.1 ha.2
77      · exact he i h1 h2
78
79/-- Sift-down hole invariant: `A` is the array with the pending value at the
80hole `K`; all parent/child pairs with parent `≥ k0` not touching `K` hold, and
81the parent of the hole is `≤` the hole value and the hole's children. -/
82def HoleInv (key : Int32 → Int32 → Bool) (A : Nat → Int32) (len k0 K : Nat) : Prop :=
83  (∀ c, 2 ≤ c → c ≤ len → k0 ≤ c / 2 → c / 2 ≠ K → c ≠ K → key (A (c / 2)) (A c) = true) ∧
84  (k0 < K → key (A (K / 2)) (A K) = true ∧
85    ∀ c, c / 2 = K → 2 ≤ c → c ≤ len → key (A (K / 2)) (A c) = true)
86
87theorem hole_init {key : Int32 → Int32 → Bool} {A : Nat → Int32} {len k0 : Nat}
88    (h : HeapOK key A len k0) : HoleInv key A len k0 k0 :=
89  ⟨fun c a b d e _ => h c a b (by omega), fun h => absurd h (Nat.lt_irrefl _)⟩
90
91/-- `j'` is a minimal child of `K`. -/
92def MinChild (key : Int32 → Int32 → Bool) (A : Nat → Int32) (len K j' : Nat) : Prop :=
93  j' / 2 = K ∧ 2 ≤ j' ∧ j' ≤ len ∧ ∀ c, c / 2 = K → 2 ≤ c → c ≤ len → key (A j') (A c) = true
94
95theorem hole_break {key : Int32 → Int32 → Bool} (hk : KeyOK key) {A : Nat → Int32} {len k0 K j' : Nat}
96    (hK : 1 ≤ k0 ∧ k0 ≤ K) (hI : HoleInv key A len k0 K) (hm : MinChild key A len K j')
97    (hv : key (A K) (A j') = true) : HeapOK key A len (k0 - 1) := by
98  intro c h2 hl hp
99  by_cases e1 : c / 2 = K
100  · rw [e1]; exact hk.trans _ _ _ hv (hm.2.2.2 c e1 h2 hl)
101  · by_cases e2 : c = K
102    · subst e2; exact (hI.2 (by omega)).1
103    · exact hI.1 c h2 hl (by omega) e1 e2
104
105theorem hole_leaf {key : Int32 → Int32 → Bool} {A : Nat → Int32} {len k0 K : Nat}
106    (hK : 1 ≤ k0 ∧ k0 ≤ K) (hI : HoleInv key A len k0 K) (hleaf : len < 2 * K) :
107    HeapOK key A len (k0 - 1) := by
108  intro c h2 hl hp
109  by_cases e1 : c / 2 = K
110  · omega
111  · by_cases e2 : c = K
112    · subst e2; exact (hI.2 (by omega)).1
113    · exact hI.1 c h2 hl (by omega) e1 e2
114
115theorem hole_step {key : Int32 → Int32 → Bool} (hk : KeyOK key) {A : Nat → Int32} {len k0 K j' : Nat}
116    (hK : 1 ≤ k0 ∧ k0 ≤ K) (hI : HoleInv key A len k0 K) (hm : MinChild key A len K j')
117    (hv : key (A K) (A j') = false) : HoleInv key (swapAt A K j') len k0 j' := by
118  obtain ⟨hj2, hj2', hjl, hmin⟩ := hm
119  have hjK : K < j' := by omega
120  have hkey : key (A j') (A K) = true := by
121    rcases hk.total (A K) (A j') with h | h
122    · rw [hv] at h; cases h
123    · exact h
124  refine ⟨?_, ?_⟩
125  · intro c h2 hl hp e1 e2
126    simp only [swapAt]
127    by_cases f1 : c / 2 = K
128    · rw [ite_eq_left f1, ite_eq_right (by omega), ite_eq_right e2]
129      exact hmin c f1 h2 hl
130    · by_cases f2 : c = K
131      · rw [ite_eq_right f1, ite_eq_right (by omega), ite_eq_left f2]
132        subst f2
133        exact (hI.2 (by omega)).2 j' hj2 hj2' hjl
134      · rw [ite_eq_right f1, ite_eq_right e1, ite_eq_right f2, ite_eq_right e2]
135        exact hI.1 c h2 hl hp f1 f2
136  · intro _
137    have hne : j' ≠ K := by omega
138    refine ⟨?_, ?_⟩
139    · simp only [swapAt, hj2, hne, ite_true, ite_false]; exact hkey
140    · intro c hc h2 hl
141      have n1 : c ≠ K := by omega
142      have n2 : c ≠ j' := by omega
143      simp only [swapAt, hj2, n1, n2, ite_true, ite_false]
144      have := hI.1 c h2 hl (by omega) (by omega) n1; rwa [hc] at this
145
146end Zlib.Trees.Proofs