From 8bbaa53546849c018d7546772080951c45ad0c34 Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Tue, 13 Aug 2024 20:47:08 +0200 Subject: Fix compilation with Lean 4.10. --- .../CompleteTree/AdditionalProofs/Contains.lean | 4 +- .../CompleteTree/AdditionalProofs/HeapPop.lean | 2 +- .../AdditionalProofs/HeapRemoveLast.lean | 152 ++++++++++----------- .../AdditionalProofs/HeapUpdateRoot.lean | 8 +- .../CompleteTree/HeapProofs/HeapRemoveLast.lean | 4 +- .../CompleteTree/HeapProofs/HeapUpdateAt.lean | 2 +- .../CompleteTree/HeapProofs/HeapUpdateRoot.lean | 12 +- BinaryHeap/CompleteTree/NatLemmas.lean | 8 -- lean-toolchain | 2 +- 9 files changed, 92 insertions(+), 102 deletions(-) diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean b/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean index e99617b..487a50f 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean @@ -73,7 +73,7 @@ private theorem if_contains_get_eq_auxl {α : Type u} {o : Nat} (tree : Complete 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] + simp only [h₅, ↓reduceDIte, Nat.add_eq] unfold get at prereq split at prereq rename_i pp ii ll _ hel hei heq _ @@ -121,7 +121,7 @@ private theorem if_contains_get_eq_auxr {α : Type u} {o : Nat} (tree : Complete exact Nat.succ.inj h₂ have : p = (branch v l r ht1 ht2 ht3).leftLen (Nat.succ_pos _) := rfl have h₅ : ¬(j < p) := by simp_arith [this, h₄] - simp only [h₅, ↓reduceDite, Nat.add_eq] + simp only [h₅, ↓reduceDIte, Nat.add_eq] unfold get at prereq split at prereq rename_i pp ii rr _ hel hei heq _ diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean index 937e6d0..796130f 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean @@ -13,7 +13,7 @@ theorem heapPopReturnsRoot {α : Type u} {n : Nat} (tree : CompleteTree α (n+1) split rename_i n m v l r _ _ _ have h₂ : 0 = n + m := Eq.symm $ Nat.eq_zero_of_le_zero $ Nat.le_of_not_gt h₁ - simp only [h₂, ↓reduceDite, id_eq, root_unfold] + simp only [h₂, ↓reduceDIte, id_eq, root_unfold] have : n = 0 := And.left $ Nat.add_eq_zero.mp h₂.symm subst n have : m = 0 := And.right $ Nat.add_eq_zero.mp h₂.symm diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean index c29fc3f..92efdbc 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean @@ -58,7 +58,7 @@ protected theorem heapRemoveLastWithIndexReturnsItemAtIndex {α : Type u} {o : N subst vv ll rr split at he₁ <;> rename_i goLeft - <;> simp only [goLeft, and_self, ↓reduceDite, Fin.isValue] + <;> simp only [goLeft, and_self, ↓reduceDIte, Fin.isValue] case' isTrue => cases l; case leaf => exact absurd goLeft.left $ Nat.not_lt_zero m @@ -80,7 +80,7 @@ protected theorem heapRemoveLastWithIndexReturnsItemAtIndex {α : Type u} {o : N case' isFalse => have : ¬j - --removed right - simp only [h₃, ↓reduceDite, Fin.isValue] at h₁ ⊢ - cases p <;> simp only [Nat.add_zero, Nat.reduceSub, Nat.reduceAdd, Fin.isValue] at h₁ ⊢ - case zero => - simp (config := { ground := true }) only [Nat.zero_add, and_true, Nat.not_lt, Nat.le_zero_eq] at h₃ - subst o - contradiction - case succ pp _ _ _ _ => - 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] - 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₁ - 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 := - have : ↑index < (o + 1) + (pp + 1) := (Nat.add_comm_right o (pp+1) 1).subst index.isLt - have : ↑index < (pp + 1) + (o + 1) := (Nat.add_comm (o+1) (pp+1)).subst this - (Nat.sub_lt_of_lt_add this (Nat.succ_le_of_lt h₆) : ↑index - (o + 1) < pp + 1) - have h₈ : ⟨↑index - o - 1, h₇⟩ > (Internal.heapRemoveLastWithIndex r).snd.snd := - Nat.lt_sub_of_add_lt (b := o+1) h₁ - rewrite[get_right' _ h₅] - rewrite[get_right' _ h₆] at hold - rewrite[←hold] - have h₉ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelationGt r ⟨↑index - o - 1, h₇⟩ h₈ - unfold Internal.heapRemoveLastWithIndex at h₉ - unfold Fin.pred Fin.subNat at h₉ - simp only [Nat.add_eq, Fin.zero_eta, Fin.isValue, Nat.succ_eq_add_one] at h₉ - simp only [Nat.add_eq, Fin.coe_pred, Fin.isValue] - have : ↑index - 1 - o - 1 = ↑index - o - 1 - 1 := - (rfl : ↑index - (o + 1 + 1) = ↑index - (o + 1 + 1)) - |> (Nat.add_comm o 1).subst (motive := λx ↦ ↑index - (x + 1) = ↑index - (o + 1 + 1)) - |> (Nat.sub_sub ↑index 1 (o+1)).substr - --exact this.substr h₉ --seems to run into a Lean 4.9 bug when proving termination - simp only [this, Nat.add_eq, Fin.isValue, h₉] --no idea why simp avoids the same issue... -case isTrue h₃ => +if h₃ : p < o ∧ (p + 1).nextPowerOfTwo = p + 1 then --removed left - simp only [h₃, and_self, ↓reduceDite, Fin.isValue] at h₁ ⊢ + simp only [h₃, and_self, ↓reduceDIte, Fin.isValue] at h₁ ⊢ cases o case zero => exact absurd h₃.left $ Nat.not_lt_zero p case succ oo _ _ _ _ => @@ -338,6 +300,43 @@ case isTrue h₃ => have h₈ : ⟨↑index - 1, Nat.lt_succ.mpr h₇⟩ > (Internal.heapRemoveLastWithIndex l).snd.snd := Nat.lt_sub_of_add_lt h₁ exact CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelationGt l ⟨↑index - 1, Nat.lt_succ.mpr h₇⟩ h₈ +else + --removed right + simp only [h₃, ↓reduceDIte, Fin.isValue] at h₁ ⊢ + cases p <;> simp only [Nat.add_zero, Nat.reduceSub, Nat.reduceAdd, Fin.isValue] at h₁ ⊢ + case zero => + simp (config := { ground := true }) only [Nat.zero_add, and_true, Nat.not_lt, Nat.le_zero_eq] at h₃ + subst o + contradiction + case succ pp _ _ _ _ => + 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] + 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₁ + 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 := + have : ↑index < (o + 1) + (pp + 1) := (Nat.add_comm_right o (pp+1) 1).subst index.isLt + have : ↑index < (pp + 1) + (o + 1) := (Nat.add_comm (o+1) (pp+1)).subst this + (Nat.sub_lt_of_lt_add this (Nat.succ_le_of_lt h₆) : ↑index - (o + 1) < pp + 1) + have h₈ : ⟨↑index - o - 1, h₇⟩ > (Internal.heapRemoveLastWithIndex r).snd.snd := + Nat.lt_sub_of_add_lt (b := o+1) h₁ + rewrite[get_right' _ h₅] + rewrite[get_right' _ h₆] at hold + rewrite[←hold] + have h₉ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelationGt r ⟨↑index - o - 1, h₇⟩ h₈ + unfold Internal.heapRemoveLastWithIndex at h₉ + unfold Fin.pred Fin.subNat at h₉ + simp only [Nat.add_eq, Fin.zero_eta, Fin.isValue, Nat.succ_eq_add_one] at h₉ + simp only [Nat.add_eq, Fin.coe_pred, Fin.isValue] + have : ↑index - 1 - o - 1 = ↑index - o - 1 - 1 := + (rfl : ↑index - (o + 1 + 1) = ↑index - (o + 1 + 1)) + |> (Nat.add_comm o 1).subst (motive := λx ↦ ↑index - (x + 1) = ↑index - (o + 1 + 1)) + |> (Nat.sub_sub ↑index 1 (o+1)).substr + --exact this.substr h₉ --seems to run into a Lean 4.10 bug when proving termination + 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) @@ -361,14 +360,41 @@ protected theorem heapRemoveLastWithIndexRelationLt {α : Type u} {n : Nat} (hea unfold Internal.heapRemoveLastWithIndex Internal.heapRemoveLastAux intro h₁ split at h₁ - rename_i o p v l r _ _ _ _ + 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, - Fin.castLE_succ, Nat.pred_eq_sub_one, reduceDite] at h₁ ⊢ - split - case isFalse h₄ => + Fin.castLE_succ, Nat.pred_eq_sub_one, reduceDIte] at h₁ ⊢ + if h₄ : p < o ∧ (p + 1).nextPowerOfTwo = p + 1 then + --removed left + --get has to go into the square hole - erm, left branch too + cases o + case zero => + exact absurd h₄.left $ Nat.not_lt_zero _ + case succ oo _ _ _ _ => + rewrite[Fin.lt_iff_val_lt_val] at h₁ + simp only [Nat.add_eq, h₄, and_self, ↓reduceDIte, Fin.isValue, Fin.val_succ, + Fin.coe_castLE] at h₁ ⊢ + have h₂₂ : index > 0 := Nat.zero_lt_of_ne_zero $ Fin.val_ne_iff.mpr h₂ + have h₆ := (Nat.add_comm_right oo 1 p).subst hi + have h₈ : (⟨index.val, h₆⟩ : Fin (oo + p + 1)) > ⟨0,Nat.succ_pos _⟩ := h₂₂ + have h₇ : (⟨index.val, h₆⟩ : Fin (oo + p + 1)) ≤ oo := by + generalize (Internal.heapRemoveLastAux l (β := λn ↦ α × Fin n) _ _ _).2.snd = i at h₁ + have a : i.val ≤ oo := Nat.le_of_lt_succ i.isLt + have b : index.val ≤ i.val := Nat.le_of_lt_succ h₁ + exact Nat.le_trans b a + 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₅ + have h₉ : ⟨↑index - 1, this⟩ < (Internal.heapRemoveLastWithIndex l).snd.snd := + Nat.sub_lt_of_lt_add h₁ h₂₂ + exact CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelationLt l ⟨↑index - 1, _⟩ h₉ + else --removed right - simp only [h₄, ↓reduceDite, Fin.isValue] at h₁ ⊢ + simp only [h₄, ↓reduceDIte, Fin.isValue] at h₁ ⊢ cases p case zero => simp (config := { ground := true }) only [Nat.zero_add, and_true, Nat.not_lt, Nat.le_zero_eq] at h₄ @@ -398,34 +424,6 @@ protected theorem heapRemoveLastWithIndexRelationLt {α : Type u} {n : Nat} (hea have h₅ : (⟨index.val, hi⟩ : Fin (o + (pp+1))) ≤ o := h₄₂ have h₆ : (⟨index.val, hi⟩ : Fin (o + (pp+1))) > ⟨0,Nat.succ_pos _⟩ := h₂₂ rw[get_left' _ h₆ h₅] - case isTrue h₄ => - --removed left - --get has to go into the square hole - erm, left branch too - cases o - case zero => - exact absurd h₄.left $ Nat.not_lt_zero _ - case succ oo _ _ _ _ => - rewrite[Fin.lt_iff_val_lt_val] at h₁ - simp only [Nat.add_eq, h₄, and_self, ↓reduceDite, Fin.isValue, Fin.val_succ, - Fin.coe_castLE] at h₁ ⊢ - have h₂₂ : index > 0 := Nat.zero_lt_of_ne_zero $ Fin.val_ne_iff.mpr h₂ - have h₆ := (Nat.add_comm_right oo 1 p).subst hi - have h₈ : (⟨index.val, h₆⟩ : Fin (oo + p + 1)) > ⟨0,Nat.succ_pos _⟩ := h₂₂ - have h₇ : (⟨index.val, h₆⟩ : Fin (oo + p + 1)) ≤ oo := by - generalize (Internal.heapRemoveLastAux l (β := λn ↦ α × Fin n) _ _ _).2.snd = i at h₁ - have a : i.val ≤ oo := Nat.le_of_lt_succ i.isLt - have b : index.val ≤ i.val := Nat.le_of_lt_succ h₁ - exact Nat.le_trans b a - 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₅ - have h₉ : ⟨↑index - 1, this⟩ < (Internal.heapRemoveLastWithIndex l).snd.snd := - Nat.sub_lt_of_lt_add h₁ h₂₂ - exact CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelationLt l ⟨↑index - 1, _⟩ h₉ protected theorem heapRemoveLastWithIndexRelation {α : Type u} {n : Nat} (heap : CompleteTree α (n+1)) (index : Fin (n+1)): let (result, removedElement, oldIndex) := CompleteTree.Internal.heapRemoveLastWithIndex heap diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean index 7ac98c9..bc7ca14 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean @@ -68,7 +68,7 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α simp if h : j < oo + 1 then -- index was in l - simp only [h, ↓reduceDite] at h₃ + simp only [h, ↓reduceDIte] at h₃ split case isTrue => simp @@ -111,7 +111,7 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α exists ⟨j, h⟩ else -- index was in r - simp only [h, ↓reduceDite] at h₃ + simp only [h, ↓reduceDIte] at h₃ rename_i h₄ _ _ _ _ have h₄ : j - (oo + 1) < pp + 1 := Nat.sub_lt_left_of_lt_add (Nat.le_of_not_gt h) (Nat.lt_of_succ_lt_succ h₄) split @@ -162,10 +162,10 @@ theorem heapUpdateRootContainsUpdatedElement {α : Type u} {n : Nat} (tree : Com unfold heapUpdateRoot split rename_i o p v l r _ _ _ h₁ - cases o <;> simp only [Nat.add_eq, Nat.succ_eq_add_one, Nat.add_one_ne_zero, ↓reduceDite] + cases o <;> simp only [Nat.add_eq, Nat.succ_eq_add_one, Nat.add_one_ne_zero, ↓reduceDIte] case zero => simp only [contains, true_or] case succ oo _ _ _ => - cases p <;> simp only [Nat.add_one_ne_zero, ↓reduceDite] + cases p <;> simp only [Nat.add_one_ne_zero, ↓reduceDIte] case zero => split case isTrue => simp only [contains, true_or] diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapRemoveLast.lean index e9c357d..29e9837 100644 --- a/BinaryHeap/CompleteTree/HeapProofs/HeapRemoveLast.lean +++ b/BinaryHeap/CompleteTree/HeapProofs/HeapRemoveLast.lean @@ -117,12 +117,12 @@ private theorem heapRemoveLastAuxIsHeap rename_i n m v l r _ _ _ exact if h₄ : 0 = (n+m) then by - simp only [h₄, reduceDite, castZeroHeap] + simp only [h₄, reduceDIte, castZeroHeap] else by simp[h₄] exact if h₅ : (m exact absurd h₅.left $ Nat.not_lt_zero m diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean index 90991d8..b50d8c5 100644 --- a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean +++ b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean @@ -26,7 +26,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 only [↓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] diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean index 0788180..e930a30 100644 --- a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean +++ b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean @@ -60,7 +60,7 @@ have h₃ : 0 < leftLen heap h₂ := heapUpdateRootPossibleRootValuesAuxL heap ( case zero => simp only[root, true_or] case succ oo => have h₆ : p = 0 := by simp at h₁; omega - simp only [h₆, ↓reduceDite] + simp only [h₆, ↓reduceDIte] cases le value (l.root _) <;> simp[heapUpdateRootReturnsRoot, root_unfold, left_unfold] @@ -81,7 +81,7 @@ have h₄ : 0 < rightLen heap h₂ := heapUpdateRootPossibleRootValuesAuxR heap case zero => simp only[root, true_or] case succ oo => have h₆ : p ≠ 0 := by simp at h₁; omega - simp only [Nat.add_one_ne_zero, ↓reduceDite, h₆] + simp only [Nat.add_one_ne_zero, ↓reduceDIte, h₆] cases le value (l.root _) <;> simp rotate_right cases le value (r.root _) <;> simp @@ -161,7 +161,7 @@ theorem heapUpdateRootIsHeap {α : Type u} {n: Nat} (le : α → α → Bool) (v rename_i o p v l r h₇ h₈ h₉ heq exact if h₁₀ : o = 0 then by - simp only [Nat.add_eq, Nat.succ_eq_add_one, h₁₀, ↓reduceDite] + simp only [Nat.add_eq, Nat.succ_eq_add_one, h₁₀, ↓reduceDIte] unfold HeapPredicate at h₂ ⊢ simp only [h₂, true_and] unfold HeapPredicate.leOrLeaf @@ -172,7 +172,7 @@ theorem heapUpdateRootIsHeap {α : Type u} {n: Nat} (le : α → α → Bool) (v case right => match p, r with | Nat.zero, _ => trivial else if h₁₁ : p = 0 then by - simp only [↓reduceDite, h₁₀, h₁₁] + simp only [↓reduceDIte, h₁₀, h₁₁] cases h₉ : le value (root l (_ : 0 < o)) <;> simp case true => unfold HeapPredicate at * @@ -202,7 +202,7 @@ theorem heapUpdateRootIsHeap {α : Type u} {n: Nat} (le : α → α → Bool) (v exact h₄ else if h₁₂ : le value (root l (Nat.zero_lt_of_ne_zero h₁₀)) ∧ le value (root r (Nat.zero_lt_of_ne_zero h₁₁)) then by unfold HeapPredicate at * - simp only [↓reduceDite, and_self, ↓reduceIte, true_and, h₁₀, h₁₁, h₁₂, h₂] + simp only [↓reduceDIte, and_self, ↓reduceIte, true_and, h₁₀, h₁₁, h₁₂, h₂] unfold HeapPredicate.leOrLeaf cases o · contradiction @@ -210,7 +210,7 @@ theorem heapUpdateRootIsHeap {α : Type u} {n: Nat} (le : α → α → Bool) (v · contradiction · assumption else by - simp only [↓reduceDite, ↓reduceIte, h₁₀, h₁₁, h₁₂] + 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₁₂ cases h₁₄ : le (root l (_ : 0 < o)) (root r (_ : 0 < p)) <;> simp only [Bool.false_eq_true, ↓reduceIte] diff --git a/BinaryHeap/CompleteTree/NatLemmas.lean b/BinaryHeap/CompleteTree/NatLemmas.lean index 8038405..5733b21 100644 --- a/BinaryHeap/CompleteTree/NatLemmas.lean +++ b/BinaryHeap/CompleteTree/NatLemmas.lean @@ -153,14 +153,6 @@ theorem sub_lt_of_lt_add {a b c : Nat} (h₁ : a < c + b) (h₂ : b ≤ a) : a - have h₈ : (a-b) + 1 ≤ c := (Nat.add_comm 1 (a-b)).subst (motive := λx ↦ x ≤ c) h₇ Nat.lt_of_succ_le h₈ -theorem sub_lt_sub_right {a b c : Nat} (h₁ : b ≤ a) (h₂ : a < c) : (a - b < c - b) := by - apply Nat.sub_lt_of_lt_add - case h₂ => assumption - case h₁ => - have h₃ : b ≤ c := Nat.le_of_lt $ Nat.lt_of_le_of_lt h₁ h₂ - rw[Nat.sub_add_cancel h₃] - assumption - theorem add_eq_zero {a b : Nat} : a + b = 0 ↔ a = 0 ∧ b = 0 := by constructor <;> intro h₁ case mpr => diff --git a/lean-toolchain b/lean-toolchain index 6ab472f..c0eeb78 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:4.9.0 +leanprover/lean4:4.10 -- cgit v1.2.3