diff options
| -rw-r--r-- | BinaryHeap/CompleteTree.lean | 1 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalOperations.lean | 51 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs.lean | 1 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/HeapOperations.lean | 48 |
4 files changed, 53 insertions, 48 deletions
diff --git a/BinaryHeap/CompleteTree.lean b/BinaryHeap/CompleteTree.lean index fd9fb3c..d883b63 100644 --- a/BinaryHeap/CompleteTree.lean +++ b/BinaryHeap/CompleteTree.lean @@ -1,6 +1,7 @@ import BinaryHeap.HeapPredicate import BinaryHeap.CompleteTree.Basic import BinaryHeap.CompleteTree.HeapOperations +import BinaryHeap.CompleteTree.AdditionalOperations import BinaryHeap.CompleteTree.HeapProofs import BinaryHeap.CompleteTree.AdditionalProofs diff --git a/BinaryHeap/CompleteTree/AdditionalOperations.lean b/BinaryHeap/CompleteTree/AdditionalOperations.lean new file mode 100644 index 0000000..53faaf8 --- /dev/null +++ b/BinaryHeap/CompleteTree/AdditionalOperations.lean @@ -0,0 +1,51 @@ +import BinaryHeap.CompleteTree.Basic +import BinaryHeap.CompleteTree.NatLemmas + +namespace BinaryHeap + +---------------------------------------------------------------------------------------------- +-- indexOf + +/--Helper function for CompleteTree.indexOf.-/ +private def CompleteTree.indexOfAux {α : Type u} (heap : CompleteTree α o) (pred : α → Bool) (currentIndex : Nat) : Option (Fin (o+currentIndex)) := + match o, heap with + | 0, .leaf => none + | (n+m+1), .branch a left right _ _ _ => + have sum_n_m_succ_curr : n + m.succ + currentIndex > 0 := Nat.add_pos_left (Nat.add_pos_right n (Nat.succ_pos m)) currentIndex + if pred a then + let result := Fin.ofNat' currentIndex sum_n_m_succ_curr + some result + else + let found_left := left.indexOfAux pred (currentIndex + 1) + let found_left : Option (Fin (n+m+1+currentIndex)) := found_left.map λ a ↦ Fin.ofNat' a sum_n_m_succ_curr + let found_right := + found_left + <|> + (right.indexOfAux pred (currentIndex + n + 1)).map ((λ a ↦ Fin.ofNat' a sum_n_m_succ_curr) : _ → Fin (n+m+1+currentIndex)) + found_right + +/--Finds the first occurance of a given element in the heap and returns its index. Indices are depth first.-/ +def CompleteTree.indexOf {α : Type u} (heap : CompleteTree α o) (pred : α → Bool) : Option (Fin o) := + indexOfAux heap pred 0 + + +---------------------------------------------------------------------------------------------- +-- get + +/--Returns the lement at the given index. Indices are depth first.-/ +def CompleteTree.get {α : Type u} {n : Nat} (index : Fin (n+1)) (heap : CompleteTree α (n+1)) : α := + match h₁ : index, h₂ : n, heap with + | 0, (_+_), .branch v _ _ _ _ _ => v + | ⟨j+1,h₃⟩, (o+p), .branch _ l r _ _ _ => + if h₄ : j < o then + match o with + | (oo+1) => get ⟨j, h₄⟩ l + else + have h₅ : n - o = p := Nat.sub_eq_of_eq_add $ (Nat.add_comm o p).subst h₂ + have : p ≠ 0 := + have h₆ : o < n := Nat.lt_of_le_of_lt (Nat.ge_of_not_lt h₄) (Nat.lt_of_succ_lt_succ h₃) + h₅.symm.substr $ Nat.sub_ne_zero_of_lt h₆ + have h₆ : j - o < p := h₅.subst $ Nat.sub_lt_sub_right (Nat.ge_of_not_lt h₄) $ Nat.lt_of_succ_lt_succ h₃ + have _termination : j - o < index.val := (Fin.val_inj.mpr h₁).substr (Nat.sub_lt_succ j o) + match p with + | (pp + 1) => get ⟨j - o, h₆⟩ r diff --git a/BinaryHeap/CompleteTree/AdditionalProofs.lean b/BinaryHeap/CompleteTree/AdditionalProofs.lean index 128dcd0..ad626e7 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs.lean @@ -1,4 +1,5 @@ import BinaryHeap.CompleteTree.Lemmas +import BinaryHeap.CompleteTree.AdditionalOperations import BinaryHeap.CompleteTree.HeapOperations namespace BinaryHeap diff --git a/BinaryHeap/CompleteTree/HeapOperations.lean b/BinaryHeap/CompleteTree/HeapOperations.lean index f16d89d..337797c 100644 --- a/BinaryHeap/CompleteTree/HeapOperations.lean +++ b/BinaryHeap/CompleteTree/HeapOperations.lean @@ -69,54 +69,6 @@ def CompleteTree.heapPush (le : α → α → Bool) (elem : α) (heap : Complete have letMeSpellItOutForYou : n + 1 + m + 1 = n + m + 1 + 1 := by simp_arith letMeSpellItOutForYou ▸ result - ----------------------------------------------------------------------------------------------- --- indexOf - -/--Helper function for CompleteTree.indexOf.-/ -private def CompleteTree.indexOfAux {α : Type u} (heap : CompleteTree α o) (pred : α → Bool) (currentIndex : Nat) : Option (Fin (o+currentIndex)) := - match o, heap with - | 0, .leaf => none - | (n+m+1), .branch a left right _ _ _ => - have sum_n_m_succ_curr : n + m.succ + currentIndex > 0 := Nat.add_pos_left (Nat.add_pos_right n (Nat.succ_pos m)) currentIndex - if pred a then - let result := Fin.ofNat' currentIndex sum_n_m_succ_curr - some result - else - let found_left := left.indexOfAux pred (currentIndex + 1) - let found_left : Option (Fin (n+m+1+currentIndex)) := found_left.map λ a ↦ Fin.ofNat' a sum_n_m_succ_curr - let found_right := - found_left - <|> - (right.indexOfAux pred (currentIndex + n + 1)).map ((λ a ↦ Fin.ofNat' a sum_n_m_succ_curr) : _ → Fin (n+m+1+currentIndex)) - found_right - -/--Finds the first occurance of a given element in the heap and returns its index. Indices are depth first.-/ -def CompleteTree.indexOf {α : Type u} (heap : CompleteTree α o) (pred : α → Bool) : Option (Fin o) := - indexOfAux heap pred 0 - - ----------------------------------------------------------------------------------------------- --- get - -/--Returns the lement at the given index. Indices are depth first.-/ -def CompleteTree.get {α : Type u} {n : Nat} (index : Fin (n+1)) (heap : CompleteTree α (n+1)) : α := - match h₁ : index, h₂ : n, heap with - | 0, (_+_), .branch v _ _ _ _ _ => v - | ⟨j+1,h₃⟩, (o+p), .branch _ l r _ _ _ => - if h₄ : j < o then - match o with - | (oo+1) => get ⟨j, h₄⟩ l - else - have h₅ : n - o = p := Nat.sub_eq_of_eq_add $ (Nat.add_comm o p).subst h₂ - have : p ≠ 0 := - have h₆ : o < n := Nat.lt_of_le_of_lt (Nat.ge_of_not_lt h₄) (Nat.lt_of_succ_lt_succ h₃) - h₅.symm.substr $ Nat.sub_ne_zero_of_lt h₆ - have h₆ : j - o < p := h₅.subst $ Nat.sub_lt_sub_right (Nat.ge_of_not_lt h₄) $ Nat.lt_of_succ_lt_succ h₃ - have _termination : j - o < index.val := (Fin.val_inj.mpr h₁).substr (Nat.sub_lt_succ j o) - match p with - | (pp + 1) => get ⟨j - o, h₆⟩ r - ---------------------------------------------------------------------------------------------- -- heapRemoveLast (with Index) |