diff options
Diffstat (limited to 'BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean')
| -rw-r--r-- | BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean | 8 |
1 files changed, 4 insertions, 4 deletions
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 |