diff options
7 files changed, 17 insertions, 19 deletions
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean index d8d1de4..e66512d 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean @@ -14,7 +14,7 @@ theorem heapRemoveAtReturnsElementAt {α : Type u} {n : Nat} (le : α → α → else simp only [h₁, ↓reduceDIte, ge_iff_le] if h₂ : index = (Internal.heapRemoveLastWithIndex heap).2.snd then - simp only [h₂, ↓reduceDIte] + simp only [h₂, ↓reduceIte] exact Eq.symm $ CompleteTree.AdditionalProofs.heapRemoveLastWithIndexReturnsItemAtIndex heap else if h₃ : (Internal.heapRemoveLastWithIndex heap).2.snd ≤ index then @@ -36,7 +36,7 @@ theorem heapRemoveAtOnlyRemovesAt {α : Type u} {n : Nat} (le : α → α → Bo else simp only [h₂, ↓reduceDIte, ge_iff_le] if h₃ : removeIndex = (Internal.heapRemoveLastWithIndex heap).2.snd then - simp only [h₃, ↓reduceDIte] + simp only [h₃, ↓reduceIte] exact CompleteTree.AdditionalProofs.heapRemoveLastWithIndexOnlyRemovesOneElement _ _ (h₃.subst h₁.symm) else if h₄ : (Internal.heapRemoveLastWithIndex heap).2.snd ≤ removeIndex then diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean index c3b77ad..d340578 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean @@ -11,7 +11,7 @@ protected theorem heapRemoveLastWithIndexReturnsItemAtIndex {α : Type u} {o : N unfold CompleteTree.Internal.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] + simp only [Nat.add_eq, Fin.zero_eta, Fin.isValue, Fin.castLE_succ] split case isTrue n_m_zero => have h₁ : n = 0 := And.left $ Nat.add_eq_zero.mp n_m_zero.symm @@ -199,7 +199,7 @@ intro h₁ split at h₁ rename_i o p v l r _ _ _ simp only [Nat.add_eq, ne_eq] at h₂ -simp only [Nat.add_eq, h₂, ↓reduceDIte, decide_eq_true_eq, Fin.zero_eta, Fin.isValue, +simp only [Nat.add_eq, h₂, ↓reduceDIte, Fin.zero_eta, Fin.isValue, Nat.succ_eq_add_one, Fin.castLE_succ, Nat.pred_eq_sub_one, gt_iff_lt] at h₁ ⊢ if h₃ : p < o ∧ (p + 1).isPowerOfTwo then --removed left @@ -218,8 +218,7 @@ if h₃ : p < o ∧ (p + 1).isPowerOfTwo then rewrite[←lens_see_through_cast _ leftLen _ (Nat.succ_pos _) _] rewrite[leftLen_unfold] assumption - 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 [Fin.coe_pred, Fin.isValue, ← lens_see_through_cast _ leftLen _ (Nat.succ_pos _) _] simp only[leftLen_unfold] apply heapRemoveLastWithIndexRelationGt_Aux case h₁ => exact Nat.add_comm_right oo 1 p @@ -261,7 +260,7 @@ else have h₅ : index.pred h₄ > o := by simp only [Nat.add_eq, Fin.coe_pred, gt_iff_lt] rewrite[Fin.lt_iff_val_lt_val] at h₁ - simp only [Nat.succ_eq_add_one, Fin.isValue, Fin.val_succ, Fin.coe_castLE, Fin.coe_addNat] at h₁ + simp only [Fin.isValue, Fin.val_succ, Fin.coe_castLE, Fin.coe_addNat] at h₁ exact Nat.lt_of_add_right $ Nat.lt_pred_of_succ_lt h₁ have h₆ : index > o := Nat.lt_of_add_left $ Nat.succ_lt_of_lt_pred h₅ have h₇ : ↑index - o - 1 < pp + 1 := @@ -308,7 +307,7 @@ protected theorem heapRemoveLastWithIndexRelationLt {α : Type u} {n : Nat} (hea split at h₁ rename_i o p v l r _ _ _ simp only [Nat.add_eq, ne_eq] at h₃ - simp only [h₃, Nat.add_eq, Fin.zero_eta, Fin.isValue, decide_eq_true_eq, Nat.succ_eq_add_one, + simp only [h₃, Nat.add_eq, Fin.zero_eta, Fin.isValue, Nat.succ_eq_add_one, Fin.castLE_succ, Nat.pred_eq_sub_one, reduceDIte] at h₁ ⊢ if h₄ : p < o ∧ (p + 1).isPowerOfTwo then --removed left diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/IndexOf.lean b/BinaryHeap/CompleteTree/AdditionalProofs/IndexOf.lean index 5cbfbf5..893b554 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/IndexOf.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/IndexOf.lean @@ -52,7 +52,7 @@ private theorem indexOfNoneImpPredFalseAux {α : Type u} {n : Nat} (tree : Compl 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₂ + simp only [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_iff] at h₂₂ @@ -172,7 +172,7 @@ private theorem indexOfAuxAddsCurrentIndex {α : Type u} {n : Nat} (tree : Compl rw[Option.eq_some_iff_get_eq] at he₂ he₁ match he₁, he₂ with | Exists.intro he₁ h₈, Exists.intro he₂ h₉ => - simp[Fin.ext_iff, Option.map_get] at h₈ h₉ + simp[Fin.ext_iff] at h₈ h₉ rw[Nat.mod_eq_of_lt (by omega), h₇] at h₈ rw[Nat.mod_eq_of_lt (by omega), h₆] at h₉ rw[←h₈, ←h₉] @@ -221,7 +221,6 @@ theorem indexOfSomeImpPredTrue {α : Type u} {n : Nat} (tree : CompleteTree α n case true => simp only [h₃, ↓reduceIte, Option.some.injEq] at he₁ subst index - simp[Fin.ofNat] at h₂ rw[←Fin.zero_eta, ←get_zero_eq_root, root_unfold] at h₂ subst v assumption @@ -247,7 +246,7 @@ theorem indexOfSomeImpPredTrue {α : Type u} {n : Nat} (tree : CompleteTree α n exact h₉ case some lindex => rw[h₄, Option.some_or, Option.some_inj] at he₁ - simp only [Option.map_map, Option.map_eq_some_iff, Function.comp_apply] at h₄ + simp only [Option.map_eq_some_iff] at h₄ 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₅ diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapPush.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapPush.lean index 4320473..146595f 100644 --- a/BinaryHeap/CompleteTree/HeapProofs/HeapPush.lean +++ b/BinaryHeap/CompleteTree/HeapProofs/HeapPush.lean @@ -48,11 +48,11 @@ theorem heapPushRootSameOrElem (elem : α) (heap : CompleteTree α o) (lt : α rename_i n m v l r _ _ _ split -- if h : m < n ∧ (n + 1).isPowerOfTwo then case h_2.isTrue h => - cases (lt elem v) <;> simp[instDecidableEqBool, Bool.decEq, root] + cases (lt elem v) <;> simp[root] case h_2.isFalse h => rw[rootSeesThroughCast n (m+1) (Nat.add_comm_right _ _ _) (Nat.succ_pos _) (Nat.succ_pos _)] cases (lt elem v) - <;> simp[instDecidableEqBool, Bool.decEq, root] + <;> simp[root] theorem heapPushEmptyElem (elem : α) (heap : CompleteTree α o) (lt : α → α → Bool) (h₂ : ¬0 < o) : (root (heap.heapPush lt elem) (Nat.succ_pos o) = elem) := have : o = 0 := Nat.eq_zero_of_le_zero $ (Nat.not_lt_eq 0 o).mp h₂ @@ -113,7 +113,7 @@ theorem heapPushIsHeap {α : Type u} {elem : α} {heap : CompleteTree α o} {le case' isTrue => have h := heapPushIsHeapAux le n m v elem l r h₁ h₂ h₃ case' isFalse => - apply HeapPredicate.seesThroughCast <;> try simp +arith[h₂] --gets rid of annoying cast. + apply HeapPredicate.seesThroughCast <;> try simp +arith --gets rid of annoying cast. have h := heapPushIsHeapAux le m n v elem r l (And.intro h₁.right.left $ And.intro h₁.left $ And.intro h₁.right.right.right h₁.right.right.left) h₂ h₃ all_goals unfold HeapPredicate diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapRemoveLast.lean index 3d8f65a..e2236f7 100644 --- a/BinaryHeap/CompleteTree/HeapProofs/HeapRemoveLast.lean +++ b/BinaryHeap/CompleteTree/HeapProofs/HeapRemoveLast.lean @@ -54,7 +54,7 @@ private theorem castZeroHeap (n m : Nat) (heap : CompleteTree α 0) (h₁ : 0=n+ cases n case succ => contradiction case zero => - simp[h₁, h₂] + simp[h₂] -- If there is only one element left, the result is a leaf. private theorem heapRemoveLastAuxLeaf diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean index 685a726..f0194ec 100644 --- a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean +++ b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean @@ -33,10 +33,10 @@ where unfold heapUpdateRoot split rename_i o p v l r h₆ h₇ h₈ h₂ - cases o <;> cases p <;> simp [↓reduceDIte,HeapPredicate.leOrLeaf, Nat.add_one_ne_zero, root_unfold, h₄, reflexive_le] + cases o <;> cases p <;> simp [↓reduceDIte,HeapPredicate.leOrLeaf, 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] + simp only [↓reduceIte, h₁₀, root_unfold, h₄, reflexive_le] have h₁₁ : le value $ r.root (by omega) := h₅ value v (r.root _) ⟨h₃, h₁.right.right.right⟩ simp only [↓reduceIte, h₁₀, h₁₁, and_self, root_unfold, h₄, reflexive_le] case isFalse => diff --git a/lean-toolchain b/lean-toolchain index 893a7f3..f434439 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:4.21.0 +leanprover/lean4:4.23.0 |