diff options
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean | 61 | ||||
| -rw-r--r-- | TODO | 2 |
2 files changed, 62 insertions, 1 deletions
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean index ca4299f..195e24d 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean @@ -27,3 +27,64 @@ theorem heapRemoveAtReturnsElementAt {α : Type u} {n : Nat} (le : α → α → have h₄ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelationLt heap index (Nat.gt_of_not_le h₃) rewrite[get_eq_get', ←h₄] exact Eq.symm $ heapUpdateAtReturnsElementAt le _ _ _ _ + +theorem heapRemoveAtOnlyRemovesAt {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α (n+1)) (removeIndex : Fin (n+1)) (otherIndex : Fin (n+1)) (h₁ : removeIndex ≠ otherIndex) : (heap.heapRemoveAt le removeIndex).fst.contains (heap.get' otherIndex) := by + unfold heapRemoveAt + if h₂ : removeIndex = 0 then + subst removeIndex + exact heapPopOnlyRemovesRoot _ _ _ h₁.symm + else + simp only [h₂, ↓reduceDIte, ge_iff_le] + if h₃ : removeIndex = (Internal.heapRemoveLastWithIndex heap).2.snd then + simp only [h₃, ↓reduceDIte] + exact CompleteTree.AdditionalProofs.heapRemoveLastWithIndexOnlyRemovesOneElement _ _ (h₃.subst h₁.symm) + else + if h₄ : (Internal.heapRemoveLastWithIndex heap).2.snd ≤ removeIndex then + simp only[h₃, h₄, ↓reduceDIte] + have h₅ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelation heap otherIndex + simp only [gt_iff_lt] at h₅ + split at h₅ + case isTrue h₆ => + rw[get_eq_get', ←h₅] + apply heapUpdateAtOnlyUpdatesAt + simp only [ne_eq, Fin.pred_inj, h₁, not_false_eq_true] + case isFalse h₆ => + split at h₅ + case isTrue h₇ => + rw[get_eq_get', ←h₅] + apply heapUpdateAtOnlyUpdatesAt + simp only [ne_eq, Fin.ext_iff, Fin.coe_pred, Fin.coe_castLT] + generalize (Internal.heapRemoveLastWithIndex heap).snd.snd = j at * + omega + case isFalse h₇ => + generalize h₈ : (Internal.heapRemoveLastWithIndex heap).snd.snd = j at * + have h₉ : otherIndex = j := by omega + subst h₉ + subst h₈ + rw[CompleteTree.AdditionalProofs.heapRemoveLastWithIndexReturnsItemAtIndex] + exact heapUpdateAtContainsValue _ _ _ _ _ + else + simp only [h₃, h₄, ↓reduceDIte] + have h₅ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelation heap otherIndex + simp only [gt_iff_lt] at h₅ + split at h₅ + case isTrue h₆ => + rw[get_eq_get', ←h₅] + apply heapUpdateAtOnlyUpdatesAt + simp[Fin.ext_iff] + generalize (Internal.heapRemoveLastWithIndex heap).snd.snd = j at * + omega --h₄ and h₆ + case isFalse h₆ => + split at h₅ + case isTrue h₇ => + rw[get_eq_get', ←h₅] + apply heapUpdateAtOnlyUpdatesAt + rw[←Fin.val_ne_iff] at h₁ ⊢ + exact h₁ + case isFalse h₇ => + generalize h₈ : (Internal.heapRemoveLastWithIndex heap).snd.snd = j at * + have h₉ : otherIndex = j := by omega + subst h₉ + subst h₈ + rw[CompleteTree.AdditionalProofs.heapRemoveLastWithIndexReturnsItemAtIndex] + exact heapUpdateAtContainsValue _ _ _ _ _ @@ -19,7 +19,7 @@ This is a rough outline of upcoming tasks: [x] Prove that CompleteTree.heapUpdateAt indeed updates the value at the given index. - Use the same approach as heapUpdateRoot [x] Prove that CompleteTree.heapRemoveAt returns the element at the given index -[ ] Prove that CompleteTree.heapRemoveAt leaves all values in the tree except at the input index. +[x] Prove that CompleteTree.heapRemoveAt leaves all values in the tree except at the input index. Stuff below is not scheduled to happen any time soon. Feel free to contribute though. |