diff options
| author | Andreas Grois <andi@grois.info> | 2025-01-07 23:15:50 +0100 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2025-01-07 23:15:50 +0100 |
| commit | fe30e1dc0a0070452edce74331aa3df21a6b8f7c (patch) | |
| tree | 12a41e7e56eee7709cbb50772f4fe8b99c3bee9f | |
| parent | 376e4bf573f754aa7cb8c5d6ed652f1efece3050 (diff) | |
Lean 4.15
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean | 4 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/HeapOperations.lean | 2 | ||||
| -rw-r--r-- | lean-toolchain | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean index 2bdc382..ce9c3e2 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean @@ -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 (config := { ground := true }) 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 (config := { ground := true }) 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 => diff --git a/BinaryHeap/CompleteTree/HeapOperations.lean b/BinaryHeap/CompleteTree/HeapOperations.lean index 9151eb0..8e34599 100644 --- a/BinaryHeap/CompleteTree/HeapOperations.lean +++ b/BinaryHeap/CompleteTree/HeapOperations.lean @@ -33,7 +33,7 @@ def heapPush (le : α → α → Bool) (elem : α) (heap : CompleteTree α o) : rewrite[s] simp[r] have difference_decreased := Nat.le_succ_of_le $ Nat.le_succ_of_le max_height_difference - let result := branch a left (right.heapPush le elem) (q) difference_decreased (by simp[(Nat.power_of_two_iff_next_power_eq (n+1)), r]) + let result := branch a left (right.heapPush le elem) (q) difference_decreased (Or.inl $ (Nat.power_of_two_iff_next_power_eq (n+1)).mpr r.right) result else have q : m ≤ n+1 := by apply (Nat.le_of_succ_le) diff --git a/lean-toolchain b/lean-toolchain index cb2924f..f1f4005 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:4.14 +leanprover/lean4:4.15.0 |