diff options
Diffstat (limited to 'Common/BinaryHeap.lean')
| -rw-r--r-- | Common/BinaryHeap.lean | 126 |
1 files changed, 113 insertions, 13 deletions
diff --git a/Common/BinaryHeap.lean b/Common/BinaryHeap.lean index 7e2724b..e876bc0 100644 --- a/Common/BinaryHeap.lean +++ b/Common/BinaryHeap.lean @@ -3,7 +3,7 @@ namespace BinaryHeap /--A heap, represented as a binary indexed tree. The heap predicate is a type parameter, the index is the element count.-/ inductive BinaryHeap (α : Type u) (lt : α → α → Bool): Nat → Type u | leaf : BinaryHeap α lt 0 - | branch : (val : α) → (left : BinaryHeap α lt n) → (right : BinaryHeap α lt m) → m ≤ n → BinaryHeap α lt (n+m+1) + | branch : (val : α) → (left : BinaryHeap α lt n) → (right : BinaryHeap α lt m) → m ≤ n → (n+1).isPowerOfTwo ∨ (m+1).isPowerOfTwo → BinaryHeap α lt (n+m+1) /--Please do not use this for anything meaningful. It's a debug function, with horrible performance.-/ instance {α : Type u} {lt : α → α → Bool} [ToString α] : ToString (BinaryHeap α lt n) where @@ -11,13 +11,13 @@ instance {α : Type u} {lt : α → α → Bool} [ToString α] : ToString (Binar --not very fast, doesn't matter, is for debugging let rec max_width := λ {m : Nat} (t : (BinaryHeap α lt m)) ↦ match m, t with | 0, .leaf => 0 - | (_+_+1), BinaryHeap.branch a left right _ => max (ToString.toString a).length $ max (max_width left) (max_width right) + | (_+_+1), BinaryHeap.branch a left right _ _ => max (ToString.toString a).length $ max (max_width left) (max_width right) let max_width := max_width t let lines_left := Nat.log2 (n+1).nextPowerOfTwo let rec print_line := λ (mw : Nat) {m : Nat} (t : (BinaryHeap α lt m)) (lines : Nat) ↦ match m, t with | 0, _ => "" - | (_+_+1), BinaryHeap.branch a left right _ => + | (_+_+1), BinaryHeap.branch a left right _ _ => let thisElem := ToString.toString a let thisElem := (List.replicate (mw - thisElem.length) ' ').asString ++ thisElem let elems_in_last_line := if lines == 0 then 0 else 2^(lines-1) @@ -39,27 +39,109 @@ def BinaryHeap.length : BinaryHeap α lt n → Nat := λ_ ↦ n /--Creates an empty BinaryHeap. Needs the heap predicate as parameter.-/ abbrev BinaryHeap.empty {α : Type u} (lt : α → α → Bool ) := BinaryHeap.leaf (α := α) (lt := lt) +private theorem eq_power_of_two_power_of_two (n : Nat) : (n.nextPowerOfTwo = n) → n.isPowerOfTwo := by + have h₂ := Nat.isPowerOfTwo_nextPowerOfTwo n + intro h₁ + revert h₂ + rewrite[h₁] + intro + assumption + +private theorem power_of_two_go_eq_eq (n : Nat) (p : n >0) : Nat.nextPowerOfTwo.go n n p = n := by + unfold Nat.nextPowerOfTwo.go + simp_arith + +private theorem smaller_smaller_exp {n m : Nat} (p : 2 ^ n < 2 ^ m) : n < m := + if h₁ : m ≤ n then + by have h₂ := Nat.pow_le_pow_of_le_right (by decide : 2 > 0) h₁ + have h₃ := Nat.lt_of_le_of_lt h₂ p + simp_arith at h₃ + else + by rewrite[Nat.not_ge_eq] at h₁ + trivial + + + +private theorem mul2_isPowerOfTwo_smaller_smaller_equal (n : Nat) (power : Nat) (h₁ : n.isPowerOfTwo) (h₂ : power.isPowerOfTwo) (h₃ : power < n) : power * 2 ≤ n := by + unfold Nat.isPowerOfTwo at h₁ h₂ + have ⟨k, h₄⟩ := h₁ + have ⟨l, h₅⟩ := h₂ + rewrite [h₅] + rewrite[←Nat.pow_succ 2 l] + rewrite[h₄] + have h₆ : 2 > 0 := by decide + apply (Nat.pow_le_pow_of_le_right h₆) + rewrite [h₅] at h₃ + rewrite [h₄] at h₃ + have h₃ := smaller_smaller_exp h₃ + simp_arith at h₃ + assumption + + +private theorem power_of_two_go_one_eq (n : Nat) (power : Nat) (h₁ : n.isPowerOfTwo) (h₂ : power.isPowerOfTwo) (h₃ : power ≤ n) : Nat.nextPowerOfTwo.go n power (Nat.pos_of_isPowerOfTwo h₂) = n := by + unfold Nat.nextPowerOfTwo.go + split + case inl h₄ => exact power_of_two_go_one_eq n (power*2) (h₁) (Nat.mul2_isPowerOfTwo_of_isPowerOfTwo h₂) (mul2_isPowerOfTwo_smaller_smaller_equal n power h₁ h₂ h₄) + case inr h₄ => rewrite[Nat.not_lt_eq power n] at h₄ + exact Nat.le_antisymm h₃ h₄ +termination_by power_of_two_go_one_eq _ p _ _ _ => n - p +decreasing_by + simp_wf + have := Nat.pos_of_isPowerOfTwo h₂ + apply Nat.nextPowerOfTwo_dec <;> assumption + +private theorem power_of_two_eq_power_of_two (n : Nat) : n.isPowerOfTwo → (n.nextPowerOfTwo = n) := by + intro h₁ + unfold Nat.nextPowerOfTwo + apply power_of_two_go_one_eq + case h₁ => assumption + case h₂ => exact Nat.one_isPowerOfTwo + case h₃ => exact (Nat.pos_of_isPowerOfTwo h₁) + +private theorem power_of_two_iff_next_power_eq (n : Nat) : n.isPowerOfTwo ↔ (n.nextPowerOfTwo = n) := + Iff.intro (power_of_two_eq_power_of_two n) (eq_power_of_two_power_of_two n) + /--Adds a new element to a given BinaryHeap.-/ def BinaryHeap.insert (elem : α) (heap : BinaryHeap α lt o) : BinaryHeap α lt (o+1) := match o, heap with - | 0, .leaf => BinaryHeap.branch elem (BinaryHeap.leaf) (BinaryHeap.leaf) (by simp) - | (n+m+1), .branch a left right p => + | 0, .leaf => BinaryHeap.branch elem (BinaryHeap.leaf) (BinaryHeap.leaf) (by simp) (by simp[Nat.one_isPowerOfTwo]) + | (n+m+1), .branch a left right p subtree_complete => let (elem, a) := if lt elem a then (a, elem) else (elem, a) -- okay, based on n and m we know if we want to add left or right. -- the left tree is full, if (n+1) is a power of two AND n != m - let leftIsFull : Bool := (n+1).nextPowerOfTwo = n+1 + let leftIsFull := (n+1).nextPowerOfTwo = n+1 if r : m < n ∧ leftIsFull then have s : (m + 1 < n + 1) = (m < n) := by simp_arith have q : m + 1 ≤ n := by apply Nat.le_of_lt_succ rewrite[Nat.succ_eq_add_one] rewrite[s] simp[r] - let result := branch a left (right.insert elem) (q) + let result := branch a left (right.insert elem) (q) (by simp[(eq_power_of_two_power_of_two (n+1)), r]) result else have q : m ≤ n+1 := by apply (Nat.le_of_succ_le) simp_arith[p] - let result := branch a (left.insert elem) right q + have right_is_power_of_two : (m+1).isPowerOfTwo := + if s : n = m then by + rewrite[s] at subtree_complete + simp at subtree_complete + exact subtree_complete + else if h₁ : leftIsFull then by + simp at h₁ + rewrite[Decidable.not_and_iff_or_not (m<n) leftIsFull] at r + cases r + case inl h₂ => rewrite[Nat.not_lt_eq] at h₂ + have h₃ := Nat.not_le_of_gt $ Nat.lt_of_le_of_ne h₂ s + contradiction + case inr h₂ => simp at h₂ + contradiction + else by + simp at h₁ + rewrite[←power_of_two_iff_next_power_eq] at h₁ + cases subtree_complete + case inl => contradiction + case inr => trivial + let result := branch a (left.insert elem) right q (Or.inr right_is_power_of_two) have letMeSpellItOutForYou : n + 1 + m + 1 = n + m + 1 + 1 := by simp_arith letMeSpellItOutForYou ▸ result @@ -68,7 +150,7 @@ def BinaryHeap.insert (elem : α) (heap : BinaryHeap α lt o) : BinaryHeap α lt def BinaryHeap.indexOfAux {α : Type u} {lt : α → α → Bool} [BEq α] (elem : α) (heap : BinaryHeap α lt o) (currentIndex : Nat) : Option (Fin (o+currentIndex)) := match o, heap with | 0, .leaf => none - | (n+m+1), .branch a left right _ => + | (n+m+1), .branch a left right _ _ => if a == elem then let result := Fin.ofNat' currentIndex (by simp_arith) some result @@ -97,7 +179,7 @@ theorem two_n_not_zero_n_not_zero (n : Nat) (p : ¬2*n = 0) : (¬n = 0) := by def BinaryHeap.popLast {α : Type u} {lt : α → α → Bool} (heap : BinaryHeap α lt (o+1)) : (α × BinaryHeap α lt o) := match o, heap with - | (n+m), .branch a (left : BinaryHeap α lt n) (right : BinaryHeap α lt m) m_le_n => + | (n+m), .branch a (left : BinaryHeap α lt n) (right : BinaryHeap α lt m) m_le_n subtree_complete => if p : 0 = (n+m) then (a, p▸BinaryHeap.leaf) else @@ -113,7 +195,11 @@ def BinaryHeap.popLast {α : Type u} {lt : α → α → Bool} (heap : BinaryHea have s : m ≤ l := match r with | .intro a _ => by apply Nat.le_of_lt_succ simp[a] - (res, q▸BinaryHeap.branch a newLeft right s) + have rightIsFull : (m+1).isPowerOfTwo := by + have r := And.right r + simp[←power_of_two_iff_next_power_eq] at r + assumption + (res, q▸BinaryHeap.branch a newLeft right s (Or.inr rightIsFull)) else --remove right have : m > 0 := by @@ -134,13 +220,27 @@ def BinaryHeap.popLast {α : Type u} {lt : α → α → Bool} (heap : BinaryHea have g := Eq.symm g revert g assumption - match m, right with + match h₂ : m, right with | (l+1), right => let (res, (newRight : BinaryHeap α lt l)) := right.popLast have s : l ≤ n := by have x := (Nat.add_le_add_left (Nat.zero_le 1) l) have x := Nat.le_trans x m_le_n assumption - (res, BinaryHeap.branch a left newRight s) + have leftIsFull : (n+1).isPowerOfTwo := by + rewrite[Decidable.not_and_iff_or_not] at r + cases r + case inl h₁ => rewrite[Nat.not_lt_eq] at h₁ + have h₂ := Nat.le_antisymm h₁ m_le_n + rewrite[←h₂] at subtree_complete + simp at subtree_complete + assumption + case inr h₁ => simp at h₁ + rewrite[←power_of_two_iff_next_power_eq] at h₁ + subst m + cases subtree_complete + case inl => assumption + case inr => contradiction + (res, BinaryHeap.branch a left newRight s (Or.inl leftIsFull)) /--Removes the element at a given index. Use `BinaryHeap.indexOf` to find the respective index.-/ def BinaryHeap.removeAt {α : Type u} {lt : α → α → Bool} {o : Nat} (index : Fin (o+1)) (heap : BinaryHeap α lt (o+1)) : BinaryHeap α lt o := |