diff options
14 files changed, 184 insertions, 181 deletions
diff --git a/BinaryHeap.lean b/BinaryHeap.lean index 774a3c3..e3c39af 100644 --- a/BinaryHeap.lean +++ b/BinaryHeap.lean @@ -41,14 +41,14 @@ def removeAt {α : Type u} {le : α → α → Bool} {n : Nat} : (BinaryHeap α ({ tree := result.fst, valid := resultValid, wellDefinedLe}, result.snd) /-- Updates the element at the given (depth-first) index and returns its previous value. O(log(n)) -/ -def updateAt {α : Type u} {le : α → α → Bool} {n : Nat} : (BinaryHeap α le (n+1)) → (Fin (n+1)) → α → (BinaryHeap α le (n+1) × α) +def updateAt {α : Type u} {le : α → α → Bool} {n : Nat} : (BinaryHeap α le n) → (Fin n) → α → (BinaryHeap α le n × α) | {tree, valid, wellDefinedLe}, index, value => - let result := tree.heapUpdateAt le index value $ Nat.succ_pos n - let resultValid := CompleteTree.heapUpdateAtIsHeap le index value tree _ valid wellDefinedLe.left wellDefinedLe.right + let result := tree.heapUpdateAt le index value + let resultValid := CompleteTree.heapUpdateAtIsHeap le index value tree valid wellDefinedLe.left wellDefinedLe.right ({ tree := result.fst, valid := resultValid, wellDefinedLe}, result.snd) /-- Searches for an element in the heap and returns its index. **O(n)** -/ -def indexOf {α : Type u} {le : α → α → Bool} {n : Nat} : BinaryHeap α le (n+1) → (pred : α → Bool) → Option (Fin (n+1)) +def indexOf {α : Type u} {le : α → α → Bool} {n : Nat} : BinaryHeap α le n → (pred : α → Bool) → Option (Fin n) | {tree, valid := _, wellDefinedLe := _}, pred => tree.indexOf pred diff --git a/BinaryHeap/CompleteTree/AdditionalOperations.lean b/BinaryHeap/CompleteTree/AdditionalOperations.lean index f103279..ee6b685 100644 --- a/BinaryHeap/CompleteTree/AdditionalOperations.lean +++ b/BinaryHeap/CompleteTree/AdditionalOperations.lean @@ -50,7 +50,7 @@ def get' {α : Type u} {n : Nat} (index : Fin (n+1)) (heap : CompleteTree α (n+ match p with | (pp + 1) => get' ⟨j - o, h₆⟩ r -def get {α : Type u} {n : Nat} (index : Fin n) (heap : CompleteTree α n) (_ : n > 0) : α := +def get {α : Type u} {n : Nat} (index : Fin n) (heap : CompleteTree α n) : α := match n, index, heap with | (_+1), index, heap => heap.get' index diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean b/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean index 487a50f..6614210 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean @@ -41,17 +41,9 @@ private theorem if_get_eq_contains {α : Type u} {o : Nat} (tree : CompleteTree apply if_get_eq_contains done -private theorem if_contains_get_eq_auxl {α : Type u} {o : Nat} (tree : CompleteTree α (o+1)) (element : α) (h₁ : o > 0) : - have : tree.leftLen (Nat.lt_succ_of_lt h₁) > 0 := by - unfold leftLen; - split - unfold length - rename_i hx _ _ - simp only [Nat.add_eq, Nat.succ_eq_add_one, Nat.reduceEqDiff] at hx - omega - ∀(indexl : Fin (tree.leftLen (Nat.succ_pos o))), (tree.left _).get indexl this = element → ∃(index : Fin (o+1)), tree.get index (Nat.lt_succ_of_lt h₁) = element +private theorem if_contains_get_eq_auxl {α : Type u} {o : Nat} (tree : CompleteTree α (o+1)) (element : α) : + ∀(indexl : Fin (tree.leftLen (Nat.succ_pos o))), (tree.left _).get indexl = element → ∃(index : Fin (o+1)), tree.get index = element := by - simp intro indexl let index : Fin (o+1) := indexl.succ.castLT (by simp only [Nat.succ_eq_add_one, Fin.val_succ, Nat.succ_lt_succ_iff, gt_iff_lt] @@ -76,9 +68,9 @@ private theorem if_contains_get_eq_auxl {α : Type u} {o : Nat} (tree : Complete simp only [h₅, ↓reduceDIte, Nat.add_eq] unfold get at prereq split at prereq - rename_i pp ii ll _ hel hei heq _ + rename_i pp ii ll hel hei heq split - rename_i ppp lll _ _ _ _ _ _ _ + rename_i ppp lll _ _ _ _ _ _ have : pp = ppp := by omega subst pp simp only [gt_iff_lt, Nat.succ_eq_add_one, Nat.add_eq, heq_eq_eq, Nat.zero_lt_succ] at * @@ -90,8 +82,8 @@ private theorem if_contains_get_eq_auxl {α : Type u} {o : Nat} (tree : Complete rw[heq] assumption -private theorem if_contains_get_eq_auxr {α : Type u} {o : Nat} (tree : CompleteTree α (o+1)) (element : α) (h₁ : tree.rightLen (Nat.succ_pos o) > 0) : - ∀(indexl : Fin (tree.rightLen (Nat.succ_pos o))), (tree.right _).get indexl h₁ = element → ∃(index : Fin (o+1)), tree.get index (Nat.succ_pos o) = element +private theorem if_contains_get_eq_auxr {α : Type u} {o : Nat} (tree : CompleteTree α (o+1)) (element : α) : + ∀(indexl : Fin (tree.rightLen (Nat.succ_pos o))), (tree.right _).get indexl = element → ∃(index : Fin (o+1)), tree.get index = element := by intro indexr let index : Fin (o+1) := ⟨(tree.leftLen (Nat.succ_pos o) + indexr.val + 1), by @@ -124,9 +116,9 @@ private theorem if_contains_get_eq_auxr {α : Type u} {o : Nat} (tree : Complete simp only [h₅, ↓reduceDIte, Nat.add_eq] unfold get at prereq split at prereq - rename_i pp ii rr _ hel hei heq _ + rename_i pp ii rr hel hei heq split - rename_i ppp rrr _ _ _ _ _ _ _ _ + rename_i ppp rrr _ _ _ _ _ _ _ have : pp = ppp := by rw[rightLen_unfold] at hel; exact Nat.succ.inj hel.symm subst pp simp only [gt_iff_lt, ne_eq, Nat.succ_eq_add_one, Nat.add_eq, Nat.reduceEqDiff, heq_eq_eq, Nat.zero_lt_succ] at * @@ -161,7 +153,7 @@ private theorem if_contains_get_eq {α : Type u} {o : Nat} (tree : CompleteTree | (nn+1), l => by have nn_lt_o : nn < o := by have : o = nn + 1 + m := Nat.succ.inj he; omega --also for termination have h₃ := if_contains_get_eq l element h₂ - have h₄ := if_contains_get_eq_auxl tree element $ Nat.zero_lt_of_lt nn_lt_o + have h₄ := if_contains_get_eq_auxl tree element simp only at h₄ simp[get_eq_get'] at h₃ ⊢ apply h₃.elim @@ -179,12 +171,7 @@ private theorem if_contains_get_eq {α : Type u} {o : Nat} (tree : CompleteTree | (mm+1), r => by have mm_lt_o : mm < o := by have : o = n + (mm + 1) := Nat.succ.inj he; omega --termination have h₃ := if_contains_get_eq r element h₂ - have : tree.rightLen (Nat.succ_pos o) > 0 := by - have := heqSameRightLen (he) (Nat.succ_pos o) heq - simp[rightLen_unfold] at this - rw[this] - exact Nat.succ_pos mm - have h₄ := if_contains_get_eq_auxr tree element this + have h₄ := if_contains_get_eq_auxr tree element simp[get_eq_get'] at h₃ ⊢ apply h₃.elim match o, tree with @@ -206,6 +193,6 @@ theorem contains_iff_index_exists' {α : Type u} {o : Nat} (tree : CompleteTree case mp => exact if_contains_get_eq tree element -theorem contains_iff_index_exists {α : Type u} {n : Nat} (tree : CompleteTree α n) (element : α) (h₁ : n > 0): tree.contains element ↔ ∃ (index : Fin n), tree.get index h₁ = element := +theorem contains_iff_index_exists {α : Type u} {n : Nat} (tree : CompleteTree α n) (element : α) (_ : n > 0): tree.contains element ↔ ∃ (index : Fin n), tree.get index = element := match n, tree with | _+1, tree => contains_iff_index_exists' tree element diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/Find.lean b/BinaryHeap/CompleteTree/AdditionalProofs/Find.lean index 83984a0..902afc4 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/Find.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/Find.lean @@ -19,46 +19,53 @@ private theorem Option.bind_some_eq_map {α β : Type u} (f : α → β) (a : Op 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 _ +private theorem indexOfNoneImpPredFalseAux {α : Type u} {n : Nat} (tree : CompleteTree α n) (pred : α → Bool) (currentIndex : Nat) : (CompleteTree.Internal.indexOfAux tree pred currentIndex).isNone → ∀(index : Fin n), ¬pred (tree.get index) := by + if h₁ : n > 0 then + 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 > 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 _ + 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 := indexOfNoneImpPredFalseAux l 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] + have := indexOfNoneImpPredFalseAux r pred (currentIndex + o + 1) + simp only [Option.isNone_iff_eq_none, Bool.not_eq_true] at this + exact this h₂₂.right _ + else + simp at h₁ + intro h₂ + intro hx + subst h₁ + cases hx + contradiction + +theorem indexOfNoneImpPredFalse {α : Type u} {n : Nat} (tree : CompleteTree α n) (pred : α → Bool) : (tree.indexOf pred).isNone → ∀(index : Fin n), ¬pred (tree.get index) := + indexOfNoneImpPredFalseAux tree pred 0 -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 +theorem indexOfSomeImpPredTrue {α : Type u} {n : Nat} (tree : CompleteTree α n) (pred : α → Bool) : (h₁ : (tree.indexOf pred).isSome) → pred (tree.get ((tree.indexOf pred).get h₁)) := by + sorry diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean b/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean index b8cd934..f872836 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean @@ -3,9 +3,9 @@ import BinaryHeap.CompleteTree.Lemmas namespace BinaryHeap.CompleteTree.AdditionalProofs -theorem get_eq_get' {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (index : Fin (n+1)) : tree.get' index = tree.get index (Nat.succ_pos n) := rfl +theorem get_eq_get' {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (index : Fin (n+1)) : tree.get' index = tree.get index := rfl -theorem get_zero_eq_root {α : Type u} {n : Nat} (tree : CompleteTree α n) (h₁ : n > 0): tree.root h₁ = tree.get ⟨0,h₁⟩ h₁ := by +theorem get_zero_eq_root {α : Type u} {n : Nat} (tree : CompleteTree α n) (h₁ : n > 0): tree.root h₁ = tree.get ⟨0,h₁⟩ := by unfold get match n with | nn+1 => @@ -29,14 +29,13 @@ theorem get_right {α : Type u} {n : Nat} (tree : CompleteTree α n) (index : Fi have : p+1+o = (o.add p).succ := by simp_arith rw[this] assumption - have h₄ : tree.rightLen h₁ > 0 := Nat.zero_lt_of_lt h₃ - tree.get index h₁ = (tree.right h₁).get ⟨index.val - (tree.leftLen h₁) - 1, h₃⟩ h₄ + tree.get index = (tree.right h₁).get ⟨index.val - (tree.leftLen h₁) - 1, h₃⟩ := match n, tree with | (o+p+1), .branch v l r _ _ _ => by simp[right_unfold, leftLen_unfold] rw[leftLen_unfold] at h₂ - generalize hnew : get ⟨↑index - o - 1, _⟩ r _ = new + generalize hnew : get ⟨↑index - o - 1, _⟩ r = new unfold get get' split case h_1 => @@ -73,19 +72,18 @@ theorem get_right' {α : Type u} {n m : Nat} {v : α} {l : CompleteTree α n} {r have : m + 1 + n = n + m + 1 := by simp_arith rw[this] assumption - (branch v l r m_le_n max_height_diff subtree_complete).get index (Nat.succ_pos _) = r.get ⟨index.val - n - 1, h₂⟩ (Nat.zero_lt_of_lt h₂) + (branch v l r m_le_n max_height_diff subtree_complete).get index = r.get ⟨index.val - n - 1, h₂⟩ := get_right (branch v l r m_le_n max_height_diff subtree_complete) index (Nat.succ_pos _) h₁ theorem get_left {α : Type u} {n : Nat} (tree : CompleteTree α n) (index : Fin n) (h₁ : n > 0) (h₂ : index > ⟨0, h₁⟩) (h₃ : index ≤ tree.leftLen h₁) : have h₃ : ↑index - 1 < tree.leftLen h₁ := Nat.lt_of_lt_of_le (Nat.pred_lt_self h₂) h₃ - have h₄ : tree.leftLen h₁ > 0 := Nat.zero_lt_of_lt h₃ - tree.get index h₁ = (tree.left h₁).get ⟨index.val - 1, h₃⟩ h₄ + tree.get index = (tree.left h₁).get ⟨index.val - 1, h₃⟩ := match n, tree with | (o+p+1), .branch v l r _ _ _ => by simp[left_unfold] - generalize hnew : get ⟨↑index - 1, _⟩ l _ = new + generalize hnew : get ⟨↑index - 1, _⟩ l = new unfold get get' split case h_1 => contradiction @@ -106,6 +104,6 @@ theorem get_left {α : Type u} {n : Nat} (tree : CompleteTree α n) (index : Fin theorem get_left' {α : Type u} {n m : Nat} {v : α} {l : CompleteTree α n} {r : CompleteTree α m} {m_le_n : m ≤ n} {max_height_diff : n < 2 * (m + 1)} {subtree_complete : (n + 1).isPowerOfTwo ∨ (m + 1).isPowerOfTwo} (index : Fin (n + m + 1)) (h₁ : index > ⟨0, Nat.succ_pos _⟩) (h₂ : index ≤ n) : have h₃ : ↑index - 1 < n := Nat.lt_of_lt_of_le (Nat.pred_lt_self h₁) h₂ - (branch v l r m_le_n max_height_diff subtree_complete).get index (Nat.succ_pos _) = l.get ⟨index.val - 1, h₃⟩ (Nat.zero_lt_of_lt h₃) + (branch v l r m_le_n max_height_diff subtree_complete).get index = l.get ⟨index.val - 1, h₃⟩ := get_left (branch v l r m_le_n max_height_diff subtree_complete) index (Nat.succ_pos _) h₁ h₂ diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean index fb5b81b..807bdcb 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean @@ -29,7 +29,7 @@ theorem heapPopReturnsRoot {α : Type u} {n : Nat} (tree : CompleteTree α (n+1) This is not a rigorous proof that the rest of the tree remained unchanged, as (1 (1 (1 1)) (2)).heapPop = (1 (2 (2 _)) (2)) would pass it too... Imho it is still a good indication that there are no obvious bugs. -/ -theorem heapPopOnlyRemovesRoot {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (le: α → α → Bool) (index : Fin (n+1)) (h₁ : index ≠ ⟨0, Nat.succ_pos _⟩) : (tree.heapPop le).fst.contains $ tree.get index (Nat.succ_pos _) := by +theorem heapPopOnlyRemovesRoot {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (le: α → α → Bool) (index : Fin (n+1)) (h₁ : index ≠ ⟨0, Nat.succ_pos _⟩) : (tree.heapPop le).fst.contains $ tree.get index := by unfold heapPop split <;> simp case isFalse h₃ => omega --contradiction. if n == 0 then index cannot be ≠ 0 diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapPush.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPush.lean index 66035a1..ea2b5a7 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapPush.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPush.lean @@ -46,13 +46,15 @@ theorem heapPushContainsValue {α : Type u} {n : Nat} (le : α → α → Bool) rw[left_unfold] exact heapPushContainsValue le l val -theorem heapPushRetainsHeapValues {α : Type u} {n: Nat} (le : α → α → Bool) (heap : CompleteTree α n) (val : α) (index : Fin n) (h₁ : n > 0) : (heap.heapPush le val).contains (heap.get index h₁) := by +theorem heapPushRetainsHeapValues {α : Type u} {n: Nat} (le : α → α → Bool) (heap : CompleteTree α n) (val : α) (index : Fin n) : (heap.heapPush le val).contains (heap.get index) := by unfold heapPush split case h_1 => + have := index.isLt contradiction case h_2 => rename_i o p v l r p_le_o max_height_difference subtree_complete + have h₁ : o+p+1 > 0 := Nat.succ_pos _ if h₂ : index = ⟨0, h₁⟩ then subst h₂ cases le val v @@ -95,7 +97,7 @@ theorem heapPushRetainsHeapValues {α : Type u} {n: Nat} (le : α → α → Boo have : index.val - 1 < o := Nat.sub_one_lt_of_le h₂₂ h₃ exists ⟨index.val - 1, this⟩ case isFalse => - exact heapPushRetainsHeapValues le l _ ⟨index.val - 1, _⟩ _ + exact heapPushRetainsHeapValues le l _ ⟨index.val - 1, _⟩ else split case' isFalse => rw[←containsSeesThroughCast] @@ -107,7 +109,7 @@ theorem heapPushRetainsHeapValues {α : Type u} {n: Nat} (le : α → α → Boo rw[right_unfold] simp only [Nat.succ_eq_add_one, leftLen_unfold] case isTrue => - exact heapPushRetainsHeapValues le r _ ⟨index.val - o - 1, _⟩ _ + exact heapPushRetainsHeapValues le r _ ⟨index.val - o - 1, _⟩ case isFalse => 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 diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean index 195e24d..a8a551f 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean @@ -21,12 +21,12 @@ theorem heapRemoveAtReturnsElementAt {α : Type u} {n : Nat} (le : α → α → 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 _ _ _ _ + 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 _ _ _ _ + 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 @@ -62,7 +62,7 @@ theorem heapRemoveAtOnlyRemovesAt {α : Type u} {n : Nat} (le : α → α → Bo subst h₉ subst h₈ rw[CompleteTree.AdditionalProofs.heapRemoveLastWithIndexReturnsItemAtIndex] - exact heapUpdateAtContainsValue _ _ _ _ _ + exact heapUpdateAtContainsValue _ _ _ _ else simp only [h₃, h₄, ↓reduceDIte] have h₅ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelation heap otherIndex @@ -87,4 +87,4 @@ theorem heapRemoveAtOnlyRemovesAt {α : Type u} {n : Nat} (le : α → α → Bo subst h₉ subst h₈ rw[CompleteTree.AdditionalProofs.heapRemoveLastWithIndexReturnsItemAtIndex] - exact heapUpdateAtContainsValue _ _ _ _ _ + exact heapUpdateAtContainsValue _ _ _ _ diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean index b852995..694a0ee 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean @@ -208,11 +208,11 @@ private theorem Fin.ne_zero_of_gt {n : Nat} {i j : Fin (n+1)} (h₁ : i > j) : i have : 0 ≤ j := Fin.zero_le _ by omega -private theorem heapRemoveLastWithIndexRelationGt_Aux {α : Type u} {o p q : Nat} (index : Fin (((o + 1).add p + 1))) (h₁ : o + 1 + p = o + p + 1) (tree : CompleteTree α (o+p+1)) (h₂ : o + 1 + p > 0) (h₃ : (h₁ ▸ tree).rightLen h₂ > 0) (h₄ : ↑index - 1 - q - 1 < (h₁ ▸ tree).rightLen h₂) (h₅ : o + p + 1 > 0) (h₆ : tree.rightLen h₅ > 0) (h₇ : ↑index - (q + 1) - 1 < tree.rightLen h₅) +private theorem heapRemoveLastWithIndexRelationGt_Aux {α : Type u} {o p q : Nat} (index : Fin (((o + 1).add p + 1))) (h₁ : o + 1 + p = o + p + 1) (tree : CompleteTree α (o+p+1)) (h₂ : o + 1 + p > 0) (h₄ : ↑index - 1 - q - 1 < (h₁ ▸ tree).rightLen h₂) (h₅ : o + p + 1 > 0) (h₇ : ↑index - (q + 1) - 1 < tree.rightLen h₅) : get ⟨↑index - 1 - q - 1, h₄⟩ - ((h₁ ▸ tree).right h₂) h₃ = - get ⟨↑index - (q + 1) - 1, h₇⟩ (tree.right h₅) h₆ + ((h₁ ▸ tree).right h₂) = + get ⟨↑index - (q + 1) - 1, h₇⟩ (tree.right h₅) := by induction p generalizing o case zero => @@ -225,9 +225,9 @@ private theorem heapRemoveLastWithIndexRelationGt_Aux {α : Type u} {o p q : Nat have hp₄ : (o + 1 + 1 + pp) = o + 1 + (pp + 1) := (Nat.add_comm_right (o+1) 1 pp).substr $ Nat.add_assoc (o+1) pp 1 rw[hp₃, hp₄] at hp₂ have : o + 1 + (pp + 1) + 1 = o + 1 + 1 + pp + 1 := Nat.add_comm_right (o + 1) (pp + 1) 1 - exact hp₂ (index.cast this) h₁ tree h₂ h₃ h₄ h₅ h₆ h₇ + exact hp₂ (index.cast this) h₁ tree h₂ h₄ h₅ h₇ -private theorem heapRemoveLastWithIndexRelationGt_Aux2 {α : Type u} {o p : Nat} (index : Fin (o + 1 + p)) (tree : CompleteTree α (o + p + 1)) (h₁ : o + p + 1 = o + 1 + p) (h₂ : o + 1 + p > 0) (h₃ : o + p + 1 > 0) (h₄ : index.val < o + p + 1) : get index (h₁▸tree) h₂ = get ⟨index.val,h₄⟩ tree h₃ := by +private theorem heapRemoveLastWithIndexRelationGt_Aux2 {α : Type u} {o p : Nat} (index : Fin (o + 1 + p)) (tree : CompleteTree α (o + p + 1)) (h₁ : o + p + 1 = o + 1 + p) (h₄ : index.val < o + p + 1) : get index (h₁▸tree) = get ⟨index.val,h₄⟩ tree := by induction p generalizing o case zero => simp @@ -236,11 +236,10 @@ private theorem heapRemoveLastWithIndexRelationGt_Aux2 {α : Type u} {o p : Nat} have hp₃ : (o + 1 + pp + 1) = o + (pp + 1) + 1 := Nat.add_comm_right o 1 (pp + 1) have hp₄ : (o + 1 + 1 + pp) = o + 1 + (pp + 1) := (Nat.add_comm_right (o+1) 1 pp).substr $ Nat.add_assoc (o+1) pp 1 rw[hp₃, hp₄] at hp₂ - exact hp₂ index tree h₁ h₂ h₃ h₄ + exact hp₂ index tree h₁ h₄ protected theorem heapRemoveLastWithIndexRelationGt {α : Type u} {n : Nat} (heap : CompleteTree α (n+1)) (index : Fin (n+1)) (h₁ : index > (CompleteTree.Internal.heapRemoveLastWithIndex heap).snd.snd) : - have : n > 0 := Nat.lt_of_lt_of_le (Fin.pos_iff_ne_zero.mpr $ Fin.ne_zero_of_gt h₁) (Nat.le_of_lt_succ index.isLt) - (CompleteTree.Internal.heapRemoveLastWithIndex heap).fst.get (index.pred $ Fin.ne_zero_of_gt h₁) this = heap.get index (Nat.succ_pos _) + (CompleteTree.Internal.heapRemoveLastWithIndex heap).fst.get (index.pred $ Fin.ne_zero_of_gt h₁) = heap.get index := by have h₂ : 0 ≠ n := Ne.symm $ Nat.ne_zero_iff_zero_lt.mpr $ Nat.lt_of_lt_of_le (Fin.pos_iff_ne_zero.mpr $ Fin.ne_zero_of_gt h₁) (Nat.le_of_lt_succ index.isLt) revert h₁ @@ -268,6 +267,7 @@ if h₃ : p < o ∧ (p + 1).nextPowerOfTwo = p + 1 then rewrite[←lens_see_through_cast _ leftLen _ (Nat.succ_pos _) _] rewrite[leftLen_unfold] assumption + omega simp only [Nat.add_eq, ne_eq, Fin.zero_eta, Nat.succ_eq_add_one, Nat.pred_eq_sub_one, Fin.coe_pred, Fin.isValue, ← lens_see_through_cast _ leftLen _ (Nat.succ_pos _) _] simp only[leftLen_unfold] @@ -278,14 +278,13 @@ if h₃ : p < o ∧ (p + 1).nextPowerOfTwo = p + 1 then -- get goes into the left branch have h₅ : index ≠ 0 := Fin.ne_zero_of_gt h₁ rewrite[heapRemoveLastWithIndexRelationGt_Aux2] - case h₃ => exact Nat.succ_pos _ case h₄ => exact Nat.le_of_not_gt h₄ |> (Nat.succ_pred (Fin.val_ne_of_ne h₅)).substr |> Nat.succ_le.mp |> Nat.lt_add_right p |> (Nat.add_comm_right oo 1 p).subst - generalize hold : get index (branch v l r _ _ _) _ = old + generalize hold : get index (branch v l r _ _ _) = old have h₆ : index.pred h₅ ≤ oo := Nat.pred_le_iff_le_succ.mpr $ Nat.le_of_not_gt h₄ have h₇ : ↑index - 1 ≤ oo := (Fin.coe_pred index h₅).subst (motive := λx↦x ≤ oo) h₆ have h₈ : ↑index ≤ oo + 1 := Nat.le_succ_of_pred_le h₇ @@ -309,7 +308,7 @@ else subst o contradiction case succ pp _ _ _ _ => - generalize hold : get index (branch v l r _ _ _) _ = oldValue + generalize hold : get index (branch v l r _ _ _) = oldValue have h₄ : index ≠ 0 := Fin.ne_zero_of_gt h₁ have h₅ : index.pred h₄ > o := by simp only [Nat.add_eq, Fin.coe_pred, gt_iff_lt] @@ -339,16 +338,15 @@ else simp only [this, Nat.add_eq, Fin.isValue, h₉] --no idea why simp avoids the same issue... protected theorem heapRemoveLastWithIndexRelationLt {α : Type u} {n : Nat} (heap : CompleteTree α (n+1)) (index : Fin (n+1)) (h₁ : index < (CompleteTree.Internal.heapRemoveLastWithIndex heap).snd.snd) : - have hn : n > 0 := Nat.lt_of_lt_of_le (Fin.pos_iff_ne_zero.mpr $ Fin.ne_zero_of_gt h₁) (Nat.le_of_lt_succ (CompleteTree.Internal.heapRemoveLastWithIndex heap).snd.snd.isLt) have : index.val < n := Nat.lt_of_lt_of_le h₁ $ Nat.lt_succ.mp (CompleteTree.Internal.heapRemoveLastWithIndex heap).snd.snd.isLt - (CompleteTree.Internal.heapRemoveLastWithIndex heap).fst.get ⟨index.val, this⟩ hn = heap.get index (Nat.succ_pos _) + (CompleteTree.Internal.heapRemoveLastWithIndex heap).fst.get ⟨index.val, this⟩ = heap.get index := have hn : n > 0 := Nat.lt_of_lt_of_le (Fin.pos_iff_ne_zero.mpr $ Fin.ne_zero_of_gt h₁) (Nat.le_of_lt_succ (CompleteTree.Internal.heapRemoveLastWithIndex heap).snd.snd.isLt) have hi : index.val < n := Nat.lt_of_lt_of_le h₁ $ Nat.lt_succ.mp (CompleteTree.Internal.heapRemoveLastWithIndex heap).snd.snd.isLt if h₂ : index = 0 then by subst index simp only [Fin.val_zero] - have := Fin.zero_eta.subst (motive := λx ↦ heap.root _ = get x heap _) $ get_zero_eq_root heap (Nat.succ_pos _) + have := Fin.zero_eta.subst (motive := λx ↦ heap.root _ = get x heap) $ get_zero_eq_root heap (Nat.succ_pos _) rewrite[←this] have := get_zero_eq_root (Internal.heapRemoveLastWithIndex heap).fst hn rewrite[←this] @@ -385,7 +383,6 @@ protected theorem heapRemoveLastWithIndexRelationLt {α : Type u} {n : Nat} (hea have h₅ : index ≤ oo+1 := Nat.le_succ_of_le h₇ rewrite[get_left' _ h₂₂ h₅] rewrite[heapRemoveLastWithIndexRelationGt_Aux2] - case h₃ => exact Nat.succ_pos _ case h₄ => exact h₆ rewrite[get_left' _ h₈ h₇] have : index.val - 1 < oo + 1 := Nat.sub_one_lt_of_le h₂₂ h₅ @@ -436,11 +433,11 @@ protected theorem heapRemoveLastWithIndexRelation {α : Type u} {n : Nat} (heap if h₁ : index > oldIndex then have : oldIndex ≥ 0 := Fin.zero_le oldIndex have : index > 0 := by omega - result.get (index.pred $ Fin.ne_of_gt this) (by omega) = heap.get index (by omega) + result.get (index.pred $ Fin.ne_of_gt this) = heap.get index else if h₂ : index < oldIndex then - result.get (index.castLT (by omega)) (by omega) = heap.get index (by omega) + result.get (index.castLT (by omega)) = heap.get index else - removedElement = heap.get index (Nat.succ_pos _) + removedElement = heap.get index := by simp split @@ -473,13 +470,12 @@ protected theorem heapRemoveLastWithIndexRelation {α : Type u} {n : Nat} (heap -/ protected theorem heapRemoveLastWithIndexOnlyRemovesOneElement {α : Type u} {n : Nat} (heap : CompleteTree α (n+1)) (index : Fin (n+1)) : let (newHeap, _, removedIndex) := Internal.heapRemoveLastWithIndex heap - (h₁ : index ≠ removedIndex) → newHeap.contains (heap.get index (Nat.succ_pos n)) + (h₁ : index ≠ removedIndex) → newHeap.contains (heap.get index) := by simp only [ne_eq] intro h₁ have h₂ : n > 0 := by omega - rw[contains_iff_index_exists] - case h₁ => exact h₂ + rw[contains_iff_index_exists _ _ h₂] have h₃ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelation heap index simp at h₃ split at h₃ @@ -498,7 +494,7 @@ protected theorem heapRemoveLastWithIndexOnlyRemovesOneElement {α : Type u} {n -/ protected theorem heapRemoveLastWithIndexEitherContainsOrReturnsElement {α : Type u} {n : Nat} (heap : CompleteTree α (n+1)) (index : Fin (n+1)) : let (newHeap, removedElement, _) := Internal.heapRemoveLastWithIndex heap - newHeap.contains (heap.get index (Nat.succ_pos n)) ∨ removedElement = heap.get index (Nat.succ_pos n) + newHeap.contains (heap.get index) ∨ removedElement = heap.get index := let removedIndex := (Internal.heapRemoveLastWithIndex heap).snd.snd if h₁ : index ≠ removedIndex then @@ -517,7 +513,7 @@ protected theorem heapRemoveLastWithIndexEitherContainsOrReturnsElement {α : Ty -/ protected theorem heapRemoveLastEitherContainsOrReturnsElement {α : Type u} {n : Nat} (heap : CompleteTree α (n+1)) (index : Fin (n+1)) : let (newHeap, removedElement) := Internal.heapRemoveLast heap - newHeap.contains (heap.get index (Nat.succ_pos n)) ∨ removedElement = heap.get index (Nat.succ_pos n) + newHeap.contains (heap.get index) ∨ removedElement = heap.get index := by have h₁ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexEitherContainsOrReturnsElement heap index simp at h₁ ⊢ diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean index 7dbe23d..be82a57 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean @@ -5,22 +5,23 @@ import BinaryHeap.CompleteTree.AdditionalProofs.Get namespace BinaryHeap.CompleteTree.AdditionalProofs -theorem heapUpdateAtReturnsElementAt {α : Type u} {n : Nat} (le : α → α → Bool) (val : α) (heap : CompleteTree α n) (index : Fin n) (h₁ : n > 0) : heap.get index h₁ = (heap.heapUpdateAt le index val h₁).snd := by +theorem heapUpdateAtReturnsElementAt {α : Type u} {n : Nat} (le : α → α → Bool) (val : α) (heap : CompleteTree α n) (index : Fin n) : heap.get index = (heap.heapUpdateAt le index val).snd := by cases index rename_i i isLt cases i case mk.zero => - unfold get get' heapUpdateAt + unfold get get' split split case h_2 hx => have hx := Fin.val_eq_of_eq hx contradiction - case h_1 v l r h₂ h₃ h₄ _ _ _=> + case h_1 v l r h₂ h₃ h₄ _ _=> exact Eq.symm $ heapUpdateRootReturnsRoot le val (.branch v l r h₂ h₃ h₄) (Nat.succ_pos _) case mk.succ j => - unfold heapUpdateAt + unfold heapUpdateAt heapUpdateAtAux generalize hj : (⟨j + 1, isLt⟩ : Fin n) = index -- otherwise split fails... + generalize heapUpdateAt.proof_1 index = h₁ -- this sounds fragile... It's the n > 0 proof split case isTrue h => simp only [←hj, beq_iff_eq, Fin.mk.injEq, Nat.add_one_ne_zero] at h --contradiction case isFalse => @@ -32,23 +33,25 @@ theorem heapUpdateAtReturnsElementAt {α : Type u} {n : Nat} (le : α → α → rw[get_left] case h₂ => exact Nat.succ_pos j case h₃ => - rw[leftLen_unfold] + rw[leftLen_unfold _ _ _ _ _ _ (Nat.succ_pos _)] exact h₂ apply heapUpdateAtReturnsElementAt case isFalse h₂ => - rw[get_right] + rw[get_right _ _] + case h₁ => exact Nat.succ_pos _ case h₂ => simp only [Nat.not_le] at h₂ simp only [leftLen_unfold, gt_iff_lt, h₂] apply heapUpdateAtReturnsElementAt -theorem heapUpdatAtRootEqUpdateRoot {α : Type u} {le : α → α → Bool} : CompleteTree.heapUpdateAt le ⟨0, h₁⟩ = CompleteTree.heapUpdateRoot le := by +theorem heapUpdatAtRootEqUpdateRoot {α : Type u} {le : α → α → Bool} : CompleteTree.heapUpdateAt le ⟨0, h₁⟩ = CompleteTree.heapUpdateRoot h₁ le := by funext - unfold heapUpdateAt + unfold heapUpdateAt heapUpdateAtAux rfl -theorem heapUpdateAtContainsValue {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α n) (h₁ : n > 0) (value : α) (index : Fin n) : (heap.heapUpdateAt le index value h₁).fst.contains value := by - unfold heapUpdateAt +theorem heapUpdateAtContainsValue {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α n) (value : α) (index : Fin n) : (heap.heapUpdateAt le index value).fst.contains value := by + unfold heapUpdateAt heapUpdateAtAux + generalize heapUpdateAt.proof_1 index = h₁ split case isTrue h₂ => apply heapUpdateRootContainsUpdatedElement @@ -77,16 +80,18 @@ theorem heapUpdateAtContainsValue {α : Type u} {n : Nat} (le : α → α → Bo apply heapUpdateAtContainsValue termination_by n -theorem heapUpdateAtOnlyUpdatesAt {α : Type u} {n : Nat} (le : α → α → Bool) (val : α) (heap : CompleteTree α n) (updateIndex : Fin n) (otherIndex : Fin n) (h₁ : n > 0) (h₂ : updateIndex ≠ otherIndex) : (heap.heapUpdateAt le updateIndex val h₁).fst.contains $ heap.get otherIndex h₁ := +theorem heapUpdateAtOnlyUpdatesAt {α : Type u} {n : Nat} (le : α → α → Bool) (val : α) (heap : CompleteTree α n) (updateIndex : Fin n) (otherIndex : Fin n) (h₂ : updateIndex ≠ otherIndex) : (heap.heapUpdateAt le updateIndex val).fst.contains $ heap.get otherIndex := + have h₁ : n > 0 := Nat.zero_lt_of_lt otherIndex.isLt if h₃ : updateIndex = ⟨0, h₁⟩ then have h₄ : otherIndex ≠ ⟨0, h₁⟩ := h₃.subst h₂.symm heapUpdateRootOnlyUpdatesRoot le heap h₁ otherIndex h₄ val - |> heapUpdatAtRootEqUpdateRoot.substr (p := λx↦(x val heap h₁).fst.contains (heap.get otherIndex h₁)) - |> h₃.substr (p := λx↦((heap.heapUpdateAt le x val h₁).fst.contains $ heap.get otherIndex h₁)) + |> heapUpdatAtRootEqUpdateRoot.substr (p := λx↦(x val heap).fst.contains (heap.get otherIndex)) + |> h₃.substr (p := λx↦((heap.heapUpdateAt le x val).fst.contains $ heap.get otherIndex)) else if h₄ : otherIndex = ⟨0, h₁⟩ then by subst h₄ rw[←get_zero_eq_root] - unfold heapUpdateAt + unfold heapUpdateAt heapUpdateAtAux + generalize heapUpdateAt.proof_1 updateIndex = h₁ --cannot use h₃ here already - it makes split fail. So, splitting twice it is... split case isTrue h => exact absurd ((beq_iff_eq _ _).mp h) h₃ @@ -116,7 +121,8 @@ theorem heapUpdateAtOnlyUpdatesAt {α : Type u} {n : Nat} (le : α → α → Bo rewrite[root_unfold] apply heapUpdateAtContainsValue else by - unfold heapUpdateAt + unfold heapUpdateAt heapUpdateAtAux + generalize heapUpdateAt.proof_1 updateIndex = h₁ split case isTrue hx => exact absurd ((beq_iff_eq _ _).mp hx) h₃ case isFalse => @@ -152,6 +158,9 @@ theorem heapUpdateAtOnlyUpdatesAt {α : Type u} {n : Nat} (le : α → α → Bo rw[contains_iff_index_exists] generalize (⟨↑otherIndex - o - 1, _⟩ : Fin _) = solution -- Allows to skip the annoying proof that Lean already has... exists solution --also solves h.h₁ goal? Okay, I don't know why, but I won't complain. + rw[rightLen_unfold] + 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 + omega case false.isFalse h₅ | true.isFalse h₅ => if h₆ : otherIndex ≤ o then have : otherIndex ≤ (branch v l r olep mhd stc).leftLen (Nat.succ_pos _) := by simp only [leftLen_unfold, h₆] @@ -162,6 +171,8 @@ theorem heapUpdateAtOnlyUpdatesAt {α : Type u} {n : Nat} (le : α → α → Bo rw[contains_iff_index_exists] generalize (⟨↑otherIndex - 1, _⟩ : Fin _) = solution exists solution + rw[leftLen_unfold] + omega else have h₆ : otherIndex > (branch v l r olep mhd stc).leftLen (Nat.succ_pos _) := by rw[leftLen_unfold]; exact Nat.gt_of_not_le h₆ rw[get_right _ _ (Nat.succ_pos _) h₆] diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean index 9912bf3..cd765bb 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean @@ -16,8 +16,8 @@ abbrev heapUpdateRootReturnsRoot {α : Type u} {n : Nat} (le : α → α → Boo This is not a rigorous proof that the rest of the tree remained unchanged. See comment on heapPopOnlyRemovesRoot. Imho it is still a good indication that there are no obvious bugs. -/ -theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α → Bool) (tree : CompleteTree α n) (h₁ : n > 0) (index : Fin n) (h₂ : index ≠ ⟨0, h₁⟩) (value : α) : (tree.heapUpdateRoot le value h₁).fst.contains $ tree.get index h₁ := by - generalize h₃ : (get index tree h₁) = oldVal +theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α → Bool) (tree : CompleteTree α n) (h₁ : n > 0) (index : Fin n) (h₂ : index ≠ ⟨0, h₁⟩) (value : α) : (tree.heapUpdateRoot h₁ le value).fst.contains $ tree.get index := by + generalize h₃ : (get index tree) = oldVal unfold get at h₃ unfold heapUpdateRoot split @@ -163,7 +163,7 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α simp only [Nat.add_one_ne_zero, not_false_eq_true] termination_by n -theorem heapUpdateRootContainsUpdatedElement {α : Type u} {n : Nat} (tree : CompleteTree α n) (le : α → α → Bool) (value : α) (h₁ : n > 0): (tree.heapUpdateRoot le value h₁).fst.contains value := by +theorem heapUpdateRootContainsUpdatedElement {α : Type u} {n : Nat} (tree : CompleteTree α n) (le : α → α → Bool) (value : α) (h₁ : n > 0): (tree.heapUpdateRoot h₁ le value).fst.contains value := by unfold heapUpdateRoot split rename_i o p v l r _ _ _ h₁ diff --git a/BinaryHeap/CompleteTree/HeapOperations.lean b/BinaryHeap/CompleteTree/HeapOperations.lean index f3ff41c..aa2eb2c 100644 --- a/BinaryHeap/CompleteTree/HeapOperations.lean +++ b/BinaryHeap/CompleteTree/HeapOperations.lean @@ -200,7 +200,7 @@ protected def Internal.heapRemoveLastWithIndex {α : Type u} {o : Nat} (heap : C /-- Helper for heapUpdateAt. Makes proofing heap predicate work in Lean 4.9 -/ -def heapUpdateRoot {α : Type u} {n : Nat} (le : α → α → Bool) (value : α) (heap : CompleteTree α n) (_ : n > 0) : CompleteTree α n × α := +def heapUpdateRoot {α : Type u} {n : Nat} (_ : n > 0) (le : α → α → Bool) (value : α) (heap : CompleteTree α n) : CompleteTree α n × α := match n, heap with | (o+p+1), .branch v l r h₃ h₄ h₅ => if h₆ : o = 0 then @@ -216,7 +216,7 @@ match n, heap with -- We would not need to recurse further, because we know o = 1. -- However, that would introduce type casts, what makes proving harder... -- have h₉: o = 1 := Nat.le_antisymm (by simp_arith[h₈] at h₄; exact h₄) (Nat.succ_le_of_lt h₇) - let ln := heapUpdateRoot le value l h₇ + let ln := heapUpdateRoot h₇ le value l (.branch ln.snd ln.fst r h₃ h₄ h₅, v) else have h₉ : p > 0 := Nat.zero_lt_of_ne_zero h₈ @@ -224,23 +224,18 @@ match n, heap with if le value lr ∧ le value rr then (.branch value l r h₃ h₄ h₅, v) else if le lr rr then -- value is gt either left or right root. Move it down accordingly - let ln := heapUpdateRoot le value l h₇ + let ln := heapUpdateRoot h₇ le value l (.branch ln.snd ln.fst r h₃ h₄ h₅, v) else - let rn := heapUpdateRoot le value r h₉ + let rn := heapUpdateRoot h₉ le value r (.branch rn.snd l rn.fst h₃ h₄ h₅, v) ---------------------------------------------------------------------------------------------- -- heapRemoveAt -/-- - Helper for heapRemoveAt. - Removes the element at index, and instead inserts the given value. - Returns the element at index, and the resulting tree. - -/ -def heapUpdateAt {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin n) (value : α) (heap : CompleteTree α n) (h₁ : n > 0) : CompleteTree α n × α := +def heapUpdateAtAux {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin n) (value : α) (heap : CompleteTree α n) (h₁ : n > 0) : CompleteTree α n × α := if h₂ : index == ⟨0,h₁⟩ then - heapUpdateRoot le value heap h₁ + heapUpdateRoot h₁ le value heap else match n, heap with | (o+p+1), .branch v l r h₃ h₄ h₅ => @@ -249,7 +244,7 @@ def heapUpdateAt {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin have h₇ : Nat.pred index.val < o := Nat.lt_of_lt_of_le (Nat.pred_lt $ Fin.val_ne_of_ne (ne_of_beq_false $ Bool.of_not_eq_true h₂)) h₆ let index_in_left : Fin o := ⟨index.val.pred, h₇⟩ have h₈ : 0 < o := Nat.zero_lt_of_lt h₇ - let result := heapUpdateAt le index_in_left value l h₈ + let result := heapUpdateAtAux le index_in_left value l h₈ (.branch v result.fst r h₃ h₄ h₅, result.snd) else have h₇ : index.val - (o + 1) < p := @@ -262,16 +257,24 @@ def heapUpdateAt {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin Nat.sub_lt_of_lt_add h₈ $ (Nat.not_le_eq index.val o).mp h₆ let index_in_right : Fin p := ⟨index.val - o - 1, h₇⟩ have h₈ : 0 < p := Nat.zero_lt_of_lt h₇ - let result := heapUpdateAt le index_in_right value r h₈ + let result := heapUpdateAtAux le index_in_right value r h₈ (.branch v l result.fst h₃ h₄ h₅, result.snd) +/-- + Helper for heapRemoveAt. + Removes the element at index, and instead inserts the given value. + Returns the element at index, and the resulting tree. + -/ +def heapUpdateAt {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin n) (value : α) (heap : CompleteTree α n) : CompleteTree α n × α := + heapUpdateAtAux le index value heap (Nat.zero_lt_of_lt index.isLt) + ---------------------------------------------------------------------------------------------- -- heapPop def heapPop {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α (n+1)) : CompleteTree α n × α := let l := Internal.heapRemoveLast heap if p : n > 0 then - heapUpdateRoot le l.snd l.fst p + heapUpdateRoot p le l.snd l.fst else l @@ -288,17 +291,13 @@ def heapRemoveAt {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin heapPop le heap else let (remaining_tree, removed_element, removed_index) := Internal.heapRemoveLastWithIndex heap - if p : index = removed_index then + if index = removed_index then (remaining_tree, removed_element) else - have n_gt_zero : n > 0 := by - cases n - case succ nn => exact Nat.zero_lt_succ nn - case zero => omega if index_lt_lastIndex : index ≥ removed_index then let index := index.pred index_ne_zero - heapUpdateAt le index removed_element remaining_tree n_gt_zero + heapUpdateAt le index removed_element remaining_tree else let h₁ : index < n := by omega let index : Fin n := ⟨index, h₁⟩ - heapUpdateAt le index removed_element remaining_tree n_gt_zero + heapUpdateAt le index removed_element remaining_tree diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean index 295fcbd..32e6fb9 100644 --- a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean +++ b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean @@ -5,11 +5,12 @@ import BinaryHeap.CompleteTree.HeapProofs.HeapUpdateRoot namespace BinaryHeap.CompleteTree -private theorem heapUpdateAtIsHeapLeRootAux_RootLeValue {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin n) (value : α) (heap : CompleteTree α n) (h₁ : HeapPredicate heap le) (h₂ : n > 0) (h₃ : le (root heap h₂) value) (h₄ : total_le le) : HeapPredicate.leOrLeaf le (root heap h₂) (heapUpdateAt le index value heap h₂).fst := by - unfold heapUpdateAt +private theorem heapUpdateAtIsHeapLeRootAux_RootLeValue {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin n) (value : α) (heap : CompleteTree α n) (h₁ : HeapPredicate heap le) (h₂ : n > 0) (h₃ : le (root heap h₂) value) (h₄ : total_le le) : HeapPredicate.leOrLeaf le (root heap h₂) (heapUpdateAt le index value heap).fst := by + unfold heapUpdateAt heapUpdateAtAux split case isTrue => exact CompleteTree.heapUpdateRootIsHeapLeRootAux le value heap h₁ h₂ h₃ case isFalse hi => + generalize heapUpdateAt.proof_1 index = h₂ split rename_i o p v l r h₆ h₇ h₈ index h₁ h₅ cases h₉ : le v value <;> simp (config := { ground := true }) only @@ -19,8 +20,9 @@ private theorem heapUpdateAtIsHeapLeRootAux_RootLeValue {α : Type u} {n : Nat} split <;> simp![reflexive_le, h₄] -private theorem heapUpdateAtIsHeapLeRootAux_ValueLeRoot {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin n) (value : α) (heap : CompleteTree α n) (h₁ : HeapPredicate heap le) (h₂ : n > 0) (h₃ : le value (root heap h₂)) (h₄ : total_le le) (h₅ : transitive_le le) : HeapPredicate.leOrLeaf le value (heapUpdateAt le index value heap h₂).fst := by - unfold heapUpdateAt +private theorem heapUpdateAtIsHeapLeRootAux_ValueLeRoot {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin n) (value : α) (heap : CompleteTree α n) (h₁ : HeapPredicate heap le) (h₂ : n > 0) (h₃ : le value (root heap h₂)) (h₄ : total_le le) (h₅ : transitive_le le) : HeapPredicate.leOrLeaf le value (heapUpdateAt le index value heap).fst := by + unfold heapUpdateAt heapUpdateAtAux + generalize heapUpdateAt.proof_1 index = h₂ split <;> rename_i h₉ case isTrue => @@ -42,11 +44,12 @@ private theorem heapUpdateAtIsHeapLeRootAux_ValueLeRoot {α : Type u} {n : Nat} <;> unfold HeapPredicate.leOrLeaf <;> simp only [root_unfold, h₃, h₄, reflexive_le] -theorem heapUpdateAtIsHeap {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin n) (value : α) (heap : CompleteTree α n) (h₁ : n > 0) (h₂ : HeapPredicate heap le) (h₃ : transitive_le le) (h₄ : total_le le) : HeapPredicate (heap.heapUpdateAt le index value h₁).fst le := by - unfold heapUpdateAt +theorem heapUpdateAtIsHeap {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin n) (value : α) (heap : CompleteTree α n) (h₂ : HeapPredicate heap le) (h₃ : transitive_le le) (h₄ : total_le le) : HeapPredicate (heap.heapUpdateAt le index value).fst le := by + unfold heapUpdateAt heapUpdateAtAux + generalize heapUpdateAt.proof_1 index = h₁ split case isTrue h₅ => - exact heapUpdateRootIsHeap le value heap h₁ h₂ h₃ h₄ + exact heapUpdateRootIsHeap le value heap _ h₂ h₃ h₄ case isFalse h₅ => split rename_i o p v l r h₆ h₇ h₈ index h₁ h₅ @@ -59,11 +62,11 @@ theorem heapUpdateAtIsHeap {α : Type u} {n : Nat} (le : α → α → Bool) (in have h₁₀ := not_le_imp_le h₄ v value (Bool.eq_false_iff.mp h₁₀) have h₁₄ : p > 0 := by cases p; exact absurd (Nat.lt_succ.mp index.isLt) h; exact Nat.zero_lt_succ _ apply And.intro <;> try apply And.intro - case left => exact heapUpdateAtIsHeap le ⟨index.val - o - 1, _⟩ v r h₁₄ h₂.right.left h₃ h₄ + case left => exact heapUpdateAtIsHeap le ⟨index.val - o - 1, _⟩ v r h₂.right.left h₃ h₄ case right.left => exact HeapPredicate.leOrLeaf_transitive h₃ h₁₀ h₂.right.right.left case right.right => - have h₁₁: HeapPredicate (heapUpdateAt le ⟨index.val - o - 1, (by omega)⟩ v r h₁₄).fst le := - (heapUpdateAtIsHeap le ⟨index.val - o - 1, (by omega)⟩ v r _ h₂.right.left h₃ h₄) + have h₁₁: HeapPredicate (heapUpdateAt le ⟨index.val - o - 1, (by omega)⟩ v r).fst le := + (heapUpdateAtIsHeap le ⟨index.val - o - 1, (by omega)⟩ v r h₂.right.left h₃ h₄) cases h₁₂ : le v (r.root h₁₄) case false => cases p @@ -77,11 +80,11 @@ theorem heapUpdateAtIsHeap {α : Type u} {n : Nat} (le : α → α → Bool) (in have h₁₀ := not_le_imp_le h₄ v value (Bool.eq_false_iff.mp h₁₀) have h₁₄ : o > 0 := by cases o; simp at h₅ h; exact absurd (Fin.val_inj.mp h : index = 0) h₅; exact Nat.zero_lt_succ _ apply And.intro <;> try apply And.intro - case left => exact heapUpdateAtIsHeap le ⟨index.val - 1, _⟩ v l h₁₄ h₂.left h₃ h₄ + case left => exact heapUpdateAtIsHeap le ⟨index.val - 1, _⟩ v l h₂.left h₃ h₄ case right.right => exact HeapPredicate.leOrLeaf_transitive h₃ h₁₀ h₂.right.right.right case right.left => - have h₁₁: HeapPredicate (heapUpdateAt le ⟨index.val - 1, (_)⟩ v l h₁₄).fst le := - (heapUpdateAtIsHeap le ⟨index.val - 1, (by omega)⟩ v l _ h₂.left h₃ h₄) + have h₁₁: HeapPredicate (heapUpdateAt le ⟨index.val - 1, (_)⟩ v l).fst le := + (heapUpdateAtIsHeap le ⟨index.val - 1, (by omega)⟩ v l h₂.left h₃ h₄) cases h₁₂ : le v (l.root h₁₄) case false => cases o @@ -94,10 +97,10 @@ theorem heapUpdateAtIsHeap {α : Type u} {n : Nat} (le : α → α → Bool) (in case true.isFalse => have h₁₄ : p > 0 := by cases p; exact absurd (Nat.lt_succ.mp index.isLt) h; exact Nat.zero_lt_succ _ apply And.intro - case left => exact heapUpdateAtIsHeap le ⟨index.val - o - 1, _⟩ value r h₁₄ h₂.right.left h₃ h₄ + case left => exact heapUpdateAtIsHeap le ⟨index.val - o - 1, _⟩ value r h₂.right.left h₃ h₄ case right => - have h₁₁: HeapPredicate (heapUpdateAt le ⟨index.val - o - 1, (by omega)⟩ v r (h₁₄)).fst le := - (heapUpdateAtIsHeap le ⟨index.val - o - 1, (by omega)⟩ v r _ h₂.right.left h₃ h₄) + have h₁₁: HeapPredicate (heapUpdateAt le ⟨index.val - o - 1, (by omega)⟩ v r).fst le := + (heapUpdateAtIsHeap le ⟨index.val - o - 1, (by omega)⟩ v r h₂.right.left h₃ h₄) cases h₁₂ : le value (r.root h₁₄) case false => have h₁₃ := heapUpdateAtIsHeapLeRootAux_RootLeValue le ⟨index.val - o - 1, (by omega)⟩ value r h₂.right.left (by omega) (not_le_imp_le h₄ value (r.root h₁₄) (Bool.eq_false_iff.mp h₁₂)) h₄ @@ -112,10 +115,10 @@ theorem heapUpdateAtIsHeap {α : Type u} {n : Nat} (le : α → α → Bool) (in case true.isTrue => have h₁₄ : o > 0 := by cases o; simp at h₅ h; exact absurd (Fin.val_inj.mp h : index = 0) h₅; exact Nat.zero_lt_succ _ apply And.intro - case left => exact heapUpdateAtIsHeap le ⟨index.val - 1, _⟩ value l h₁₄ h₂.left h₃ h₄ + case left => exact heapUpdateAtIsHeap le ⟨index.val - 1, _⟩ value l h₂.left h₃ h₄ case right => - have h₁₁: HeapPredicate (heapUpdateAt le ⟨index.val - 1, (by omega)⟩ v l h₁₄).fst le := - (heapUpdateAtIsHeap le ⟨index.val - 1, (by omega)⟩ v l _ h₂.left h₃ h₄) + have h₁₁: HeapPredicate (heapUpdateAt le ⟨index.val - 1, (by omega)⟩ v l).fst le := + (heapUpdateAtIsHeap le ⟨index.val - 1, (by omega)⟩ v l h₂.left h₃ h₄) cases h₁₂ : le value (l.root h₁₄) case false => have h₁₃ := heapUpdateAtIsHeapLeRootAux_RootLeValue le ⟨index.val - 1, (by omega)⟩ value l h₂.left (by omega) (not_le_imp_le h₄ value (l.root h₁₄) (Bool.eq_false_iff.mp h₁₂)) h₄ diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean index e930a30..c6b421f 100644 --- a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean +++ b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean @@ -3,7 +3,7 @@ import BinaryHeap.CompleteTree.Lemmas namespace BinaryHeap.CompleteTree -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 h₁ le value).snd = heap.root h₁ := by unfold heapUpdateRoot split rename_i o p v l r h₃ h₄ h₅ h₁ @@ -37,7 +37,7 @@ private theorem heapUpdateRootPossibleRootValuesAuxR {α : Type u} (heap : Compl case zero => simp_arith at h₁; simp at h₃; exact absurd h₁ (Nat.not_le_of_gt h₃) case succ q => exact Nat.zero_lt_succ q -private theorem heapUpdateRootPossibleRootValues1 {α : Type u} (le : α → α → Bool) (value : α) (heap : CompleteTree α n) (h₁ : n = 1) : (heap.heapUpdateRoot le value (h₁.substr (Nat.lt_succ_self 0))).fst.root (h₁.substr (Nat.lt_succ_self 0)) = value := by +private theorem heapUpdateRootPossibleRootValues1 {α : Type u} (le : α → α → Bool) (value : α) (heap : CompleteTree α n) (h₁ : n = 1) : (heap.heapUpdateRoot (h₁.substr (p := λx ↦ 0<x) (Nat.lt_succ_self 0)) le value).fst.root (h₁.substr (Nat.lt_succ_self 0)) = value := by unfold heapUpdateRoot generalize (h₁.substr (Nat.lt_succ_self 0) : n > 0) = hx split @@ -48,8 +48,8 @@ private theorem heapUpdateRootPossibleRootValues1 {α : Type u} (le : α → α private theorem heapUpdateRootPossibleRootValues2 {α : Type u} (le : α → α → Bool) (value : α) (heap : CompleteTree α n) (h₁ : n = 2) : have h₂ : 0 < n := Nat.lt_trans (Nat.lt_succ_self 0) $ h₁.substr (Nat.lt_succ_self 1) have h₃ : 0 < leftLen heap h₂ := heapUpdateRootPossibleRootValuesAuxL heap (h₁.substr (Nat.lt_succ_self 1)) -(heap.heapUpdateRoot le value h₂).fst.root h₂ = value -∨ (heap.heapUpdateRoot le value h₂).fst.root h₂ = (heap.left h₂).root h₃ +(heap.heapUpdateRoot h₂ le value).fst.root h₂ = value +∨ (heap.heapUpdateRoot h₂ le value).fst.root h₂ = (heap.left h₂).root h₃ := by simp unfold heapUpdateRoot @@ -68,9 +68,9 @@ private theorem heapUpdateRootPossibleRootValues3 {α : Type u} (le : α → α have h₂ : 0 < n := Nat.lt_trans (Nat.lt_succ_self 0) $ Nat.lt_trans (Nat.lt_succ_self 1) h₁ have h₃ : 0 < leftLen heap h₂ := heapUpdateRootPossibleRootValuesAuxL heap $ Nat.lt_trans (Nat.lt_succ_self 1) h₁ have h₄ : 0 < rightLen heap h₂ := heapUpdateRootPossibleRootValuesAuxR heap h₁ -(heap.heapUpdateRoot le value h₂).fst.root h₂ = value -∨ (heap.heapUpdateRoot le value h₂).fst.root h₂ = (heap.left h₂).root h₃ -∨ (heap.heapUpdateRoot le value h₂).fst.root h₂ = (heap.right h₂).root h₄ +(heap.heapUpdateRoot h₂ le value).fst.root h₂ = value +∨ (heap.heapUpdateRoot h₂ le value).fst.root h₂ = (heap.left h₂).root h₃ +∨ (heap.heapUpdateRoot h₂ le value).fst.root h₂ = (heap.right h₂).root h₄ := by simp only unfold heapUpdateRoot @@ -90,9 +90,9 @@ have h₄ : 0 < rightLen heap h₂ := heapUpdateRootPossibleRootValuesAuxR heap cases le (l.root _) (r.root _) <;> simp only [Bool.false_eq_true, ↓reduceIte, heapUpdateRootReturnsRoot, root_unfold, left_unfold, right_unfold, true_or, or_true] -protected theorem heapUpdateRootIsHeapLeRootAux {α : Type u} (le : α → α → Bool) (value : α) (heap : CompleteTree α n) (h₁ : HeapPredicate heap le) (h₂ : n > 0) (h₃ : le (root heap h₂) value) : HeapPredicate.leOrLeaf le (root heap h₂) (heapUpdateRoot le value heap h₂).fst := +protected theorem heapUpdateRootIsHeapLeRootAux {α : Type u} (le : α → α → Bool) (value : α) (heap : CompleteTree α n) (h₁ : HeapPredicate heap le) (h₂ : n > 0) (h₃ : le (root heap h₂) value) : HeapPredicate.leOrLeaf le (root heap h₂) (heapUpdateRoot h₂ le value heap).fst := if h₄ : n = 1 then by - have h₅ : le (heap.root h₂) ( (heapUpdateRoot le value heap h₂).fst.root h₂) := by simp only[h₃, h₄, heapUpdateRootPossibleRootValues1] + have h₅ : le (heap.root h₂) ( (heapUpdateRoot h₂ le value heap).fst.root h₂) := by simp only[h₃, h₄, heapUpdateRootPossibleRootValues1] unfold HeapPredicate.leOrLeaf split · rfl @@ -101,7 +101,7 @@ protected theorem heapUpdateRootIsHeapLeRootAux {α : Type u} (le : α → α have h₆ := heapUpdateRootPossibleRootValues2 le value heap h₅ cases h₆ case inl h₆ => - have h₇ : le (heap.root h₂) ( (heapUpdateRoot le value heap h₂).fst.root h₂) := by simp only [h₆, h₃] + have h₇ : le (heap.root h₂) ((heapUpdateRoot h₂ le value heap).fst.root h₂) := by simp only [h₆, h₃] unfold HeapPredicate.leOrLeaf split · rfl @@ -130,7 +130,7 @@ protected theorem heapUpdateRootIsHeapLeRootAux {α : Type u} (le : α → α unfold HeapPredicate at h₁ cases h₇ case inl h₇ => - have h₈ : le (heap.root h₂) ( (heapUpdateRoot le value heap h₂).fst.root h₂) := by simp only [h₇, h₃] + have h₈ : le (heap.root h₂) ( (heapUpdateRoot h₂ le value heap).fst.root h₂) := by simp only [h₇, h₃] unfold HeapPredicate.leOrLeaf split · rfl @@ -155,7 +155,7 @@ private theorem heapUpdateRootIsHeapLeRootAuxLe {α : Type u} (le : α → α | .inr h₅ => not_le_imp_le h₂ _ _ h₅ | .inl h₅ => h₁ b c a ⟨h₃,not_le_imp_le h₂ _ _ h₅⟩ -theorem heapUpdateRootIsHeap {α : Type u} {n: Nat} (le : α → α → Bool) (value : α) (heap : CompleteTree α n) (h₁ : n > 0) (h₂ : HeapPredicate heap le) (h₃ : transitive_le le) (h₄ : total_le le) : HeapPredicate (heap.heapUpdateRoot le value h₁).fst le := by +theorem heapUpdateRootIsHeap {α : Type u} {n: Nat} (le : α → α → Bool) (value : α) (heap : CompleteTree α n) (h₁ : n > 0) (h₂ : HeapPredicate heap le) (h₃ : transitive_le le) (h₄ : total_le le) : HeapPredicate (heap.heapUpdateRoot h₁ le value).fst le := by unfold heapUpdateRoot split rename_i o p v l r h₇ h₈ h₉ heq |