diff options
| -rw-r--r-- | BinaryHeap/Aux.lean | 2 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/Get.lean | 6 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean | 12 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean | 4 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/IndexOf.lean | 7 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/HeapOperations.lean | 8 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/HeapProofs/HeapPush.lean | 13 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/HeapProofs/HeapRemoveLast.lean | 22 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean | 6 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean | 8 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/NatLemmas.lean | 16 | ||||
| -rw-r--r-- | lean-toolchain | 2 |
12 files changed, 53 insertions, 53 deletions
diff --git a/BinaryHeap/Aux.lean b/BinaryHeap/Aux.lean index 1b23bbf..e922a32 100644 --- a/BinaryHeap/Aux.lean +++ b/BinaryHeap/Aux.lean @@ -42,7 +42,7 @@ def pushList {α : Type u} {n : Nat} {le : α → α → Bool} (heap : BinaryHea match l with | [] => heap | a :: as => - have : n + 1 + as.length = n + (a :: as).length := by simp_arith[List.length_cons a as] + have : n + 1 + as.length = n + (a :: as).length := by simp +arith[List.length_cons a as] this▸pushList (heap.push a) as private def ofForInAux [ForIn Id ρ α] {le : α → α → Bool} (h₁ : TotalAndTransitiveLe le) (c : ρ) : (h : Nat) ×' BinaryHeap α le h := Id.run do diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean b/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean index b8d94e5..7379638 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean @@ -24,7 +24,7 @@ theorem get_right {α : Type u} {n : Nat} (tree : CompleteTree α n) (index : Fi omega apply Nat.sub_lt_right_of_lt_add omega - have : p+1+o = (o.add p).succ := by simp_arith + have : p+1+o = (o.add p).succ := (Nat.add_assoc o p 1).substr $ Nat.add_comm (p +1) o rw[this] assumption tree.get index = (tree.right h₁).get ⟨index.val - (tree.leftLen h₁) - 1, h₃⟩ @@ -45,7 +45,7 @@ theorem get_right' {α : Type u} {n m : Nat} {v : α} {l : CompleteTree α n} {r omega apply Nat.sub_lt_right_of_lt_add omega - have : m + 1 + n = n + m + 1 := by simp_arith + have : m + 1 + n = n + m + 1 := (Nat.add_assoc m n 1).substr $ Nat.add_comm (m +1 ) n rw[this] assumption (branch v l r m_le_n max_height_diff subtree_complete).get index = r.get ⟨index.val - n - 1, h₂⟩ @@ -93,7 +93,7 @@ theorem get_unfold {α : Type u} {n : Nat} (tree : CompleteTree α n) (index : F omega apply Nat.sub_lt_right_of_lt_add omega - have : p+1+o = (o.add p).succ := by simp_arith + have : p+1+o = (o.add p).succ := (Nat.add_assoc o p 1).substr $ Nat.add_comm (p +1) o rw[this] assumption (tree.right h₁).get ⟨index.val - (tree.leftLen h₁) - 1, h₃⟩ diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean index ce9c3e2..8222879 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean @@ -31,10 +31,10 @@ protected theorem heapRemoveLastWithIndexReturnsItemAtIndex {α : Type u} {o : N case isFalse goRight => dsimp only [Nat.pred_eq_sub_one, Nat.succ_eq_add_one, Fin.isValue] cases r -- to work around cast - case leaf => simp (config:={ground:=true}) at goRight; exact absurd goRight.symm n_m_not_zero + case leaf => simp +ground at goRight; exact absurd goRight.symm n_m_not_zero case branch rv rl rr rm_le_n rmax_height_difference rsubtree_full => rw[get_right, right_unfold] - case h₂ => simp_arith[leftLen_unfold] + case h₂ => simp +arith[leftLen_unfold] simp only [Fin.isValue, Fin.val_succ, Fin.coe_castLE, Fin.coe_addNat, leftLen_unfold] have : ∀(a : Nat), a + n + 1 - n - 1 = a := λa↦(Nat.add_sub_cancel _ _).subst $ (Nat.add_assoc a n 1).subst (motive := λx↦a+n+1-n-1 = x-(n+1)) $ (Nat.sub_sub (a+n+1) n 1).subst rfl simp only[this] @@ -76,7 +76,7 @@ protected theorem heapRemoveLastWithIndexHeapRemoveLastSameTree {α : Type u} {n simp only cases p case zero => - simp (config := { ground := true }) only [Nat.zero_add, decide_true, and_true, Nat.not_lt, Nat.le_zero_eq] at h₂ + simp +ground only [Nat.zero_add, decide_true, and_true, Nat.not_lt, Nat.le_zero_eq] at h₂ simp only [Nat.add_zero] at h₁ exact absurd h₂.symm h₁ case succ pp => @@ -111,7 +111,7 @@ protected theorem heapRemoveLastWithIndexHeapRemoveLastSameElement {α : Type u} simp only cases p case zero => - simp (config := { ground := true }) only [Nat.zero_add, decide_true, and_true, Nat.not_lt, Nat.le_zero_eq] at h₂ + simp +ground only [Nat.zero_add, decide_true, and_true, Nat.not_lt, Nat.le_zero_eq] at h₂ simp only [Nat.add_zero] at h₁ exact absurd h₂.symm h₁ case succ pp => @@ -258,7 +258,7 @@ else 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₃ + simp +ground only [Nat.zero_add, and_true, Nat.not_lt, Nat.le_zero_eq] at h₃ subst o contradiction case succ pp _ _ _ _ => @@ -348,7 +348,7 @@ protected theorem heapRemoveLastWithIndexRelationLt {α : Type u} {n : Nat} (hea 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₄ + simp +ground only [Nat.zero_add, and_true, Nat.not_lt, Nat.le_zero_eq] at h₄ subst o contradiction case succ pp _ _ _ _ => diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean index fe64a72..6193643 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean @@ -94,7 +94,7 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α right left rw[←h₃, left_unfold] - have : oo + 1 < oo + 1 + pp + 1 + 1 := by simp_arith --termination + have : oo + 1 < oo + 1 + pp + 1 + 1 := by simp +arith --termination apply heapUpdateRootOnlyUpdatesRoot apply Fin.val_ne_iff.mp exact Nat.succ_ne_zero _ @@ -147,7 +147,7 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α right right rw[←h₃, right_unfold] - have : pp + 1 < oo + 1 + pp + 1 + 1 := by simp_arith --termination + have : pp + 1 < oo + 1 + pp + 1 + 1 := by simp +arith --termination apply heapUpdateRootOnlyUpdatesRoot apply Fin.ne_of_val_ne simp only [ne_eq, Nat.add_one_ne_zero, not_false_eq_true] diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/IndexOf.lean b/BinaryHeap/CompleteTree/AdditionalProofs/IndexOf.lean index 0d69ebc..e913a59 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/IndexOf.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/IndexOf.lean @@ -118,7 +118,7 @@ private theorem indexOfAuxAddsCurrentIndex {α : Type u} {n : Nat} (tree : Compl case h_2 o p v l r _ _ _ => split case isTrue => - have : currentIndex < o + p + 1 + currentIndex := by simp_arith + have : currentIndex < o + p + 1 + currentIndex := by simp +arith simp only [Nat.add_eq, Nat.succ_eq_add_one, Option.get_some, Fin.val_ofNat', this, Nat.mod_eq_of_lt, Nat.add_zero, Nat.zero_lt_succ, Nat.zero_add] case isFalse => @@ -175,7 +175,7 @@ private theorem indexOfAuxAddsCurrentIndex {α : Type u} {n : Nat} (tree : Compl 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₉] - simp_arith[o1, o2] + simp +arith[o1, o2] 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 @@ -187,7 +187,7 @@ private theorem indexOfSomeImpPredTrueAuxR {α : Type u} {p : Nat} (r : Complete exact this.subst (motive := λx↦x=index.val) h₄ rw[←this] have := indexOfAuxAddsCurrentIndex r pred (o+1) (indexOfSomeImpPredTrueAux2 0 _ h₂) h₂ - simp_arith at this + have := (Nat.add_assoc _ o 1).substr (p := λx ↦ ((Internal.indexOfAux r pred (o + 1)).get _).val = x) this rw[←this] simp only [h₃, Option.get_some] @@ -201,7 +201,6 @@ private theorem indexOfSomeImpPredTrueAuxL {α : Type u} {o : Nat} (l : Complete exact this.subst (motive := λx↦x=index.val) h₄ rw[←this] have := indexOfAuxAddsCurrentIndex l pred 1 (indexOfSomeImpPredTrueAux2 0 _ h₂) h₂ - simp_arith at this rw[←this] simp only [h₃, Option.get_some] diff --git a/BinaryHeap/CompleteTree/HeapOperations.lean b/BinaryHeap/CompleteTree/HeapOperations.lean index e2b0019..b5d8f01 100644 --- a/BinaryHeap/CompleteTree/HeapOperations.lean +++ b/BinaryHeap/CompleteTree/HeapOperations.lean @@ -95,7 +95,7 @@ private theorem power_of_two_mul_two_le {n m : Nat} (h₁ : (n+1).isPowerOfTwo) have h₈ : n ≠ 0 := Ne.symm $ Nat.ne_of_lt h₇ have h₉ : (n+1).isEven := (Nat.isPowerOfTwo_even_or_one h₁).resolve_left $ if h : n+1=1 then absurd (Nat.succ.inj h) h₈ else h - have h₉ : n.isOdd := Nat.pred_even_odd h₉ (by simp_arith[h₇]) + have h₉ : n.isOdd := Nat.pred_even_odd h₉ (Nat.succ_pos n) have h₁₀ : ¬n.isOdd := Nat.even_not_odd_even.mp $ Nat.mul_2_is_even h₆ absurd h₉ h₁₀ else @@ -121,7 +121,7 @@ private theorem stillInRange {n m : Nat} (r : ¬(m < n ∧ ((m+1).nextPowerOfTwo | inl h₁ => have m_eq_n : m = n := Nat.le_antisymm m_le_n (Nat.not_lt.mp h₁) have m_lt_2_m : m < 2 * m := (Nat.one_mul m).subst (motive := λ x ↦ x < 2 * m) $ Nat.mul_lt_mul_of_pos_right Nat.one_lt_two m_gt_0 exact m_eq_n.subst (motive := λx ↦ x < 2 * m) m_lt_2_m - | inr h₁ => simp (config := { zetaDelta := true }) only [← Nat.power_of_two_iff_next_power_eq, decide_eq_true_eq] at h₁ + | inr h₁ => simp +zetaDelta only [← Nat.power_of_two_iff_next_power_eq, decide_eq_true_eq] at h₁ apply power_of_two_mul_two_le <;> assumption /-- @@ -155,7 +155,7 @@ protected def Internal.heapRemoveLastAux have s : m ≤ l := Nat.le_of_lt_succ r.left have rightIsFull : (m+1).isPowerOfTwo := (Nat.power_of_two_iff_next_power_eq (m+1)).mpr $ decide_eq_true_eq.mp r.right have l_lt_2_m_succ : l < 2 * (m+1) := Nat.lt_of_succ_lt max_height_difference - let res := auxl res (by simp_arith) + let res := auxl res (Nat.lt_of_le_of_lt (Nat.le_add_right (l+1) m) (Nat.lt_succ_self (l+1+m))) (q▸CompleteTree.branch a newLeft right s l_lt_2_m_succ (Or.inr rightIsFull), res) else --remove right @@ -167,7 +167,7 @@ protected def Internal.heapRemoveLastAux absurd ⟨hn, hr⟩ r | mm+1 => Nat.succ_pos mm let l := m.pred - have h₂ : l.succ = m := Nat.succ_pred $ Nat.not_eq_zero_of_lt m_gt_0 + have h₂ : l.succ = m := Nat.succ_pred $ Nat.ne_zero_of_lt m_gt_0 let ((newRight : CompleteTree α l), res) := Internal.heapRemoveLastAux (h₂▸right : CompleteTree α l.succ) aux0 auxl auxr have leftIsFull : (n+1).isPowerOfTwo := removeRightLeftIsFull r m_le_n subtree_complete have still_in_range : n < 2 * (l+1) := h₂.substr (p := λx ↦ n < 2 * x) $ stillInRange r m_le_n m_gt_0 leftIsFull max_height_difference diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapPush.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapPush.lean index 1ce9e56..52cba4c 100644 --- a/BinaryHeap/CompleteTree/HeapProofs/HeapPush.lean +++ b/BinaryHeap/CompleteTree/HeapProofs/HeapPush.lean @@ -13,8 +13,8 @@ private theorem rootSeesThroughCast case zero => simp case succ o ho => have h₄ := ho (n+1) - have h₅ : n + 1 + 1 + o = n + 1 + (Nat.succ o) := by simp_arith - have h₆ : n + 1 + o + 1 = n + (Nat.succ o + 1) := by simp_arith + have h₅ : n + 1 + 1 + o = n + 1 + (Nat.succ o) := Nat.add_right_comm (n+1) 1 o + have h₆ : n + 1 + o + 1 = n + (Nat.succ o + 1) := (Nat.add_comm 1 o).subst (motive := λx ↦ n + 1 + o + 1 = n + (x + 1)) (Nat.add_assoc n 1 (o+1)) rewrite[h₅, h₆] at h₄ revert heap h₁ h₂ h₃ assumption @@ -32,9 +32,10 @@ private theorem HeapPredicate.seesThroughCast case zero => simp[h₄] case succ o ho => have h₅ := ho (n+1) - have h₆ : n+1+1+o+1 = n+1+(Nat.succ o)+1 := by simp_arith + have h₆ : n+1+1+o+1 = n+1+(Nat.succ o)+1 := + congrArg Nat.succ $ (Nat.add_comm 1 o).subst (motive := λx ↦ n+1+1+o = n + 1 + x) (Nat.add_assoc (n+1) 1 o) rw[h₆] at h₅ - have h₆ : n + 1 + o + 1 + 1 = n + (Nat.succ o + 1 + 1) := by simp_arith + have h₆ : n + 1 + o + 1 + 1 = n + (Nat.succ o + 1 + 1) := (Nat.add_comm 1 o).subst (motive := λx ↦ n + 1 + o + 1 + 1 = n + (x + 1 + 1)) (Nat.add_assoc n 1 (o + 1 + 1)) rewrite[h₆] at h₅ revert heap h₁ h₂ h₃ assumption @@ -49,7 +50,7 @@ theorem heapPushRootSameOrElem (elem : α) (heap : CompleteTree α o) (lt : α case h_2.isTrue h => cases (lt elem v) <;> simp[instDecidableEqBool, Bool.decEq, root] case h_2.isFalse h => - rw[rootSeesThroughCast n (m+1) (by simp_arith) (by simp_arith) (by simp_arith)] + rw[rootSeesThroughCast n (m+1) (Nat.add_comm_right _ _ _) (Nat.succ_pos _) (Nat.succ_pos _)] cases (lt elem v) <;> simp[instDecidableEqBool, Bool.decEq, root] @@ -112,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[h₂] --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 29e9837..8eec6df 100644 --- a/BinaryHeap/CompleteTree/HeapProofs/HeapRemoveLast.lean +++ b/BinaryHeap/CompleteTree/HeapProofs/HeapRemoveLast.lean @@ -16,8 +16,8 @@ private theorem rootSeesThroughCast2 case zero => simp case succ mm mh => have h₄ := mh (n+1) - have h₅ : n + 1 + mm + 1 = n + Nat.succ mm + 1 := by simp_arith - have h₆ : n + 1 + 1 + mm = n + 1 + Nat.succ mm := by simp_arith + have h₅ : n + 1 + mm + 1 = n + Nat.succ mm + 1 := congrArg Nat.succ $ (Nat.add_comm 1 mm).subst (motive := λx ↦ _ = n + (x)) (Nat.add_assoc n 1 mm) + have h₆ : n + 1 + 1 + mm = n + 1 + Nat.succ mm := Nat.add_comm_right _ _ _ rw[h₅, h₆] at h₄ revert heap h₁ h₂ h₃ assumption @@ -35,9 +35,9 @@ private theorem HeapPredicate.seesThroughCast2 case zero => simp[h₄] case succ o ho => have h₅ := ho (n+1) - have h₆ : n+1+o+1 = n+(Nat.succ o)+1 := by simp_arith + have h₆ : n+1+o+1 = n+(Nat.succ o)+1 := congrArg Nat.succ $ Nat.add_comm_right _ _ _ rw[h₆] at h₅ - have h₆ : n + 1 + 1 + o = n + 1 + Nat.succ o := by simp_arith + have h₆ : n + 1 + 1 + o = n + 1 + Nat.succ o := Nat.add_comm_right (n+1) 1 o rewrite[h₆] at h₅ revert heap h₁ h₂ h₃ assumption @@ -82,7 +82,7 @@ protected theorem heapRemoveLastAuxLeavesRoot unfold CompleteTree.Internal.heapRemoveLastAux split rename_i o p v l r _ _ _ - have h₃ : (0 ≠ o + p) := Ne.symm $ Nat.not_eq_zero_of_lt h₁ + have h₃ : (0 ≠ o + p) := Ne.symm $ Nat.ne_zero_of_lt h₁ simp[h₃] exact if h₄ : p < o ∧ Nat.nextPowerOfTwo (p + 1) = p + 1 then by @@ -91,16 +91,16 @@ protected theorem heapRemoveLastAuxLeavesRoot case zero => exact absurd h₄.left $ Nat.not_lt_zero p case succ oo _ _ _ => simp -- redundant, but makes goal easier to read - rw[rootSeesThroughCast2 oo p _ (by simp_arith) _] + rw[rootSeesThroughCast2 oo p _ (Nat.succ_pos _) _] apply root_unfold else by simp[h₄] cases p case zero => - simp_arith at h₁ -- basically o ≠ 0 - simp_arith (config := {ground := true})[h₁] at h₄ -- the second term in h₄ is decidable and True. What remains is ¬(0 < o), or o = 0 + have h₁ : 0 < o := (Nat.add_zero o).subst h₁ + simp +ground[h₁] at h₄ -- the second term in h₄ is decidable and True. What remains is ¬(0 < o), or o = 0 case succ pp hp => - simp_arith + simp +arith apply root_unfold private theorem heapRemoveLastAuxIsHeap @@ -128,7 +128,7 @@ private theorem heapRemoveLastAuxIsHeap exact absurd h₅.left $ Nat.not_lt_zero m case succ ll h₆ h₇ h₈ => simp only - apply HeapPredicate.seesThroughCast2 <;> try simp_arith + apply HeapPredicate.seesThroughCast2; exact Nat.lt_add_right m (Nat.succ_pos _); exact Nat.succ_pos _ cases ll case a.zero => -- if ll is zero, then (heapRemoveLast l).snd is a leaf. have h₆ := heapRemoveLastAuxLeaf l aux0 auxl auxr @@ -149,7 +149,7 @@ private theorem heapRemoveLastAuxIsHeap cases m case zero => simp only [Nat.add_zero] at h₄ -- n ≠ 0 - simp (config := { ground := true }) only [Nat.zero_add, and_true, Nat.not_lt, Nat.le_zero_eq, Ne.symm h₄] at h₅ -- the second term in h₅ is decidable and True. What remains is ¬(0 < n), or n = 0 + simp +ground only [Nat.zero_add, and_true, Nat.not_lt, Nat.le_zero_eq, Ne.symm h₄] at h₅ -- the second term in h₅ is decidable and True. What remains is ¬(0 < n), or n = 0 case succ mm h₆ h₇ h₈ => unfold HeapPredicate at * simp only [h₁, heapRemoveLastAuxIsHeap aux0 auxl auxr h₁.right.left h₂ h₃, true_and] diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean index c12f76f..86d2499 100644 --- a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean +++ b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean @@ -13,7 +13,7 @@ private theorem heapUpdateAtIsHeapLeRootAux_RootLeValue {α : Type u} {n : Nat} generalize heapUpdateAt.proof_1 index = h₂ split rename_i o p v l r h₆ h₇ h₈ index h₁ h₅ - cases h₉ : le v value <;> simp (config := { ground := true }) only + cases h₉ : le v value <;> simp only case false => rw[root_unfold] at h₃; exact absurd h₃ ((Bool.not_eq_true (le v value)).substr h₉) case true => rw[root_unfold] @@ -39,7 +39,7 @@ private theorem heapUpdateAtIsHeapLeRootAux_ValueLeRoot {α : Type u} {n : Nat} split rename_i o p v l r h₆ h₇ h₈ index h₂ hi cases le v value - <;> simp (config := { ground := true }) only [root_unfold, Nat.pred_eq_sub_one] at h₃ ⊢ + <;> simp +ground only [root_unfold, Nat.pred_eq_sub_one] at h₃ ⊢ <;> split <;> unfold HeapPredicate.leOrLeaf <;> simp only [reduceIte, root_unfold, h₃, h₄, reflexive_le] @@ -53,7 +53,7 @@ theorem heapUpdateAtIsHeap {α : Type u} {n : Nat} (le : α → α → Bool) (in case isFalse h₅ => split rename_i o p v l r h₆ h₇ h₈ index h₁ h₅ - cases h₁₀ : le v value <;> simp (config := {ground := true}) -- this could probably be solved without this split, but readability... + cases h₁₀ : le v value <;> simp +ground -- this could probably be solved without this split, but readability... <;> split <;> rename_i h -- h is the same name as used in the function <;> unfold HeapPredicate at h₂ ⊢ diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean index d712b8e..d3e7017 100644 --- a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean +++ b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean @@ -34,7 +34,7 @@ private theorem heapUpdateRootPossibleRootValuesAuxR {α : Type u} (heap : Compl | (o+p+1), .branch v l r h₂ h₃ h₄ => by simp[rightLen, length] cases p - case zero => simp_arith at h₁; simp at h₃; exact absurd h₁ (Nat.not_le_of_gt h₃) + case zero => exact absurd (Nat.le_of_lt_succ h₁) (Nat.not_le_of_gt h₃) case succ q => exact Nat.zero_lt_succ q private theorem heapUpdateRootPossibleRootValues1 {α : Type u} (le : α → α → Bool) (value : α) (heap : CompleteTree α n) (h₁ : n = 1) : (heap.heapUpdateRoot (h₁.substr (p := λx ↦ 0<x) (Nat.lt_succ_self 0)) le value).fst.root (h₁.substr (Nat.lt_succ_self 0)) = value := by @@ -114,8 +114,8 @@ protected theorem heapUpdateRootIsHeapLeRootAux {α : Type u} (le : α → α case h_2 o p v l r h₇ h₈ h₉ => have h₁₁ : p = 0 := by simp at h₅ - cases o; simp only [Nat.le_zero_eq] at h₇; exact h₇; simp_arith[Nat.add_eq_zero] at h₅; exact h₅.right - have h₁₀ : o = 1 := by simp_arith[h₁₁] at h₅; assumption + cases o; simp only [Nat.le_zero_eq] at h₇; exact h₇; simp +arith only [Nat.add_eq_zero_iff] at h₅; exact h₅.left + have h₁₀ : o = 1 := by simp only [h₁₁, Nat.add_zero, Nat.reduceEqDiff] at h₅; assumption simp only rw[h₆] have h₁₂ := h₁.right.right.left @@ -186,7 +186,7 @@ theorem heapUpdateRootIsHeap {α : Type u} {n: Nat} (le : α → α → Bool) (v case false => rw[heapUpdateRootReturnsRoot] have h₁₂ : le (l.root (Nat.zero_lt_of_ne_zero h₁₀)) value := by simp[h₉, h₄, not_le_imp_le] - have h₁₃ : o = 1 := Nat.le_antisymm (by simp_arith[h₁₁] at h₈; exact h₈) (Nat.succ_le_of_lt (Nat.zero_lt_of_ne_zero h₁₀)) + have h₁₃ : o = 1 := Nat.le_antisymm (by simp[h₁₁] at h₈; exact Nat.le_of_lt_succ h₈) (Nat.succ_le_of_lt (Nat.zero_lt_of_ne_zero h₁₀)) unfold HeapPredicate at * simp only [h₂, true_and] --closes one sub-goal apply And.intro <;> try apply And.intro diff --git a/BinaryHeap/CompleteTree/NatLemmas.lean b/BinaryHeap/CompleteTree/NatLemmas.lean index f9b730c..56b3203 100644 --- a/BinaryHeap/CompleteTree/NatLemmas.lean +++ b/BinaryHeap/CompleteTree/NatLemmas.lean @@ -2,9 +2,9 @@ namespace Nat theorem smaller_smaller_exp {n m o : Nat} (p : o ^ n < o ^ m) (q : o > 0) : n < m := if h₁ : m ≤ n then - by have h₂ := Nat.pow_le_pow_of_le_right (q) h₁ + by have h₂ := Nat.pow_le_pow_right (q) h₁ have h₃ := Nat.lt_of_le_of_lt h₂ p - simp_arith at h₃ + simp at h₃ else by rewrite[Nat.not_ge_eq] at h₁ trivial @@ -17,11 +17,11 @@ private theorem mul2_isPowerOfTwo_smaller_smaller_equal (n : Nat) (power : Nat) rewrite[←Nat.pow_succ 2 l] rewrite[h₄] have h₆ : 2 > 0 := by decide - apply (Nat.pow_le_pow_of_le_right h₆) + apply (Nat.pow_le_pow_right h₆) rewrite [h₅] at h₃ rewrite [h₄] at h₃ have h₃ := smaller_smaller_exp h₃ - simp_arith at h₃ + simp at h₃ assumption private theorem power_of_two_go_one_eq (n : Nat) (power : Nat) (h₁ : n.isPowerOfTwo) (h₂ : power.isPowerOfTwo) (h₃ : power ≤ n) : Nat.nextPowerOfTwo.go n power (Nat.pos_of_isPowerOfTwo h₂) = n := by @@ -70,7 +70,7 @@ theorem mul2_ispowerOfTwo_iff_isPowerOfTwo (n : Nat) : n.isPowerOfTwo ↔ (2*n). cases n with | zero => contradiction | succ m => cases k with - | zero => simp_arith at h₄ + | zero => simp +arith at h₄ | succ l => rewrite[Nat.pow_succ 2 l] at h₄ rewrite[Nat.mul_comm (2^l) 2] at h₄ have h₄ := Nat.eq_of_mul_eq_mul_left (by decide : 0<2) h₄ @@ -91,7 +91,7 @@ end theorem mul_2_is_even {n m : Nat} (h₁ : n = 2 * m) : Nat.isEven n := by cases m with | zero => simp[Nat.isEven, h₁] - | succ o => simp_arith at h₁ + | succ o => simp +arith at h₁ simp[Nat.isEven, Nat.isOdd, h₁] exact Nat.mul_2_is_even (rfl) @@ -99,7 +99,7 @@ theorem isPowerOfTwo_even_or_one {n : Nat} (h₁ : n.isPowerOfTwo) : (n = 1 ∨ simp[Nat.isPowerOfTwo] at h₁ let ⟨k,h₂⟩ := h₁ cases k with - | zero => simp_arith[h₂] + | zero => simp[h₂] | succ l => rewrite[Nat.pow_succ] at h₂ rewrite[Nat.mul_comm (2^l) 2] at h₂ exact Or.inr $ Nat.mul_2_is_even h₂ @@ -157,7 +157,7 @@ theorem add_eq_zero {a b : Nat} : a + b = 0 ↔ a = 0 ∧ b = 0 := by case mpr => simp[h₁] case mp => - cases a <;> simp_arith at *; assumption + cases a <;> simp at *; assumption -- Yes, this is trivial. Still, I needed it so often, that it deserves its own lemma. theorem add_comm_right (a b c : Nat) : a + b + c = a + c + b := diff --git a/lean-toolchain b/lean-toolchain index db29c97..9f78e65 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:4.17.0 +leanprover/lean4:4.18.0 |