From 07aac66e82b04f5195d844ceea85ec39654710bc Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Sat, 3 Aug 2024 12:21:42 +0200 Subject: Partial proof that HeapUpdateRoot only changes the root. --- BinaryHeap/CompleteTree/AdditionalProofs.lean | 1 + BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) 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₁ -- cgit v1.2.3