diff options
| author | Andreas Grois <andi@grois.info> | 2024-08-20 23:50:11 +0200 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2024-08-20 23:50:11 +0200 |
| commit | 7df84f9a3e399587c65a149bf4247154d9b07cc7 (patch) | |
| tree | 035388c2093a1541c2da4e94eccbbd80e7098f0f | |
| parent | 7d5df252a6e885f8b1ffab49196e0a4cc4b0131a (diff) | |
heapRemoveAtReturnsElementAt
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs.lean | 1 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean | 29 |
2 files changed, 30 insertions, 0 deletions
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs.lean b/BinaryHeap/CompleteTree/AdditionalProofs.lean index 3659fa4..4ab43f0 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs.lean @@ -3,3 +3,4 @@ import BinaryHeap.CompleteTree.AdditionalProofs.HeapRemoveLast import BinaryHeap.CompleteTree.AdditionalProofs.HeapUpdateRoot import BinaryHeap.CompleteTree.AdditionalProofs.HeapPop import BinaryHeap.CompleteTree.AdditionalProofs.HeapUpdateAt +import BinaryHeap.CompleteTree.AdditionalProofs.HeapRemoveAt diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean new file mode 100644 index 0000000..ca4299f --- /dev/null +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean @@ -0,0 +1,29 @@ +import BinaryHeap.CompleteTree.AdditionalProofs.HeapUpdateAt +import BinaryHeap.CompleteTree.AdditionalProofs.Get +import BinaryHeap.CompleteTree.AdditionalProofs.HeapPop +import BinaryHeap.CompleteTree.AdditionalProofs.HeapRemoveLast + +namespace BinaryHeap.CompleteTree.AdditionalProofs + +theorem heapRemoveAtReturnsElementAt {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α (n+1)) (index : Fin (n+1)) : (heap.heapRemoveAt le index).snd = heap.get' index := by + unfold heapRemoveAt + if h₁ : index = 0 then + simp only [h₁, ↓reduceDIte] + rw[get_eq_get', ←Fin.zero_eta, ←get_zero_eq_root] + exact heapPopReturnsRoot heap le + else + simp only [h₁, ↓reduceDIte, ge_iff_le] + if h₂ : index = (Internal.heapRemoveLastWithIndex heap).2.snd then + simp only [h₂, ↓reduceDIte] + exact Eq.symm $ CompleteTree.AdditionalProofs.heapRemoveLastWithIndexReturnsItemAtIndex heap + else + if h₃ : (Internal.heapRemoveLastWithIndex heap).2.snd ≤ index then + simp only[h₂, h₃, ↓reduceDIte] + have h₄ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelationGt heap index $ Nat.lt_of_le_of_ne h₃ (Fin.val_ne_iff.mpr (Ne.symm h₂)) + rewrite[get_eq_get', ←h₄] + exact Eq.symm $ heapUpdateAtReturnsElementAt le _ _ _ _ + else + simp only[h₂, h₃, ↓reduceDIte] + have h₄ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelationLt heap index (Nat.gt_of_not_le h₃) + rewrite[get_eq_get', ←h₄] + exact Eq.symm $ heapUpdateAtReturnsElementAt le _ _ _ _ |