diff options
| -rw-r--r-- | BinaryHeap.lean | 4 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalOperations.lean | 18 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs.lean | 146 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/HeapOperations.lean | 32 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/HeapProofs.lean | 2 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/Lemmas.lean | 23 |
6 files changed, 190 insertions, 35 deletions
diff --git a/BinaryHeap.lean b/BinaryHeap.lean index 9d1da1b..779c3ed 100644 --- a/BinaryHeap.lean +++ b/BinaryHeap.lean @@ -54,11 +54,11 @@ def indexOf {α : Type u} {le : α → α → Bool} {n : Nat} : BinaryHeap α le instance : GetElem (BinaryHeap α le n) (Nat) α (λ _ index ↦ index > 0 ∧ index < n) where getElem := λ heap index h₁ ↦ match n, heap, index with - | (_+1), {tree, ..}, index => tree.get ⟨index, h₁.right⟩ + | (_+1), {tree, ..}, index => tree.get' ⟨index, h₁.right⟩ instance : GetElem (BinaryHeap α le n) (Fin n) α (λ _ _ ↦ n > 0) where getElem := λ heap index _ ↦ match n, heap, index with - | (_+1), {tree, ..}, index => tree.get index + | (_+1), {tree, ..}, index => tree.get' index /--Helper for the common case of using natural numbers for sorting.-/ theorem nat_ble_to_heap_le_total : total_le Nat.ble := by diff --git a/BinaryHeap/CompleteTree/AdditionalOperations.lean b/BinaryHeap/CompleteTree/AdditionalOperations.lean index 3327e70..1caf47d 100644 --- a/BinaryHeap/CompleteTree/AdditionalOperations.lean +++ b/BinaryHeap/CompleteTree/AdditionalOperations.lean @@ -1,13 +1,13 @@ import BinaryHeap.CompleteTree.Basic import BinaryHeap.CompleteTree.NatLemmas -namespace BinaryHeap +namespace BinaryHeap.CompleteTree ---------------------------------------------------------------------------------------------- -- indexOf /--Helper function for CompleteTree.indexOf.-/ -private def CompleteTree.indexOfAux {α : Type u} (heap : CompleteTree α o) (pred : α → Bool) (currentIndex : Nat) : Option (Fin (o+currentIndex)) := +private def indexOfAux {α : Type u} (heap : CompleteTree α o) (pred : α → Bool) (currentIndex : Nat) : Option (Fin (o+currentIndex)) := match o, heap with | 0, .leaf => none | (n+m+1), .branch a left right _ _ _ => @@ -25,7 +25,7 @@ private def CompleteTree.indexOfAux {α : Type u} (heap : CompleteTree α o) (pr found_right /--Finds the first occurance of a given element in the heap and returns its index. Indices are depth first.-/ -def CompleteTree.indexOf {α : Type u} (heap : CompleteTree α o) (pred : α → Bool) : Option (Fin o) := +def indexOf {α : Type u} (heap : CompleteTree α o) (pred : α → Bool) : Option (Fin o) := indexOfAux heap pred 0 @@ -33,13 +33,13 @@ def CompleteTree.indexOf {α : Type u} (heap : CompleteTree α o) (pred : α → -- get /--Returns the lement at the given index. Indices are depth first.-/ -def CompleteTree.get {α : Type u} {n : Nat} (index : Fin (n+1)) (heap : CompleteTree α (n+1)) : α := +def get' {α : Type u} {n : Nat} (index : Fin (n+1)) (heap : CompleteTree α (n+1)) : α := match h₁ : index, h₂ : n, heap with | 0, (_+_), .branch v _ _ _ _ _ => v | ⟨j+1,h₃⟩, (o+p), .branch _ l r _ _ _ => if h₄ : j < o then match o with - | (oo+1) => get ⟨j, h₄⟩ l + | (oo+1) => get' ⟨j, h₄⟩ l else have h₅ : n - o = p := Nat.sub_eq_of_eq_add $ (Nat.add_comm o p).subst h₂ have : p ≠ 0 := @@ -48,12 +48,16 @@ def CompleteTree.get {α : Type u} {n : Nat} (index : Fin (n+1)) (heap : Complet have h₆ : j - o < p := h₅.subst $ Nat.sub_lt_sub_right (Nat.ge_of_not_lt h₄) $ Nat.lt_of_succ_lt_succ h₃ have _termination : j - o < index.val := (Fin.val_inj.mpr h₁).substr (Nat.sub_lt_succ j o) match p with - | (pp + 1) => get ⟨j - o, h₆⟩ r + | (pp + 1) => get' ⟨j - o, h₆⟩ r + +def get {α : Type u} {n : Nat} (index : Fin n) (heap : CompleteTree α n) (_ : n > 0) : α := + match n, index, heap with + | (_+1), index, heap => heap.get' index ---------------------------------------------------------------------------------------------- -- contains - implemented as decidable proposition -def CompleteTree.contains {α : Type u} {n : Nat} (tree : CompleteTree α n) (element : α) : Prop := +def contains {α : Type u} {n : Nat} (tree : CompleteTree α n) (element : α) : Prop := match n, tree with | 0, .leaf => False | (_+_+1), .branch v l r _ _ _ => v = element ∨ (l.contains element) ∨ (r.contains element) diff --git a/BinaryHeap/CompleteTree/AdditionalProofs.lean b/BinaryHeap/CompleteTree/AdditionalProofs.lean index ad626e7..1b3ef50 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs.lean @@ -2,17 +2,153 @@ import BinaryHeap.CompleteTree.Lemmas import BinaryHeap.CompleteTree.AdditionalOperations import BinaryHeap.CompleteTree.HeapOperations -namespace BinaryHeap +namespace BinaryHeap.CompleteTree.AdditionalProofs + +private theorem if_get_eq_contains {α : Type u} {o : Nat} (tree : CompleteTree α (o+1)) (element : α) (index : Fin (o+1)) : tree.get' index = element → tree.contains element := by + unfold get' contains + simp only [Nat.succ_eq_add_one, Fin.zero_eta, Nat.add_eq, ne_eq] + split + case h_1 p q v l r _ _ _ _ => + intro h₁ + split; omega + rename α => vv + rename_i hsum heq + have h₂ := heqSameRoot (hsum) (Nat.succ_pos (p+q)) heq + rw[root_unfold] at h₂ + rw[root_unfold] at h₂ + simp only [←h₂, h₁, true_or] + case h_2 index p q v l r _ _ _ _ h₃ => + intro h₄ + split ; rename_i hx _; exact absurd hx (Nat.succ_ne_zero _) + case h_2 pp qq vv ll rr _ _ _ h₅ heq => + have : p = pp := heqSameLeftLen h₅ (Nat.succ_pos _) heq + have : q = qq := heqSameRightLen h₅ (Nat.succ_pos _) heq + subst pp qq + simp only [Nat.add_eq, Nat.succ_eq_add_one, heq_eq_eq, branch.injEq] at heq + have : v = vv := heq.left + have : l = ll := heq.right.left + have : r = rr := heq.right.right + subst vv ll rr + revert h₄ + split + all_goals + split + intro h₄ + right + case' isTrue => left + case' isFalse => right + all_goals + revert h₄ + 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 +:= 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] + exact Nat.lt_of_lt_of_le indexl.isLt $ Nat.le_of_lt_succ $ leftLenLtN tree (Nat.succ_pos o) + ) + intro prereq + exists index + unfold get + simp + unfold get' + generalize hindex : index = i + split + case h_1 => + have : index.val = 0 := Fin.val_eq_of_eq hindex + contradiction + case h_2 j p q v l r ht1 ht2 ht3 _ _ => + have h₂ : index.val = indexl.val + 1 := rfl + have h₃ : index.val = j.succ := Fin.val_eq_of_eq hindex + have h₄ : j = indexl.val := Nat.succ.inj $ h₃.subst (motive := λx↦ x = indexl.val + 1) h₂ + have : p = (branch v l r ht1 ht2 ht3).leftLen (Nat.succ_pos _) := rfl + have h₅ : j < p := by simp only [this, indexl.isLt, h₄] + simp only [h₅, ↓reduceDite, Nat.add_eq] + unfold get at prereq + split at prereq + rename_i pp ii ll _ hel hei heq _ + split + 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 * + have : j = ii.val := by omega + subst j + simp + rw[←hei] at prereq + rw[left_unfold] at heq + rw[heq] + assumption + +private theorem if_contains_get_eq {α : Type u} {o : Nat} (tree : CompleteTree α (o+1)) (element : α) (h₁ : tree.contains element) : ∃(index : Fin (o+1)), tree.get' index = element := by + revert h₁ + unfold contains + split ; rename_i hx _; exact absurd hx (Nat.succ_ne_zero o) + rename_i n m v l r _ _ _ he heq + intro h₁ + cases h₁ + case h_2.inl h₂ => + unfold get' + exists 0 + split + case h_2 hx => have hx := Fin.val_eq_of_eq hx; simp at hx; + case h_1 vv _ _ _ _ _ _ _ => + have h₃ := heqSameRoot he (Nat.succ_pos _) heq + simp only[root_unfold] at h₃ + simp only[h₃, h₂] + rename_i h + cases h + case h_2.inr.inl h₂ => exact + match hn : n, hl: l with + | 0, .leaf => by contradiction + | (nn+1), l => by + have nn_lt_o : nn < o := by have : o = nn + 1 + m := Nat.succ.inj he; omega + have blah := if_contains_get_eq l element h₂ + have blupp := if_contains_get_eq_auxl tree element $ Nat.zero_lt_of_lt nn_lt_o + simp at blupp + simp[get_eq_get'] at blah ⊢ + apply blah.elim + match o, tree with + | (yy+_), .branch _ ll _ _ _ _ => + simp_all[left_unfold, leftLen_unfold] + have : yy = nn+1 := heqSameLeftLen (by omega) (Nat.succ_pos _) heq + subst yy + have : _ = m := heqSameRightLen (by omega) (Nat.succ_pos _) heq + subst m + simp_all + exact blupp + case h_2.inr.inr h₂ => sorry + termination_by o + + +theorem contains_iff_index_exists {α : Type u} {o : Nat} (tree : CompleteTree α (o+1)) (element : α) : tree.contains element ↔ ∃ (index : Fin (o+1)), tree.get' index = element := by + constructor + case mpr => + simp only [forall_exists_index] + exact if_get_eq_contains tree element + case mp => + exact if_contains_get_eq tree element /--Shows that the index and value returned by heapRemoveLastWithIndex are consistent.-/ -private theorem CompleteTree.heapRemoveLastWithIndexReturnsItemAtIndex {α : Type u} {o : Nat} (heap : CompleteTree α (o+1)) : heap.get heap.heapRemoveLastWithIndex.snd.snd = heap.heapRemoveLastWithIndex.snd.fst := by +protected theorem heapRemoveLastWithIndexReturnsItemAtIndex {α : Type u} {o : Nat} (heap : CompleteTree α (o+1)) : heap.get' heap.heapRemoveLastWithIndex.snd.snd = heap.heapRemoveLastWithIndex.snd.fst := by unfold CompleteTree.heapRemoveLastWithIndex CompleteTree.Internal.heapRemoveLastAux split rename_i n m v l r m_le_n max_height_difference subtree_full simp only [Nat.add_eq, Fin.zero_eta, Fin.isValue, decide_eq_true_eq, Fin.castLE_succ] split case isTrue n_m_zero => - unfold get + unfold get' split case h_1 nn mm vv ll rr mm_le_nn _ _ _ _ he₁ he₂ => have h₁ : n = 0 := And.left $ Nat.add_eq_zero.mp n_m_zero.symm @@ -24,7 +160,7 @@ private theorem CompleteTree.heapRemoveLastWithIndexReturnsItemAtIndex {α : Typ case h_2 => omega -- to annoying to deal with Fin.ofNat... There's a hypothesis that says 0 = ⟨1,_⟩. case isFalse n_m_not_zero => - unfold get + unfold get' split case h_1 nn mm vv ll rr mm_le_nn max_height_difference_2 subtree_full2 _ he₁ he₂ he₃ => --aaaaaaaaaaaaaaaaaaaaaaaaaaaaaa @@ -81,5 +217,5 @@ private theorem CompleteTree.heapRemoveLastWithIndexReturnsItemAtIndex {α : Typ simp only [this, ↓reduceDite, Nat.pred_succ, Fin.isValue] subst j -- overkill, but unlike rw it works simp only [Nat.pred_succ, Fin.isValue, Nat.add_sub_cancel, Fin.eta] - apply heapRemoveLastWithIndexReturnsItemAtIndex + apply AdditionalProofs.heapRemoveLastWithIndexReturnsItemAtIndex done diff --git a/BinaryHeap/CompleteTree/HeapOperations.lean b/BinaryHeap/CompleteTree/HeapOperations.lean index 337797c..1c9a27e 100644 --- a/BinaryHeap/CompleteTree/HeapOperations.lean +++ b/BinaryHeap/CompleteTree/HeapOperations.lean @@ -1,7 +1,7 @@ import BinaryHeap.CompleteTree.Basic import BinaryHeap.CompleteTree.NatLemmas -namespace BinaryHeap +namespace BinaryHeap.CompleteTree ---------------------------------------------------------------------------------------------- -- heapPush @@ -18,9 +18,9 @@ private theorem power_of_two_mul_two_lt {n m : Nat} (h₁ : m.isPowerOfTwo) (h Nat.lt_of_le_of_ne ((Nat.not_lt_eq _ _).mp h₄) h₅ /--Adds a new element to a given CompleteTree.-/ -def CompleteTree.heapPush (le : α → α → Bool) (elem : α) (heap : CompleteTree α o) : CompleteTree α (o+1) := +def heapPush (le : α → α → Bool) (elem : α) (heap : CompleteTree α o) : CompleteTree α (o+1) := match o, heap with - | 0, .leaf => CompleteTree.branch elem (CompleteTree.leaf) (CompleteTree.leaf) (by simp) (by simp) (by simp[Nat.one_isPowerOfTwo]) + | 0, .leaf => .branch elem (.leaf) (.leaf) (by simp) (by simp) (by simp[Nat.one_isPowerOfTwo]) | (n+m+1), .branch a left right p max_height_difference subtree_complete => let (elem, a) := if le elem a then (a, elem) else (elem, a) -- okay, based on n and m we know if we want to add left or right. @@ -95,7 +95,7 @@ private theorem power_of_two_mul_two_le {n m : Nat} (h₁ : (n+1).isPowerOfTwo) h₅.resolve_left h₆ /-- Helper for heapRemoveLastAux -/ -private theorem CompleteTree.removeRightRightNotEmpty {n m : Nat} (m_gt_0_or_rightIsFull : m > 0 ∨ ((m+1).nextPowerOfTwo = m+1 : Bool)) (h₁ : 0 ≠ n + m) (h₂ : ¬(m < n ∧ ((m+1).nextPowerOfTwo = m+1 : Bool))) : m > 0 := +private theorem removeRightRightNotEmpty {n m : Nat} (m_gt_0_or_rightIsFull : m > 0 ∨ ((m+1).nextPowerOfTwo = m+1 : Bool)) (h₁ : 0 ≠ n + m) (h₂ : ¬(m < n ∧ ((m+1).nextPowerOfTwo = m+1 : Bool))) : m > 0 := match m_gt_0_or_rightIsFull with | Or.inl h => h | Or.inr h => by @@ -108,7 +108,7 @@ private theorem CompleteTree.removeRightRightNotEmpty {n m : Nat} (m_gt_0_or_rig . exact Nat.succ_pos _ /-- Helper for heapRemoveLastAux -/ -private theorem CompleteTree.removeRightLeftIsFull {n m : Nat} (r : ¬(m < n ∧ ((m+1).nextPowerOfTwo = m+1 : Bool))) (m_le_n : m ≤ n) (subtree_complete : (n + 1).isPowerOfTwo ∨ (m + 1).isPowerOfTwo) : (n+1).isPowerOfTwo := by +private theorem removeRightLeftIsFull {n m : Nat} (r : ¬(m < n ∧ ((m+1).nextPowerOfTwo = m+1 : Bool))) (m_le_n : m ≤ n) (subtree_complete : (n + 1).isPowerOfTwo ∨ (m + 1).isPowerOfTwo) : (n+1).isPowerOfTwo := by rewrite[Decidable.not_and_iff_or_not] at r cases r case inl h₁ => rewrite[Nat.not_lt_eq] at h₁ @@ -121,7 +121,7 @@ private theorem CompleteTree.removeRightLeftIsFull {n m : Nat} (r : ¬(m < n ∧ assumption /-- Helper for heapRemoveLastAux -/ -private theorem CompleteTree.stillInRange {n m : Nat} (r : ¬(m < n ∧ ((m+1).nextPowerOfTwo = m+1 : Bool))) (m_le_n : m ≤ n) (m_gt_0 : m > 0) (leftIsFull : (n+1).isPowerOfTwo) (max_height_difference: n < 2 * (m + 1)) : n < 2*m := by +private theorem stillInRange {n m : Nat} (r : ¬(m < n ∧ ((m+1).nextPowerOfTwo = m+1 : Bool))) (m_le_n : m ≤ n) (m_gt_0 : m > 0) (leftIsFull : (n+1).isPowerOfTwo) (max_height_difference: n < 2 * (m + 1)) : n < 2*m := by rewrite[Decidable.not_and_iff_or_not] at r cases r with | inl h₁ => have m_eq_n : m = n := Nat.le_antisymm m_le_n (Nat.not_lt.mp h₁) @@ -136,7 +136,7 @@ private theorem CompleteTree.stillInRange {n m : Nat} (r : ¬(m < n ∧ ((m+1).n **BEWARE** that "last" here means the underlying complete tree. It is *not* the elemenent at the largest index, nor is it the largest element in the heap. -/ -protected def CompleteTree.Internal.heapRemoveLastAux +protected def Internal.heapRemoveLastAux {α : Type u} {β : Nat → Type u} {o : Nat} @@ -179,7 +179,7 @@ protected def CompleteTree.Internal.heapRemoveLastAux Removes the last element in the complete Tree. This is **NOT** the element with the largest index, nor is it the largest element in the heap. -/ -protected def CompleteTree.Internal.heapRemoveLast {α : Type u} {o : Nat} (heap : CompleteTree α (o+1)) : (CompleteTree α o × α) := +protected def Internal.heapRemoveLast {α : Type u} {o : Nat} (heap : CompleteTree α (o+1)) : (CompleteTree α o × α) := Internal.heapRemoveLastAux heap id (λ(a : α) _ ↦ a) (λa _ _ ↦ a) /-- @@ -188,7 +188,7 @@ protected def CompleteTree.Internal.heapRemoveLast {α : Type u} {o : Nat} (heap Also returns the index of the removed element. -/ -protected def CompleteTree.heapRemoveLastWithIndex {α : Type u} {o : Nat} (heap : CompleteTree α (o+1)) : (CompleteTree α o × α × Fin (o+1)) := +protected def heapRemoveLastWithIndex {α : Type u} {o : Nat} (heap : CompleteTree α (o+1)) : (CompleteTree α o × α × Fin (o+1)) := Internal.heapRemoveLastAux heap (β := λn ↦ α × Fin n) (λ(a : α) ↦ (a, Fin.mk 0 (Nat.succ_pos 0))) (λ(a, prev_idx) h₁ ↦ (a, prev_idx.succ.castLE $ Nat.succ_le_of_lt h₁) ) @@ -198,9 +198,9 @@ protected def CompleteTree.heapRemoveLastWithIndex {α : Type u} {o : Nat} (heap -- heapUpdateRoot /-- - Helper for CompleteTree.heapUpdateAt. Makes proofing heap predicate work in Lean 4.9 + Helper for heapUpdateAt. Makes proofing heap predicate work in Lean 4.9 -/ -def CompleteTree.heapUpdateRoot {α : Type u} {n : Nat} (le : α → α → Bool) (value : α) (heap : CompleteTree α n) (_ : n > 0) : CompleteTree α n × α := +def heapUpdateRoot {α : Type u} {n : Nat} (le : α → α → Bool) (value : α) (heap : CompleteTree α n) (_ : n > 0) : CompleteTree α n × α := match n, heap with | (o+p+1), .branch v l r h₃ h₄ h₅ => if h₆ : o = 0 then @@ -234,11 +234,11 @@ match n, heap with -- heapRemoveAt /-- - Helper for CompleteTree.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 CompleteTree.heapUpdateAt {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin n) (value : α) (heap : CompleteTree α n) (h₁ : n > 0) : CompleteTree α n × α := +def heapUpdateAt {α : 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₁ else @@ -268,7 +268,7 @@ def CompleteTree.heapUpdateAt {α : Type u} {n : Nat} (le : α → α → Bool) ---------------------------------------------------------------------------------------------- -- heapPop -def CompleteTree.heapPop {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α (n+1)) : CompleteTree α n × α := +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 @@ -278,8 +278,8 @@ def CompleteTree.heapPop {α : Type u} {n : Nat} (le : α → α → Bool) (heap ---------------------------------------------------------------------------------------------- -- heapRemoveAt -/--Removes the element at a given index. Use `CompleteTree.indexOf` to find the respective index.-/ -def CompleteTree.heapRemoveAt {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin (n+1)) (heap : CompleteTree α (n+1)) : CompleteTree α n × α := +/--Removes the element at a given index. Use `indexOf` to find the respective index.-/ +def heapRemoveAt {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin (n+1)) (heap : CompleteTree α (n+1)) : CompleteTree α n × α := --Since we cannot even temporarily break the completeness property, we go with the --version from Wikipedia: We first remove the last element, and then update values in the tree --indices are depth first, but "last" means last element of the complete tree. diff --git a/BinaryHeap/CompleteTree/HeapProofs.lean b/BinaryHeap/CompleteTree/HeapProofs.lean index d56e5b5..a41f963 100644 --- a/BinaryHeap/CompleteTree/HeapProofs.lean +++ b/BinaryHeap/CompleteTree/HeapProofs.lean @@ -3,7 +3,7 @@ import BinaryHeap.CompleteTree.Lemmas namespace BinaryHeap -theorem CompleteTree.emptyIsHeap {α : Type u} (le : α → α → Bool) : HeapPredicate CompleteTree.empty le := by trivial +theorem CompleteTree.emptyIsHeap {α : Type u} (le : α → α → Bool) : HeapPredicate CompleteTree.empty le := True.intro ---------------------------------------------------------------------------------------------- -- heapPush diff --git a/BinaryHeap/CompleteTree/Lemmas.lean b/BinaryHeap/CompleteTree/Lemmas.lean index 2e4bda1..dc26dd5 100644 --- a/BinaryHeap/CompleteTree/Lemmas.lean +++ b/BinaryHeap/CompleteTree/Lemmas.lean @@ -1,4 +1,5 @@ import BinaryHeap.CompleteTree.Basic +import BinaryHeap.CompleteTree.AdditionalOperations import BinaryHeap.HeapPredicate namespace BinaryHeap @@ -21,17 +22,31 @@ theorem CompleteTree.root_unfold {α : Type u} {o p : Nat} (v : α) (l : Complet /-- Helper to rw away left, because Lean 4.9 makes it unnecessarily hard to deal with match in tactics mode... -/ theorem CompleteTree.left_unfold {α : Type u} {o p : Nat} (v : α) (l : CompleteTree α o) (r : CompleteTree α p) (h₁ : p ≤ o) (h₂ : o < 2 * (p + 1)) (h₃ : (o + 1).isPowerOfTwo ∨ (p + 1).isPowerOfTwo) (h₄ : o + p + 1 > 0): (CompleteTree.branch v l r h₁ h₂ h₃).left h₄ = l := rfl +theorem CompleteTree.leftLen_unfold {α : Type u} {o p : Nat} (v : α) (l : CompleteTree α o) (r : CompleteTree α p) (h₁ : p ≤ o) (h₂ : o < 2 * (p + 1)) (h₃ : (o + 1).isPowerOfTwo ∨ (p + 1).isPowerOfTwo) (h₄ : o + p + 1 > 0): (CompleteTree.branch v l r h₁ h₂ h₃).leftLen h₄ = o := rfl + /-- Helper to rw away right, because Lean 4.9 makes it unnecessarily hard to deal with match in tactics mode... -/ theorem CompleteTree.right_unfold {α : Type u} {o p : Nat} (v : α) (l : CompleteTree α o) (r : CompleteTree α p) (h₁ : p ≤ o) (h₂ : o < 2 * (p + 1)) (h₃ : (o + 1).isPowerOfTwo ∨ (p + 1).isPowerOfTwo) (h₄ : o + p + 1 > 0): (CompleteTree.branch v l r h₁ h₂ h₃).right h₄ = r := rfl theorem CompleteTree.heqSameLeftLen {α : Type u} {n m : Nat} {a : CompleteTree α n} {b : CompleteTree α m} (h₁ : n = m) (h₂ : n > 0) (h₃ : HEq a b) : a.leftLen h₂ = b.leftLen (h₁.subst h₂) := by subst n have h₃ : a = b := eq_of_heq h₃ - subst a - rfl + congr theorem CompleteTree.heqSameRightLen {α : Type u} {n m : Nat} {a : CompleteTree α n} {b : CompleteTree α m} (h₁ : n = m) (h₂ : n > 0) (h₃ : HEq a b) : a.rightLen h₂ = b.rightLen (h₁.subst h₂) := by subst n have h₃ : a = b := eq_of_heq h₃ - subst a - rfl + congr + +theorem CompleteTree.heqSameRoot {α : Type u} {n m : Nat} {a : CompleteTree α n} {b : CompleteTree α m} (h₁ : n = m) (h₂ : n > 0) (h₃ : HEq a b) : a.root h₂ = b.root (h₁.subst h₂) := by + subst n + have h₃ : a = b := eq_of_heq h₃ + congr + +theorem CompleteTree.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 CompleteTree.leftLenLtN {α : Type u} {n : Nat} (tree : CompleteTree α n) (h₁ : n>0) : tree.leftLen h₁ < n := by + unfold leftLen + split + rw[length] + rename_i o p _ _ _ _ _ _ _ + exact Nat.lt_of_le_of_lt (Nat.le_add_right o p) (Nat.lt_succ_self (o+p)) |