diff options
Diffstat (limited to 'Common')
| -rw-r--r-- | Common/BinaryHeap.lean | 56 |
1 files changed, 28 insertions, 28 deletions
diff --git a/Common/BinaryHeap.lean b/Common/BinaryHeap.lean index 16a1933..4cbc802 100644 --- a/Common/BinaryHeap.lean +++ b/Common/BinaryHeap.lean @@ -431,7 +431,7 @@ def CompleteTree.indexOfLast {α : Type u} (heap : CompleteTree α (o+1)) : Fin | .succ mm => ⟨r.indexOfLast.val + 1 + n, by omega⟩ -/-- Helper for removeLast -/ +/-- Helper for heapRemoveLast -/ private theorem CompleteTree.removeRightRightNotEmpty {n m : Nat} (m_gt_0_or_rightIsFull : m > 0 ∨ ((m+1).nextPowerOfTwo = m+1 : Bool)) (h₁ : 0 ≠ n + m) (h₂ : ¬(m < n ∧ ((m+1).nextPowerOfTwo = m+1 : Bool))) : m > 0 := match m_gt_0_or_rightIsFull with | Or.inl h => h @@ -444,7 +444,7 @@ private theorem CompleteTree.removeRightRightNotEmpty {n m : Nat} (m_gt_0_or_rig . exact absurd h₂ $ Nat.not_succ_le_zero q . exact Nat.succ_pos _ -/-- Helper for removeLast -/ +/-- Helper for heapRemoveLast -/ private theorem CompleteTree.removeRightLeftIsFull {n m : Nat} (r : ¬(m < n ∧ ((m+1).nextPowerOfTwo = m+1 : Bool))) (m_le_n : m ≤ n) (subtree_complete : (n + 1).isPowerOfTwo ∨ (m + 1).isPowerOfTwo) : (n+1).isPowerOfTwo := by rewrite[Decidable.not_and_iff_or_not] at r cases r @@ -457,7 +457,7 @@ private theorem CompleteTree.removeRightLeftIsFull {n m : Nat} (r : ¬(m < n ∧ simp[h₁] at subtree_complete assumption -/-- Helper for removeLast-/ +/-- Helper for heapRemoveLast-/ private theorem CompleteTree.stillInRange {n m : Nat} (r : ¬(m < n ∧ ((m+1).nextPowerOfTwo = m+1 : Bool))) (m_le_n : m ≤ n) (m_gt_0 : m > 0) (leftIsFull : (n+1).isPowerOfTwo) (max_height_difference: n < 2 * (m + 1)) : n < 2*m := by rewrite[Decidable.not_and_iff_or_not] at r cases r with @@ -467,7 +467,7 @@ private theorem CompleteTree.stillInRange {n m : Nat} (r : ¬(m < n ∧ ((m+1).n | inr h₁ => simp (config := { zetaDelta := true }) only [← Nat.power_of_two_iff_next_power_eq, decide_eq_true_eq] at h₁ apply power_of_two_mul_two_le <;> assumption -private def CompleteTree.removeLast {α : Type u} (heap : CompleteTree α (o+1)) : (CompleteTree α o × α) := +private def CompleteTree.heapRemoveLast {α : Type u} (heap : CompleteTree α (o+1)) : (CompleteTree α o × α) := match o, heap with | (n+m), .branch a (left : CompleteTree α n) (right : CompleteTree α m) m_le_n max_height_difference subtree_complete => if p : 0 = (n+m) then @@ -479,7 +479,7 @@ private def CompleteTree.removeLast {α : Type u} (heap : CompleteTree α (o+1)) --remove left match n, left with | (l+1), left => - let ((newLeft : CompleteTree α l), res) := left.removeLast + let ((newLeft : CompleteTree α l), res) := left.heapRemoveLast have q : l + m + 1 = l + 1 + m := Nat.add_right_comm l m 1 have s : m ≤ l := Nat.le_of_lt_succ r.left have rightIsFull : (m+1).isPowerOfTwo := (Nat.power_of_two_iff_next_power_eq (m+1)).mpr $ decide_eq_true_eq.mp r.right @@ -490,7 +490,7 @@ private def CompleteTree.removeLast {α : Type u} (heap : CompleteTree α (o+1)) have m_gt_0 : m > 0 := removeRightRightNotEmpty m_gt_0_or_rightIsFull p r let l := m.pred have h₂ : l.succ = m := (Nat.succ_pred $ Nat.not_eq_zero_of_lt (Nat.gt_of_not_le $ Nat.not_le_of_gt m_gt_0)) - let ((newRight : CompleteTree α l), res) := (h₂.symm▸right).removeLast + let ((newRight : CompleteTree α l), res) := (h₂.symm▸right).heapRemoveLast have leftIsFull : (n+1).isPowerOfTwo := removeRightLeftIsFull r m_le_n subtree_complete have still_in_range : n < 2 * (l+1) := h₂.substr (p := λx ↦ n < 2 * x) $ stillInRange r m_le_n m_gt_0 leftIsFull max_height_difference (h₂▸CompleteTree.branch a left newRight (Nat.le_of_succ_le (h₂▸m_le_n)) still_in_range (Or.inl leftIsFull), res) @@ -530,14 +530,14 @@ private theorem HeapPredicate.seesThroughCast2 assumption -- If there is only one element left, the result is a leaf. -private theorem CompleteTree.removeLastLeaf (heap : CompleteTree α 1) : heap.removeLast.fst = CompleteTree.leaf := by - let l := heap.removeLast.fst +private theorem CompleteTree.heapRemoveLastLeaf (heap : CompleteTree α 1) : heap.heapRemoveLast.fst = CompleteTree.leaf := by + let l := heap.heapRemoveLast.fst have h₁ : l = CompleteTree.leaf := match l with | .leaf => rfl exact h₁ -private theorem CompleteTree.removeLastLeavesRoot (heap : CompleteTree α (n+1)) (h₁ : n > 0) : heap.root (Nat.zero_lt_of_ne_zero $ Nat.succ_ne_zero n) = heap.removeLast.fst.root (h₁) := by - unfold removeLast +private theorem CompleteTree.heapRemoveLastLeavesRoot (heap : CompleteTree α (n+1)) (h₁ : n > 0) : heap.root (Nat.zero_lt_of_ne_zero $ Nat.succ_ne_zero n) = heap.heapRemoveLast.fst.root (h₁) := by + unfold heapRemoveLast split rename_i o p v l r _ _ _ have h₃ : (0 ≠ o + p) := Ne.symm $ Nat.not_eq_zero_of_lt h₁ @@ -561,8 +561,8 @@ private theorem CompleteTree.removeLastLeavesRoot (heap : CompleteTree α (n+1)) simp_arith apply root_unfold -private theorem CompleteTree.removeLastIsHeap {heap : CompleteTree α (o+1)} {le : α → α → Bool} (h₁ : HeapPredicate heap le) (h₂ : transitive_le le) (h₃ : total_le le) : HeapPredicate (heap.removeLast.fst) le := by - unfold removeLast +private theorem CompleteTree.heapRemoveLastIsHeap {heap : CompleteTree α (o+1)} {le : α → α → Bool} (h₁ : HeapPredicate heap le) (h₂ : transitive_le le) (h₃ : total_le le) : HeapPredicate (heap.heapRemoveLast.fst) le := by + unfold heapRemoveLast split rename_i n m v l r _ _ _ exact @@ -580,19 +580,19 @@ private theorem CompleteTree.removeLastIsHeap {heap : CompleteTree α (o+1)} {le simp apply HeapPredicate.seesThroughCast2 <;> try simp_arith cases ll - case a.zero => -- if ll is zero, then (removeLast l).snd is a leaf. - have h₆ : l.removeLast.fst = .leaf := removeLastLeaf l + case a.zero => -- if ll is zero, then (heapRemoveLast l).snd is a leaf. + have h₆ : l.heapRemoveLast.fst = .leaf := heapRemoveLastLeaf l rw[h₆] unfold HeapPredicate at * have h₇ : HeapPredicate .leaf le := by trivial have h₈ : HeapPredicate.leOrLeaf le v .leaf := by trivial exact ⟨h₇,h₁.right.left, h₈, h₁.right.right.right⟩ - case a.succ nn => -- if ll is not zero, then the root element before and after removeLast is the same. + case a.succ nn => -- if ll is not zero, then the root element before and after heapRemoveLast is the same. unfold HeapPredicate at * - simp[h₁.right.left, h₁.right.right.right, removeLastIsHeap h₁.left h₂ h₃] + simp[h₁.right.left, h₁.right.right.right, heapRemoveLastIsHeap h₁.left h₂ h₃] unfold HeapPredicate.leOrLeaf simp - rw[←removeLastLeavesRoot] + rw[←heapRemoveLastLeavesRoot] exact h₁.right.right.left else by simp[h₅] @@ -603,20 +603,20 @@ private theorem CompleteTree.removeLastIsHeap {heap : CompleteTree α (o+1)} {le case succ mm h₆ h₇ h₈ => simp unfold HeapPredicate at * - simp[h₁, removeLastIsHeap h₁.right.left h₂ h₃] + simp[h₁, heapRemoveLastIsHeap h₁.right.left h₂ h₃] unfold HeapPredicate.leOrLeaf exact match mm with | 0 => rfl | o+1 => - have h₉ : le v ((r.removeLast).fst.root (Nat.zero_lt_succ o)) := by - rw[←removeLastLeavesRoot] + have h₉ : le v ((r.heapRemoveLast).fst.root (Nat.zero_lt_succ o)) := by + rw[←heapRemoveLastLeavesRoot] exact h₁.right.right.right h₉ -private def BinaryHeap.removeLast {α : Type u} {le : α → α → Bool} {n : Nat} : (BinaryHeap α le (n+1)) → BinaryHeap α le n × α +private def BinaryHeap.heapRemoveLast {α : Type u} {le : α → α → Bool} {n : Nat} : (BinaryHeap α le (n+1)) → BinaryHeap α le n × α | {tree, valid, wellDefinedLe} => - let result := tree.removeLast - let resultValid := CompleteTree.removeLastIsHeap valid wellDefinedLe.left wellDefinedLe.right + let result := tree.heapRemoveLast + let resultValid := CompleteTree.heapRemoveLastIsHeap valid wellDefinedLe.left wellDefinedLe.right ({ tree := result.fst, valid := resultValid, wellDefinedLe}, result.snd) /-- @@ -1037,14 +1037,14 @@ theorem CompleteTree.heapUpdateAtIsHeap {α : Type u} {n : Nat} (le : α → α exact h₁₀ def CompleteTree.heapPop {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α (n+1)) : CompleteTree α n × α := - let l := heap.removeLast + let l := heap.heapRemoveLast if p : n > 0 then heapUpdateRoot le l.snd l.fst p else l theorem CompleteTree.heapPopIsHeap {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α (n+1)) (h₁ : HeapPredicate heap le) (wellDefinedLe : transitive_le le ∧ total_le le) : HeapPredicate (heap.heapPop le).fst le := by - have h₂ : HeapPredicate heap.removeLast.fst le := removeLastIsHeap h₁ wellDefinedLe.left wellDefinedLe.right + have h₂ : HeapPredicate heap.heapRemoveLast.fst le := heapRemoveLastIsHeap h₁ wellDefinedLe.left wellDefinedLe.right unfold heapPop cases n <;> simp[h₂, heapUpdateRootIsHeap, wellDefinedLe] @@ -1064,7 +1064,7 @@ def CompleteTree.heapRemoveAt {α : Type u} {n : Nat} (le : α → α → Bool) heapPop le heap else let lastIndex := heap.indexOfLast - let l := heap.removeLast + let l := heap.heapRemoveLast if p : index = lastIndex then l else @@ -1081,7 +1081,7 @@ def CompleteTree.heapRemoveAt {α : Type u} {n : Nat} (le : α → α → Bool) heapUpdateAt le index l.snd l.fst n_gt_zero theorem CompleteTree.heapRemoveAtIsHeap {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin (n+1)) (heap : CompleteTree α (n+1)) (h₁ : HeapPredicate heap le) (wellDefinedLe : transitive_le le ∧ total_le le) : HeapPredicate (heap.heapRemoveAt le index).fst le := by - have h₂ : HeapPredicate heap.removeLast.fst le := removeLastIsHeap h₁ wellDefinedLe.left wellDefinedLe.right + have h₂ : HeapPredicate heap.heapRemoveLast.fst le := heapRemoveLastIsHeap h₁ wellDefinedLe.left wellDefinedLe.right unfold heapRemoveAt split case isTrue => exact heapPopIsHeap le heap h₁ wellDefinedLe @@ -1120,7 +1120,7 @@ private def TestHeap := |> ins 3 #eval TestHeap -#eval TestHeap.removeLast +#eval TestHeap.heapRemoveLast #eval TestHeap.indexOf (13 = ·) #eval TestHeap.heapRemoveAt (.≤.) 7 |