diff options
| author | Andreas Grois <andi@grois.info> | 2024-08-03 12:21:42 +0200 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2024-08-03 12:21:42 +0200 |
| commit | 07aac66e82b04f5195d844ceea85ec39654710bc (patch) | |
| tree | df4bf331efeecb7489d1bff4cbaaf4088f38aae3 | |
| parent | ede4ba0d37480186f333ad7d7bb2e3d48a7e7d52 (diff) | |
Partial proof that HeapUpdateRoot only changes the root.
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs.lean | 1 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean | 2 |
2 files changed, 2 insertions, 1 deletions
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs.lean b/BinaryHeap/CompleteTree/AdditionalProofs.lean index fc46ce8..1050dba 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs.lean @@ -1,2 +1,3 @@ import BinaryHeap.CompleteTree.AdditionalProofs.Contains import BinaryHeap.CompleteTree.AdditionalProofs.HeapRemoveLast +import BinaryHeap.CompleteTree.AdditionalProofs.HeapUpdateRoot diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean index c2cc072..0788180 100644 --- a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean +++ b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean @@ -3,7 +3,7 @@ import BinaryHeap.CompleteTree.Lemmas namespace BinaryHeap.CompleteTree -private theorem heapUpdateRootReturnsRoot {α : Type u} {n : Nat} (le : α → α → Bool) (value : α) (heap : CompleteTree α n) (h₁ : n > 0) : (heap.heapUpdateRoot le value h₁).snd = heap.root h₁ := by +theorem heapUpdateRootReturnsRoot {α : Type u} {n : Nat} (le : α → α → Bool) (value : α) (heap : CompleteTree α n) (h₁ : n > 0) : (heap.heapUpdateRoot le value h₁).snd = heap.root h₁ := by unfold heapUpdateRoot split rename_i o p v l r h₃ h₄ h₅ h₁ |