indexOfNoneImpPredFalse

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
diff --git a/TODO b/TODO
index 45b469d..5ad9eb6 100644
--- a/TODO
+++ b/TODO
@@ -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.