diff options
Diffstat (limited to 'BinaryHeap')
10 files changed, 27 insertions, 24 deletions
diff --git a/BinaryHeap/CompleteTree/AdditionalOperations.lean b/BinaryHeap/CompleteTree/AdditionalOperations.lean index 8038555..100af76 100644 --- a/BinaryHeap/CompleteTree/AdditionalOperations.lean +++ b/BinaryHeap/CompleteTree/AdditionalOperations.lean @@ -11,17 +11,17 @@ protected def Internal.indexOfAux {α : Type u} (heap : CompleteTree α o) (pred match o, heap with | 0, .leaf => none | (n+m+1), .branch a left right _ _ _ => - have sum_n_m_succ_curr : n + m.succ + currentIndex > 0 := Nat.add_pos_left (Nat.add_pos_right n (Nat.succ_pos m)) currentIndex + have : NeZero (n + m + 1 + currentIndex) := ⟨Nat.pos_iff_ne_zero.mp $ Nat.add_pos_left (Nat.add_pos_right n (Nat.succ_pos m)) currentIndex⟩ if pred a then - let result := Fin.ofNat' currentIndex sum_n_m_succ_curr + let result := Fin.ofNat' _ currentIndex some result else let found_left := CompleteTree.Internal.indexOfAux left pred (currentIndex + 1) - let found_left : Option (Fin (n+m+1+currentIndex)) := found_left.map λ a ↦ Fin.ofNat' a sum_n_m_succ_curr + let found_left : Option (Fin (n+m+1+currentIndex)) := found_left.map λ a ↦ Fin.ofNat' _ a let found_right := found_left <|> - (CompleteTree.Internal.indexOfAux right pred (currentIndex + n + 1)).map ((λ a ↦ Fin.ofNat' a sum_n_m_succ_curr) : _ → Fin (n+m+1+currentIndex)) + (CompleteTree.Internal.indexOfAux right pred (currentIndex + n + 1)).map ((λ a ↦ Fin.ofNat' _ a) : _ → Fin (n+m+1+currentIndex)) found_right /--Finds the first occurance of a given element in the heap and returns its index. Indices are depth first.-/ diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean b/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean index 1012ef5..5c9552b 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean @@ -8,7 +8,8 @@ theorem get_zero_eq_root {α : Type u} {n : Nat} (tree : CompleteTree α n) (h | (_+_+1), 0, .branch v _ _ _ _ _ => rfl | nn+1, ⟨j+1,h₄⟩, _ => by subst h₂ - simp only [heq_eq_eq, Fin.ext_iff] at h₃ + simp only [Nat.succ_eq_add_one, Fin.zero_eta, heq_eq_eq, Fin.ext_iff, Fin.val_zero, + Nat.self_eq_add_left, Nat.add_one_ne_zero] at h₃ theorem get_right {α : Type u} {n : Nat} (tree : CompleteTree α n) (index : Fin n) (h₂ : index > tree.leftLen (Nat.zero_lt_of_lt index.isLt)) : have h₁ : n > 0 := Nat.zero_lt_of_lt index.isLt diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean index d68aedc..2bdc382 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean @@ -153,9 +153,9 @@ protected theorem heapRemoveLastWithIndexIndexNeZeroForNGt1 {α : Type u} {n : N rename_i o p v l r _ _ _ simp at h₁ simp[h₁] - have : o = 0 := And.left $ Nat.add_eq_zero_iff.mp h₁ + have : o = 0 := And.left h₁ subst o - have : p = 0 := And.right $ Nat.add_eq_zero_iff.mp h₁ + have : p = 0 := And.right h₁ subst p rfl diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean index 09ea532..c233355 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean @@ -87,7 +87,7 @@ theorem heapUpdateAtOnlyUpdatesAt {α : Type u} {n : Nat} (le : α → α → Bo 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₃ + case isTrue h => exact absurd (beq_iff_eq.mp h) h₃ split rename_i d1 d2 d3 d4 d5 o p v l r _ _ _ updateIndex _ _ clear d1 d2 d3 d4 d5 @@ -117,7 +117,7 @@ theorem heapUpdateAtOnlyUpdatesAt {α : Type u} {n : Nat} (le : α → α → Bo unfold heapUpdateAt heapUpdateAtAux generalize heapUpdateAt.proof_1 updateIndex = h₁ split - case isTrue hx => exact absurd ((beq_iff_eq _ _).mp hx) h₃ + case isTrue hx => exact absurd (beq_iff_eq.mp hx) h₃ case isFalse => split rename_i d1 d2 d3 d4 d5 o p v l r olep mhd stc index _ _ diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean index 48ba8ca..fe64a72 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean @@ -150,7 +150,7 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α have : pp + 1 < oo + 1 + pp + 1 + 1 := by simp_arith --termination apply heapUpdateRootOnlyUpdatesRoot apply Fin.ne_of_val_ne - simp only [Nat.add_one_ne_zero, not_false_eq_true] + simp only [ne_eq, Nat.add_one_ne_zero, not_false_eq_true] 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 diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/IndexOf.lean b/BinaryHeap/CompleteTree/AdditionalProofs/IndexOf.lean index 110afb0..0d69ebc 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/IndexOf.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/IndexOf.lean @@ -98,8 +98,9 @@ private theorem indexOfSomeImpPredTrueAux2 {α : Type u} {p : Nat} {r : Complete case isTrue => simp only [Option.isSome_some, imp_self] case isFalse => + unfold Function.comp + simp only [Option.map_some'] repeat rw[Option.bind_some_eq_map] - simp only [Option.map_map] simp only [Option.orElse_is_some, Bool.or_eq_true, Option.is_some_map] intro h₁ cases h₁ @@ -177,7 +178,7 @@ private theorem indexOfAuxAddsCurrentIndex {α : Type u} {n : Nat} (tree : Compl simp_arith[o1, o2] -private theorem indexOfSomeImpPredTrueAuxR {α : Type u} {p : Nat} (r : CompleteTree α p) (pred : α → Bool) {o : Nat} (index : Fin ((o+p)+1)) (h₁ : o + p + 1 > 0) (h₂ : (Internal.indexOfAux r pred 0).isSome) : ∀(a : Fin (p + (o + 1))), (Internal.indexOfAux r pred (o + 1) = some a ∧ Fin.ofNat' ↑a h₁ = index) → (Internal.indexOfAux r pred 0).get h₂ + o + 1 = index.val := by +private theorem indexOfSomeImpPredTrueAuxR {α : Type u} {p : Nat} (r : CompleteTree α p) (pred : α → Bool) {o : Nat} (index : Fin ((o+p)+1)) (h₂ : (Internal.indexOfAux r pred 0).isSome) : ∀(a : Fin (p + (o + 1))), (Internal.indexOfAux r pred (o + 1) = some a ∧ Fin.ofNat' (o+p+1) ↑a = index) → (Internal.indexOfAux r pred 0).get h₂ + o + 1 = index.val := by simp only [Nat.add_zero, and_imp] intros index₂ h₃ h₄ have : index₂.val = index.val := by @@ -190,7 +191,7 @@ private theorem indexOfSomeImpPredTrueAuxR {α : Type u} {p : Nat} (r : Complete rw[←this] simp only [h₃, Option.get_some] -private theorem indexOfSomeImpPredTrueAuxL {α : Type u} {o : Nat} (l : CompleteTree α o) (pred : α → Bool) {p : Nat} (index : Fin ((o+p)+1)) (h₁ : o + p + 1 > 0) (h₂ : (Internal.indexOfAux l pred 0).isSome) : ∀(a : Fin ((o + 1))), (Internal.indexOfAux l pred 1 = some a ∧ Fin.ofNat' ↑a h₁ = index) → (Internal.indexOfAux l pred 0).get h₂ + 1 = index.val := by +private theorem indexOfSomeImpPredTrueAuxL {α : Type u} {o : Nat} (l : CompleteTree α o) (pred : α → Bool) {p : Nat} (index : Fin ((o+p)+1)) (h₂ : (Internal.indexOfAux l pred 0).isSome) : ∀(a : Fin ((o + 1))), (Internal.indexOfAux l pred 1 = some a ∧ Fin.ofNat' (o+p+1) ↑a = index) → (Internal.indexOfAux l pred 0).get h₂ + 1 = index.val := by simp only [Nat.add_zero, and_imp] intros index₂ h₃ h₄ have : index₂.val = index.val := by @@ -226,15 +227,16 @@ theorem indexOfSomeImpPredTrue {α : Type u} {n : Nat} (tree : CompleteTree α n assumption case false => --unfold HOrElse.hOrElse instHOrElseOfOrElse at he₁ - simp only [h₃, Bool.false_eq_true, ↓reduceIte, Option.bind_some_eq_map ] at he₁ - cases h₄ : (Option.map (fun a => Fin.ofNat' a _) (Option.map Fin.val (Internal.indexOfAux l pred 1))) + unfold Function.comp at he₁ + simp only [h₃, Bool.false_eq_true, ↓reduceIte, Option.map_some', Option.bind_some_eq_map] at he₁ + cases h₄ : (Option.map (fun a => Fin.ofNat' (o+p+1) a.val) (Internal.indexOfAux l pred 1)) case none => rw[h₄, Option.none_orElse] at he₁ simp only [Option.map_map, Option.map_eq_some', Function.comp_apply] at he₁ rw[Nat.zero_add] at he₁ have h₅ : (Internal.indexOfAux r pred (o + 1)).isSome := Option.isSome_iff_exists.mpr (Exists.imp (λx ↦ And.left) he₁) have h₆ := indexOfSomeImpPredTrueAux2 _ 0 h₅ - have h₇ := indexOfSomeImpPredTrueAuxR r pred index (Nat.succ_pos _) h₆ + have h₇ := indexOfSomeImpPredTrueAuxR r pred index h₆ have h₈ := he₁.elim h₇ have h₉ := indexOfSomeImpPredTrue r pred h₆ rw[get_right' _ (Nat.lt_of_add_right $ Nat.lt_of_succ_le $ Nat.le_of_eq h₈)] at h₂ @@ -249,7 +251,7 @@ theorem indexOfSomeImpPredTrue {α : Type u} {n : Nat} (tree : CompleteTree α n subst lindex have h₅ : (Internal.indexOfAux l pred 1).isSome := Option.isSome_iff_exists.mpr (Exists.imp (λx ↦ And.left) h₄) have h₆ := indexOfSomeImpPredTrueAux2 _ 0 h₅ - have h₇ := indexOfSomeImpPredTrueAuxL l pred index (Nat.succ_pos _) h₆ + have h₇ := indexOfSomeImpPredTrueAuxL l pred index h₆ have h₈ := h₄.elim h₇ have h₉ := indexOfSomeImpPredTrue l pred h₆ have h₁₀ : index.val ≤ o := Nat.le_trans (Nat.le_of_eq h₈.symm) (((Internal.indexOfAux l pred 0).get h₆).isLt) diff --git a/BinaryHeap/CompleteTree/HeapOperations.lean b/BinaryHeap/CompleteTree/HeapOperations.lean index 038a32c..9151eb0 100644 --- a/BinaryHeap/CompleteTree/HeapOperations.lean +++ b/BinaryHeap/CompleteTree/HeapOperations.lean @@ -44,7 +44,7 @@ def heapPush (le : α → α → Bool) (elem : α) (heap : CompleteTree α o) : simp at subtree_complete exact subtree_complete else if h₁ : leftIsFull then by - rewrite[Decidable.not_and_iff_or_not (m<n) leftIsFull] at r + rewrite[Decidable.not_and_iff_or_not (p := m<n) (q := leftIsFull)] at r cases r case inl h₂ => rewrite[Nat.not_lt_eq] at h₂ have h₃ := Nat.not_le_of_gt $ Nat.lt_of_le_of_ne h₂ s @@ -58,7 +58,7 @@ def heapPush (le : α → α → Bool) (elem : α) (heap : CompleteTree α o) : case inl => contradiction case inr => trivial have still_in_range : n + 1 < 2 * (m + 1) := by - rewrite[Decidable.not_and_iff_or_not (m<n) leftIsFull] at r + rewrite[Decidable.not_and_iff_or_not (p := m<n) (q := leftIsFull)] at r cases r case inl h₁ => rewrite[Nat.not_gt_eq n m] at h₁ simp_arith[Nat.le_antisymm h₁ p] diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapPush.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapPush.lean index 8a6e48c..1ce9e56 100644 --- a/BinaryHeap/CompleteTree/HeapProofs/HeapPush.lean +++ b/BinaryHeap/CompleteTree/HeapProofs/HeapPush.lean @@ -118,5 +118,5 @@ theorem heapPushIsHeap {α : Type u} {elem : α} {heap : CompleteTree α o} {le unfold HeapPredicate cases h₆ : (le elem v) <;> simp only [h₆, Bool.false_eq_true, reduceIte] at h - <;> simp only [instDecidableEqBool, Bool.decEq, h, and_self] + <;> simp only [Bool.false_eq_true, ↓reduceIte, h, and_self] end diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean index 32e6fb9..c12f76f 100644 --- a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean +++ b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean @@ -29,7 +29,7 @@ private theorem heapUpdateAtIsHeapLeRootAux_ValueLeRoot {α : Type u} {n : Nat} unfold heapUpdateRoot split rename_i o p v l r h₆ h₇ h₈ h₂ - cases o <;> cases p <;> simp only [↓reduceDIte,HeapPredicate.leOrLeaf, root_unfold, h₄, reflexive_le] + cases o <;> cases p <;> simp [↓reduceDIte,HeapPredicate.leOrLeaf, Nat.add_one_ne_zero, root_unfold, h₄, reflexive_le] <;> unfold HeapPredicate at h₁ <;> have h₁₀ : le value $ l.root (by omega) := h₅ value v (l.root _) ⟨h₃, h₁.right.right.left⟩ simp only [↓reduceIte, Nat.add_zero, h₁₀, root_unfold, h₄, reflexive_le] @@ -42,7 +42,7 @@ private theorem heapUpdateAtIsHeapLeRootAux_ValueLeRoot {α : Type u} {n : Nat} <;> simp (config := { ground := true }) only [root_unfold, Nat.pred_eq_sub_one] at h₃ ⊢ <;> split <;> unfold HeapPredicate.leOrLeaf - <;> simp only [root_unfold, h₃, h₄, reflexive_le] + <;> simp only [reduceIte, root_unfold, h₃, h₄, reflexive_le] 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 diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean index c6b421f..d712b8e 100644 --- a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean +++ b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean @@ -78,7 +78,7 @@ have h₄ : 0 < rightLen heap h₂ := heapUpdateRootPossibleRootValuesAuxR heap split rename_i o p v l r h₃ h₄ h₅ h₂ cases o - case zero => simp only[root, true_or] + case zero => simp only [root, reduceDIte, true_or] case succ oo => have h₆ : p ≠ 0 := by simp at h₁; omega simp only [Nat.add_one_ne_zero, ↓reduceDIte, h₆] @@ -211,7 +211,7 @@ theorem heapUpdateRootIsHeap {α : Type u} {n: Nat} (le : α → α → Bool) (v · assumption else by simp only [↓reduceDIte, ↓reduceIte, h₁₀, h₁₁, h₁₂] - have h₁₃ : ¬le value (root l _) ∨ ¬le value (root r _) := (Decidable.not_and_iff_or_not (le value (root l (Nat.zero_lt_of_ne_zero h₁₀)) = true) (le value (root r (Nat.zero_lt_of_ne_zero h₁₁)) = true)).mp h₁₂ + have h₁₃ : ¬le value (root l _) ∨ ¬le value (root r _) := Decidable.not_and_iff_or_not.mp h₁₂ cases h₁₄ : le (root l (_ : 0 < o)) (root r (_ : 0 < p)) <;> simp only [Bool.false_eq_true, ↓reduceIte] <;> unfold HeapPredicate at * |