diff options
Diffstat (limited to 'BinaryHeap')
5 files changed, 12 insertions, 21 deletions
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean b/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean index 7a0c893..950183b 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean @@ -82,14 +82,10 @@ private theorem if_contains_get_eq {α : Type u} {n : Nat} (tree : CompleteTree assumption -theorem contains_iff_index_exists' {α : Type u} {n : Nat} (tree : CompleteTree α n) (element : α) : tree.contains element ↔ ∃ (index : Fin n), tree.get index = element := by +theorem contains_iff_index_exists {α : Type u} {n : Nat} (tree : CompleteTree α n) (element : α) : tree.contains element ↔ ∃ (index : Fin n), 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 - -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/HeapPush.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPush.lean index 62b0e2c..1585b99 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapPush.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPush.lean @@ -93,7 +93,7 @@ theorem heapPushRetainsHeapValues {α : Type u} {n: Nat} (le : α → α → Boo rw[left_unfold] rw[left_unfold] case isTrue => - rw[contains_iff_index_exists _ _ (Nat.lt_of_lt_of_le (Fin.lt_iff_val_lt_val.mp h₂₂) h₃)] + rw[contains_iff_index_exists _ _] have : index.val - 1 < o := Nat.sub_one_lt_of_le h₂₂ h₃ exists ⟨index.val - 1, this⟩ case isFalse => @@ -113,5 +113,6 @@ theorem heapPushRetainsHeapValues {α : Type u} {n: Nat} (le : α → α → Boo 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 - rw[contains_iff_index_exists _ _ this] - exists ⟨index.val - o - 1, by omega⟩ + rw[contains_iff_index_exists _ _] + have : index.val - o - 1 < p := by omega + exists ⟨index.val - o - 1, this⟩ diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean index cf0774f..d68aedc 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean @@ -428,8 +428,7 @@ protected theorem heapRemoveLastWithIndexOnlyRemovesOneElement {α : Type u} {n := by simp only [ne_eq] intro h₁ - have h₂ : n > 0 := by omega - rw[contains_iff_index_exists _ _ h₂] + rw[contains_iff_index_exists _ _] have h₃ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelation heap index simp at h₃ split at h₃ diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean index 606b687..09ea532 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean @@ -150,10 +150,7 @@ theorem heapUpdateAtOnlyUpdatesAt {α : Type u} {n : Nat} (le : α → α → Bo simp only[leftLen_unfold] 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 + exists solution 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₆] @@ -164,8 +161,6 @@ 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 _ _ h₆] diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean index 1a44da1..48ba8ca 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean @@ -56,7 +56,7 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α rw[contains_as_root_left_right _ _ h₄] right left - rewrite[contains_iff_index_exists'] + rewrite[contains_iff_index_exists] exists ⟨j, (Nat.succ_pred (Fin.val_ne_iff.mpr h₂)).substr (p := λx ↦ x ≤ oo + 1) this⟩ case succ pp _ _ _ => have h₂ := Fin.val_ne_iff.mpr h₂ @@ -74,7 +74,7 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α rw[contains_as_root_left_right _ _ (Nat.succ_pos _)] right left - rw[←h₃, contains_iff_index_exists', left_unfold] + rw[←h₃, contains_iff_index_exists, left_unfold] exists ⟨j,h⟩ case isFalse => split @@ -104,7 +104,7 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α right left simp only [left_unfold] - rw[←h₃, contains_iff_index_exists'] + rw[←h₃, contains_iff_index_exists] exists ⟨j, h⟩ else -- index was in r @@ -117,7 +117,7 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α rw[contains_as_root_left_right _ _ (Nat.succ_pos _)] right right - rw[←h₃, contains_iff_index_exists', right_unfold] + rw[←h₃, contains_iff_index_exists, right_unfold] exists ⟨j-(oo+1), h₄⟩ case isFalse => split @@ -128,7 +128,7 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α right right simp only [right_unfold] - rw[←h₃, contains_iff_index_exists'] + rw[←h₃, contains_iff_index_exists] exists ⟨j- (oo + 1), h₄⟩ case isFalse => --r.root gets moved up |