From 4d67d2e1597d1ed976fb4d1eb0062171925a45cb Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Fri, 19 Jul 2024 17:03:45 +0200 Subject: Make CompleteTree.heapRemoveLast private. It's confusing, because it uses breadth-first indexing, and regular indices are depth-first. Also, it's not needed in the public API, as there is the removeAt function that can do the same. --- Common/BinaryHeap.lean | 78 ++++++++++++++++++++++++-------------------------- 1 file changed, 38 insertions(+), 40 deletions(-) diff --git a/Common/BinaryHeap.lean b/Common/BinaryHeap.lean index e54dfaa..16a1933 100644 --- a/Common/BinaryHeap.lean +++ b/Common/BinaryHeap.lean @@ -159,7 +159,7 @@ private theorem power_of_two_mul_two_le {n m : Nat} (h₁ : (n+1).isPowerOfTwo) assumption /--Adds a new element to a given CompleteTree.-/ -def CompleteTree.heapInsert (le : α → α → Bool) (elem : α) (heap : CompleteTree α o) : CompleteTree α (o+1) := +def CompleteTree.heapPush (le : α → α → Bool) (elem : α) (heap : CompleteTree α o) : CompleteTree α (o+1) := match o, heap with | 0, .leaf => CompleteTree.branch elem (CompleteTree.leaf) (CompleteTree.leaf) (by simp) (by simp) (by simp[Nat.one_isPowerOfTwo]) | (n+m+1), .branch a left right p max_height_difference subtree_complete => @@ -174,7 +174,7 @@ def CompleteTree.heapInsert (le : α → α → Bool) (elem : α) (heap : Comple rewrite[s] simp[r] have difference_decreased := Nat.le_succ_of_le $ Nat.le_succ_of_le max_height_difference - let result := branch a left (right.heapInsert le elem) (q) difference_decreased (by simp[(Nat.power_of_two_iff_next_power_eq (n+1)), r]) + let result := branch a left (right.heapPush le elem) (q) difference_decreased (by simp[(Nat.power_of_two_iff_next_power_eq (n+1)), r]) result else have q : m ≤ n+1 := by apply (Nat.le_of_succ_le) @@ -206,7 +206,7 @@ def CompleteTree.heapInsert (le : α → α → Bool) (elem : α) (heap : Comple case inr h₁ => simp[←Nat.power_of_two_iff_next_power_eq, leftIsFull] at h₁ simp[h₁] at subtree_complete exact power_of_two_mul_two_lt subtree_complete max_height_difference h₁ - let result := branch a (left.heapInsert le elem) right q still_in_range (Or.inr right_is_power_of_two) + let result := branch a (left.heapPush le elem) right q still_in_range (Or.inr right_is_power_of_two) have letMeSpellItOutForYou : n + 1 + m + 1 = n + m + 1 + 1 := by simp_arith letMeSpellItOutForYou ▸ result @@ -243,8 +243,8 @@ private theorem CompleteTree.rootSeesThroughCast2 revert heap h₁ h₂ h₃ assumption -theorem CompleteTree.heapInsertRootSameOrElem (elem : α) (heap : CompleteTree α o) (lt : α → α → Bool) (h₂ : 0 < o): (CompleteTree.root (heap.heapInsert lt elem) (Nat.succ_pos o) = elem) ∨ (CompleteTree.root (heap.heapInsert lt elem) (Nat.succ_pos o) = CompleteTree.root heap h₂) := by - unfold heapInsert +theorem CompleteTree.heapPushRootSameOrElem (elem : α) (heap : CompleteTree α o) (lt : α → α → Bool) (h₂ : 0 < o): (CompleteTree.root (heap.heapPush lt elem) (Nat.succ_pos o) = elem) ∨ (CompleteTree.root (heap.heapPush lt elem) (Nat.succ_pos o) = CompleteTree.root heap h₂) := by + unfold heapPush split --match o, heap contradiction simp @@ -257,10 +257,10 @@ theorem CompleteTree.heapInsertRootSameOrElem (elem : α) (heap : CompleteTree cases (lt elem v) <;> simp[instDecidableEqBool, Bool.decEq, CompleteTree.root] -theorem CompleteTree.heapInsertEmptyElem (elem : α) (heap : CompleteTree α o) (lt : α → α → Bool) (h₂ : ¬0 < o) : (CompleteTree.root (heap.heapInsert lt elem) (Nat.succ_pos o) = elem) := +theorem CompleteTree.heapPushEmptyElem (elem : α) (heap : CompleteTree α o) (lt : α → α → Bool) (h₂ : ¬0 < o) : (CompleteTree.root (heap.heapPush lt elem) (Nat.succ_pos o) = elem) := have : o = 0 := Nat.eq_zero_of_le_zero $ (Nat.not_lt_eq 0 o).mp h₂ match o, heap with - | 0, .leaf => by simp[CompleteTree.heapInsert, root] + | 0, .leaf => by simp[CompleteTree.heapPush, root] theorem HeapPredicate.leOrLeaf_transitive (h₁ : transitive_le le) : le a b → HeapPredicate.leOrLeaf le b h → HeapPredicate.leOrLeaf le a h := by @@ -293,60 +293,60 @@ private theorem HeapPredicate.seesThroughCast mutual /-- - Helper for CompleteTree.heapInsertIsHeap, to make one function out of both branches. + Helper for CompleteTree.heapPushIsHeap, to make one function out of both branches. Sorry for the ugly signature, but this was the easiest thing to extract. -/ -private theorem CompleteTree.heapInsertIsHeapAux {α : Type u} (le : α → α → Bool) (n m : Nat) (v elem : α) (l : CompleteTree α n) (r : CompleteTree α m) (h₁ : HeapPredicate l le ∧ HeapPredicate r le ∧ HeapPredicate.leOrLeaf le v l ∧ HeapPredicate.leOrLeaf le v r) (h₂ : transitive_le le) (h₃ : total_le le): HeapPredicate l le ∧ +private theorem CompleteTree.heapPushIsHeapAux {α : Type u} (le : α → α → Bool) (n m : Nat) (v elem : α) (l : CompleteTree α n) (r : CompleteTree α m) (h₁ : HeapPredicate l le ∧ HeapPredicate r le ∧ HeapPredicate.leOrLeaf le v l ∧ HeapPredicate.leOrLeaf le v r) (h₂ : transitive_le le) (h₃ : total_le le): HeapPredicate l le ∧ let smaller := (if le elem v then elem else v) let larger := (if le elem v then v else elem) - HeapPredicate (heapInsert le larger r) le + HeapPredicate (heapPush le larger r) le ∧ HeapPredicate.leOrLeaf le smaller l - ∧ HeapPredicate.leOrLeaf le smaller (heapInsert le larger r) + ∧ HeapPredicate.leOrLeaf le smaller (heapPush le larger r) := by cases h₆ : (le elem v) <;> simp only [Bool.false_eq_true, reduceIte] case true => - have h₇ : (HeapPredicate (CompleteTree.heapInsert le v r) le) := CompleteTree.heapInsertIsHeap h₁.right.left h₂ h₃ + have h₇ : (HeapPredicate (CompleteTree.heapPush le v r) le) := CompleteTree.heapPushIsHeap h₁.right.left h₂ h₃ simp only [true_and, h₁, h₇, HeapPredicate.leOrLeaf_transitive h₂ h₆ h₁.right.right.left] cases m case zero => - have h₈ := heapInsertEmptyElem v r le (Nat.not_lt_zero 0) + have h₈ := heapPushEmptyElem v r le (Nat.not_lt_zero 0) simp only [HeapPredicate.leOrLeaf, Nat.succ_eq_add_one, Nat.reduceAdd, h₈] assumption case succ _ => simp only [HeapPredicate.leOrLeaf] - cases heapInsertRootSameOrElem v r le (Nat.succ_pos _) + cases heapPushRootSameOrElem v r le (Nat.succ_pos _) <;> rename_i h₇ <;> rw[h₇] . assumption apply h₂ elem v exact ⟨h₆, h₁.right.right.right⟩ case false => - have h₇ : (HeapPredicate (CompleteTree.heapInsert le elem r) le) := CompleteTree.heapInsertIsHeap h₁.right.left h₂ h₃ + have h₇ : (HeapPredicate (CompleteTree.heapPush le elem r) le) := CompleteTree.heapPushIsHeap h₁.right.left h₂ h₃ simp only [true_and, h₁, h₇] have h₈ : le v elem := not_le_imp_le h₃ elem v (by simp only [h₆, Bool.false_eq_true, not_false_eq_true]) cases m case zero => - have h₇ := heapInsertEmptyElem elem r le (Nat.not_lt_zero 0) + have h₇ := heapPushEmptyElem elem r le (Nat.not_lt_zero 0) simp only [HeapPredicate.leOrLeaf, Nat.succ_eq_add_one, Nat.reduceAdd, h₇] assumption case succ _ => - cases heapInsertRootSameOrElem elem r le (Nat.succ_pos _) + cases heapPushRootSameOrElem elem r le (Nat.succ_pos _) <;> rename_i h₉ <;> simp only [HeapPredicate.leOrLeaf, Nat.succ_eq_add_one, h₈, h₉] exact h₁.right.right.right -theorem CompleteTree.heapInsertIsHeap {α : Type u} {elem : α} {heap : CompleteTree α o} {le : α → α → Bool} (h₁ : HeapPredicate heap le) (h₂ : transitive_le le) (h₃ : total_le le) : HeapPredicate (heap.heapInsert le elem) le := by - unfold heapInsert +theorem CompleteTree.heapPushIsHeap {α : Type u} {elem : α} {heap : CompleteTree α o} {le : α → α → Bool} (h₁ : HeapPredicate heap le) (h₂ : transitive_le le) (h₃ : total_le le) : HeapPredicate (heap.heapPush le elem) le := by + unfold heapPush split -- match o, heap with trivial case h_2 n m v l r m_le_n _ _ => simp split -- if h₅ : m < n ∧ Nat.nextPowerOfTwo (n + 1) = n + 1 then case' isTrue => - have h := heapInsertIsHeapAux le n m v elem l r h₁ h₂ h₃ + have h := heapPushIsHeapAux le n m v elem l r h₁ h₂ h₃ case' isFalse => apply HeapPredicate.seesThroughCast <;> try simp_arith[h₂] --gets rid of annoying cast. - have h := heapInsertIsHeapAux le m n v elem r l (And.intro h₁.right.left $ And.intro h₁.left $ And.intro h₁.right.right.right h₁.right.right.left) h₂ h₃ + have h := heapPushIsHeapAux le m n v elem r l (And.intro h₁.right.left $ And.intro h₁.left $ And.intro h₁.right.right.right h₁.right.right.left) h₂ h₃ all_goals unfold HeapPredicate cases h₆ : (le elem v) @@ -356,8 +356,8 @@ end def BinaryHeap.insert {α : Type u} {lt : α → α → Bool} {n : Nat} : α → BinaryHeap α lt n → BinaryHeap α lt (n+1) | elem, BinaryHeap.mk tree valid wellDefinedLe => - let valid := tree.heapInsertIsHeap valid wellDefinedLe.left wellDefinedLe.right - let tree := tree.heapInsert lt elem + let valid := tree.heapPushIsHeap valid wellDefinedLe.left wellDefinedLe.right + let tree := tree.heapPush lt elem {tree, valid, wellDefinedLe} /--Helper function for CompleteTree.indexOf.-/ @@ -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 -def CompleteTree.removeLast {α : Type u} (heap : CompleteTree α (o+1)) : (CompleteTree α o × α) := +private def CompleteTree.removeLast {α : 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 @@ -495,7 +495,7 @@ def CompleteTree.removeLast {α : Type u} (heap : CompleteTree α (o+1)) : (Comp 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) -theorem CompleteTree.castZeroHeap (n m : Nat) (heap : CompleteTree α 0) (h₁ : 0=n+m) {le : α → α → Bool} : HeapPredicate (h₁ ▸ heap) le := by +private theorem CompleteTree.castZeroHeap (n m : Nat) (heap : CompleteTree α 0) (h₁ : 0=n+m) {le : α → α → Bool} : HeapPredicate (h₁ ▸ heap) le := by have h₂ : heap = (CompleteTree.empty : CompleteTree α 0) := by simp[empty] match heap with @@ -530,13 +530,13 @@ private theorem HeapPredicate.seesThroughCast2 assumption -- If there is only one element left, the result is a leaf. -theorem CompleteTree.removeLastLeaf (heap : CompleteTree α 1) : heap.removeLast.fst = CompleteTree.leaf := by +private theorem CompleteTree.removeLastLeaf (heap : CompleteTree α 1) : heap.removeLast.fst = CompleteTree.leaf := by let l := heap.removeLast.fst have h₁ : l = CompleteTree.leaf := match l with | .leaf => rfl exact h₁ -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 +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 split rename_i o p v l r _ _ _ @@ -561,9 +561,7 @@ theorem CompleteTree.removeLastLeavesRoot (heap : CompleteTree α (n+1)) (h₁ : simp_arith apply root_unfold - -set_option linter.unusedVariables false in -- Lean 4.2 thinks h₁ is unused. It very much is not unused. -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 +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 split rename_i n m v l r _ _ _ @@ -615,7 +613,7 @@ theorem CompleteTree.removeLastIsHeap {heap : CompleteTree α (o+1)} {le : α exact h₁.right.right.right h₉ -def BinaryHeap.removeLast {α : Type u} {le : α → α → Bool} {n : Nat} : (BinaryHeap α le (n+1)) → BinaryHeap α le n × α +private def BinaryHeap.removeLast {α : 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 @@ -1038,22 +1036,22 @@ theorem CompleteTree.heapUpdateAtIsHeap {α : Type u} {n : Nat} (le : α → α apply HeapPredicate.leOrLeaf_transitive h₃ _ h₁₃ exact h₁₀ -def CompleteTree.heapRemoveRoot {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α (n+1)) : CompleteTree α n × α := +def CompleteTree.heapPop {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α (n+1)) : CompleteTree α n × α := let l := heap.removeLast if p : n > 0 then heapUpdateRoot le l.snd l.fst p else l -theorem CompleteTree.heapRemoveRootIsHeap {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α (n+1)) (h₁ : HeapPredicate heap le) (wellDefinedLe : transitive_le le ∧ total_le le) : HeapPredicate (heap.heapRemoveRoot le).fst le := by +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 - unfold heapRemoveRoot + unfold heapPop cases n <;> simp[h₂, heapUpdateRootIsHeap, wellDefinedLe] def BinaryHeap.RemoveRoot {α : Type u} {le : α → α → Bool} {n : Nat} : (BinaryHeap α le (n+1)) → (BinaryHeap α le n × α) | {tree, valid, wellDefinedLe} => - let result := tree.heapRemoveRoot le - let resultValid := CompleteTree.heapRemoveRootIsHeap le tree valid wellDefinedLe + let result := tree.heapPop le + let resultValid := CompleteTree.heapPopIsHeap le tree valid wellDefinedLe ({ tree := result.fst, valid := resultValid, wellDefinedLe}, result.snd) /--Removes the element at a given index. Use `CompleteTree.indexOf` to find the respective index.-/ @@ -1063,7 +1061,7 @@ def CompleteTree.heapRemoveAt {α : Type u} {n : Nat} (le : α → α → Bool) --indices are depth first, but "last" means last element of the complete tree. --sooo: if index_ne_zero : index = 0 then - heapRemoveRoot le heap + heapPop le heap else let lastIndex := heap.indexOfLast let l := heap.removeLast @@ -1086,7 +1084,7 @@ theorem CompleteTree.heapRemoveAtIsHeap {α : Type u} {n : Nat} (le : α → α have h₂ : HeapPredicate heap.removeLast.fst le := removeLastIsHeap h₁ wellDefinedLe.left wellDefinedLe.right unfold heapRemoveAt split - case isTrue => exact heapRemoveRootIsHeap le heap h₁ wellDefinedLe + case isTrue => exact heapPopIsHeap le heap h₁ wellDefinedLe case isFalse h₃ => cases h: (index = heap.indexOfLast : Bool) <;> simp_all @@ -1102,7 +1100,7 @@ def BinaryHeap.RemoveAt {α : Type u} {le : α → α → Bool} {n : Nat} : (Bin ------------------------------------------------------------------------------------------------------- private def TestHeap := - let ins : {n: Nat} → Nat → CompleteTree Nat n → CompleteTree Nat (n+1) := λ x y ↦ CompleteTree.heapInsert (.≤.) x y + let ins : {n: Nat} → Nat → CompleteTree Nat n → CompleteTree Nat (n+1) := λ x y ↦ CompleteTree.heapPush (.≤.) x y ins 5 CompleteTree.empty |> ins 3 |> ins 7 @@ -1128,7 +1126,7 @@ private def TestHeap := #eval TestHeap.heapRemoveAt (.≤.) 7 private def TestHeap2 := - let ins : {n: Nat} → Nat → CompleteTree Nat n → CompleteTree Nat (n+1) := λ x y ↦ CompleteTree.heapInsert (.≤.) x y + let ins : {n: Nat} → Nat → CompleteTree Nat n → CompleteTree Nat (n+1) := λ x y ↦ CompleteTree.heapPush (.≤.) x y ins 5 CompleteTree.empty |> ins 1 |> ins 2 -- cgit v1.2.3