diff options
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalOperations.lean | 8 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs.lean | 1 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/Find.lean | 64 | ||||
| -rw-r--r-- | TODO | 1 |
4 files changed, 70 insertions, 4 deletions
diff --git a/BinaryHeap/CompleteTree/AdditionalOperations.lean b/BinaryHeap/CompleteTree/AdditionalOperations.lean index 1caf47d..f103279 100644 --- a/BinaryHeap/CompleteTree/AdditionalOperations.lean +++ b/BinaryHeap/CompleteTree/AdditionalOperations.lean @@ -7,7 +7,7 @@ namespace BinaryHeap.CompleteTree -- indexOf /--Helper function for CompleteTree.indexOf.-/ -private def indexOfAux {α : Type u} (heap : CompleteTree α o) (pred : α → Bool) (currentIndex : Nat) : Option (Fin (o+currentIndex)) := +protected def Internal.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 _ _ _ => @@ -16,17 +16,17 @@ private def indexOfAux {α : Type u} (heap : CompleteTree α o) (pred : α → B let result := Fin.ofNat' currentIndex sum_n_m_succ_curr some result else - let found_left := left.indexOfAux pred (currentIndex + 1) + let found_left := CompleteTree.Internal.indexOfAux left 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)) + (CompleteTree.Internal.indexOfAux right 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 indexOf {α : Type u} (heap : CompleteTree α o) (pred : α → Bool) : Option (Fin o) := - indexOfAux heap pred 0 + CompleteTree.Internal.indexOfAux heap pred 0 ---------------------------------------------------------------------------------------------- diff --git a/BinaryHeap/CompleteTree/AdditionalProofs.lean b/BinaryHeap/CompleteTree/AdditionalProofs.lean index 4643be9..86a895d 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs.lean @@ -5,3 +5,4 @@ import BinaryHeap.CompleteTree.AdditionalProofs.HeapPop import BinaryHeap.CompleteTree.AdditionalProofs.HeapUpdateAt import BinaryHeap.CompleteTree.AdditionalProofs.HeapRemoveAt import BinaryHeap.CompleteTree.AdditionalProofs.HeapPush +import BinaryHeap.CompleteTree.AdditionalProofs.Find diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/Find.lean b/BinaryHeap/CompleteTree/AdditionalProofs/Find.lean new file mode 100644 index 0000000..83984a0 --- /dev/null +++ b/BinaryHeap/CompleteTree/AdditionalProofs/Find.lean @@ -0,0 +1,64 @@ +import BinaryHeap.CompleteTree.AdditionalOperations +import BinaryHeap.CompleteTree.AdditionalProofs.Get + +namespace BinaryHeap.CompleteTree.AdditionalProofs + +private theorem Option.orElse_result_none_both_none : Option.orElse a (λ_↦y) = none → a = none ∧ y = none := by + intro h₁ + cases a + case some => contradiction + case none => + simp + cases y + case some => contradiction + case none => rfl + +private theorem Option.bind_some_eq_map {α β : Type u} (f : α → β) (a : Option α) : Option.bind a (λy ↦ some (f y)) = Option.map f a := by + unfold Option.bind Option.map + cases a + case none => rfl + case some => rfl + +private theorem indexOfNoneImpPredFalseAux {α : Type u} {n : Nat} (tree : CompleteTree α n) (h₁ : n > 0) (pred : α → Bool) (currentIndex : Nat) : (CompleteTree.Internal.indexOfAux tree pred currentIndex).isNone → ∀(index : Fin n), ¬pred (tree.get index h₁) := by + intro h₂ + intro index + simp only [Option.isNone_iff_eq_none] at h₂ + simp only [Bool.not_eq_true] + unfold CompleteTree.Internal.indexOfAux at h₂ + split at h₂ ; contradiction + rename_i o p v l r p_le_o max_height_difference subtree_complete + split at h₂; contradiction + unfold HOrElse.hOrElse instHOrElseOfOrElse at h₂ + unfold OrElse.orElse Option.instOrElse at h₂ + simp only [Nat.add_zero, Nat.reduceAdd, Option.pure_def, Option.bind_eq_bind] at h₂ + have h₂₂ := Option.orElse_result_none_both_none h₂ + repeat rw[Option.bind_some_eq_map] at h₂₂ + simp only [Option.map_eq_none'] at h₂₂ + if h₃ : index = ⟨0,h₁⟩ then + subst index + rw[←get_zero_eq_root, root_unfold] + rename_i solution + simp only [Bool.not_eq_true] at solution + exact solution + else + have h₃₂ : index > ⟨0,h₁⟩ := Fin.pos_iff_ne_zero.mpr h₃ + if h₄ : index ≤ o then + rw[get_left (.branch v l r p_le_o max_height_difference subtree_complete) _ h₁ h₃₂ h₄] + rw[left_unfold] + have : o > 0 := by omega + have := indexOfNoneImpPredFalseAux l this pred (currentIndex + 1) + simp only [Option.isNone_iff_eq_none, Bool.not_eq_true] at this + exact this h₂₂.left _ + else + have h₄₂ : index > o := Nat.gt_of_not_le h₄ + rw[get_right (.branch v l r p_le_o max_height_difference subtree_complete) _ (Nat.succ_pos _) h₄₂] + rw[right_unfold] + -- if you are wondering: this is needed to make omega work below. + have : (o.add p).succ = p + (o + 1) := (Nat.add_assoc p o 1).substr $ (Nat.add_comm o p).subst (motive := λx ↦ (o+p)+1 = x + 1) rfl + have : p > 0 := by omega + have := indexOfNoneImpPredFalseAux r this pred (currentIndex + o + 1) + simp only [Option.isNone_iff_eq_none, Bool.not_eq_true] at this + exact this h₂₂.right _ + +theorem indexOfNoneImpPredFalse {α : Type u} {n : Nat} (tree : CompleteTree α n) (h₁ : n > 0) (pred : α → Bool) : (tree.indexOf pred).isNone → ∀(index : Fin n), ¬pred (tree.get index h₁) := + indexOfNoneImpPredFalseAux tree h₁ pred 0 @@ -9,6 +9,7 @@ This is a rough outline of upcoming tasks: [x] This automatically serves as a proof for CompleteTree.heapRemoveLast, once it is shown that they yield the same tree - Done by showing how indices relate between both trees. +[x] Prove that if CompleteTree.indexOf returns none, no index exists for which the predicate is true. [ ] Prove that if CompleteTree.indexOf returns some, CompleteTree.get with that result fulfills the predicate. [x] Prove that CompleteTree.heapUpdateRoot indeed exchanges the value at the root. - Done by showing that the new tree contains all elements except the root, and the updated value. |